Cyclotomic ℤₚ-extension

The assertion that a field extension is a cyclotomic $p^∞$-extension

@[reducible, inline]

abbrev IsCyclotomicPinfExtension (p : ℕ) (A : Type u_3) (B : Type u_4) [CommRing A] [CommRing B] [Algebra A B] : Prop

IsCyclotomicPinfExtension p A B is the assertion that B / A is a cyclotomic $p^∞$-extension. See IsCyclotomicExtension for more details.

Equations

• IsCyclotomicPinfExtension p A B = IsCyclotomicExtension (Set.range fun (x : ℕ) => p ^ x) A B

theorem IsCyclotomicPinfExtension.equiv (p : ℕ) (A : Type u_3) (B : Type u_4) [CommRing A] [CommRing B] [Algebra A B] {C : Type u_5} [CommRing C] [Algebra A C] [IsCyclotomicPinfExtension p A B] (f : B ≃ₐ[A] C) : IsCyclotomicPinfExtension p A C

The field $K(μ_{p^∞})$

def CyclotomicPinfField (p : ℕ) (K : Type u) [Field K] : Type u

The field $K(μ_{p^∞})$ inside the separable closure of K. Internally it is defined to be an IntermediateField K (SeparableClosure K), but please avoid using it in the public interface. Instead, use IsSepClosed.lift to construct a map of it to SeparableClosure K.

Equations

• CyclotomicPinfField p K = ↥(IntermediateField.adjoin K {x : SeparableClosure K | ∃ (n : ℕ), x ^ p ^ n = 1})

noncomputable instance CyclotomicPinfField.instField (p : ℕ) (K : Type u) [Field K] : Field (CyclotomicPinfField p K)

Equations

• CyclotomicPinfField.instField p K = inferInstanceAs (Field ↥(IntermediateField.adjoin K {x : SeparableClosure K | ∃ (n : ℕ), x ^ p ^ n = 1}))

noncomputable instance CyclotomicPinfField.algebra (p : ℕ) (K : Type u) [Field K] : Algebra K (CyclotomicPinfField p K)

Equations

• CyclotomicPinfField.algebra p K = inferInstanceAs (Algebra K ↥(IntermediateField.adjoin K {x : SeparableClosure K | ∃ (n : ℕ), x ^ p ^ n = 1}))

noncomputable instance CyclotomicPinfField.instInhabited (p : ℕ) (K : Type u) [Field K] : Inhabited (CyclotomicPinfField p K)

Equations

• CyclotomicPinfField.instInhabited p K = { default := 0 }

instance CyclotomicPinfField.instCharZero (p : ℕ) (K : Type u) [Field K] [CharZero K] : CharZero (CyclotomicPinfField p K)

instance CyclotomicPinfField.instCharP (p : ℕ) (K : Type u) [Field K] (p' : ℕ) [CharP K p'] : CharP (CyclotomicPinfField p K) p'

instance CyclotomicPinfField.instExpChar (p : ℕ) (K : Type u) [Field K] (p' : ℕ) [ExpChar K p'] : ExpChar (CyclotomicPinfField p K) p'

noncomputable instance CyclotomicPinfField.algebra' (p : ℕ) (K : Type u) [Field K] (R : Type u_3) [CommRing R] [Algebra R K] : Algebra R (CyclotomicPinfField p K)

Equations

• CyclotomicPinfField.algebra' p K R = inferInstanceAs (Algebra R ↥(IntermediateField.adjoin K {x : SeparableClosure K | ∃ (n : ℕ), x ^ p ^ n = 1}))

instance CyclotomicPinfField.instIsScalarTower (p : ℕ) (K : Type u) [Field K] (R : Type u_3) [CommRing R] [Algebra R K] : IsScalarTower R K (CyclotomicPinfField p K)

instance CyclotomicPinfField.instNoZeroSMulDivisors (p : ℕ) (K : Type u) [Field K] (R : Type u_3) [CommRing R] [Algebra R K] [IsFractionRing R K] : NoZeroSMulDivisors R (CyclotomicPinfField p K)

instance CyclotomicPinfField.isSeparable (p : ℕ) (K : Type u) [Field K] : Algebra.IsSeparable K (CyclotomicPinfField p K)

theorem CyclotomicPinfField.isCyclotomicExtension (p : ℕ) (K : Type u) [Field K] [NeZero ↑p] (s : Set ℕ) (h1 : s ⊆ {0} ∪ Set.range fun (x : ℕ) => p ^ x) (h2 : ∀ (N : ℕ), ∃ n ≥ N, p ^ n ∈ s) : IsCyclotomicExtension s K (CyclotomicPinfField p K)

instance CyclotomicPinfField.isCyclotomicPinfExtension (p : ℕ) (K : Type u) [Field K] [NeZero ↑p] : IsCyclotomicPinfExtension p K (CyclotomicPinfField p K)

instance CyclotomicPinfField.hasEnoughRootsOfUnity (p : ℕ) (K : Type u) [Field K] [NeZero ↑p] (i : ℕ) : HasEnoughRootsOfUnity (CyclotomicPinfField p K) (p ^ i)

theorem CyclotomicPinfField.nonempty_algEquiv_prime_pow_mul (p : ℕ) (K : Type u) [Field K] (q k : ℕ) [ExpChar K q] : Nonempty (CyclotomicPinfField (q ^ k * p) K ≃ₐ[K] CyclotomicPinfField p K)

instance CyclotomicPinfField.isAbelianGalois (p : ℕ) (K : Type u) [Field K] [NeZero p] : IsAbelianGalois K (CyclotomicPinfField p K)

noncomputable def CyclotomicPinfField.cyclotomicZpSubfield (p : ℕ) (K : Type u) [Field K] : IntermediateField K (CyclotomicPinfField p K)

The intermediate field of $K(μ_{p^∞}) / K$ fixed by the torsion subgroup of the Galois group of $K(μ_{p^∞}) / K$. CyclotomicPinfField.isCyclotomicZpExtension_cyclotomicZpSubfield shows that, if $K(μ_{p^∞}) / K$ is an infinite extension, then this field over K is a cyclotomic ℤₚ-extension.

Equations

• CyclotomicPinfField.cyclotomicZpSubfield p K = if h : p ≠ 0 then IntermediateField.fixedField (CommGroup.torsion Gal(CyclotomicPinfField p K/K)) else ⊥

theorem CyclotomicPinfField.cyclotomicZpSubfield_eq_fixedField (p : ℕ) (K : Type u) [Field K] [NeZero p] : cyclotomicZpSubfield p K = IntermediateField.fixedField (CommGroup.torsion Gal(CyclotomicPinfField p K/K))

Some complemenatry results on cyclotomic character

noncomputable def continuousCyclotomicCharacter (p : ℕ) (K : Type u) [Field K] (L : Type u_3) [Field L] [Algebra K L] [Fact (Nat.Prime p)] : Gal(L/K) →ₜ* ℤ_[p]ˣ

The restriction of cyclotomicCharacter to L ≃ₐ[K] L and which is continuous.

Equations

• continuousCyclotomicCharacter p K L = { toMonoidHom := (cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L), continuous_toFun := ⋯ }

@[simp]

theorem continuousCyclotomicCharacter_toMonoidHom (p : ℕ) (K : Type u) [Field K] (L : Type u_3) [Field L] [Algebra K L] [Fact (Nat.Prime p)] : (continuousCyclotomicCharacter p K L).toMonoidHom = (cyclotomicCharacter L p).comp (MulSemiringAction.toRingAut Gal(L/K) L)

theorem continuousCyclotomicCharacter_apply (p : ℕ) (K : Type u) [Field K] (L : Type u_3) [Field L] [Algebra K L] [Fact (Nat.Prime p)] (f : Gal(L/K)) : (continuousCyclotomicCharacter p K L) f = (cyclotomicCharacter L p) ↑f

theorem isClosed_ker_continuousCyclotomicCharacter (p : ℕ) (K : Type u) [Field K] (L : Type u_3) [Field L] [Algebra K L] [Fact (Nat.Prime p)] : IsClosed ↑(continuousCyclotomicCharacter p K L).ker

theorem IntermediateField.adjoin_le_fixedField_ker_continuousCyclotomicCharacter (p : ℕ) (K : Type u) [Field K] (L : Type u_3) [Field L] [Algebra K L] [Fact (Nat.Prime p)] [∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)] : adjoin K {x : L | ∃ (n : ℕ), x ^ p ^ n = 1} ≤ fixedField (continuousCyclotomicCharacter p K L).ker

theorem IntermediateField.adjoin_eq_fixedField_ker_continuousCyclotomicCharacter (p : ℕ) (K : Type u) [Field K] (L : Type u_3) [Field L] [Algebra K L] [Fact (Nat.Prime p)] [∀ (i : ℕ), HasEnoughRootsOfUnity L (p ^ i)] [IsGalois K L] : adjoin K {x : L | ∃ (n : ℕ), x ^ p ^ n = 1} = fixedField (continuousCyclotomicCharacter p K L).ker

theorem continuousCyclotomicCharacter_injective (p : ℕ) (K : Type u) [Field K] (L : Type u_3) [Field L] [Algebra K L] [Fact (Nat.Prime p)] [IsCyclotomicPinfExtension p K L] : Function.Injective ⇑(continuousCyclotomicCharacter p K L)

theorem IsCyclotomicPinfExtension.finite_torsion_gal (p : ℕ) (K : Type u) [Field K] (L : Type u_3) [Field L] [Algebra K L] [Fact (Nat.Prime p)] [IsCyclotomicPinfExtension p K L] : Finite ↥(CommGroup.torsion Gal(L/K))

noncomputable def CyclotomicPinfField.torsionGal (p : ℕ) (K : Type u) [Field K] [Fact (Nat.Prime p)] [NeZero ↑p] : ClosedSubgroup Gal(CyclotomicPinfField p K/K)

The torsion subgroup of the Galois group of $K(μ_{p^∞}) / K$, which is a closed subgroup.

Equations

• CyclotomicPinfField.torsionGal p K = { toSubgroup := CommGroup.torsion Gal(CyclotomicPinfField p K/K), isClosed' := ⋯ }

@[simp]

theorem CyclotomicPinfField.torsionGal_toSubgroup (p : ℕ) (K : Type u) [Field K] [Fact (Nat.Prime p)] [NeZero ↑p] : ↑(torsionGal p K) = CommGroup.torsion Gal(CyclotomicPinfField p K/K)

theorem CyclotomicPinfField.fixingSubgroup_cyclotomicZpSubfield (p : ℕ) (K : Type u) [Field K] [Fact (Nat.Prime p)] [NeZero ↑p] : (cyclotomicZpSubfield p K).fixingSubgroup = CommGroup.torsion Gal(CyclotomicPinfField p K/K)

instance CyclotomicPinfField.finite_torsionGal (p : ℕ) (K : Type u) [Field K] [Fact (Nat.Prime p)] [NeZero ↑p] : Finite ↥(torsionGal p K)

The assertion that a field extension is a cyclotomic ℤₚ-extension

structure IsCyclotomicZpExtension (p : ℕ) (K : Type u) (Kinf : Type u_1) [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] [Fact (Nat.Prime p)] : Prop

K∞ / K is a cyclotomic ℤₚ-extension, if it is a ℤₚ-extension, and K∞ can be realized as an intermediate field of $K(μ_{p^∞}) / K$.

• isZpExtension : IsMvZpExtension p 1 K Kinf
• nonempty_algHom_cyclotomicPinfField : Nonempty (Kinf →ₐ[K] CyclotomicPinfField p K)

theorem isCyclotomicZpExtension_iff (p : ℕ) (K : Type u) (Kinf : Type u_1) [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] [Fact (Nat.Prime p)] : IsCyclotomicZpExtension p K Kinf ↔ IsMvZpExtension p 1 K Kinf ∧ Nonempty (Kinf →ₐ[K] CyclotomicPinfField p K)

theorem IsCyclotomicZpExtension.congr {p : ℕ} {K : Type u} {Kinf : Type u_1} {Kinf' : Type u_2} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] [Field Kinf'] [Algebra K Kinf'] [IsGalois K Kinf'] [Fact (Nat.Prime p)] (H : IsCyclotomicZpExtension p K Kinf) (f : Kinf ≃ₐ[K] Kinf') : IsCyclotomicZpExtension p K Kinf'

theorem IsCyclotomicZpExtension.infinite_dimensional {p : ℕ} {K : Type u} {Kinf : Type u_1} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] [Fact (Nat.Prime p)] (H : IsCyclotomicZpExtension p K Kinf) : ¬FiniteDimensional K Kinf

theorem IsCyclotomicZpExtension.infinite_dimensional_cyclotomicPinfField {p : ℕ} {K : Type u} {Kinf : Type u_1} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] [Fact (Nat.Prime p)] (H : IsCyclotomicZpExtension p K Kinf) : ¬FiniteDimensional K (CyclotomicPinfField p K)

theorem IsCyclotomicZpExtension.neZero {p : ℕ} {K : Type u} {Kinf : Type u_1} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] [Fact (Nat.Prime p)] (H : IsCyclotomicZpExtension p K Kinf) : NeZero ↑p

noncomputable def IsCyclotomicZpExtension.algHomCyclotomicPinfField {p : ℕ} {K : Type u} {Kinf : Type u_1} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] [Fact (Nat.Prime p)] (H : IsCyclotomicZpExtension p K Kinf) : Kinf →ₐ[K] CyclotomicPinfField p K

A random map from K∞ to $K(μ_{p^∞})$.

Equations

• H.algHomCyclotomicPinfField = ⋯.some

theorem IsCyclotomicZpExtension.fieldRange_eq_cyclotomicZpSubfield {p : ℕ} {K : Type u} {Kinf : Type u_1} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] [Fact (Nat.Prime p)] (H : IsCyclotomicZpExtension p K Kinf) (f : Kinf →ₐ[K] CyclotomicPinfField p K) : f.fieldRange = CyclotomicPinfField.cyclotomicZpSubfield p K

theorem IsCyclotomicZpExtension.isCyclotomicZpExtension_cyclotomicZpSubfield {p : ℕ} {K : Type u} {Kinf : Type u_1} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] [Fact (Nat.Prime p)] (H : IsCyclotomicZpExtension p K Kinf) : IsCyclotomicZpExtension p K ↥(CyclotomicPinfField.cyclotomicZpSubfield p K)

theorem IsCyclotomicZpExtension.unique {p : ℕ} {K : Type u} {Kinf : Type u_1} {Kinf' : Type u_2} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] [Field Kinf'] [Algebra K Kinf'] [IsGalois K Kinf'] [Fact (Nat.Prime p)] (H : IsCyclotomicZpExtension p K Kinf) (H' : IsCyclotomicZpExtension p K Kinf') : Nonempty (Kinf ≃ₐ[K] Kinf')

noncomputable def InfiniteGalois.normalAutContinuousEquivQuotient {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] [IsGalois k K] (H : ClosedSubgroup Gal(K/k)) [(↑H).Normal] : Gal(K/k) ⧸ ↑H ≃ₜ* Gal(↥(IntermediateField.fixedField ↑H)/k)

If H is a closed normal subgroup of Gal(K / k), then Gal(fixedField H / k) is isomorphic to Gal(K / k) ⧸ H as a topological group.

TODO: should go to mathlib

Equations

• InfiniteGalois.normalAutContinuousEquivQuotient H = { toMulEquiv := InfiniteGalois.normalAutEquivQuotient H, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem InfiniteGalois.normalAutContinuousEquivQuotient_toMulEquiv {k : Type u_3} {K : Type u_4} [Field k] [Field K] [Algebra k K] [IsGalois k K] (H : ClosedSubgroup Gal(K/k)) [(↑H).Normal] : (normalAutContinuousEquivQuotient H).toMulEquiv = normalAutEquivQuotient H

theorem CyclotomicPinfField.isCyclotomicZpExtension_cyclotomicZpSubfield (p : ℕ) (K : Type u) [Field K] [Fact (Nat.Prime p)] [NeZero ↑p] (H : ¬FiniteDimensional K (CyclotomicPinfField p K)) : IsCyclotomicZpExtension p K ↥(cyclotomicZpSubfield p K)

If $K(μ_{p^∞}) / K$ is an infinite extension, then $K(μ_{p^∞})^Δ / K$ is a cyclotomic ℤₚ-extension, where Δ is the torsion subgroup of the Galois group of $K(μ_{p^∞}) / K$.

theorem isCyclotomicZpExtension_iff_exists_fieldRange_eq_cyclotomicZpSubfield (p : ℕ) (K : Type u) (Kinf : Type u_1) [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] [Fact (Nat.Prime p)] : IsCyclotomicZpExtension p K Kinf ↔ ↑p ≠ 0 ∧ ¬FiniteDimensional K (CyclotomicPinfField p K) ∧ ∃ (f : Kinf →ₐ[K] CyclotomicPinfField p K), f.fieldRange = CyclotomicPinfField.cyclotomicZpSubfield p K

The assertion that a field have a cyclotomic ℤₚ-extension

class HasCyclotomicZpExtension (p : ℕ) (K : Type u) [Field K] [Fact (Nat.Prime p)] : Prop

HasCyclotomicZpExtension p K is the assertion that the field K have a cyclotomic ℤₚ-extension.

• exists_isCyclotomicZpExtension : ∃ (Kinf : Type u) (x : Field Kinf) (x_1 : Algebra K Kinf) (x_2 : IsGalois K Kinf), IsCyclotomicZpExtension p K Kinf

theorem hasCyclotomicZpExtension_iff (p : ℕ) (K : Type u) [Field K] [Fact (Nat.Prime p)] : HasCyclotomicZpExtension p K ↔ ∃ (Kinf : Type u) (x : Field Kinf) (x_1 : Algebra K Kinf) (x_2 : IsGalois K Kinf), IsCyclotomicZpExtension p K Kinf

theorem hasCyclotomicZpExtension_iff_isCyclotomicZpExtension_cyclotomicZpSubfield (p : ℕ) (K : Type u) [Field K] [Fact (Nat.Prime p)] : HasCyclotomicZpExtension p K ↔ IsCyclotomicZpExtension p K ↥(CyclotomicPinfField.cyclotomicZpSubfield p K)

theorem IsCyclotomicZpExtension.hasCyclotomicZpExtension {p : ℕ} {K : Type u} {Kinf : Type u_1} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] [Fact (Nat.Prime p)] (H : IsCyclotomicZpExtension p K Kinf) : HasCyclotomicZpExtension p K

theorem hasCyclotomicZpExtension_iff_infinite_dimensional (p : ℕ) (K : Type u) [Field K] [Fact (Nat.Prime p)] : HasCyclotomicZpExtension p K ↔ ↑p ≠ 0 ∧ ¬FiniteDimensional K (CyclotomicPinfField p K)

K have a cyclotomic ℤₚ-extension if and only if $K(μ_{p^∞}) / K$ is an infinite extension.

instance NumberField.hasCyclotomicZpExtension (p : ℕ) (K : Type u) [Field K] [Fact (Nat.Prime p)] [NumberField K] : HasCyclotomicZpExtension p K

Any number field has a cyclotomic ℤₚ-extension.