Module

TopologyModelTypes.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnitPadicAction.TopologyModelTypes

37 declarations indexed from sourceView source ↗

Module documentation

Type-level topology models for principal units

Adic principal units, discrete finite quotients, and the prodiscrete inverse limit are represented by distinct wrapper types so that their topologies cannot be confused by instance selection.

Topology is part of the type

The algebraic quotient and inverse-limit types above deliberately carry no preferred topology. The following models distinguish the topologies used in the p-adic action at the type level. In particular, no theorem below can silently reinterpret the same quotient as both a quotient-topological and a discrete space.

Imports2

Imported by5

def

principalUnitAdicTopology

L52 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitAdicTopology

Documentation

The topology on additive first principal units induced by the maximal- ideal adic topology on the valuation ring.

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 principalUnitAdicTopology
    (F : CompleteDVF.{u, v} K) :
    TopologicalSpace
      (Additive
        ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1))

structure

AdicPrincipalUnits

L63 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.AdicPrincipalUnits

Documentation

First principal units with their canonical adic topology fixed in the type.

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 · full declaration

structure AdicPrincipalUnits (F : CompleteDVF.{u, v} K) where
  /-- The underlying additive principal unit. -/
  val : Additive
    ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1)

def

equiv

L71 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.AdicPrincipalUnits.equiv

Documentation

The carrier equivalence of the adic model.

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 AdicPrincipalUnits

Lean source · full declaration

def equiv (F : CompleteDVF.{u, v} K) :
    AdicPrincipalUnits F ≃
      Additive
        ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1) where
  toFun := AdicPrincipalUnits.val
  invFun := fun x => ⟨x⟩
  left_inv := fun x => by cases x; rfl
  right_inv := fun _ => rfl

instance

(anonymous instance)

L84 ↗

Documentation

Equips the target with its canonical TopologicalSpace structure, namely TopologicalSpace (AdicPrincipalUnits F).

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 AdicPrincipalUnits

Lean source · statement

instance (F : CompleteDVF.{u, v} K) :
    TopologicalSpace (AdicPrincipalUnits F)

def

homeomorph

L89 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.AdicPrincipalUnits.homeomorph

Documentation

Forget the wrapper while retaining the topology recorded in its type.

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 AdicPrincipalUnits

Lean source · full declaration

def homeomorph (F : CompleteDVF.{u, v} K) :
    AdicPrincipalUnits F ≃ₜ
      WithTopology
        (Additive
          ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1))
        (principalUnitAdicTopology F) where
  toEquiv := (equiv F).trans
    (WithTopology.equiv _ (principalUnitAdicTopology F)).symm
  continuous_toFun := by
    let : TopologicalSpace
        (Additive
          ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1)) :=
      principalUnitAdicTopology F
    change Continuous fun x : AdicPrincipalUnits F =>
      WithTopology.toTopology (principalUnitAdicTopology F) x.val
    exact
      (WithTopology.continuous_toTopology (principalUnitAdicTopology F)).comp
        continuous_induced_dom
  continuous_invFun := by
    let : TopologicalSpace
        (Additive
          ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1)) :=
      principalUnitAdicTopology F
    change Continuous fun x : WithTopology
        (Additive
          ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1))
        (principalUnitAdicTopology F) =>
      (⟨x.ofTopology⟩ : AdicPrincipalUnits F)
    exact
      continuous_induced_rng.2
        (WithTopology.continuous_ofTopology (principalUnitAdicTopology F))

instance

(anonymous instance)

L125 ↗

Documentation

Equips the target with its canonical AddCommGroup structure, namely AddCommGroup (AdicPrincipalUnits F).

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 AdicPrincipalUnits

Lean source · statement

instance (F : CompleteDVF.{u, v} K) : AddCommGroup (AdicPrincipalUnits F)

def

of

L129 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.AdicPrincipalUnits.of

Documentation

Put a first principal unit into the canonical adic model.

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 AdicPrincipalUnits

Lean source · statement

def of (F : CompleteDVF.{u, v} K)
    (x : Additive
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1)) :
    AdicPrincipalUnits F

theorem

val_of

L136 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.AdicPrincipalUnits.val_of

Documentation

Establishes the identity (of F x).val = x.

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 AdicPrincipalUnits

Lean source · statement

theorem val_of (F : CompleteDVF.{u, v} K)
    (x : Additive
      ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1)) :
    (of F x).val = x

theorem

of_val

L142 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.AdicPrincipalUnits.of_val

Documentation

Establishes the identity of F x.val = x.

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 AdicPrincipalUnits

Lean source · statement

theorem of_val (F : CompleteDVF.{u, v} K)
    (x : AdicPrincipalUnits F) : of F x.val = x

def

addEquiv

L148 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.AdicPrincipalUnits.addEquiv

Documentation

The algebraic equivalence underlying the adic model.

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 AdicPrincipalUnits

Lean source · statement

def addEquiv (F : CompleteDVF.{u, v} K) :
    AdicPrincipalUnits F ≃+
      Additive
        ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup F) 1)

structure

DiscretePrincipalUnitQuotient

L159 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient

Documentation

The n-th principal-unit quotient with its mathematically intended discrete topology fixed in the type. Its carrier is finite when F is a LocalField, but not for an arbitrary CompleteDVF.

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 · full declaration

structure DiscretePrincipalUnitQuotient
    (F : CompleteDVF.{u, v} K) (n : ℕ) where
  /-- The underlying quotient class. -/
  val : Additive (Internal.principalUnitQuotientCarrier F n)

theorem

ext

L168 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient.ext

Documentation

Establishes the identity x = y.

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 DiscretePrincipalUnitQuotient

Lean source · statement

theorem ext {F : CompleteDVF.{u, v} K} {n : ℕ}
    {x y : DiscretePrincipalUnitQuotient F n} (h : x.val = y.val) : x = y

def

equiv

L176 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient.equiv

Documentation

The carrier equivalence of a discrete coordinate.

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 DiscretePrincipalUnitQuotient

Lean source · full declaration

def equiv (F : CompleteDVF.{u, v} K) (n : ℕ) :
    DiscretePrincipalUnitQuotient F n ≃
      Additive (Internal.principalUnitQuotientCarrier F n) where
  toFun := DiscretePrincipalUnitQuotient.val
  invFun := fun x => ⟨x⟩
  left_inv := fun x => by cases x; rfl
  right_inv := fun _ => rfl

instance

(anonymous instance)

L188 ↗

Documentation

Equips the target with its canonical TopologicalSpace structure, namely TopologicalSpace (DiscretePrincipalUnitQuotient F n).

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 DiscretePrincipalUnitQuotient

Lean source · statement

instance (F : CompleteDVF.{u, v} K) (n : ℕ) :
    TopologicalSpace (DiscretePrincipalUnitQuotient F n)

instance

(anonymous instance)

L195 ↗

Documentation

Equips the target with its canonical DiscreteTopology structure, namely DiscreteTopology (DiscretePrincipalUnitQuotient F n).

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 DiscretePrincipalUnitQuotient

Lean source · statement

instance (F : CompleteDVF.{u, v} K) (n : ℕ) :
    DiscreteTopology (DiscretePrincipalUnitQuotient F n)

instance

(anonymous instance)

L203 ↗

Documentation

Equips the target with its canonical AddCommGroup structure, namely AddCommGroup (DiscretePrincipalUnitQuotient F n).

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 DiscretePrincipalUnitQuotient

Lean source · statement

instance (F : CompleteDVF.{u, v} K) (n : ℕ) :
    AddCommGroup (DiscretePrincipalUnitQuotient F n)

def

addEquiv

L208 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient.addEquiv

Documentation

Algebraic equivalence forgetting the discrete coordinate wrapper.

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 DiscretePrincipalUnitQuotient

Lean source · statement

def addEquiv (F : CompleteDVF.{u, v} K) (n : ℕ) :
    DiscretePrincipalUnitQuotient F n ≃+
      Additive (Internal.principalUnitQuotientCarrier F n)

theorem

addEquiv_apply

L214 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient.addEquiv_apply

Documentation

The defining evaluation formula for addEquiv is addEquiv F n x = x.val.

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 DiscretePrincipalUnitQuotient

Lean source · statement

theorem addEquiv_apply (F : CompleteDVF.{u, v} K) (n : ℕ)
    (x : DiscretePrincipalUnitQuotient F n) :
    addEquiv F n x = x.val

def

of

L220 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient.of

Documentation

Put a quotient class into its discrete model.

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 DiscretePrincipalUnitQuotient

Lean source · statement

def of (F : CompleteDVF.{u, v} K) (n : ℕ)
    (x : Additive (Internal.principalUnitQuotientCarrier F n)) :
    DiscretePrincipalUnitQuotient F n

theorem

addEquiv_symm_apply

L226 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient.addEquiv_symm_apply

Documentation

The defining evaluation formula for addEquiv is (addEquiv F n).symm x = of F n x.

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 DiscretePrincipalUnitQuotient

Lean source · statement

theorem addEquiv_symm_apply (F : CompleteDVF.{u, v} K) (n : ℕ)
    (x : Additive (Internal.principalUnitQuotientCarrier F n)) :
    (addEquiv F n).symm x = of F n x

theorem

val_of

L232 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient.val_of

Documentation

Establishes the identity (of F n x).val = x.

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 DiscretePrincipalUnitQuotient

Lean source · statement

theorem val_of (F : CompleteDVF.{u, v} K) (n : ℕ)
    (x : Additive (Internal.principalUnitQuotientCarrier F n)) :
    (of F n x).val = x

theorem

addEquiv_of

L237 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient.addEquiv_of

Documentation

Establishes the identity addEquiv F n (of F n x) = x.

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 DiscretePrincipalUnitQuotient

Lean source · statement

theorem addEquiv_of (F : CompleteDVF.{u, v} K) (n : ℕ)
    (x : Additive (Internal.principalUnitQuotientCarrier F n)) :
    addEquiv F n (of F n x) = x

theorem

of_val

L243 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient.of_val

Documentation

Establishes the identity of F n x.val = x.

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 DiscretePrincipalUnitQuotient

Lean source · statement

theorem of_val (F : CompleteDVF.{u, v} K) (n : ℕ)
    (x : DiscretePrincipalUnitQuotient F n) :
    of F n x.val = x

def

principalUnitProdiscreteTopology

L254 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitProdiscreteTopology

Documentation

The product topology of the discrete coordinates on the additive principal-unit inverse 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 principalUnitProdiscreteTopology
    (F : CompleteDVF.{u, v} K) :
    TopologicalSpace (Additive (Internal.principalUnitInverseLimitCarrier F))

structure

PrincipalUnitProdiscreteLimit

L264 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.PrincipalUnitProdiscreteLimit

Documentation

The principal-unit inverse limit with its prodiscrete topology fixed in the type. For a local field, the coordinate quotients are finite and this specializes to the usual profinite topology.

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 · full declaration

structure PrincipalUnitProdiscreteLimit (F : CompleteDVF.{u, v} K) where
  /-- The underlying compatible family. -/
  val : Additive (Internal.principalUnitInverseLimitCarrier F)

def

equiv

L271 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.PrincipalUnitProdiscreteLimit.equiv

Documentation

The carrier equivalence of the prodiscrete inverse-limit model.

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 PrincipalUnitProdiscreteLimit

Lean source · full declaration

def equiv (F : CompleteDVF.{u, v} K) :
    PrincipalUnitProdiscreteLimit F ≃
      Additive (Internal.principalUnitInverseLimitCarrier F) where
  toFun := PrincipalUnitProdiscreteLimit.val
  invFun := fun x => ⟨x⟩
  left_inv := fun x => by cases x; rfl
  right_inv := fun _ => rfl

instance

(anonymous instance)

L283 ↗

Documentation

Equips the target with its canonical TopologicalSpace structure, namely TopologicalSpace (PrincipalUnitProdiscreteLimit F).

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 PrincipalUnitProdiscreteLimit

Lean source · statement

instance (F : CompleteDVF.{u, v} K) :
    TopologicalSpace (PrincipalUnitProdiscreteLimit F)

def

homeomorph

L288 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.PrincipalUnitProdiscreteLimit.homeomorph

Documentation

Forget the wrapper while retaining its fixed prodiscrete topology.

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 PrincipalUnitProdiscreteLimit

Lean source · full declaration

def homeomorph (F : CompleteDVF.{u, v} K) :
    PrincipalUnitProdiscreteLimit F ≃ₜ
      WithTopology
        (Additive (Internal.principalUnitInverseLimitCarrier F))
        (principalUnitProdiscreteTopology F) where
  toEquiv := (equiv F).trans
    (WithTopology.equiv _ (principalUnitProdiscreteTopology F)).symm
  continuous_toFun := by
    let : TopologicalSpace
        (Additive (Internal.principalUnitInverseLimitCarrier F)) :=
      principalUnitProdiscreteTopology F
    change Continuous fun x : PrincipalUnitProdiscreteLimit F =>
      WithTopology.toTopology (principalUnitProdiscreteTopology F) x.val
    exact
      (WithTopology.continuous_toTopology (principalUnitProdiscreteTopology F)).comp
        continuous_induced_dom
  continuous_invFun := by
    let : TopologicalSpace
        (Additive (Internal.principalUnitInverseLimitCarrier F)) :=
      principalUnitProdiscreteTopology F
    change Continuous fun x : WithTopology
        (Additive (Internal.principalUnitInverseLimitCarrier F))
        (principalUnitProdiscreteTopology F) =>
      (⟨x.ofTopology⟩ : PrincipalUnitProdiscreteLimit F)
    exact
      continuous_induced_rng.2
        (WithTopology.continuous_ofTopology (principalUnitProdiscreteTopology F))

instance

(anonymous instance)

L320 ↗

Documentation

Equips the target with its canonical AddCommGroup structure, namely AddCommGroup (PrincipalUnitProdiscreteLimit F).

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 PrincipalUnitProdiscreteLimit

Lean source · statement

instance (F : CompleteDVF.{u, v} K) :
    AddCommGroup (PrincipalUnitProdiscreteLimit F)

def

addEquiv

L325 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.PrincipalUnitProdiscreteLimit.addEquiv

Documentation

The algebraic equivalence forgetting the type-level prodiscrete model.

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 PrincipalUnitProdiscreteLimit

Lean source · statement

def addEquiv (F : CompleteDVF.{u, v} K) :
    PrincipalUnitProdiscreteLimit F ≃+
      Additive (Internal.principalUnitInverseLimitCarrier F)

theorem

addEquiv_apply

L331 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.PrincipalUnitProdiscreteLimit.addEquiv_apply

Documentation

The defining evaluation formula for addEquiv is addEquiv F x = x.val.

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 PrincipalUnitProdiscreteLimit

Lean source · statement

theorem addEquiv_apply (F : CompleteDVF.{u, v} K)
    (x : PrincipalUnitProdiscreteLimit F) :
    addEquiv F x = x.val

def

of

L337 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.PrincipalUnitProdiscreteLimit.of

Documentation

Put a compatible family into its prodiscrete model.

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 PrincipalUnitProdiscreteLimit

Lean source · statement

def of (F : CompleteDVF.{u, v} K)
    (x : Additive (Internal.principalUnitInverseLimitCarrier F)) :
    PrincipalUnitProdiscreteLimit F

theorem

addEquiv_symm_apply

L343 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.PrincipalUnitProdiscreteLimit.addEquiv_symm_apply

Documentation

The defining evaluation formula for addEquiv is (addEquiv F).symm x = of F x.

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 PrincipalUnitProdiscreteLimit

Lean source · statement

theorem addEquiv_symm_apply (F : CompleteDVF.{u, v} K)
    (x : Additive (Internal.principalUnitInverseLimitCarrier F)) :
    (addEquiv F).symm x = of F x

theorem

val_of

L349 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.PrincipalUnitProdiscreteLimit.val_of

Documentation

Establishes the identity (of F x).val = x.

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 PrincipalUnitProdiscreteLimit

Lean source · statement

theorem val_of (F : CompleteDVF.{u, v} K)
    (x : Additive (Internal.principalUnitInverseLimitCarrier F)) :
    (of F x).val = x

theorem

of_val

L354 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.PrincipalUnitProdiscreteLimit.of_val

Documentation

Establishes the identity of F x.val = x.

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 PrincipalUnitProdiscreteLimit

Lean source · statement

theorem of_val (F : CompleteDVF.{u, v} K)
    (x : PrincipalUnitProdiscreteLimit F) : of F x.val = x

def

coordinate

L360 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.PrincipalUnitProdiscreteLimit.coordinate

Documentation

Evaluation at one discrete coordinate, as an additive homomorphism.

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 PrincipalUnitProdiscreteLimit

Lean source · statement

def coordinate (F : CompleteDVF.{u, v} K) (n : ℕ) :
    PrincipalUnitProdiscreteLimit F →+
      DiscretePrincipalUnitQuotient F n

theorem

coordinate_apply

L373 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.PrincipalUnitProdiscreteLimit.coordinate_apply

Documentation

The defining evaluation formula for coordinate is coordinate F n x = DiscretePrincipalUnitQuotient.of F n (Additive.ofMul (Internal.principalUnitInverseLimitCarrierEval F n (Additive.toMul (addEquiv F x)))).

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 PrincipalUnitProdiscreteLimit

Lean source · statement

theorem coordinate_apply (F : CompleteDVF.{u, v} K) (n : ℕ)
    (x : PrincipalUnitProdiscreteLimit F) :
    coordinate F n x = DiscretePrincipalUnitQuotient.of F n
      (Additive.ofMul
        (Internal.principalUnitInverseLimitCarrierEval F n
          (Additive.toMul (addEquiv F x))))

Module documentation

Type-level topology models for principal units

Topology is part of the type

Declarations