Module

UnramifiedConductor.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.UnramifiedConductor

10 declarations indexed from sourceView source ↗

Module documentation

Conductors and unramified extensions

For an unramified finite abelian extension, normalized valuation identifies the norm subgroup and shows that all base-field units are norms. Hence its conductor ideal is 1.

Conversely, conductor one identifies the norm quotient order with the residue degree. Finite local reciprocity and the degree formula then force the ramification index to be one.

Imports5

Mathlib.SetTheory.Cardinal.Finite
Mathlib.FieldTheory.Galois.Abelian
Mathlib.GroupTheory.Abelianization.Defs
Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.Conductor
Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.UnramifiedNormComparison

Imported by5

theorem

normQuotientFiniteOfIsAbelianGalois

L35 ↗

LocalClassFieldTheory.normQuotientFiniteOfIsAbelianGalois

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel IsMulCommutative
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem normQuotientFiniteOfIsAbelianGalois
    (K L : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [Algebra K L] [FiniteDimensional K L] [IsAbelianGalois K L] :
    Finite (NormQuotient K L)

def

chosenNormQuotientEquivZModResidueFinrank_of_fieldPrincipalUnits_zero_le

L50 ↗

LocalClassFieldTheory.chosenNormQuotientEquivZModResidueFinrank_of_fieldPrincipalUnits_zero_le

Documentation

If every base integer unit is a norm, the actual norm quotient is the cyclic quotient of the normalized value group by the residue degree.

This value-group comparison uses the separable norm-valuation formula for its residue degree; no unramifiedness assumption is made here.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel IsMulCommutative
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

def
    chosenNormQuotientEquivZModResidueFinrank_of_fieldPrincipalUnits_zero_le
    (K L : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [IsGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (hU : LocalFieldTheory.fieldPrincipalUnits K 0 ≤ localNormSubgroup K L) :
    NormQuotient K L ≃*
      Multiplicative
        (ZMod
          (@Module.finrank 𝓀[K] 𝓀[L] _ _
            (IsLocalRing.ResidueField.instModule
              (R := 𝒪[K])
              (S := 𝒪[L]))))

theorem

card_normQuotient_eq_finrank_of_isAbelianGalois

L115 ↗

LocalClassFieldTheory.card_normQuotient_eq_finrank_of_isAbelianGalois

Documentation

Finite local reciprocity gives the order of the norm quotient in a finite abelian extension: it is the field degree.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel IsMulCommutative
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · full declaration

theorem card_normQuotient_eq_finrank_of_isAbelianGalois
    (K L : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [Algebra K L] [FiniteDimensional K L] [IsAbelianGalois K L] :
    letI : Finite (NormQuotient K L) :=
      normQuotientFiniteOfIsAbelianGalois K L
    Nat.card (NormQuotient K L) = Module.finrank K L := by
  let : Finite (NormQuotient K L) :=
    normQuotientFiniteOfIsAbelianGalois K L
  let : Finite (Abelianization Gal(L / K)) :=
    Finite.of_equiv Gal(L / K)
      (Abelianization.equivOfComm (H := Gal(L / K))).toEquiv
  calc
    Nat.card (NormQuotient K L) =
        Nat.card (Abelianization Gal(L / K)) :=
      Nat.card_congr (abelianizationEquivNormQuotient K L).toEquiv.symm
    _ = Nat.card Gal(L / K) :=
      Nat.card_congr (Abelianization.equivOfComm
        (H := Gal(L / K))).toEquiv.symm
    _ = Module.finrank K L := galoisGroup_card_eq_finrank K L

theorem

fieldPrincipalUnits_zero_le_normSubgroup_of_unramifiedValuation

L139 ↗

LocalClassFieldTheory.fieldPrincipalUnits_zero_le_normSubgroup_of_unramifiedValuation

Documentation

In an actual finite unramified abelian extension, every base-field integer unit lies in the field-norm subgroup.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel IsMulCommutative
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem fieldPrincipalUnits_zero_le_normSubgroup_of_unramifiedValuation
    (K L : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [IsAbelianGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] :
    LocalFieldTheory.fieldPrincipalUnits K 0 ≤ localNormSubgroup K L

theorem

localConductorExponent_eq_zero_of_unramifiedValuation

L159 ↗

LocalClassFieldTheory.localConductorExponent_eq_zero_of_unramifiedValuation

Documentation

An unramified finite abelian extension has conductor exponent zero.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel IsMulCommutative
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem localConductorExponent_eq_zero_of_unramifiedValuation
    (K L : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [IsAbelianGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] :
    localConductorExponent K L = 0

theorem

localConductorIdeal_eq_one_of_unramifiedValuation

L176 ↗

LocalClassFieldTheory.localConductorIdeal_eq_one_of_unramifiedValuation

Documentation

An unramified finite abelian extension has conductor ideal 1.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel IsMulCommutative
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem localConductorIdeal_eq_one_of_unramifiedValuation
    (K L : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [IsAbelianGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L] :
    localConductorIdeal K L = 1

theorem

isFiniteUnramifiedValuationExtension_of_localConductorIdeal_eq_one

L198 ↗

LocalClassFieldTheory.isFiniteUnramifiedValuationExtension_of_localConductorIdeal_eq_one

Documentation

A finite abelian extension whose conductor ideal is 1 is unramified.

The proof compares two computations of the actual norm quotient. Its order is the residue degree by the norm-valuation formula and the conductor-one unit inclusion, while finite local reciprocity gives the field degree. Cancelling the positive residue degree gives ramification index one.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel IsMulCommutative
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem isFiniteUnramifiedValuationExtension_of_localConductorIdeal_eq_one
    (K L : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [IsAbelianGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    (hcond : localConductorIdeal K L = 1) :
    LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L

theorem

isFiniteUnramifiedValuationExtension_iff_localConductorIdeal_eq_one

L286 ↗

LocalClassFieldTheory.isFiniteUnramifiedValuationExtension_iff_localConductorIdeal_eq_one

Documentation

A finite abelian extension is unramified if and only if its conductor ideal is 1.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel IsMulCommutative
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem isFiniteUnramifiedValuationExtension_iff_localConductorIdeal_eq_one
    (K L : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [IsAbelianGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]] :
    LocalFieldTheory.IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L ↔
      localConductorIdeal K L = 1

theorem

isUnramifiedValuedExtension_iff_localConductorExponent_eq_zero

L308 ↗

LocalClassFieldTheory.isUnramifiedValuedExtension_iff_localConductorExponent_eq_zero

Documentation

A concrete finite abelian local extension is unramified exactly when its local conductor exponent is zero.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel IsMulCommutative
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem isUnramifiedValuedExtension_iff_localConductorExponent_eq_zero
    (K L : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [IsAbelianGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]] :
    IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L ↔
      localConductorExponent K L = 0

theorem

not_isUnramifiedValuedExtension_iff_localConductorExponent_ne_zero

L327 ↗

LocalClassFieldTheory.not_isUnramifiedValuedExtension_iff_localConductorExponent_ne_zero

Documentation

Equivalently, a concrete finite abelian local extension is ramified exactly when its local conductor exponent is nonzero.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel IsMulCommutative
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField

Lean source · statement

theorem
    not_isUnramifiedValuedExtension_iff_localConductorExponent_ne_zero
    (K L : Type)
    [Field K] [ValuativeRel K] [TopologicalSpace K]
    [IsNonarchimedeanLocalField K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L]
    [Algebra K L] [FiniteDimensional K L] [IsAbelianGalois K L]
    [Valuation.HasExtension (ValuativeRel.valuation K)
      (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]] :
    ¬ IsNonarchimedeanLocalField.IsUnramifiedValuedExtension K L ↔
      localConductorExponent K L ≠ 0

Module documentation

Conductors and unramified extensions

Declarations