NYLL
Module

InverseLimitCore.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnitPadicAction.InverseLimitCore
22 declarations indexed from sourceView source ↗

Module documentation

The canonical p-adic action on first principal units

This file constructs the common source used in both cases of LubinTate, The field-unit structure theorem. A first principal unit is recovered from its classes in the level quotients U^1 / U^(n+1). For a local field these quotients are finite and have exponent dividing p^(f*n), where the residue field has cardinality p^f. Reduction of a p-adic integer modulo these powers therefore acts on every finite coordinate, and compatibility of reduction transports the action to U^1.

Restriction of the adic inverse-limit equivalence to first principal units

Imports2
Imported by4

Declarations

def

chosenPrincipalUnitPadicUniformizer

L46 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.chosenPrincipalUnitPadicUniformizer
Documentation

A fixed uniformizer used only to invoke the direct quotient form of the adic inverse-limit equivalence. The resulting p-adic action is characterized below by its ordinary integral powers.

Source context 12 commands

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

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

chosenPrincipalUnitPadicUniformizer_isUniformizer

L51 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.chosenPrincipalUnitPadicUniformizer_isUniformizer
Documentation

The chosen principal-unit parameter has valuation one and is a uniformizer.

Source context 12 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
Lean source · statement
theorem chosenPrincipalUnitPadicUniformizer_isUniformizer
    (F : CompleteDVF.{u, v} K) :
    F.valuation.IsUniformizer (chosenPrincipalUnitPadicUniformizer F : K)
theorem

chosenPrincipalUnitPadicUniformizer_irreducible

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

The chosen valuation-ring uniformizer is irreducible.

Source context 12 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
Lean source · statement
theorem chosenPrincipalUnitPadicUniformizer_irreducible
    (F : CompleteDVF.{u, v} K) :
    Irreducible (chosenPrincipalUnitPadicUniformizer F)
theorem

higherUnitSubgroup_chosenPrincipalUnitPadicUniformizer

L66 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.higherUnitSubgroup_chosenPrincipalUnitPadicUniformizer
Documentation

For the chosen uniformizer, the higher-unit subgroup 1 + pi^n O is the intrinsic n-th higher principal-unit group.

Source context 12 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
Lean source · statement
theorem higherUnitSubgroup_chosenPrincipalUnitPadicUniformizer
    (F : CompleteDVF.{u, v} K) (n : ℕ) :
    higherUnitSubgroup (chosenPrincipalUnitPadicUniformizer F) n =
      (LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) n
def

higherUnitQuotientTransition

L90 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.higherUnitQuotientTransition
Documentation

Transition on the intrinsic quotients O^*/U^(n+1).

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · statement
def Internal.higherUnitQuotientTransition
    (F : CompleteDVF.{u, v} K) {m n : ℕ} (hmn : m ≤ n) :
    F.valuationSubringˣ ⧸ (higherPrincipalUnitGroup F) (n + 1) →*
      F.valuationSubringˣ ⧸ (higherPrincipalUnitGroup F) (m + 1)
abbrev

higherUnitInverseLimitCarrier

L101 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.higherUnitInverseLimitCarrier
Documentation

The intrinsic full unit inverse limit lim O^*/U^(n+1).

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · statement
abbrev Internal.higherUnitInverseLimitCarrier
    (F : CompleteDVF.{u, v} K) : Type u
def

uniformizerHigherUnitQuotientEquiv

L115 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.uniformizerHigherUnitQuotientEquiv
Documentation

Changing from the uniformizer presentation of a level quotient to the intrinsic principal-unit presentation.

Source context 14 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · statement
def Internal.uniformizerHigherUnitQuotientEquiv
    (F : CompleteDVF.{u, v} K) (n : ℕ) :
    F.valuationSubringˣ ⧸
        higherUnitSubgroup (chosenPrincipalUnitPadicUniformizer F) (n + 1) ≃*
      F.valuationSubringˣ ⧸ (higherPrincipalUnitGroup F) (n + 1)
theorem

uniformizerHigherUnitQuotientEquiv_mk

L127 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.uniformizerHigherUnitQuotientEquiv_mk
Documentation

Establishes the identity uniformizerHigherUnitQuotientEquiv F n (QuotientGroup.mk x) = QuotientGroup.mk x.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
theorem Internal.uniformizerHigherUnitQuotientEquiv_mk
    (F : CompleteDVF.{u, v} K) (n : ℕ) (x : F.valuationSubringˣ) :
    uniformizerHigherUnitQuotientEquiv F n (QuotientGroup.mk x) =
      QuotientGroup.mk x
def

uniformizerHigherUnitInverseLimitEquiv

L138 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.uniformizerHigherUnitInverseLimitEquiv
Documentation

The uniformizer and intrinsic presentations give the same full inverse limit.

Source context 14 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · statement
def Internal.uniformizerHigherUnitInverseLimitEquiv
    (F : CompleteDVF.{u, v} K) :
    dvrHigherUnitQuotientInverseLimit
        (chosenPrincipalUnitPadicUniformizer F) ≃*
      Internal.higherUnitInverseLimitCarrier F
def

unitsEquivHigherUnitQuotientInverseLimit

L166 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.unitsEquivHigherUnitQuotientInverseLimit
Documentation

The direct quotient isomorphism of the adic inverse-limit equivalence, rewritten using the intrinsic higher principal-unit filtration.

Source context 13 commands

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

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

unitsEquivHigherUnitQuotientInverseLimit_apply

L186 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.unitsEquivHigherUnitQuotientInverseLimit_apply
Documentation

The defining evaluation formula for Internal.unitsEquivHigherUnitQuotientInverseLimit is (unitsEquivHigherUnitQuotientInverseLimit F x).1 n = QuotientGroup.mk x.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
theorem Internal.unitsEquivHigherUnitQuotientInverseLimit_apply
    (F : CompleteDVF.{u, v} K) (x : F.valuationSubringˣ) (n : ℕ) :
    (unitsEquivHigherUnitQuotientInverseLimit F x).1 n =
      QuotientGroup.mk x
def

uniformizerHigherUnitInverseLimitHomeomorphIntrinsic

L213 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.uniformizerHigherUnitInverseLimitHomeomorphIntrinsic
Documentation

The change from the uniformizer presentation of the full unit inverse limit to the intrinsic presentation is a homeomorphism when all quotient coordinates are discrete.

Source context 14 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · full declaration
def Internal.uniformizerHigherUnitInverseLimitHomeomorphIntrinsic
    (F : CompleteDVF.{u, v} K) :
    letI : (n : ℕ) → TopologicalSpace
        (F.valuationSubringˣ ⧸
          higherUnitSubgroup (chosenPrincipalUnitPadicUniformizer F) (n + 1)) :=
      fun _ => ⊥
    letI : (n : ℕ) → TopologicalSpace
        (F.valuationSubringˣ ⧸ (higherPrincipalUnitGroup F) (n + 1)) :=
      fun _ => ⊥
    dvrHigherUnitQuotientInverseLimit
        (chosenPrincipalUnitPadicUniformizer F) ≃ₜ
      Internal.higherUnitInverseLimitCarrier F := by
  letI : (n : ℕ) → TopologicalSpace
      (F.valuationSubringˣ ⧸
        higherUnitSubgroup (chosenPrincipalUnitPadicUniformizer F) (n + 1)) :=
    fun _ => ⊥
  letI : (n : ℕ) → TopologicalSpace
      (F.valuationSubringˣ ⧸ (higherPrincipalUnitGroup F) (n + 1)) :=
    fun _ => ⊥
  letI : (n : ℕ) → DiscreteTopology
      (F.valuationSubringˣ ⧸
        higherUnitSubgroup (chosenPrincipalUnitPadicUniformizer F) (n + 1)) :=
    fun _ => ⟨rfl⟩
  letI : (n : ℕ) → DiscreteTopology
      (F.valuationSubringˣ ⧸ (higherPrincipalUnitGroup F) (n + 1)) :=
    fun _ => ⟨rfl⟩
  let e := uniformizerHigherUnitInverseLimitEquiv F
  refine
    { toFun := e
      invFun := e.symm
      left_inv := e.left_inv
      right_inv := e.right_inv
      continuous_toFun := ?_
      continuous_invFun := ?_ }
  · change Continuous fun x => e x
    exact Continuous.subtype_mk
      (continuous_pi fun n => by
        change Continuous fun x :
            dvrHigherUnitQuotientInverseLimit
              (chosenPrincipalUnitPadicUniformizer F) =>
          uniformizerHigherUnitQuotientEquiv F n
            (dvrHigherUnitQuotientInverseLimit_eval
              (chosenPrincipalUnitPadicUniformizer F) n x)
        have heval : Continuous fun x :
            dvrHigherUnitQuotientInverseLimit
              (chosenPrincipalUnitPadicUniformizer F) =>
            dvrHigherUnitQuotientInverseLimit_eval
              (chosenPrincipalUnitPadicUniformizer F) n x :=
          (DiscreteHigherUnitQuotient.homeomorph
            (chosenPrincipalUnitPadicUniformizer F) (n + 1)).continuous.comp
            (dvrHigherUnitQuotientInverseLimit_discreteEval_continuous
              (chosenPrincipalUnitPadicUniformizer F) n)
        exact continuous_of_discreteTopology.comp heval)
      (fun x : dvrHigherUnitQuotientInverseLimit
          (chosenPrincipalUnitPadicUniformizer F) => by
        intro i j hij
        change higherUnitQuotientTransition F hij
            (uniformizerHigherUnitQuotientEquiv F j
              (dvrHigherUnitQuotientInverseLimit_eval
                (chosenPrincipalUnitPadicUniformizer F) j x)) =
          uniformizerHigherUnitQuotientEquiv F i
            (dvrHigherUnitQuotientInverseLimit_eval
              (chosenPrincipalUnitPadicUniformizer F) i x)
        exact (e x).2 hij)
  · change Continuous fun x => e.symm x
    apply (dvrHigherUnitQuotientInverseLimit_continuous_iff
      (chosenPrincipalUnitPadicUniformizer F) (fun x => e.symm x)).2
    intro n
    change Continuous fun x : Internal.higherUnitInverseLimitCarrier F =>
      DiscreteHigherUnitQuotient.of
        (chosenPrincipalUnitPadicUniformizer F) (n + 1)
        ((uniformizerHigherUnitQuotientEquiv F n).symm (x.1 n))
    exact
      (DiscreteHigherUnitQuotient.homeomorph
        (chosenPrincipalUnitPadicUniformizer F) (n + 1)).symm.continuous.comp
        (continuous_of_discreteTopology.comp
          ((continuous_apply n).comp continuous_subtype_val))
def

unitsHomeomorphHigherUnitQuotientInverseLimit

L295 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.unitsHomeomorphHigherUnitQuotientInverseLimit
Documentation

Topological full-unit form of the adic inverse-limit equivalence, rewritten intrinsically.

Source context 14 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · full declaration
def Internal.unitsHomeomorphHigherUnitQuotientInverseLimit
    (F : CompleteDVF.{u, v} K) :
    letI : TopologicalSpace F.valuationSubring :=
      (uniformizerPowerIdeal (chosenPrincipalUnitPadicUniformizer F) 1).adicTopology
    letI : (n : ℕ) → TopologicalSpace
        (F.valuationSubringˣ ⧸ (higherPrincipalUnitGroup F) (n + 1)) :=
      fun _ => ⊥
    F.valuationSubringˣ ≃ₜ Internal.higherUnitInverseLimitCarrier F := by
  let pi := chosenPrincipalUnitPadicUniformizer F
  letI : TopologicalSpace F.valuationSubring :=
    (uniformizerPowerIdeal pi 1).adicTopology
  letI : (n : ℕ) → TopologicalSpace
      (F.valuationSubringˣ ⧸ (higherPrincipalUnitGroup F) (n + 1)) :=
    fun _ => ⊥
  letI : (n : ℕ) → TopologicalSpace
      (F.valuationSubringˣ ⧸ higherUnitSubgroup pi (n + 1)) :=
    fun _ => ⊥
  have hpi : Irreducible pi := chosenPrincipalUnitPadicUniformizer_irreducible F
  letI : IsAdicComplete (uniformizerPowerIdeal pi 1) F.valuationSubring := by
    have hmax : uniformizerPowerIdeal pi 1 = F.maximalIdeal := by
      rw [uniformizerPowerIdeal, pow_one,
        ← F.maximalIdeal_eq_span_uniformizer
          (chosenPrincipalUnitPadicUniformizer_isUniformizer F)]
    rw [hmax]
    exact ValuationTheory.DiscreteValuationField.Valuation.isAdicComplete F.valuation
  exact
    (WithTopology.homeomorph
      (α := F.valuationSubringˣ)
      (topology := adicUnitsTopology (uniformizerPowerIdeal pi 1))).symm.trans
      ((unitsEquivHigherUnitQuotientInverseLimitHomeomorph hpi).trans
        (Internal.uniformizerHigherUnitInverseLimitHomeomorphIntrinsic F))
theorem

unitsHomeomorphHigherUnitQuotientInverseLimit_apply

L334 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.unitsHomeomorphHigherUnitQuotientInverseLimit_apply
Documentation

The unit-to-inverse-limit homeomorphism sends a unit to its canonical class at every higher-unit quotient level.

Source context 14 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · full declaration
theorem Internal.unitsHomeomorphHigherUnitQuotientInverseLimit_apply
    (F : CompleteDVF.{u, v} K) (x : F.valuationSubringˣ) (n : ℕ) :
    letI : TopologicalSpace F.valuationSubring :=
      (uniformizerPowerIdeal (chosenPrincipalUnitPadicUniformizer F) 1).adicTopology
    letI : (n : ℕ) → TopologicalSpace
        (F.valuationSubringˣ ⧸ (higherPrincipalUnitGroup F) (n + 1)) :=
      fun _ => ⊥
    (Internal.unitsHomeomorphHigherUnitQuotientInverseLimit F x).1 n =
      QuotientGroup.mk x := by
  let pi := chosenPrincipalUnitPadicUniformizer F
  let : TopologicalSpace F.valuationSubring :=
    (uniformizerPowerIdeal pi 1).adicTopology
  let : (n : ℕ) → TopologicalSpace
      (F.valuationSubringˣ ⧸ (higherPrincipalUnitGroup F) (n + 1)) :=
    fun _ => ⊥
  let : (n : ℕ) → TopologicalSpace
      (F.valuationSubringˣ ⧸ higherUnitSubgroup pi (n + 1)) :=
    fun _ => ⊥
  have hpi : Irreducible pi := chosenPrincipalUnitPadicUniformizer_irreducible F
  let : IsAdicComplete (uniformizerPowerIdeal pi 1) F.valuationSubring := by
    have hmax : uniformizerPowerIdeal pi 1 = F.maximalIdeal := by
      rw [uniformizerPowerIdeal, pow_one,
        ← F.maximalIdeal_eq_span_uniformizer
          (chosenPrincipalUnitPadicUniformizer_isUniformizer F)]
    rw [hmax]
    exact ValuationTheory.DiscreteValuationField.Valuation.isAdicComplete F.valuation
  change uniformizerHigherUnitQuotientEquiv F n
      (dvrHigherUnitQuotientInverseLimit_eval pi n
        (unitsEquivHigherUnitQuotientInverseLimitHomeomorph
          hpi
          (WithTopology.toTopology (adicUnitsTopology (uniformizerPowerIdeal pi 1)) x))) =
    QuotientGroup.mk x
  change uniformizerHigherUnitQuotientEquiv F n (QuotientGroup.mk x) =
    QuotientGroup.mk x
  exact uniformizerHigherUnitQuotientEquiv_mk F n x
abbrev

principalUnitQuotientCarrier

L373 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitQuotientCarrier
Documentation

The raw carrier of the n-th coordinate U^1/U^(n+1).

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
abbrev Internal.principalUnitQuotientCarrier
    (F : CompleteDVF.{u, v} K) (n : ℕ) : Type u
def

principalUnitQuotientCarrierTransition

L379 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitQuotientCarrierTransition
Documentation

Transition U^1/U^(n+1) -> U^1/U^(m+1) for m <= n.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
def Internal.principalUnitQuotientCarrierTransition
    (F : CompleteDVF.{u, v} K) {m n : ℕ} (hmn : m ≤ n) :
    Internal.principalUnitQuotientCarrier F n →*
      Internal.principalUnitQuotientCarrier F m
theorem

principalUnitQuotientCarrierTransition_mk

L401 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitQuotientCarrierTransition_mk
Documentation

Establishes the identity principalUnitQuotientCarrierTransition F hmn ((higherPrincipalUnitGroup.toPrincipalUnitFiltration F).principalUnitSubquotientMk 1 (n + 1) x) = (higherPrincipalUnitGroup.toPrincipalUnitFiltration F).principalUnitSubquotientMk 1 (m + 1) x.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
theorem Internal.principalUnitQuotientCarrierTransition_mk
    (F : CompleteDVF.{u, v} K) {m n : ℕ} (hmn : m ≤ n)
    (x : (LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1) :
    principalUnitQuotientCarrierTransition F hmn
        ((higherPrincipalUnitGroup.toPrincipalUnitFiltration F).principalUnitSubquotientMk
          1 (n + 1) x) =
      (higherPrincipalUnitGroup.toPrincipalUnitFiltration F).principalUnitSubquotientMk
        1 (m + 1) x
abbrev

principalUnitInverseLimitCarrier

L412 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitInverseLimitCarrier
Documentation

The projective limit lim_n U^1/U^(n+1).

Source context 13 commands

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

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

principalUnitInverseLimitCarrierEval

L419 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitInverseLimitCarrierEval
Documentation

Evaluation of a principal-unit compatible family at level n.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
def Internal.principalUnitInverseLimitCarrierEval
    (F : CompleteDVF.{u, v} K) (n : ℕ) :
    Internal.principalUnitInverseLimitCarrier F →*
      Internal.principalUnitQuotientCarrier F n
theorem

principalUnitInverseLimitCarrierEval_apply

L432 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitInverseLimitCarrierEval_apply
Documentation

The defining evaluation formula for Internal.principalUnitInverseLimitCarrierEval is principalUnitInverseLimitCarrierEval F n x = x.1 n.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
theorem Internal.principalUnitInverseLimitCarrierEval_apply
    (F : CompleteDVF.{u, v} K) (n : ℕ)
    (x : Internal.principalUnitInverseLimitCarrier F) :
    principalUnitInverseLimitCarrierEval F n x = x.1 n
theorem

principalUnitInverseLimitCarrier_compatible

L439 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitInverseLimitCarrier_compatible
Documentation

Named compatibility law for a principal-unit inverse-limit family.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
theorem Internal.principalUnitInverseLimitCarrier_compatible
    (F : CompleteDVF.{u, v} K)
    (x : Internal.principalUnitInverseLimitCarrier F)
    {m n : ℕ} (hmn : m ≤ n) :
    principalUnitQuotientCarrierTransition F hmn
        (principalUnitInverseLimitCarrierEval F n x) =
      principalUnitInverseLimitCarrierEval F m x
theorem

principalUnitInverseLimitCarrier_ext

L453 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitInverseLimitCarrier_ext
Documentation

Principal-unit inverse-limit families are determined by their coordinates.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
theorem Internal.principalUnitInverseLimitCarrier_ext
    (F : CompleteDVF.{u, v} K)
    {x y : Internal.principalUnitInverseLimitCarrier F}
    (h : ∀ n, principalUnitInverseLimitCarrierEval F n x =
      principalUnitInverseLimitCarrierEval F n y) : x = y

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