Maximal unramified abelian p-extension Lₙ / Kₙ in a ℤₚ-extension tower K∞ / K

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

The maximal unramified abelian p-extension Lₙ / Kₙ of Kₙ, defined as an intermediate field of Hₙ / Kₙ where Hₙ is the Hilbert class field (NumberField.HilbertClassField) of Kₙ.

Equations

• H.Ln n = IntermediateField.maximalAbelianPExtension (↥(H.Kn n)) (NumberField.HilbertClassField ↥(H.Kn n)) p

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

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

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

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

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

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