Module

ResidueCharProdiscreteModule.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnitPadicAction.ResidueCharProdiscreteModule

4 declarations indexed from sourceView source ↗

Module documentation

P-adic scalars on the principal-unit prodiscrete limit

The compatible quotient actions define an action on the actual inverse-limit carrier. Its module laws and joint continuity follow coordinate by coordinate, without a finiteness assumption on the residue field.

Imports2

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnitPadicAction.QuotientPadicContinuity
Mathlib.Algebra.Module.MinimalAxioms

Imported by2

def

padicSMulOfResidueChar

L28 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.PrincipalUnitProdiscreteLimit.padicSMulOfResidueChar

Documentation

Coordinatewise scalar multiplication is a compatible family.

Source context 6 commands

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

namespace LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
namespace PrincipalUnitProdiscreteLimit
universe u v
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
variable (p : ℕ) [Fact p.Prime] [CharP F.residueField p]

Lean source · full declaration

def padicSMulOfResidueChar :
    SMul ℤ_[p] (PrincipalUnitProdiscreteLimit F) where
  smul a x := ⟨Additive.ofMul ⟨fun n => Additive.toMul
    (((DiscretePrincipalUnitQuotient.padicModule F p n).toSMul.smul
      a (coordinate F n x)).val), by
    intro m n hmn
    have hcompat : DiscretePrincipalUnitQuotient.transition F hmn (coordinate F n x) =
        coordinate F m x := by
      apply DiscretePrincipalUnitQuotient.ext
      exact congrArg Additive.ofMul ((Additive.toMul x.val).2 hmn)
    have h := DiscretePrincipalUnitQuotient.transition_padic_smul F p hmn a
      (coordinate F n x)
    rw [hcompat] at h
    exact congrArg
      (fun y : DiscretePrincipalUnitQuotient F m => Additive.toMul y.val) h⟩⟩

def

padicModuleOfResidueChar

L46 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.PrincipalUnitProdiscreteLimit.padicModuleOfResidueChar

Documentation

The principal-unit prodiscrete limit is a p-adic module for any residue field of characteristic p. The structure is explicit, not a global instance.

Source context 6 commands

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

namespace LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
namespace PrincipalUnitProdiscreteLimit
universe u v
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
variable (p : ℕ) [Fact p.Prime] [CharP F.residueField p]

Lean source · statement

def padicModuleOfResidueChar :
    Module ℤ_[p] (PrincipalUnitProdiscreteLimit F)

theorem

coordinate_padic_smulOfResidueChar

L86 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.PrincipalUnitProdiscreteLimit.coordinate_padic_smulOfResidueChar

Documentation

The constructed scalar multiplication has the specified quotient coordinates.

Source context 6 commands

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

namespace LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
namespace PrincipalUnitProdiscreteLimit
universe u v
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
variable (p : ℕ) [Fact p.Prime] [CharP F.residueField p]

Lean source · statement

theorem coordinate_padic_smulOfResidueChar (n : ℕ) (a : ℤ_[p])
    (x : PrincipalUnitProdiscreteLimit F) :
    coordinate F n ((padicModuleOfResidueChar F p).toSMul.smul a x) =
      (DiscretePrincipalUnitQuotient.padicModule F p n).toSMul.smul
        a (coordinate F n x)

theorem

padicContinuousSMulOfResidueChar

L93 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.PrincipalUnitProdiscreteLimit.padicContinuousSMulOfResidueChar

Documentation

The actual coordinatewise p-adic action is jointly continuous.

Source context 6 commands

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

namespace LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
namespace PrincipalUnitProdiscreteLimit
universe u v
variable {K : Type u} [Field K]
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
variable (p : ℕ) [Fact p.Prime] [CharP F.residueField p]

Lean source · statement

theorem padicContinuousSMulOfResidueChar :
    @ContinuousSMul ℤ_[p] (PrincipalUnitProdiscreteLimit F)
      (padicModuleOfResidueChar F p).toSMul inferInstance inferInstance

Module documentation

P-adic scalars on the principal-unit prodiscrete limit

Declarations

padicSMulOfResidueChar

padicModuleOfResidueChar

coordinate_padic_smulOfResidueChar

padicContinuousSMulOfResidueChar