Module

UnramifiedNormComparison.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Finite.LocalReciprocity.UnramifiedNormComparison

12 declarations indexed from sourceView source ↗

Module documentation

Norm quotients for unramified local extensions

For a finite unramified Galois extension, the field-norm subgroup is exactly the subgroup of elements whose normalized valuation is divisible by the extension degree. The inclusion is the normalized norm formula; the reverse inclusion follows from finite local reciprocity because the norm quotient and the valuation quotient have the same finite cardinality.

Imports5

Imported by7

theorem

localNormSubgroup_le_unramifiedNormSubgroup

L47 ↗

LocalClassFieldTheory.localNormSubgroup_le_unramifiedNormSubgroup

Documentation

Every field norm has normalized valuation divisible by the degree.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (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]
  [Module.Finite 𝒪[K] 𝒪[L]]
  [IsUnramifiedValuedExtension K L]

Lean source · statement

theorem localNormSubgroup_le_unramifiedNormSubgroup :
    localNormSubgroup K L ≤
      unramifiedNormSubgroup K (Module.finrank K L)

def

normQuotientToUnramifiedNormQuotient

L62 ↗

LocalClassFieldTheory.normQuotientToUnramifiedNormQuotient

Documentation

The canonical map from the norm quotient to the valuation quotient.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (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]
  [Module.Finite 𝒪[K] 𝒪[L]]
  [IsUnramifiedValuedExtension K L]

Lean source · statement

def normQuotientToUnramifiedNormQuotient :
    NormQuotient K L →*
      Kˣ ⧸ unramifiedNormSubgroup K (Module.finrank K L)

theorem

normQuotientToUnramifiedNormQuotient_mk

L75 ↗

LocalClassFieldTheory.normQuotientToUnramifiedNormQuotient_mk

Documentation

The comparison map sends a norm class to the corresponding unramified valuation class.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (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]
  [Module.Finite 𝒪[K] 𝒪[L]]
  [IsUnramifiedValuedExtension K L]

Lean source · statement

theorem normQuotientToUnramifiedNormQuotient_mk (x : Kˣ) :
    normQuotientToUnramifiedNormQuotient K L
        (normClass K L x) =
      unramifiedNormClass K (Module.finrank K L) x

theorem

normQuotientToUnramifiedNormQuotient_surjective

L82 ↗

LocalClassFieldTheory.normQuotientToUnramifiedNormQuotient_surjective

Documentation

Every unramified valuation class is represented by an actual norm quotient class.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (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]
  [Module.Finite 𝒪[K] 𝒪[L]]
  [IsUnramifiedValuedExtension K L]

Lean source · statement

theorem normQuotientToUnramifiedNormQuotient_surjective :
    Function.Surjective
      (normQuotientToUnramifiedNormQuotient K L)

def

galoisGroupEquivAbelianizationOfUnramifiedValuation

L95 ↗

LocalClassFieldTheory.galoisGroupEquivAbelianizationOfUnramifiedValuation

Documentation

Cyclicity identifies the unramified Galois group with its abelianization.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (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]
  [Module.Finite 𝒪[K] 𝒪[L]]
  [IsUnramifiedValuedExtension K L]

Lean source · statement

def galoisGroupEquivAbelianizationOfUnramifiedValuation :
    Gal(L / K) ≃* Abelianization (Gal(L / K))

theorem

galoisGroupEquivAbelianizationOfUnramifiedValuation_apply

L105 ↗

LocalClassFieldTheory.galoisGroupEquivAbelianizationOfUnramifiedValuation_apply

Documentation

The cyclic Galois-group equivalence is the canonical map to the abelianization.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (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]
  [Module.Finite 𝒪[K] 𝒪[L]]
  [IsUnramifiedValuedExtension K L]

Lean source · statement

theorem galoisGroupEquivAbelianizationOfUnramifiedValuation_apply
    (σ : Gal(L/K)) :
    galoisGroupEquivAbelianizationOfUnramifiedValuation K L σ =
      Abelianization.of σ

instance

unramifiedNormComparisonNormQuotientFinite

L111 ↗

LocalClassFieldTheory.unramifiedNormComparisonNormQuotientFinite

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (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]
  [Module.Finite 𝒪[K] 𝒪[L]]
  [IsUnramifiedValuedExtension K L]

Lean source · statement

instance unramifiedNormComparisonNormQuotientFinite :
    Finite (NormQuotient K L)

theorem

normQuotient_card_eq_finrank

L117 ↗

LocalClassFieldTheory.normQuotient_card_eq_finrank

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (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]
  [Module.Finite 𝒪[K] 𝒪[L]]
  [IsUnramifiedValuedExtension K L]
noncomputable local instance unramifiedNormComparisonNormQuotientFinite :
    Finite (NormQuotient K L) :=
  Finite.of_equiv (Gal(L / K))
    ((galoisGroupEquivAbelianizationOfUnramifiedValuation K L).toEquiv.trans
      (abelianizationEquivNormQuotient K L).toEquiv)

Lean source · statement

theorem normQuotient_card_eq_finrank :
    Nat.card (NormQuotient K L) = Module.finrank K L

theorem

normQuotientToUnramifiedNormQuotient_injective

L132 ↗

LocalClassFieldTheory.normQuotientToUnramifiedNormQuotient_injective

Documentation

The comparison from the actual norm quotient to the valuation quotient is injective.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (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]
  [Module.Finite 𝒪[K] 𝒪[L]]
  [IsUnramifiedValuedExtension K L]
noncomputable local instance unramifiedNormComparisonNormQuotientFinite :
    Finite (NormQuotient K L) :=
  Finite.of_equiv (Gal(L / K))
    ((galoisGroupEquivAbelianizationOfUnramifiedValuation K L).toEquiv.trans
      (abelianizationEquivNormQuotient K L).toEquiv)

Lean source · statement

theorem normQuotientToUnramifiedNormQuotient_injective :
    Function.Injective
      (normQuotientToUnramifiedNormQuotient K L)

theorem

normSubgroup_eq_unramifiedNormSubgroup_of_isIntegralClosure

L157 ↗

LocalClassFieldTheory.normSubgroup_eq_unramifiedNormSubgroup_of_isIntegralClosure

Documentation

The actual norm subgroup is the valuation-divisibility subgroup.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (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]
  [Module.Finite 𝒪[K] 𝒪[L]]
  [IsUnramifiedValuedExtension K L]
noncomputable local instance unramifiedNormComparisonNormQuotientFinite :
    Finite (NormQuotient K L) :=
  Finite.of_equiv (Gal(L / K))
    ((galoisGroupEquivAbelianizationOfUnramifiedValuation K L).toEquiv.trans
      (abelianizationEquivNormQuotient K L).toEquiv)

Lean source · statement

theorem normSubgroup_eq_unramifiedNormSubgroup_of_isIntegralClosure :
    localNormSubgroup K L =
      unramifiedNormSubgroup K (Module.finrank K L)

def

normQuotientUnramifiedValuationEquivZModOfIsIntegralClosure

L170 ↗

LocalClassFieldTheory.normQuotientUnramifiedValuationEquivZModOfIsIntegralClosure

Documentation

The actual unramified norm quotient is the normalized valuation quotient.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (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]
  [Module.Finite 𝒪[K] 𝒪[L]]
  [IsUnramifiedValuedExtension K L]
noncomputable local instance unramifiedNormComparisonNormQuotientFinite :
    Finite (NormQuotient K L) :=
  Finite.of_equiv (Gal(L / K))
    ((galoisGroupEquivAbelianizationOfUnramifiedValuation K L).toEquiv.trans
      (abelianizationEquivNormQuotient K L).toEquiv)

Lean source · statement

def normQuotientUnramifiedValuationEquivZModOfIsIntegralClosure :
    NormQuotient K L ≃*
      Multiplicative (ZMod (Module.finrank K L))

theorem

normQuotientUnramifiedValuationEquivZModOfIsIntegralClosure_mk

L180 ↗

LocalClassFieldTheory.normQuotientUnramifiedValuationEquivZModOfIsIntegralClosure_mk

Documentation

The unramified norm-quotient equivalence sends a unit class to its reduced valuation.

Source context 7 commands

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

noncomputable section
namespace LocalClassFieldTheory
open scoped ValuativeRel
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (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]
  [Module.Finite 𝒪[K] 𝒪[L]]
  [IsUnramifiedValuedExtension K L]
noncomputable local instance unramifiedNormComparisonNormQuotientFinite :
    Finite (NormQuotient K L) :=
  Finite.of_equiv (Gal(L / K))
    ((galoisGroupEquivAbelianizationOfUnramifiedValuation K L).toEquiv.trans
      (abelianizationEquivNormQuotient K L).toEquiv)

Lean source · statement

theorem normQuotientUnramifiedValuationEquivZModOfIsIntegralClosure_mk
    (x : Kˣ) :
    normQuotientUnramifiedValuationEquivZModOfIsIntegralClosure K L
        (normClass K L x) =
      valuationModDegreeMulHom K (Module.finrank K L) x

Module documentation

Norm quotients for unramified local extensions

Declarations