ℤₚ-extension of fields

In this file, when Kinf / K is a Galois extension of fields, we define MvZpExtension p ι K Kinf, which is an isomorphism of Gal(Kinf / K) and Multiplicative (ι → ℤ_[p]) as topological groups.

To state that Gal(Kinf / K) is isomorphic to Multiplicative (ι → ℤ_[p]) as topological groups, use Nonempty (MvZpExtension p ι K Kinf). As a special case, to state that Kinf / K is a ℤₚᵈ-extension, use Nonempty (MvZpExtension p (Fin d) K Kinf).

ℤₚᵈ-extension

@[reducible, inline]

abbrev 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 Gal(Kinf/K) 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 f = EquivMvZp.congr H f.continuousAutCongr e

noncomputable def MvZpExtension.congrFinOfCardEq {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) {d : ℕ} (h : Nat.card ι = d) {Kinf' : Type u_4} [Field Kinf'] [Algebra K Kinf'] (f : Kinf ≃ₐ[K] Kinf') [IsGalois K Kinf'] : MvZpExtension p (Fin d) K Kinf'

Version of MvZpExtension.congr for finite case.

Equations

• H.congrFinOfCardEq h f = H.congr (Finite.equivFinOfCardEq h) f

theorem MvZpExtension.isAbelianGalois_Kinf {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) : IsAbelianGalois K Kinf

K∞ / K is abelian.

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.

theorem MvZpExtension.isAbelianGalois {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) : IsAbelianGalois K ↥K'

Any intermediate field of K∞ / K is abelian.

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.

instance MvZpExtension.isAbelianGalois_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 : ℕ) : IsAbelianGalois K ↥(H.Kn n)

Kₙ / K is abelian.

@[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_finiteDimensional {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_finiteDimensional {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.

theorem MvZpExtension.finiteDimensional_iff_isEmpty {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) : FiniteDimensional K Kinf ↔ IsEmpty ι

theorem MvZpExtension.finiteDimensional_iff_card_eq_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) : FiniteDimensional K Kinf ↔ Nat.card ι = 0

theorem MvZpExtension.infinite_dimensional {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 ι] : ¬FiniteDimensional K Kinf

ℤₚ-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 : Gal(Kinf/K) ≃ₜ* 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.nonempty_iff_of_unique {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] : Nonempty (MvZpExtension p ι K Kinf) ↔ Nonempty (Gal(Kinf/K) ≃ₜ* Multiplicative ℤ_[p])

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_finiteDimensional {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_dimensional {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ₙ.