Module

AdicPadicModule.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnitPadicAction.AdicPadicModule

15 declarations indexed from sourceView source ↗

Module documentation

The p-adic module on adic principal units

The coordinatewise p-adic action is transported across the canonical adic/prodiscrete comparison, producing its linear and topological forms on first principal units.

Imports3

Mathlib.Algebra.Module.MinimalAxioms
Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnitPadicAction.ProdiscretePadicModule
Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnitPadicAction.AdicProdiscreteComparison

Imported by3

instance

principalUnitPadicSMul

L42 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitPadicSMul

Documentation

Transport the coordinatewise p-adic scalar multiplication from the inverse limit to U^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 · full declaration

instance principalUnitPadicSMul
    (F : LocalField.{u, v} K) :
    SMul ℤ_[F.residueCharacteristic]
      (Additive ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
        F.toCompleteDVF) 1)) where
  smul a x :=
    (principalUnitAddEquivInverseLimitCarrier F.toCompleteDVF).symm
      (a • principalUnitAddEquivInverseLimitCarrier F.toCompleteDVF x)

theorem

principalUnitPadic_smul_def

L55 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitPadic_smul_def

Documentation

Establishes the identity a • x = (principalUnitAddEquivInverseLimitCarrier F.toCompleteDVF).symm (a • principalUnitAddEquivInverseLimitCarrier F.toCompleteDVF 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 principalUnitPadic_smul_def
    (F : LocalField.{u, v} K)
    (a : ℤ_[F.residueCharacteristic])
    (x : Additive ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
      F.toCompleteDVF) 1)) :
    a • x =
      (principalUnitAddEquivInverseLimitCarrier F.toCompleteDVF).symm
        (a • principalUnitAddEquivInverseLimitCarrier F.toCompleteDVF x)

instance

principalUnitPadicModule

L67 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitPadicModule

Documentation

The standard Z_p-module structure on the first principal units of a local field.

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 principalUnitPadicModule
    (F : LocalField.{u, v} K) :
    Module ℤ_[F.residueCharacteristic]
      (Additive ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
        F.toCompleteDVF) 1))

instance

adicPrincipalUnitsPadicModule

L112 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.adicPrincipalUnitsPadicModule

Documentation

Equips the target in Module ℤ_[F.residueCharacteristic] (AdicPrincipalUnits F.toCompleteDVF) with the indicated module structure.

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 adicPrincipalUnitsPadicModule
    (F : LocalField.{u, v} K) :
    Module ℤ_[F.residueCharacteristic]
      (AdicPrincipalUnits F.toCompleteDVF)

theorem

addEquiv_map_smul

L128 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.AdicPrincipalUnits.addEquiv_map_smul

Documentation

Establishes the identity AdicPrincipalUnits.addEquiv F.toCompleteDVF (a • x) = a • AdicPrincipalUnits.addEquiv F.toCompleteDVF 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 AdicPrincipalUnits.addEquiv_map_smul
    (F : LocalField.{u, v} K) (a : ℤ_[F.residueCharacteristic])
    (x : AdicPrincipalUnits F.toCompleteDVF) :
    AdicPrincipalUnits.addEquiv F.toCompleteDVF (a • x) =
      a • AdicPrincipalUnits.addEquiv F.toCompleteDVF x

def

linearEquivUnderlying

L137 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.AdicPrincipalUnits.linearEquivUnderlying

Documentation

The adic wrapper and its underlying principal-unit module are canonically Z_p-linearly equivalent.

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 AdicPrincipalUnits.linearEquivUnderlying
    (F : LocalField.{u, v} K) :
    AdicPrincipalUnits F.toCompleteDVF ≃ₗ[ℤ_[F.residueCharacteristic]]
      Additive
        ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
          F.toCompleteDVF) 1)

theorem

principalUnitAddEquivInverseLimitCarrier_map_smul

L150 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitAddEquivInverseLimitCarrier_map_smul

Documentation

Establishes the identity principalUnitAddEquivInverseLimitCarrier F.toCompleteDVF (a • x) = a • principalUnitAddEquivInverseLimitCarrier F.toCompleteDVF 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.principalUnitAddEquivInverseLimitCarrier_map_smul
    (F : LocalField.{u, v} K)
    (a : ℤ_[F.residueCharacteristic])
    (x : Additive ((LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
      F.toCompleteDVF) 1)) :
    principalUnitAddEquivInverseLimitCarrier F.toCompleteDVF (a • x) =
      a • principalUnitAddEquivInverseLimitCarrier F.toCompleteDVF x

theorem

principalUnitPadic_smul_carrier_coordinate

L169 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitPadic_smul_carrier_coordinate

Documentation

Coordinate formula for the canonical action: the class of a • x at level n is obtained by reducing a modulo p^(f*n) and acting on the class of 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.principalUnitPadic_smul_carrier_coordinate
    (F : LocalField.{u, v} K)
    (a : ℤ_[F.residueCharacteristic])
    (x : (LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
      F.toCompleteDVF) 1) (n : ℕ) :
    Additive.ofMul
        ((principalUnitMulEquivInverseLimitCarrier F.toCompleteDVF
          (Additive.toMul (a • Additive.ofMul x))).1 n) =
      principalUnitQuotientCarrierPadicScalar F n a
        (Additive.ofMul
          ((principalUnitMulEquivInverseLimitCarrier F.toCompleteDVF x).1 n))

theorem

adicPrincipalUnitsHomeomorphProdiscreteLimit_map_smul

L191 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.adicPrincipalUnitsHomeomorphProdiscreteLimit_map_smul

Documentation

The canonical identification of adic principal units with the prodiscrete limit respects the p-adic action.

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_map_smul
    (F : LocalField.{u, v} K)
    (a : ℤ_[F.residueCharacteristic])
    (x : AdicPrincipalUnits F.toCompleteDVF) :
    adicPrincipalUnitsHomeomorphProdiscreteLimit F.toCompleteDVF (a • x) =
      a • adicPrincipalUnitsHomeomorphProdiscreteLimit F.toCompleteDVF x

theorem

adicPrincipalUnitsAddEquivProdiscreteLimit_map_smul

L209 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.adicPrincipalUnitsAddEquivProdiscreteLimit_map_smul

Documentation

Establishes the identity adicPrincipalUnitsAddEquivProdiscreteLimit F.toCompleteDVF (a • x) = a • adicPrincipalUnitsAddEquivProdiscreteLimit F.toCompleteDVF 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 adicPrincipalUnitsAddEquivProdiscreteLimit_map_smul
    (F : LocalField.{u, v} K)
    (a : ℤ_[F.residueCharacteristic])
    (x : AdicPrincipalUnits F.toCompleteDVF) :
    adicPrincipalUnitsAddEquivProdiscreteLimit F.toCompleteDVF (a • x) =
      a • adicPrincipalUnitsAddEquivProdiscreteLimit F.toCompleteDVF x

def

adicPrincipalUnitsLinearEquivProdiscreteLimit

L233 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.adicPrincipalUnitsLinearEquivProdiscreteLimit

Documentation

Z_p-linear form of the canonical adic/prodiscrete comparison.

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 adicPrincipalUnitsLinearEquivProdiscreteLimit
    (F : LocalField.{u, v} K) :
    AdicPrincipalUnits F.toCompleteDVF ≃ₗ[ℤ_[F.residueCharacteristic]]
      PrincipalUnitProdiscreteLimit F.toCompleteDVF

def

adicPrincipalUnitsCoordinateLinear

L242 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.adicPrincipalUnitsCoordinateLinear

Documentation

Projection from adic first principal units to one wrapped quotient coordinate.

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 adicPrincipalUnitsCoordinateLinear
    (F : LocalField.{u, v} K) (n : ℕ) :
    AdicPrincipalUnits F.toCompleteDVF →ₗ[ℤ_[F.residueCharacteristic]]
      DiscretePrincipalUnitQuotient F.toCompleteDVF n

theorem

continuous_adicPrincipalUnitsPadic_smul

L253 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.continuous_adicPrincipalUnitsPadic_smul

Documentation

The specified map is continuous: Continuous fun z : ℤ_[F.residueCharacteristic] × AdicPrincipalUnits F.toCompleteDVF => z.1 • z.2.

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

theorem continuous_adicPrincipalUnitsPadic_smul
    (F : LocalField.{u, v} K) :
    Continuous fun z : ℤ_[F.residueCharacteristic] ×
        AdicPrincipalUnits F.toCompleteDVF =>
      z.1 • z.2 := by
  let e := adicPrincipalUnitsHomeomorphProdiscreteLimit F.toCompleteDVF
  have hpair : Continuous fun z : ℤ_[F.residueCharacteristic] ×
      AdicPrincipalUnits F.toCompleteDVF =>
      (z.1, e z.2) :=
    continuous_fst.prodMk (e.continuous.comp continuous_snd)
  have htransport := e.continuous_symm.comp (continuous_smul.comp hpair)
  exact htransport

instance

adicPrincipalUnitsContinuousSMul

L270 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.adicPrincipalUnitsContinuousSMul

Documentation

The scalar action in ContinuousSMul ℤ_[F.residueCharacteristic] (AdicPrincipalUnits F.toCompleteDVF) is continuous.

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 adicPrincipalUnitsContinuousSMul
    (F : LocalField.{u, v} K) :
    ContinuousSMul ℤ_[F.residueCharacteristic]
      (AdicPrincipalUnits F.toCompleteDVF)

instance

adicPrincipalUnitsContinuousAdd

L277 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.adicPrincipalUnitsContinuousAdd

Documentation

Addition on the adic principal-unit model is continuous.

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 adicPrincipalUnitsContinuousAdd
    (F : LocalField.{u, v} K) :
    ContinuousAdd (AdicPrincipalUnits F.toCompleteDVF)

Module documentation

The p-adic module on adic principal units

Declarations