Module

Valuation.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.ClassFormation.Valuation

13 declarations indexed from sourceView source ↗

Module documentation

Provides the public declarations in the LocalClassFieldTheory.ClassFormation.Valuation Lean module.

Imports4

Imported by6

def

galoisGroupFieldUnitsMulDistribMulAction

L30 ↗

LocalClassFieldTheory.galoisGroupFieldUnitsMulDistribMulAction

Documentation

The actual Gal(L / K) action on field units, obtained by applying each field automorphism to a unit.

Source context 6 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open IsNonarchimedeanLocalField

Lean source · full declaration

def galoisGroupFieldUnitsMulDistribMulAction
    (K L : Type u) [Field K] [Field L] [Algebra K L] :
    MulDistribMulAction (Gal(L / K)) Lˣ where
  smul σ x := Units.mapEquiv σ.toMulEquiv x
  one_smul := by
    intro x
    ext
    rfl
  mul_smul := by
    intro σ τ x
    ext
    rfl
  smul_mul := by
    intro σ x y
    exact map_mul (Units.mapEquiv σ.toMulEquiv) x y
  smul_one := by
    intro σ
    exact map_one (Units.mapEquiv σ.toMulEquiv)

theorem

galoisGroupFieldUnitsMulDistribMulAction_smul

L51 ↗

LocalClassFieldTheory.galoisGroupFieldUnitsMulDistribMulAction_smul

Documentation

States the theorem galoisGroupFieldUnitsMulDistribMulAction_smul.

Source context 6 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open IsNonarchimedeanLocalField

Lean source · full declaration

theorem galoisGroupFieldUnitsMulDistribMulAction_smul
    (K L : Type u) [Field K] [Field L] [Algebra K L]
    (σ : Gal(L/K)) (x : Lˣ) :
    letI := galoisGroupFieldUnitsMulDistribMulAction K L
    σ • x = Units.mapEquiv σ.toMulEquiv x :=
  rfl

def

galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure

L61 ↗

LocalClassFieldTheory.galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure

Documentation

The actual Gal(L / K) action on integer units. Its source is the restriction of the field automorphism to the integral closure 𝒪[L].

Source context 6 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open IsNonarchimedeanLocalField

Lean source · full declaration

def galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L] :
    MulDistribMulAction (Gal(L / K)) 𝒪[L]ˣ where
  smul σ x := Units.mapEquiv
    (galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ).toMulEquiv x
  one_smul := by
    intro x
    ext
    rfl
  mul_smul := by
    intro σ τ x
    ext
    rfl
  smul_mul := by
    intro σ x y
    exact map_mul
      (Units.mapEquiv
        (galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ).toMulEquiv) x y
  smul_one := by
    intro σ
    exact map_one
      (Units.mapEquiv
        (galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ).toMulEquiv)

theorem

galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure_smul

L90 ↗

LocalClassFieldTheory.galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure_smul

Documentation

States the theorem galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure_smul.

Source context 6 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open IsNonarchimedeanLocalField

Lean source · full declaration

theorem galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure_smul
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (σ : Gal(L/K)) (x : 𝒪[L]ˣ) :
    letI := galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L
    σ • x = Units.mapEquiv
      (galoisGroupIntegerRingEquivOfIsIntegralClosure K L σ).toMulEquiv x :=
  rfl

def

galoisGroupValueGroupMulDistribMulAction

L104 ↗

LocalClassFieldTheory.galoisGroupValueGroupMulDistribMulAction

Documentation

The trivial Galois action on the value group ℤ, written multiplicatively so that it is a multiplicative Galois module.

Source context 6 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open IsNonarchimedeanLocalField

Lean source · full declaration

def galoisGroupValueGroupMulDistribMulAction
    (K L : Type u) [Field K] [Field L] [Algebra K L] :
    MulDistribMulAction (Gal(L / K)) (Multiplicative Int) where
  smul _ n := n
  one_smul := by intro n; rfl
  mul_smul := by intro _ _ n; rfl
  smul_mul := by intro _ m n; rfl
  smul_one := by intro _; rfl

theorem

galoisGroupValueGroupMulDistribMulAction_smul

L115 ↗

LocalClassFieldTheory.galoisGroupValueGroupMulDistribMulAction_smul

Documentation

States the theorem galoisGroupValueGroupMulDistribMulAction_smul.

Source context 6 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open IsNonarchimedeanLocalField

Lean source · full declaration

theorem galoisGroupValueGroupMulDistribMulAction_smul
    (K L : Type u) [Field K] [Field L] [Algebra K L]
    (σ : Gal(L/K)) (n : Multiplicative Int) :
    letI := galoisGroupValueGroupMulDistribMulAction K L
    σ • n = n :=
  rfl

theorem

integerUnitsToFieldUnits_galoisGroup_equivariant

L123 ↗

LocalClassFieldTheory.integerUnitsToFieldUnits_galoisGroup_equivariant

Documentation

The inclusion 𝒪_Lˣ → Lˣ is equivariant for the actual actions.

Source context 6 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open IsNonarchimedeanLocalField

Lean source · full declaration

theorem integerUnitsToFieldUnits_galoisGroup_equivariant
    (K L : Type u) [Field K] [ValuativeRel K] [Field L] [ValuativeRel L]
    [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (σ : Gal(L/K)) (x : 𝒪[L]ˣ) :
    letI := galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L
    letI := galoisGroupFieldUnitsMulDistribMulAction K L
    integerUnitsToFieldUnits L (σ • x) =
      σ • integerUnitsToFieldUnits L x := by
  let := galoisGroupIntegerUnitsMulDistribMulActionOfIsIntegralClosure K L
  let := galoisGroupFieldUnitsMulDistribMulAction K L
  ext
  rfl

theorem

valuationMap_unitsMapEquiv_galoisGroup

L142 ↗

LocalClassFieldTheory.valuationMap_unitsMapEquiv_galoisGroup

Documentation

A Galois automorphism preserves the normalized additive valuation. The proof uses only the actual integral-closure restriction to 𝒪_L, the DVR normalization of an irreducible uniformizer, and the unit--uniformizer decomposition of Lˣ; no extension-invariant package is assumed.

Source context 6 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open IsNonarchimedeanLocalField

Lean source · statement

theorem valuationMap_unitsMapEquiv_galoisGroup
    (K L : Type u) [Field K] [ValuativeRel K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (σ : Gal(L/K)) (x : Lˣ) :
    valuationMap L
        (Additive.ofMul (Units.mapEquiv σ.toMulEquiv x)) =
      valuationMap L (Additive.ofMul x)

theorem

valuationUnitsMulHom_galoisGroup_equivariant

L209 ↗

LocalClassFieldTheory.valuationUnitsMulHom_galoisGroup_equivariant

Documentation

The normalized valuation on Lˣ is equivariant for the actual Galois action and the trivial action on its value group.

Source context 6 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open IsNonarchimedeanLocalField

Lean source · full declaration

theorem valuationUnitsMulHom_galoisGroup_equivariant
    (K L : Type u) [Field K] [ValuativeRel K]
    [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] [Algebra K L]
    [Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    (σ : Gal(L/K)) (x : Lˣ) :
    letI := galoisGroupFieldUnitsMulDistribMulAction K L
    letI := galoisGroupValueGroupMulDistribMulAction K L
    valuationUnitsMulHom L (σ • x) =
      σ • valuationUnitsMulHom L x := by
  let := galoisGroupFieldUnitsMulDistribMulAction K L
  let := galoisGroupValueGroupMulDistribMulAction K L
  exact congrArg Multiplicative.ofAdd
    (valuationMap_unitsMapEquiv_galoisGroup K L σ x)

theorem

valuationUnitsMulHom_eq_one_iff_valuationMap_eq_zero

L227 ↗

LocalClassFieldTheory.valuationUnitsMulHom_eq_one_iff_valuationMap_eq_zero

Documentation

Multiplicative and additive presentations of valuation-one/valuation-zero agree for a field unit.

Source context 6 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open IsNonarchimedeanLocalField

Lean source · statement

theorem valuationUnitsMulHom_eq_one_iff_valuationMap_eq_zero
    (L : Type u) [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] (x : Lˣ) :
    valuationUnitsMulHom L x = 1 ↔
      valuationMap L (Additive.ofMul x) = 0

theorem

valuationUnitsMulHom_eq_one_iff_exists_integerUnit

L243 ↗

LocalClassFieldTheory.valuationUnitsMulHom_eq_one_iff_exists_integerUnit

Documentation

Exactness at Lˣ: the kernel of normalized valuation consists exactly of the units of the valuation integer ring.

Source context 6 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open IsNonarchimedeanLocalField

Lean source · statement

theorem valuationUnitsMulHom_eq_one_iff_exists_integerUnit
    (L : Type u) [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] (x : Lˣ) :
    valuationUnitsMulHom L x = 1 ↔
      ∃ y : 𝒪[L]ˣ, integerUnitsToFieldUnits L y = x

theorem

integerUnitsToFieldUnits_range_eq_ker_valuationUnitsMulHom

L260 ↗

LocalClassFieldTheory.integerUnitsToFieldUnits_range_eq_ker_valuationUnitsMulHom

Documentation

Exactness of the multiplicative valuation sequence at Lˣ, stated as the equality of the actual range and kernel subgroups.

Source context 6 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open IsNonarchimedeanLocalField

Lean source · statement

theorem integerUnitsToFieldUnits_range_eq_ker_valuationUnitsMulHom
    (L : Type u) [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] :
    MonoidHom.range (integerUnitsToFieldUnits L) =
      MonoidHom.ker (valuationUnitsMulHom L)

theorem

valuationUnitsMulHom_surjective

L272 ↗

LocalClassFieldTheory.valuationUnitsMulHom_surjective

Documentation

The multiplicative normalized valuation Lˣ → Multiplicative ℤ is surjective.

Source context 6 commands

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

namespace LocalClassFieldTheory
open LocalFieldTheory
noncomputable section
universe u
open scoped ValuativeRel
open IsNonarchimedeanLocalField

Lean source · statement

theorem valuationUnitsMulHom_surjective
    (L : Type u) [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] :
    Function.Surjective (valuationUnitsMulHom L)

Module documentation

Declarations