ℤₚ-extension of fields

Main definitions

• MvZpExtension: a Galois extension with a fixed isomorphism of its Galois group to ℤₚᵈ as topological groups.

• IsMvZpExtension: a Prop which asserts that a Galois extension is with Galois group isomorphic to ℤₚᵈ as a topological group.

theorem AlgEquiv.continuous_autCongr {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [Field R] [Field A₁] [Field A₂] [Algebra R A₁] [Algebra R A₂] (ϕ : A₁ ≃ₐ[R] A₂) : Continuous ⇑ϕ.autCongr

def AlgEquiv.continuousAutCongr {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [Field R] [Field A₁] [Field A₂] [Algebra R A₁] [Algebra R A₂] (ϕ : A₁ ≃ₐ[R] A₂) : (A₁ ≃ₐ[R] A₁) ≃ₜ* A₂ ≃ₐ[R] A₂

Continuous version of AlgEquiv.autCongr.

Equations

• ϕ.continuousAutCongr = { toMulEquiv := ϕ.autCongr, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem AlgEquiv.continuousAutCongr_toMulEquiv {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [Field R] [Field A₁] [Field A₂] [Algebra R A₁] [Algebra R A₂] (ϕ : A₁ ≃ₐ[R] A₂) : ϕ.continuousAutCongr.toMulEquiv = ϕ.autCongr

@[simp]

theorem AlgEquiv.continuousAutCongr_apply {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [Field R] [Field A₁] [Field A₂] [Algebra R A₁] [Algebra R A₂] (ϕ : A₁ ≃ₐ[R] A₂) (ψ : A₁ ≃ₐ[R] A₁) : ϕ.continuousAutCongr ψ = ϕ.symm.trans (ψ.trans ϕ)

ℤₚᵈ-extension

def MvZpExtension (p : ℕ) [Fact (Nat.Prime p)] (ι : Type u_1) (K : Type u_2) (Kinf : Type u_3) [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] : Type (max u_3 u_1)

MvZpExtension is an isomorphism of the Galois group of a Galois extension K∞ / K to ℤₚᵈ as topological groups.

Equations

• MvZpExtension p ι K Kinf = EquivMvZp (Kinf ≃ₐ[K] Kinf) p ι

noncomputable def MvZpExtension.congr {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : MvZpExtension p ι K Kinf) {ι' : Type u_4} (e : ι ≃ ι') (Kinf' : Type u_5) [Field Kinf'] [Algebra K Kinf'] (f : Kinf ≃ₐ[K] Kinf') [IsGalois K Kinf'] : MvZpExtension p ι' K Kinf'

Transfer MvZpExtension along field isomorphisms.

Equations

• H.congr e Kinf' f = EquivMvZp.congr H f.continuousAutCongr e

instance MvZpExtension.normal {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : MvZpExtension p ι K Kinf) (G : Subgroup (EquivMvZp.Γ H)) : G.Normal

Any subgroup in Γ is a normal subgroup.

noncomputable def MvZpExtension.Kn {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [Finite ι] [IsGalois K Kinf] (H : MvZpExtension p ι K Kinf) (n : ℕ) : IntermediateField K Kinf

The intermediate field Kₙ of K∞ / K fixed by Γ ^ (p ^ n).

Equations

• H.Kn n = IntermediateField.fixedField ↑(EquivMvZp.Γpow H n).toOpenSubgroup

@[simp]

theorem MvZpExtension.Kn_zero {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [Finite ι] [IsGalois K Kinf] (H : MvZpExtension p ι K Kinf) : H.Kn 0 = ⊥

K₀ = K.

theorem MvZpExtension.isGalois {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : MvZpExtension p ι K Kinf) (K' : IntermediateField K Kinf) : IsGalois K ↥K'

Any intermediate field of K∞ / K is Galois.

instance MvZpExtension.isGalois_Kn {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [Finite ι] [IsGalois K Kinf] (H : MvZpExtension p ι K Kinf) (n : ℕ) : IsGalois K ↥(H.Kn n)

Kₙ / K is Galois.

@[simp]

theorem MvZpExtension.fixingSubgroup_Kn {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [Finite ι] [IsGalois K Kinf] (H : MvZpExtension p ι K Kinf) (n : ℕ) : (H.Kn n).fixingSubgroup = ↑(EquivMvZp.Γpow H n).toOpenSubgroup

The fixing subgroup of Kₙ is Γ ^ (p ^ n).

instance MvZpExtension.finiteDimensional_Kn {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [Finite ι] [IsGalois K Kinf] (H : MvZpExtension p ι K Kinf) (n : ℕ) : FiniteDimensional K ↥(H.Kn n)

Kₙ / K is a finite extension.

@[simp]

theorem MvZpExtension.finrank_Kn {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [Finite ι] [IsGalois K Kinf] (H : MvZpExtension p ι K Kinf) (n : ℕ) : Module.finrank K ↥(H.Kn n) = p ^ (n * Nat.card ι)

Kₙ / K is of degree p ^ (n * #ι).

theorem MvZpExtension.monotone_Kn {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [Finite ι] [IsGalois K Kinf] (H : MvZpExtension p ι K Kinf) : Monotone H.Kn

If m ≤ n then Kₘ ≤ Kₙ.

theorem MvZpExtension.strictMono_Kn {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [Finite ι] [IsGalois K Kinf] (H : MvZpExtension p ι K Kinf) [Nonempty ι] : StrictMono H.Kn

If m < n then Kₘ < Kₙ.

theorem MvZpExtension.le_Kn_of_finite {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [Finite ι] [IsGalois K Kinf] (H : MvZpExtension p ι K Kinf) (K' : IntermediateField K Kinf) [FiniteDimensional K ↥K'] : ∃ (n : ℕ), K' ≤ H.Kn n

If K' is a finite extension of K contained in K∞, then it's contained in Kₙ for some n.

theorem MvZpExtension.finrank_eq_pow_of_finite {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [Finite ι] [IsGalois K Kinf] (H : MvZpExtension p ι K Kinf) (K' : IntermediateField K Kinf) [FiniteDimensional K ↥K'] : ∃ (n : ℕ), Module.finrank K ↥K' = p ^ n

If K' is a finite extension of K contained in K∞, then [K' : K] = p ^ n for some n.

ℤₚ-extension

noncomputable def MvZpExtension.ofContinuousMulEquiv₁ {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [Unique ι] [IsGalois K Kinf] (e : (Kinf ≃ₐ[K] Kinf) ≃ₜ* Multiplicative ℤ_[p]) : MvZpExtension p ι K Kinf

An isomorphism from Γ to ℤₚ gives an MvZpExtension when ι consists of exactly one element.

Equations

• MvZpExtension.ofContinuousMulEquiv₁ e = EquivMvZp.ofContinuousMulEquiv₁ e

theorem MvZpExtension.finrank_Kn₁ {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [Unique ι] [IsGalois K Kinf] (H : MvZpExtension p ι K Kinf) (n : ℕ) : Module.finrank K ↥(H.Kn n) = p ^ n

Kₙ / K is of degree p ^ n.

theorem MvZpExtension.eq_Kn_of_finite {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [Unique ι] [IsGalois K Kinf] (H : MvZpExtension p ι K Kinf) (K' : IntermediateField K Kinf) [FiniteDimensional K ↥K'] : ∃ (n : ℕ), K' = H.Kn n

If K' is a finite extension of K contained in K∞, then it's equal to Kₙ for some n.

theorem MvZpExtension.eq_top_or_Kn {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [Unique ι] [IsGalois K Kinf] (H : MvZpExtension p ι K Kinf) (K' : IntermediateField K Kinf) : K' = ⊤ ∨ ∃ (n : ℕ), K' = H.Kn n

If K' is an extension of K contained in K∞, then it's equal to K∞ or Kₙ for some n.

theorem MvZpExtension.eq_top_of_infinite {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [Unique ι] [IsGalois K Kinf] (H : MvZpExtension p ι K Kinf) (K' : IntermediateField K Kinf) (h : ¬FiniteDimensional K ↥K') : K' = ⊤

If K' is an infinite extension of K contained in K∞, then it's equal to K∞.

theorem MvZpExtension.eq_Kn_of_finrank_eq {p : ℕ} [Fact (Nat.Prime p)] {ι : Type u_1} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [Unique ι] [IsGalois K Kinf] (H : MvZpExtension p ι K Kinf) (K' : IntermediateField K Kinf) {n : ℕ} (h : Module.finrank K ↥K' = p ^ n) : K' = H.Kn n

If K' is an extension of K of degree p ^ n contained in K∞, then it's equal to Kₙ.

Prop version

def IsMvZpExtension (p : ℕ) [Fact (Nat.Prime p)] (d : ℕ) (K : Type u_2) (Kinf : Type u_3) [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] : Prop

IsMvZpExtension is a Prop which asserts that a Galois extension is with Galois group isomorphic to ℤₚᵈ as a topological group.

Equations

• IsMvZpExtension p d K Kinf = IsEquivMvZp (Kinf ≃ₐ[K] Kinf) p d

theorem IsMvZpExtension.congr {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (Kinf' : Type u_4) [Field Kinf'] [Algebra K Kinf'] (f : Kinf ≃ₐ[K] Kinf') [IsGalois K Kinf'] : IsMvZpExtension p d K Kinf'

Transfer IsMvZpExtension along field isomorphisms.

noncomputable def IsMvZpExtension.mvZpExtension {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) : MvZpExtension p (Fin d) K Kinf

A random isomorphism from Γ to ℤₚᵈ.

Equations

• H.mvZpExtension = Nonempty.some H

instance IsMvZpExtension.normal {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (G : Subgroup (IsEquivMvZp.Γ H)) : G.Normal

Any subgroup in Γ is a normal subgroup.

noncomputable def IsMvZpExtension.Kn {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (n : ℕ) : IntermediateField K Kinf

The intermediate field Kₙ of K∞ / K fixed by Γ ^ (p ^ n).

Equations

• H.Kn n = H.mvZpExtension.Kn n

@[simp]

theorem IsMvZpExtension.Kn_zero {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) : H.Kn 0 = ⊥

K₀ = K.

theorem IsMvZpExtension.isGalois {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (K' : IntermediateField K Kinf) : IsGalois K ↥K'

Any intermediate field of K∞ / K is Galois.

instance IsMvZpExtension.isGalois_Kn {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (n : ℕ) : IsGalois K ↥(H.Kn n)

Kₙ / K is Galois.

@[simp]

theorem IsMvZpExtension.fixingSubgroup_Kn {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (n : ℕ) : (H.Kn n).fixingSubgroup = ↑(IsEquivMvZp.Γpow H n).toOpenSubgroup

The fixing subgroup of Kₙ is Γ ^ (p ^ n).

instance IsMvZpExtension.finiteDimensional_Kn {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (n : ℕ) : FiniteDimensional K ↥(H.Kn n)

Kₙ / K is a finite extension.

@[simp]

theorem IsMvZpExtension.finrank_Kn {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (n : ℕ) : Module.finrank K ↥(H.Kn n) = p ^ (n * d)

Kₙ / K is of degree p ^ (n * d).

theorem IsMvZpExtension.monotone_Kn {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) : Monotone H.Kn

If m ≤ n then Kₘ ≤ Kₙ.

theorem IsMvZpExtension.strictMono_Kn {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) [NeZero d] : StrictMono H.Kn

If m < n then Kₘ < Kₙ.

theorem IsMvZpExtension.le_Kn_of_finite {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (K' : IntermediateField K Kinf) [FiniteDimensional K ↥K'] : ∃ (n : ℕ), K' ≤ H.Kn n

If K' is a finite extension of K contained in K∞, then it's contained in Kₙ for some n.

theorem IsMvZpExtension.finrank_eq_pow_of_finite {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p d K Kinf) (K' : IntermediateField K Kinf) [FiniteDimensional K ↥K'] : ∃ (n : ℕ), Module.finrank K ↥K' = p ^ n

If K' is a finite extension of K contained in K∞, then [K' : K] = p ^ n for some n.

ℤₚ-extension

theorem isMvZpExtension₁_iff {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] : IsMvZpExtension p 1 K Kinf ↔ Nonempty ((Kinf ≃ₐ[K] Kinf) ≃ₜ* Multiplicative ℤ_[p])

theorem IsMvZpExtension.finrank_Kn₁ {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p 1 K Kinf) (n : ℕ) : Module.finrank K ↥(H.Kn n) = p ^ n

Kₙ / K is of degree p ^ n.

theorem IsMvZpExtension.eq_Kn_of_finite {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p 1 K Kinf) (K' : IntermediateField K Kinf) [FiniteDimensional K ↥K'] : ∃ (n : ℕ), K' = H.Kn n

If K' is a finite extension of K contained in K∞, then it's equal to Kₙ for some n.

theorem IsMvZpExtension.eq_top_or_Kn {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p 1 K Kinf) (K' : IntermediateField K Kinf) : K' = ⊤ ∨ ∃ (n : ℕ), K' = H.Kn n

If K' is an extension of K contained in K∞, then it's equal to K∞ or Kₙ for some n.

theorem IsMvZpExtension.eq_top_of_infinite {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p 1 K Kinf) (K' : IntermediateField K Kinf) (h : ¬FiniteDimensional K ↥K') : K' = ⊤

If K' is an infinite extension of K contained in K∞, then it's equal to K∞.

theorem IsMvZpExtension.eq_Kn_of_finrank_eq {p : ℕ} [Fact (Nat.Prime p)] {K : Type u_2} {Kinf : Type u_3} [Field K] [Field Kinf] [Algebra K Kinf] [IsGalois K Kinf] (H : IsMvZpExtension p 1 K Kinf) (K' : IntermediateField K Kinf) {n : ℕ} (h : Module.finrank K ↥K' = p ^ n) : K' = H.Kn n

If K' is an extension of K of degree p ^ n contained in K∞, then it's equal to Kₙ.