Module

FieldUnitLogExtension.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.FieldUnitLogExtension

14 declarations indexed from sourceView source ↗

Module documentation

Extending the logarithm to the field-unit group

The logarithm on first principal units does not extend by killing a chosen uniformizer. Its uniformizer value must instead be chosen so that the distinguished rational prime has logarithm zero. This file isolates that algebraic construction.

Imports1

Nyll.ValuedFieldTheory.LocalField.Analytic.LogExpSeries.Homomorphisms

Imported by2

def

fieldUnitDecompositionLogHomWithUniformizerValue

L36 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitDecompositionLogHomWithUniformizerValue

Documentation

Extend a homomorphism on first principal units to the three factors in the uniformizer–residue–principal-unit decomposition, killing the residue-root factor and assigning the additive value c to one power of the 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 · full declaration

def fieldUnitDecompositionLogHomWithUniformizerValue
    (F : CompleteDVF K) [Finite F.residueField]
    {A : Type*} [AddCommGroup A]
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A) (c : A) :
    CompleteDVF.higherPrincipalUnitGroup.fieldUnitDecompositionFactors F →*
      Multiplicative A where
  toFun z :=
    φ z.1.2 * Multiplicative.ofAdd (Multiplicative.toAdd z.2 • c)
  map_one' := by simp
  map_mul' z w := by
    apply Multiplicative.toAdd.injective
    change
      Multiplicative.toAdd (φ (z.1.2 * w.1.2)) +
          (Multiplicative.toAdd z.2 + Multiplicative.toAdd w.2) • c =
        (Multiplicative.toAdd (φ z.1.2) + Multiplicative.toAdd z.2 • c) +
          (Multiplicative.toAdd (φ w.1.2) + Multiplicative.toAdd w.2 • c)
    rw [φ.map_mul]
    simp only [toAdd_mul, add_zsmul]
    abel

theorem

fieldUnitDecompositionLogHomWithUniformizerValue_apply

L61 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitDecompositionLogHomWithUniformizerValue_apply

Documentation

The defining evaluation formula for fieldUnitDecompositionLogHomWithUniformizerValue is fieldUnitDecompositionLogHomWithUniformizerValue F φ c z = φ z.1.2 * Multiplicative.ofAdd (Multiplicative.toAdd z.2 • c).

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 fieldUnitDecompositionLogHomWithUniformizerValue_apply
    (F : CompleteDVF K) [Finite F.residueField]
    {A : Type*} [AddCommGroup A]
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A) (c : A)
    (z : CompleteDVF.higherPrincipalUnitGroup.fieldUnitDecompositionFactors F) :
    fieldUnitDecompositionLogHomWithUniformizerValue F φ c z =
      φ z.1.2 * Multiplicative.ofAdd (Multiplicative.toAdd z.2 • c)

theorem

fieldUnitDecompositionLogHomWithUniformizerValue_root

L74 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitDecompositionLogHomWithUniformizerValue_root

Documentation

Establishes the identity fieldUnitDecompositionLogHomWithUniformizerValue F φ c ((ζ, 1), (1 : Multiplicative ℤ)) = 1.

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 fieldUnitDecompositionLogHomWithUniformizerValue_root
    (F : CompleteDVF K) [Finite F.residueField]
    {A : Type*} [AddCommGroup A]
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A) (c : A)
    (ζ : CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F) :
    fieldUnitDecompositionLogHomWithUniformizerValue F φ c
        ((ζ, 1), (1 : Multiplicative ℤ)) = 1

theorem

fieldUnitDecompositionLogHomWithUniformizerValue_principal

L88 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitDecompositionLogHomWithUniformizerValue_principal

Documentation

Establishes the identity fieldUnitDecompositionLogHomWithUniformizerValue F φ c (((1 : CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F), u), (1 : Multiplicative ℤ)) = φ u.

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 fieldUnitDecompositionLogHomWithUniformizerValue_principal
    (F : CompleteDVF K) [Finite F.residueField]
    {A : Type*} [AddCommGroup A]
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A) (c : A)
    (u : (LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1) :
    fieldUnitDecompositionLogHomWithUniformizerValue F φ c
        (((1 : CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F), u),
          (1 : Multiplicative ℤ)) = φ u

theorem

fieldUnitDecompositionLogHomWithUniformizerValue_uniformizer

L104 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitDecompositionLogHomWithUniformizerValue_uniformizer

Documentation

Establishes the identity fieldUnitDecompositionLogHomWithUniformizerValue F φ c (((1 : CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F), (1 : (CompleteDVF.higherPrincipalUnitGroup F) 1)), Multiplicative.ofAdd m) = Multiplicative.ofAdd (m • c).

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 fieldUnitDecompositionLogHomWithUniformizerValue_uniformizer
    (F : CompleteDVF K) [Finite F.residueField]
    {A : Type*} [AddCommGroup A]
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A) (c : A)
    (m : ℤ) :
    fieldUnitDecompositionLogHomWithUniformizerValue F φ c
        (((1 : CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F),
            (1 : (CompleteDVF.higherPrincipalUnitGroup F) 1)),
          Multiplicative.ofAdd m) = Multiplicative.ofAdd (m • c)

def

fieldUnitLogHomWithUniformizerValue

L118 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogHomWithUniformizerValue

Documentation

Transport the corrected factor logarithm across a chosen the uniformizer–residue–principal-unit decomposition decomposition of the field-unit group.

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

def fieldUnitLogHomWithUniformizerValue
    (F : CompleteDVF K) [Finite F.residueField]
    {A : Type*} [AddCommGroup A]
    (d : CompleteDVF.higherPrincipalUnitGroup.fieldUnitDecompositionFactors F ≃* Kˣ)
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A) (c : A) :
    Kˣ →* Multiplicative A

theorem

fieldUnitLogHomWithUniformizerValue_apply

L132 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogHomWithUniformizerValue_apply

Documentation

The defining evaluation formula for fieldUnitLogHomWithUniformizerValue is fieldUnitLogHomWithUniformizerValue F d φ c x = φ (d.symm x).1.2 * Multiplicative.ofAdd (Multiplicative.toAdd (d.symm x).2 • c).

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 fieldUnitLogHomWithUniformizerValue_apply
    (F : CompleteDVF K) [Finite F.residueField]
    {A : Type*} [AddCommGroup A]
    (d : CompleteDVF.higherPrincipalUnitGroup.fieldUnitDecompositionFactors F ≃* Kˣ)
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A) (c : A) (x : Kˣ) :
    fieldUnitLogHomWithUniformizerValue F d φ c x =
      φ (d.symm x).1.2 *
        Multiplicative.ofAdd (Multiplicative.toAdd (d.symm x).2 • c)

theorem

fieldUnitLogHomWithUniformizerValue_apply_of_decomposition_eq

L146 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogHomWithUniformizerValue_apply_of_decomposition_eq

Documentation

Establishes the identity fieldUnitLogHomWithUniformizerValue F d φ c x = φ z.1.2 * Multiplicative.ofAdd (Multiplicative.toAdd z.2 • c).

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 fieldUnitLogHomWithUniformizerValue_apply_of_decomposition_eq
    (F : CompleteDVF K) [Finite F.residueField]
    {A : Type*} [AddCommGroup A]
    (d : CompleteDVF.higherPrincipalUnitGroup.fieldUnitDecompositionFactors F ≃* Kˣ)
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A) (c : A)
    (z : CompleteDVF.higherPrincipalUnitGroup.fieldUnitDecompositionFactors F)
    {x : Kˣ} (hx : d z = x) :
    fieldUnitLogHomWithUniformizerValue F d φ c x =
      φ z.1.2 * Multiplicative.ofAdd (Multiplicative.toAdd z.2 • c)

theorem

fieldUnitLogHomWithUniformizerValue_eq_of_principal_decomposition

L159 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogHomWithUniformizerValue_eq_of_principal_decomposition

Documentation

Establishes the identity fieldUnitLogHomWithUniformizerValue F d φ c x = φ u.

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 fieldUnitLogHomWithUniformizerValue_eq_of_principal_decomposition
    (F : CompleteDVF K) [Finite F.residueField]
    {A : Type*} [AddCommGroup A]
    (d : CompleteDVF.higherPrincipalUnitGroup.fieldUnitDecompositionFactors F ≃* Kˣ)
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A) (c : A)
    (u : (CompleteDVF.higherPrincipalUnitGroup F) 1) {x : Kˣ}
    (hx :
      d (((1 : CompleteDVF.higherPrincipalUnitGroup.residueRootsOfUnityGroup F), u),
          (1 : Multiplicative ℤ)) = x) :
    fieldUnitLogHomWithUniformizerValue F d φ c x = φ u

theorem

fieldUnitLogHomWithUniformizerValue_eq_of_completeDVF_principal

L181 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogHomWithUniformizerValue_eq_of_completeDVF_principal

Documentation

On first principal units, the corrected field logarithm agrees with the given principal-unit logarithm, for the decomposition supplied by a chosen uniformizer.

Source context 8 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]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
  (fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
   fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF_apply) in

Lean source · statement

theorem fieldUnitLogHomWithUniformizerValue_eq_of_completeDVF_principal
    (F : CompleteDVF K) [Finite F.residueField]
    {π : F.valuationSubring} (hπ : F.valuation.IsUniformizer (π : K))
    {A : Type*} [AddCommGroup A]
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A) (c : A)
    (u : (LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1) :
    fieldUnitLogHomWithUniformizerValue F
        (fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_completeDVF
          F hπ) φ c
        (CompleteDVF.higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
          (u : F.valuationSubringˣ)) = φ u

theorem

continuous_fieldUnitDecompositionLogHomWithUniformizerValue

L204 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.continuous_fieldUnitDecompositionLogHomWithUniformizerValue

Documentation

Continuity of the corrected logarithm on the three decomposition factors. The uniformizer coordinate is discrete, while continuity on the principal-unit coordinate is exactly the supplied continuity of φ.

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 continuous_fieldUnitDecompositionLogHomWithUniformizerValue
    [TopologicalSpace K] (F : CompleteDVF K) [Finite F.residueField]
    {A : Type*} [AddCommGroup A] [TopologicalSpace A]
    [IsTopologicalAddGroup A]
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A) (c : A)
    (hφ : Continuous φ) :
    Continuous (fieldUnitDecompositionLogHomWithUniformizerValue F φ c)

theorem

continuous_fieldUnitLogHomWithUniformizerValue

L232 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.continuous_fieldUnitLogHomWithUniformizerValue

Documentation

Continuity after transporting the corrected factor logarithm across the topological decomposition from the uniformizer–residue–principal-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 continuous_fieldUnitLogHomWithUniformizerValue
    [TopologicalSpace K] (F : CompleteDVF K) [Finite F.residueField]
    {A : Type*} [AddCommGroup A] [TopologicalSpace A]
    [IsTopologicalAddGroup A]
    (d : CompleteDVF.higherPrincipalUnitGroup.fieldUnitDecompositionFactors F ≃ₜ* Kˣ)
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative A) (c : A)
    (hφ : Continuous φ) :
    Continuous (fieldUnitLogHomWithUniformizerValue F d.toMulEquiv φ c)

def

uniformizerLogValueKilling

L247 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.uniformizerLogValueKilling

Documentation

The uniformizer value forced by the requirement that a distinguished field unit a have logarithm zero. The nonzero-exponent condition needed for that conclusion is stated separately.

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

def uniformizerLogValueKilling
    (F : CompleteDVF K) [Finite F.residueField] [CharZero K]
    (d : CompleteDVF.higherPrincipalUnitGroup.fieldUnitDecompositionFactors F ≃* Kˣ)
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative K) (a : Kˣ) : K

theorem

fieldUnitLogHomWithUniformizerValue_uniformizerLogValueKilling

L257 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldUnitLogHomWithUniformizerValue_uniformizerLogValueKilling

Documentation

With the forced uniformizer value, the distinguished field unit is sent to zero (written as 1 in Multiplicative K) whenever its uniformizer exponent 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 fieldUnitLogHomWithUniformizerValue_uniformizerLogValueKilling
    (F : CompleteDVF K) [Finite F.residueField] [CharZero K]
    (d : CompleteDVF.higherPrincipalUnitGroup.fieldUnitDecompositionFactors F ≃* Kˣ)
    (φ : (CompleteDVF.higherPrincipalUnitGroup F) 1 →* Multiplicative K) (a : Kˣ)
    (ha : Multiplicative.toAdd (d.symm a).2 ≠ 0) :
    fieldUnitLogHomWithUniformizerValue F d φ
        (uniformizerLogValueKilling F d φ a) a = 1

Module documentation

Extending the logarithm to the field-unit group

Declarations