NYLL
Module

TeichmullerDecomposition.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnits.TeichmullerDecomposition
23 declarations indexed from sourceView source ↗

Module documentation

Teichmuller and principal-unit decompositions

Decomposes valuation-ring units and field units into residue roots, first principal units, and a uniformizer factor.

Imports2
Imported by5

Declarations

def

residueRootsTimesPrincipalUnitMulHom

L41 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueRootsTimesPrincipalUnitMulHom
Documentation

Multiplication of a Teichmuller representative and a first principal unit, as a homomorphism into the full valuation-ring unit group.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · full declaration
def residueRootsTimesPrincipalUnitMulHom
    [Finite F.residueField] :
    higherPrincipalUnitGroup.residueRootsOfUnityGroup F ×
        higherPrincipalUnitGroup F 1 →*
      F.valuationSubringˣ where
  toFun z := (z.1 : F.valuationSubringˣ) * (z.2 : F.valuationSubringˣ)
  map_one' := by
    simp
  map_mul' := by
    intro x y
    simp [mul_left_comm, mul_comm]
theorem

residueRootsTimesPrincipalUnitMulHom_surjective

L57 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueRootsTimesPrincipalUnitMulHom_surjective
Documentation

The specified map is surjective: Function.Surjective (higherPrincipalUnitGroup.residueRootsTimesPrincipalUnitMulHom F).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem residueRootsTimesPrincipalUnitMulHom_surjective
    [Finite F.residueField] :
    Function.Surjective
      (higherPrincipalUnitGroup.residueRootsTimesPrincipalUnitMulHom F)
theorem

residueRootsTimesPrincipalUnitMulHom_injective

L85 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueRootsTimesPrincipalUnitMulHom_injective
Documentation

The specified map is injective: Function.Injective (higherPrincipalUnitGroup.residueRootsTimesPrincipalUnitMulHom F).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem residueRootsTimesPrincipalUnitMulHom_injective
    [Finite F.residueField] :
    Function.Injective
      (higherPrincipalUnitGroup.residueRootsTimesPrincipalUnitMulHom F)
theorem

residueRootsTimesPrincipalUnitMulHom_bijective

L140 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueRootsTimesPrincipalUnitMulHom_bijective
Documentation

The specified map is bijective: Function.Bijective (higherPrincipalUnitGroup.residueRootsTimesPrincipalUnitMulHom F).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem residueRootsTimesPrincipalUnitMulHom_bijective
    [Finite F.residueField] :
    Function.Bijective
      (higherPrincipalUnitGroup.residueRootsTimesPrincipalUnitMulHom F)
def

valuationSubringUnitsEquivRootsTimesPrincipalUnits

L149 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.valuationSubringUnitsEquivRootsTimesPrincipalUnits
Documentation

Unit-level form of the multiplicative unit decomposition: O^* is the product of the lifted (q - 1)-roots of unity and U^1.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
def valuationSubringUnitsEquivRootsTimesPrincipalUnits
    [Finite F.residueField] :
    higherPrincipalUnitGroup.residueRootsOfUnityGroup F ×
        higherPrincipalUnitGroup F 1 ≃*
      F.valuationSubringˣ
theorem

valuationSubringUnitsEquivRootsTimesPrincipalUnits_apply

L163 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.valuationSubringUnitsEquivRootsTimesPrincipalUnits_apply
Documentation

The defining evaluation formula for valuationSubringUnitsEquivRootsTimesPrincipalUnits is higherPrincipalUnitGroup.valuationSubringUnitsEquivRootsTimesPrincipalUnits F z = (z.1 : F.valuationSubringˣ) * (z.2 : F.valuationSubringˣ).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem valuationSubringUnitsEquivRootsTimesPrincipalUnits_apply
    [Finite F.residueField]
    (z :
      higherPrincipalUnitGroup.residueRootsOfUnityGroup F ×
        higherPrincipalUnitGroup F 1) :
    higherPrincipalUnitGroup.valuationSubringUnitsEquivRootsTimesPrincipalUnits
        F z =
      (z.1 : F.valuationSubringˣ) * (z.2 : F.valuationSubringˣ)
def

valuationSubringUnitFieldUnitHom

L175 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom
Documentation

The natural inclusion of valuation-ring units into field units, kept local to the principal-unit API to state the field-unit form of the multiplicative unit decomposition.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
def valuationSubringUnitFieldUnitHom :
    F.valuationSubringˣ →* Kˣ
theorem

coe_valuationSubringUnitFieldUnitHom_apply

L184 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.coe_valuationSubringUnitFieldUnitHom_apply
Documentation

The defining evaluation formula for coe_valuationSubringUnitFieldUnitHom is ((higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F u : Kˣ) : K) = (u : F.valuationSubring).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem coe_valuationSubringUnitFieldUnitHom_apply
    (u : F.valuationSubringˣ) :
    ((higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F u : Kˣ) :
        K) =
      (u : F.valuationSubring)
theorem

valuationSubringUnitFieldUnitHom_injective

L195 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom_injective
Documentation

The specified map is injective: Function.Injective (higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem valuationSubringUnitFieldUnitHom_injective :
    Function.Injective
      (higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F)
theorem

mem_zeroSubgroup_iff_exists_valuationSubringUnitFieldUnitHom_eq

L208 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.mem_zeroSubgroup_iff_exists_valuationSubringUnitFieldUnitHom_eq
Documentation

If the zero-valuation subgroup of a field-unit valuation is the usual unit group of the valuation subring, then it is exactly the image of valuation-ring units under valuationSubringUnitFieldUnitHom.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem mem_zeroSubgroup_iff_exists_valuationSubringUnitFieldUnitHom_eq
    (V : MultiplicativeIntegerValuation Kˣ)
    (hzero : V.zeroSubgroup = F.valuation.valuationSubring.unitGroup)
    (y : Kˣ) :
    y ∈ V.zeroSubgroup ↔
      ∃ u : F.valuationSubringˣ,
        higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F u = y
theorem

exists_roots_principalUnit_uniformizer_zpow

L232 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.exists_roots_principalUnit_uniformizer_zpow
Documentation

Field-unit representative form of the multiplicative unit decomposition.

Given an existing unit-uniformizer decomposition for a normalized integer-valued valuation whose zero subgroup is exactly the image of O^*, every field unit is a product of a Teichmuller root, a first principal unit, and a power of the chosen uniformizer.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem exists_roots_principalUnit_uniformizer_zpow
    [Finite F.residueField]
    (V : MultiplicativeIntegerValuation Kˣ)
    (hzero :
      ∀ y : Kˣ, y ∈ V.zeroSubgroup ↔
        ∃ u : F.valuationSubringˣ,
          higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F u = y)
    {ϖ : Kˣ} (hϖ : V.IsUniformizer ϖ) (x : Kˣ) :
    ∃ ζ : higherPrincipalUnitGroup.residueRootsOfUnityGroup F,
    ∃ p : higherPrincipalUnitGroup F 1,
    ∃ n : ℤ,
      x =
        higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
            (ζ : F.valuationSubringˣ) *
          higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
            (p : F.valuationSubringˣ) *
          ϖ ^ n
theorem

exists_roots_principalUnit_uniformizer_zpow_of_zeroSubgroup_eq_unitGroup

L283 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.exists_roots_principalUnit_uniformizer_zpow_of_zeroSubgroup_eq_unitGroup
Documentation

Field-unit form with the standard subgroup equality hypothesis V.zeroSubgroup = O^*.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem exists_roots_principalUnit_uniformizer_zpow_of_zeroSubgroup_eq_unitGroup
    [Finite F.residueField]
    (V : MultiplicativeIntegerValuation Kˣ)
    (hzero : V.zeroSubgroup = F.valuation.valuationSubring.unitGroup)
    {ϖ : Kˣ} (hϖ : V.IsUniformizer ϖ) (x : Kˣ) :
    ∃ ζ : higherPrincipalUnitGroup.residueRootsOfUnityGroup F,
    ∃ p : higherPrincipalUnitGroup F 1,
    ∃ n : ℤ,
      x =
        higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
            (ζ : F.valuationSubringˣ) *
          higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
            (p : F.valuationSubringˣ) *
          ϖ ^ n
theorem

roots_principalUnit_uniformizer_zpow_eq_iff

L307 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.roots_principalUnit_uniformizer_zpow_eq_iff
Documentation

Uniqueness of the field-unit form of the multiplicative unit decomposition: with a fixed uniformizer, the Teichmuller representative, the first principal unit, and the exponent are all uniquely determined.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem roots_principalUnit_uniformizer_zpow_eq_iff
    [Finite F.residueField]
    (V : MultiplicativeIntegerValuation Kˣ)
    (hzero :
      ∀ y : Kˣ, y ∈ V.zeroSubgroup ↔
        ∃ u : F.valuationSubringˣ,
          higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F u = y)
    {ϖ : Kˣ} (hϖ : V.IsUniformizer ϖ)
    (ζ η : higherPrincipalUnitGroup.residueRootsOfUnityGroup F)
    (p q : higherPrincipalUnitGroup F 1) (m n : ℤ) :
    higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
          (ζ : F.valuationSubringˣ) *
        higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
          (p : F.valuationSubringˣ) *
        ϖ ^ m =
      higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
          (η : F.valuationSubringˣ) *
        higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
          (q : F.valuationSubringˣ) *
        ϖ ^ n ↔
      ζ = η ∧ p = q ∧ m = n
theorem

roots_principalUnit_uniformizer_zpow_eq_iff_of_zeroSubgroup_eq_unitGroup

L372 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.roots_principalUnit_uniformizer_zpow_eq_iff_of_zeroSubgroup_eq_unitGroup
Documentation

Uniqueness form under the standard subgroup equality hypothesis V.zeroSubgroup = O^*.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem roots_principalUnit_uniformizer_zpow_eq_iff_of_zeroSubgroup_eq_unitGroup
    [Finite F.residueField]
    (V : MultiplicativeIntegerValuation Kˣ)
    (hzero : V.zeroSubgroup = F.valuation.valuationSubring.unitGroup)
    {ϖ : Kˣ} (hϖ : V.IsUniformizer ϖ)
    (ζ η : higherPrincipalUnitGroup.residueRootsOfUnityGroup F)
    (p q : higherPrincipalUnitGroup F 1) (m n : ℤ) :
    higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
          (ζ : F.valuationSubringˣ) *
        higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
          (p : F.valuationSubringˣ) *
        ϖ ^ m =
      higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
          (η : F.valuationSubringˣ) *
        higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
          (q : F.valuationSubringˣ) *
        ϖ ^ n ↔
      ζ = η ∧ p = q ∧ m = n
abbrev

fieldUnitDecompositionFactors

L399 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.fieldUnitDecompositionFactors
Documentation

The three factors in the multiplicative field-unit decomposition: Teichmuller roots, first principal units, and an integral power of a fixed uniformizer.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
abbrev fieldUnitDecompositionFactors [Finite F.residueField] :
    Type u
def

rootsPrincipalUnitUniformizerMulHom

L407 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.rootsPrincipalUnitUniformizerMulHom
Documentation

Multiplication map from the three the multiplicative unit decomposition factors to field units.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · full declaration
def rootsPrincipalUnitUniformizerMulHom
    [Finite F.residueField] (ϖ : Kˣ) :
    higherPrincipalUnitGroup.fieldUnitDecompositionFactors F →* Kˣ where
  toFun z :=
    higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
        (z.1.1 : F.valuationSubringˣ) *
      higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
        (z.1.2 : F.valuationSubringˣ) *
      ϖ ^ Multiplicative.toAdd z.2
  map_one' := by
    simp
  map_mul' := by
    intro x y
    simp [higherPrincipalUnitGroup.fieldUnitDecompositionFactors,
      mul_assoc, mul_left_comm, mul_comm, zpow_add]
theorem

rootsPrincipalUnitUniformizerMulHom_apply

L430 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.rootsPrincipalUnitUniformizerMulHom_apply
Documentation

The defining evaluation formula for rootsPrincipalUnitUniformizerMulHom is higherPrincipalUnitGroup.rootsPrincipalUnitUniformizerMulHom F ϖ z = higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F (z.1.1 : F.valuationSubringˣ) * higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F (z.1.2 : F.valuationSubringˣ) * ϖ ^ Multiplicative.toAdd z.2.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem rootsPrincipalUnitUniformizerMulHom_apply
    [Finite F.residueField] (ϖ : Kˣ)
    (z : higherPrincipalUnitGroup.fieldUnitDecompositionFactors F) :
    higherPrincipalUnitGroup.rootsPrincipalUnitUniformizerMulHom F ϖ z =
      higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
          (z.1.1 : F.valuationSubringˣ) *
        higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
          (z.1.2 : F.valuationSubringˣ) *
        ϖ ^ Multiplicative.toAdd z.2
theorem

rootsPrincipalUnitUniformizerMulHom_surjective

L445 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.rootsPrincipalUnitUniformizerMulHom_surjective
Documentation

The specified map is surjective: Function.Surjective (higherPrincipalUnitGroup.rootsPrincipalUnitUniformizerMulHom F ϖ).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem rootsPrincipalUnitUniformizerMulHom_surjective
    [Finite F.residueField]
    (V : MultiplicativeIntegerValuation Kˣ)
    (hzero :
      ∀ y : Kˣ, y ∈ V.zeroSubgroup ↔
        ∃ u : F.valuationSubringˣ,
          higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F u = y)
    {ϖ : Kˣ} (hϖ : V.IsUniformizer ϖ) :
    Function.Surjective
      (higherPrincipalUnitGroup.rootsPrincipalUnitUniformizerMulHom F ϖ)
theorem

rootsPrincipalUnitUniformizerMulHom_injective

L467 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.rootsPrincipalUnitUniformizerMulHom_injective
Documentation

The specified map is injective: Function.Injective (higherPrincipalUnitGroup.rootsPrincipalUnitUniformizerMulHom F ϖ).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem rootsPrincipalUnitUniformizerMulHom_injective
    [Finite F.residueField]
    (V : MultiplicativeIntegerValuation Kˣ)
    (hzero :
      ∀ y : Kˣ, y ∈ V.zeroSubgroup ↔
        ∃ u : F.valuationSubringˣ,
          higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F u = y)
    {ϖ : Kˣ} (hϖ : V.IsUniformizer ϖ) :
    Function.Injective
      (higherPrincipalUnitGroup.rootsPrincipalUnitUniformizerMulHom F ϖ)
theorem

rootsPrincipalUnitUniformizerMulHom_bijective

L503 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.rootsPrincipalUnitUniformizerMulHom_bijective
Documentation

The specified map is bijective: Function.Bijective (higherPrincipalUnitGroup.rootsPrincipalUnitUniformizerMulHom F ϖ).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem rootsPrincipalUnitUniformizerMulHom_bijective
    [Finite F.residueField]
    (V : MultiplicativeIntegerValuation Kˣ)
    (hzero :
      ∀ y : Kˣ, y ∈ V.zeroSubgroup ↔
        ∃ u : F.valuationSubringˣ,
          higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F u = y)
    {ϖ : Kˣ} (hϖ : V.IsUniformizer ϖ) :
    Function.Bijective
      (higherPrincipalUnitGroup.rootsPrincipalUnitUniformizerMulHom F ϖ)
def

fieldUnitsEquivRootsPrincipalUnitsUniformizer

L521 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.fieldUnitsEquivRootsPrincipalUnitsUniformizer
Documentation

Group-isomorphism form of the multiplicative unit decomposition: after fixing a uniformizer, Kˣ is the product of the lifted residue roots of unity, the first principal units, and the infinite cyclic uniformizer factor.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
def fieldUnitsEquivRootsPrincipalUnitsUniformizer
    [Finite F.residueField]
    (V : MultiplicativeIntegerValuation Kˣ)
    (hzero :
      ∀ y : Kˣ, y ∈ V.zeroSubgroup ↔
        ∃ u : F.valuationSubringˣ,
          higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F u = y)
    {ϖ : Kˣ} (hϖ : V.IsUniformizer ϖ) :
    higherPrincipalUnitGroup.fieldUnitDecompositionFactors F ≃* Kˣ
theorem

fieldUnitsEquivRootsPrincipalUnitsUniformizer_apply

L542 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.fieldUnitsEquivRootsPrincipalUnitsUniformizer_apply
Documentation

The defining evaluation formula for fieldUnitsEquivRootsPrincipalUnitsUniformizer is higherPrincipalUnitGroup.fieldUnitsEquivRootsPrincipalUnitsUniformizer (F := F) V hzero hϖ z = higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F (z.1.1 : F.valuationSubringˣ) * higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F (z.1.2 : F.valuationSubringˣ) * ϖ ^ Multiplicative.toAdd z.2.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem fieldUnitsEquivRootsPrincipalUnitsUniformizer_apply
    [Finite F.residueField]
    (V : MultiplicativeIntegerValuation Kˣ)
    (hzero :
      ∀ y : Kˣ, y ∈ V.zeroSubgroup ↔
        ∃ u : F.valuationSubringˣ,
          higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F u = y)
    {ϖ : Kˣ} (hϖ : V.IsUniformizer ϖ)
    (z : higherPrincipalUnitGroup.fieldUnitDecompositionFactors F) :
    higherPrincipalUnitGroup.fieldUnitsEquivRootsPrincipalUnitsUniformizer
        (F := F) V hzero hϖ z =
      higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
          (z.1.1 : F.valuationSubringˣ) *
        higherPrincipalUnitGroup.valuationSubringUnitFieldUnitHom F
          (z.1.2 : F.valuationSubringˣ) *
        ϖ ^ Multiplicative.toAdd z.2
def

fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_zeroSubgroup_eq_unitGroup

L562 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_zeroSubgroup_eq_unitGroup
Documentation

Group-isomorphism form under the standard subgroup equality hypothesis V.zeroSubgroup = O^*.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
def fieldUnitsEquivRootsPrincipalUnitsUniformizer_of_zeroSubgroup_eq_unitGroup
    [Finite F.residueField]
    (V : MultiplicativeIntegerValuation Kˣ)
    (hzero : V.zeroSubgroup = F.valuation.valuationSubring.unitGroup)
    {ϖ : Kˣ} (hϖ : V.IsUniformizer ϖ) :
    higherPrincipalUnitGroup.fieldUnitDecompositionFactors F ≃* Kˣ

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.