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)) (SeparableClosure Kinf)
The maximal unramified abelian p-extension Lₙ / Kₙ of Kₙ, defined to be an
intermediate field of Kₙ and the separable closure of K∞.
Equations
- H.Ln n = IntermediateField.lift (IntermediateField.maximalGaloisSExtension ↥(H.Kn n) ↥(NumberField.maximalUnramifiedAbelianExtension (↥(H.Kn n)) (SeparableClosure Kinf)) {p})
Instances For
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 : ℕ)
:
theorem
IsSepClosure.ofSeparable
(K : Type u_4)
(J : Type u_5)
(L : Type u_6)
[Field K]
[Field J]
[Field L]
[Algebra K J]
[Algebra J L]
[IsSepClosure J L]
[Algebra K L]
[IsScalarTower K J L]
[Algebra.IsSeparable K J]
:
IsSepClosure K L
TODO: go mathlib