NYLL
Module

ProdiscretePadicModule.lean

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

Module documentation

The p-adic module on the prodiscrete principal-unit limit

Coordinatewise scalar multiplication makes the prodiscrete inverse limit a topological module over the p-adic integers.

The inverse-limit module and transport to U^1

Imports2
Imported by3

Declarations

instance

principalUnitInverseLimitCarrierPadicSMul

L43 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitInverseLimitCarrierPadicSMul
Documentation

Coordinatewise p-adic scalar multiplication on the compatible 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 · full declaration
instance Internal.principalUnitInverseLimitCarrierPadicSMul
    (F : LocalField.{u, v} K) :
    SMul ℤ_[F.residueCharacteristic]
      (Additive (Internal.principalUnitInverseLimitCarrier F.toCompleteDVF)) where
  smul a x := Additive.ofMul
    ⟨fun n => Additive.toMul
        (a • Additive.ofMul ((Additive.toMul x).1 n)), by
      intro m n hmn
      apply Additive.ofMul.injective
      change
        principalUnitQuotientCarrierTransitionAdd F.toCompleteDVF hmn
            (a • Additive.ofMul ((Additive.toMul x).1 n)) =
          a • Additive.ofMul ((Additive.toMul x).1 m)
      rw [principalUnitQuotientCarrierTransitionAdd_map_smul]
      change
        a • Additive.ofMul
            (principalUnitQuotientCarrierTransition F.toCompleteDVF hmn
              ((Additive.toMul x).1 n)) =
          a • Additive.ofMul ((Additive.toMul x).1 m)
      rw [(Additive.toMul x).2 hmn]⟩
theorem

principalUnitInverseLimitCarrierPadic_smul_apply

L70 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitInverseLimitCarrierPadic_smul_apply
Documentation

The defining evaluation formula for Internal.principalUnitInverseLimitCarrierPadic_smul is Additive.ofMul (Internal.principalUnitInverseLimitCarrierEval F.toCompleteDVF n (Additive.toMul (a • x))) = a • Additive.ofMul (Internal.principalUnitInverseLimitCarrierEval F.toCompleteDVF n (Additive.toMul 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.principalUnitInverseLimitCarrierPadic_smul_apply
    (F : LocalField.{u, v} K)
    (a : ℤ_[F.residueCharacteristic])
    (x : Additive (Internal.principalUnitInverseLimitCarrier F.toCompleteDVF))
    (n : ℕ) :
    Additive.ofMul
        (Internal.principalUnitInverseLimitCarrierEval F.toCompleteDVF n
          (Additive.toMul (a • x))) =
      a • Additive.ofMul
        (Internal.principalUnitInverseLimitCarrierEval F.toCompleteDVF n
          (Additive.toMul x))
instance

principalUnitInverseLimitCarrierPadicModule

L87 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitInverseLimitCarrierPadicModule
Documentation

Equips the target in Module ℤ_[F.residueCharacteristic] (Additive (Internal.principalUnitInverseLimitCarrier 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 Internal.principalUnitInverseLimitCarrierPadicModule
    (F : LocalField.{u, v} K) :
    Module ℤ_[F.residueCharacteristic]
      (Additive (Internal.principalUnitInverseLimitCarrier F.toCompleteDVF))
instance

principalUnitProdiscreteLimitPadicModule

L161 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitProdiscreteLimitPadicModule
Documentation

Equips the target in Module ℤ_[F.residueCharacteristic] (PrincipalUnitProdiscreteLimit 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 principalUnitProdiscreteLimitPadicModule
    (F : LocalField.{u, v} K) :
    Module ℤ_[F.residueCharacteristic]
      (PrincipalUnitProdiscreteLimit F.toCompleteDVF)
theorem

addEquiv_map_smul

L175 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.PrincipalUnitProdiscreteLimit.addEquiv_map_smul
Documentation

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

coordinate_smul

L186 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.PrincipalUnitProdiscreteLimit.coordinate_smul
Documentation

Establishes the identity PrincipalUnitProdiscreteLimit.coordinate F.toCompleteDVF n (a • x) = a • PrincipalUnitProdiscreteLimit.coordinate F.toCompleteDVF n 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 PrincipalUnitProdiscreteLimit.coordinate_smul
    (F : LocalField.{u, v} K) (n : ℕ)
    (a : ℤ_[F.residueCharacteristic])
    (x : PrincipalUnitProdiscreteLimit F.toCompleteDVF) :
    PrincipalUnitProdiscreteLimit.coordinate F.toCompleteDVF n (a • x) =
      a • PrincipalUnitProdiscreteLimit.coordinate F.toCompleteDVF n x
def

coordinateLinear

L203 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.PrincipalUnitProdiscreteLimit.coordinateLinear
Documentation

Evaluation at a wrapped coordinate as a Z_p-linear map.

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
def PrincipalUnitProdiscreteLimit.coordinateLinear
    (F : LocalField.{u, v} K) (n : ℕ) :
    PrincipalUnitProdiscreteLimit F.toCompleteDVF →ₗ[
      ℤ_[F.residueCharacteristic]]
      DiscretePrincipalUnitQuotient F.toCompleteDVF n where
  toFun := PrincipalUnitProdiscreteLimit.coordinate F.toCompleteDVF n
  map_add' := fun x y =>
    (PrincipalUnitProdiscreteLimit.coordinate F.toCompleteDVF n).map_add x y
  map_smul' := PrincipalUnitProdiscreteLimit.coordinate_smul F n
theorem

continuous_principalUnitInverseLimitCarrierPadic_smul

L215 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.continuous_principalUnitInverseLimitCarrierPadic_smul
Documentation

Joint continuity of the coordinatewise p-adic action on the inverse limit of discrete finite quotients.

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 Internal.continuous_principalUnitInverseLimitCarrierPadic_smul
    (F : LocalField.{u, v} K) :
    letI : (n : ℕ) → TopologicalSpace
        (Internal.principalUnitQuotientCarrier F.toCompleteDVF n) := fun _ => ⊥
    Continuous fun z : ℤ_[F.residueCharacteristic] ×
        Additive (Internal.principalUnitInverseLimitCarrier F.toCompleteDVF) =>
      z.1 • z.2 := by
  let : (n : ℕ) → TopologicalSpace
      (Internal.principalUnitQuotientCarrier F.toCompleteDVF n) := fun _ => ⊥
  let : (n : ℕ) → DiscreteTopology
      (Internal.principalUnitQuotientCarrier F.toCompleteDVF n) := fun _ => ⟨rfl⟩
  have hmul : Continuous fun z : ℤ_[F.residueCharacteristic] ×
      Additive (Internal.principalUnitInverseLimitCarrier F.toCompleteDVF) =>
      Additive.toMul (z.1 • z.2) := by
    exact Continuous.subtype_mk
      (continuous_pi fun n => by
        have hlimval : Continuous fun x : Additive
            (Internal.principalUnitInverseLimitCarrier F.toCompleteDVF) =>
            (Additive.toMul x).1 :=
          continuous_subtype_val
        have hcoord : Continuous fun z : ℤ_[F.residueCharacteristic] ×
            Additive (Internal.principalUnitInverseLimitCarrier F.toCompleteDVF) =>
            Additive.ofMul ((Additive.toMul z.2).1 n) :=
          ((continuous_apply n).comp hlimval).comp continuous_snd
        have hs := (Internal.continuous_principalUnitQuotientCarrierPadicScalar F n).comp
          (continuous_fst.prodMk hcoord)
        change Continuous fun z : ℤ_[F.residueCharacteristic] ×
            Additive (Internal.principalUnitInverseLimitCarrier F.toCompleteDVF) =>
          Additive.toMul
            (principalUnitQuotientCarrierPadicScalar F n z.1
              (Additive.ofMul ((Additive.toMul z.2).1 n)))
        exact hs)
      (fun z : ℤ_[F.residueCharacteristic] ×
          Additive (Internal.principalUnitInverseLimitCarrier F.toCompleteDVF) => by
        intro i j hij
        exact (Additive.toMul (z.1 • z.2)).2 hij)
  exact hmul
theorem

continuous_principalUnitProdiscreteLimitPadic_smul

L257 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.continuous_principalUnitProdiscreteLimitPadic_smul
Documentation

The specified map is continuous: Continuous fun z : ℤ_[F.residueCharacteristic] × PrincipalUnitProdiscreteLimit 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_principalUnitProdiscreteLimitPadic_smul
    (F : LocalField.{u, v} K) :
    Continuous fun z : ℤ_[F.residueCharacteristic] ×
        PrincipalUnitProdiscreteLimit F.toCompleteDVF =>
      z.1 • z.2 := by
  let : (n : ℕ) → TopologicalSpace
      (Internal.principalUnitQuotientCarrier F.toCompleteDVF n) := fun _ => ⊥
  let e := (PrincipalUnitProdiscreteLimit.homeomorph F.toCompleteDVF).trans
    (WithTopology.homeomorph
      (α := Additive
        (Internal.principalUnitInverseLimitCarrier F.toCompleteDVF))
      (topology := principalUnitProdiscreteTopology F.toCompleteDVF))
  have hpair : Continuous fun z : ℤ_[F.residueCharacteristic] ×
      PrincipalUnitProdiscreteLimit F.toCompleteDVF =>
      (z.1, e z.2) :=
    continuous_fst.prodMk (e.continuous.comp continuous_snd)
  have h := e.continuous_symm.comp
    ((Internal.continuous_principalUnitInverseLimitCarrierPadic_smul F).comp hpair)
  exact h
instance

principalUnitProdiscreteLimitContinuousSMul

L281 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitProdiscreteLimitContinuousSMul
Documentation

The scalar action in ContinuousSMul ℤ_[F.residueCharacteristic] (PrincipalUnitProdiscreteLimit 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 principalUnitProdiscreteLimitContinuousSMul
    (F : LocalField.{u, v} K) :
    ContinuousSMul ℤ_[F.residueCharacteristic]
      (PrincipalUnitProdiscreteLimit F.toCompleteDVF)
instance

principalUnitProdiscreteLimitContinuousAdd

L289 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitProdiscreteLimitContinuousAdd
Documentation

Addition on the type-level prodiscrete principal-unit limit 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 principalUnitProdiscreteLimitContinuousAdd
    (F : LocalField.{u, v} K) :
    ContinuousAdd (PrincipalUnitProdiscreteLimit F.toCompleteDVF)

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