NYLL
Module

AdicProdiscreteComparison.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnitPadicAction.AdicProdiscreteComparison
11 declarations indexed from sourceView source ↗

Module documentation

Adic and prodiscrete principal-unit models

The adic topology on first principal units agrees with the prodiscrete topology carried by the inverse limit of finite quotient coordinates.

Imports1
Imported by5

Declarations

def

adicPrincipalUnitsHomeomorphUnderlying

L42 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.adicPrincipalUnitsHomeomorphUnderlying
Documentation

Internal comparison from the type-level adic model to the raw instance-parametric carrier.

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
namespace Internal
Lean source · full declaration
def adicPrincipalUnitsHomeomorphUnderlying
    (F : CompleteDVF.{u, v} K) :
    letI : TopologicalSpace F.valuationSubring :=
      (uniformizerPowerIdeal
        (chosenPrincipalUnitPadicUniformizer F) 1).adicTopology
    AdicPrincipalUnits F ≃ₜ
      Additive
        ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1) := by
  letI : TopologicalSpace F.valuationSubring :=
    (uniformizerPowerIdeal
      (chosenPrincipalUnitPadicUniformizer F) 1).adicTopology
  exact (AdicPrincipalUnits.homeomorph F).trans
    (WithTopology.homeomorph
      (α := Additive
        ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1))
      (topology := principalUnitAdicTopology F))
theorem

adicPrincipalUnitsHomeomorphUnderlying_apply

L64 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.adicPrincipalUnitsHomeomorphUnderlying_apply
Documentation

The homeomorphism from the adic principal-unit model evaluates through its underlying additive equivalence.

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
namespace Internal
Lean source · full declaration
theorem adicPrincipalUnitsHomeomorphUnderlying_apply
    (F : CompleteDVF.{u, v} K) (x : AdicPrincipalUnits F) :
    letI : TopologicalSpace F.valuationSubring :=
      (uniformizerPowerIdeal
        (chosenPrincipalUnitPadicUniformizer F) 1).adicTopology
    adicPrincipalUnitsHomeomorphUnderlying F x =
      AdicPrincipalUnits.addEquiv F x :=
  rfl
def

principalUnitProdiscreteLimitHomeomorphUnderlying

L75 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitProdiscreteLimitHomeomorphUnderlying
Documentation

Internal comparison from the type-level prodiscrete model to the raw instance-parametric inverse-limit carrier.

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
namespace Internal
Lean source · full declaration
def principalUnitProdiscreteLimitHomeomorphUnderlying
    (F : CompleteDVF.{u, v} K) :
    letI : (n : ℕ) → TopologicalSpace (Internal.principalUnitQuotientCarrier F n) :=
      fun _ => ⊥
    PrincipalUnitProdiscreteLimit F ≃ₜ
      Additive (Internal.principalUnitInverseLimitCarrier F) := by
  letI : (n : ℕ) → TopologicalSpace (Internal.principalUnitQuotientCarrier F n) :=
    fun _ => ⊥
  exact (PrincipalUnitProdiscreteLimit.homeomorph F).trans
    (WithTopology.homeomorph
      (α := Additive (Internal.principalUnitInverseLimitCarrier F))
      (topology := principalUnitProdiscreteTopology F))
theorem

principalUnitProdiscreteLimitHomeomorphUnderlying_apply

L93 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitProdiscreteLimitHomeomorphUnderlying_apply
Documentation

The homeomorphism from the prodiscrete limit evaluates through its underlying additive equivalence.

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
namespace Internal
Lean source · full declaration
theorem principalUnitProdiscreteLimitHomeomorphUnderlying_apply
    (F : CompleteDVF.{u, v} K) (x : PrincipalUnitProdiscreteLimit F) :
    letI : (n : ℕ) → TopologicalSpace
        (Internal.principalUnitQuotientCarrier F n) := fun _ => ⊥
    principalUnitProdiscreteLimitHomeomorphUnderlying F x =
      PrincipalUnitProdiscreteLimit.addEquiv F x :=
  rfl
def

adicPrincipalUnitsHomeomorphProdiscreteLimit

L106 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.adicPrincipalUnitsHomeomorphProdiscreteLimit
Documentation

The only bridge where the raw instance-parametric presentations are installed. Public topology APIs use AdicPrincipalUnits and PrincipalUnitProdiscreteLimit instead.

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 adicPrincipalUnitsHomeomorphProdiscreteLimit
    (F : CompleteDVF.{u, v} K) :
    AdicPrincipalUnits F ≃ₜ PrincipalUnitProdiscreteLimit F
theorem

adicPrincipalUnitsHomeomorphProdiscreteLimit_to_addEquiv

L125 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.adicPrincipalUnitsHomeomorphProdiscreteLimit_to_addEquiv
Documentation

Establishes the identity PrincipalUnitProdiscreteLimit.addEquiv F (adicPrincipalUnitsHomeomorphProdiscreteLimit F x) = principalUnitAddEquivInverseLimitCarrier F (AdicPrincipalUnits.addEquiv F 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 adicPrincipalUnitsHomeomorphProdiscreteLimit_to_addEquiv
    (F : CompleteDVF.{u, v} K) (x : AdicPrincipalUnits F) :
    PrincipalUnitProdiscreteLimit.addEquiv F
        (adicPrincipalUnitsHomeomorphProdiscreteLimit F x) =
      principalUnitAddEquivInverseLimitCarrier F
        (AdicPrincipalUnits.addEquiv F x)
instance

principalUnitProdiscreteLimitT2Space

L151 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitProdiscreteLimitT2Space
Documentation

The prodiscrete principal-unit limit is Hausdorff.

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
instance principalUnitProdiscreteLimitT2Space
    (F : CompleteDVF.{u, v} K) :
    T2Space (PrincipalUnitProdiscreteLimit F)
def

adicPrincipalUnitsAddEquivProdiscreteLimit

L171 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.adicPrincipalUnitsAddEquivProdiscreteLimit
Documentation

Algebraic form of the canonical identification between adic principal units and their prodiscrete limit.

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 adicPrincipalUnitsAddEquivProdiscreteLimit
    (F : CompleteDVF.{u, v} K) :
    AdicPrincipalUnits F ≃+ PrincipalUnitProdiscreteLimit F
theorem

adicPrincipalUnitsHomeomorphProdiscreteLimit_apply

L183 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.adicPrincipalUnitsHomeomorphProdiscreteLimit_apply
Documentation

The defining evaluation formula for adicPrincipalUnitsHomeomorphProdiscreteLimit is adicPrincipalUnitsHomeomorphProdiscreteLimit F x = adicPrincipalUnitsAddEquivProdiscreteLimit F 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 adicPrincipalUnitsHomeomorphProdiscreteLimit_apply
    (F : CompleteDVF.{u, v} K) (x : AdicPrincipalUnits F) :
    adicPrincipalUnitsHomeomorphProdiscreteLimit F x =
      adicPrincipalUnitsAddEquivProdiscreteLimit F x
def

adicPrincipalUnitsContinuousAddEquivProdiscreteLimit

L200 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.adicPrincipalUnitsContinuousAddEquivProdiscreteLimit
Documentation

Additive topological form of adicPrincipalUnitsHomeomorphProdiscreteLimit.

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 adicPrincipalUnitsContinuousAddEquivProdiscreteLimit
    (F : CompleteDVF.{u, v} K) :
    AdicPrincipalUnits F ≃ₜ+ PrincipalUnitProdiscreteLimit F
instance

adicPrincipalUnitsT2Space

L210 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.adicPrincipalUnitsT2Space
Documentation

The topology on the type in T2Space (AdicPrincipalUnits F) is Hausdorff.

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
instance adicPrincipalUnitsT2Space
    (F : CompleteDVF.{u, v} K) : T2Space (AdicPrincipalUnits F)

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