Module

FieldUnitLogUniqueness.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.FieldUnitLogUniqueness

4 declarations indexed from sourceView source ↗

Module documentation

Uniqueness of logarithms on local-field units

This module isolates the torsion and unit-decomposition argument used to prove that an extension of the principal-unit logarithm is determined by its value on a uniformizer.

Imports1

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.FieldUnitDecomposition

Imported by2

theorem

residueField_card_sub_one_ne_zero

L33 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.residueField_card_sub_one_ne_zero

Documentation

In a complete discretely valued field with finite residue field, q - 1 is nonzero.

Source context 7 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem residueField_card_sub_one_ne_zero
    (F : CompleteDVF K) [Finite F.residueField] :
    Nat.card F.residueField - 1 ≠ 0

theorem

residueRootsOfUnity_fieldUnitHom_pow_card_sub_one_eq_one

L46 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.residueRootsOfUnity_fieldUnitHom_pow_card_sub_one_eq_one

Documentation

A Teichmüller factor in the field-unit decomposition has order dividing the residue-field cardinality minus one.

Source context 7 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem residueRootsOfUnity_fieldUnitHom_pow_card_sub_one_eq_one
    (F : CompleteDVF K) [Finite F.residueField]
    (ζ : CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F) :
    (CompleteDVF.higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
        (ζ : F.valuationSubringˣ)) ^ (Nat.card F.residueField - 1) = 1

theorem

monoidHom_toMultiplicative_residueRoot_eq_one

L66 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.monoidHom_toMultiplicative_residueRoot_eq_one

Documentation

Every homomorphism from field units to a torsion-free additive group kills the Teichmüller factor in the field-unit decomposition.

Source context 7 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem monoidHom_toMultiplicative_residueRoot_eq_one
    {A : Type*} [AddCommGroup A] [IsAddTorsionFree A]
    (F : CompleteDVF K) [Finite F.residueField]
    (φ : Kˣ →* Multiplicative A)
    (ζ : CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F) :
    φ (CompleteDVF.higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
        (ζ : F.valuationSubringˣ)) = 1

theorem

monoidHom_toMultiplicative_ext_of_agree_principalUnits_and_uniformizer

L91 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.monoidHom_toMultiplicative_ext_of_agree_principalUnits_and_uniformizer

Documentation

A homomorphism on field units with torsion-free additive target is determined by its values on principal units and on a chosen uniformizer.

Source context 7 commands

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

noncomputable section
universe u
open ValuationTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
namespace LocalFieldTheory.DiscreteValuationField
namespace MultiplicativeIntegerValuation
variable {K : Type u} [Field K]

Lean source · statement

theorem monoidHom_toMultiplicative_ext_of_agree_principalUnits_and_uniformizer
    {A : Type*} [AddCommGroup A] [IsAddTorsionFree A]
    (F : CompleteDVF K) [Finite F.residueField]
    (V : MultiplicativeIntegerValuation Kˣ)
    (hzero :
      ∀ y : Kˣ, y ∈ V.zeroSubgroup ↔
        ∃ u : F.valuationSubringˣ,
          CompleteDVF.higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F u = y)
    {ϖ : Kˣ} (hϖ : V.IsUniformizer ϖ)
    (φ ψ : Kˣ →* Multiplicative A)
    (hprincipal :
      ∀ u : (CompleteDVF.higherPrincipalUnitGroup F) 1,
        φ (CompleteDVF.higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
            (u : F.valuationSubringˣ)) =
          ψ (CompleteDVF.higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
            (u : F.valuationSubringˣ)))
    (huniformizer : φ ϖ = ψ ϖ) :
    φ = ψ

Module documentation

Uniqueness of logarithms on local-field units

Declarations

residueField_card_sub_one_ne_zero

residueRootsOfUnity_fieldUnitHom_pow_card_sub_one_eq_one

monoidHom_toMultiplicative_residueRoot_eq_one

monoidHom_toMultiplicative_ext_of_agree_principalUnits_and_uniformizer