Module

QuotientPadicContinuity.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnitPadicAction.QuotientPadicContinuity

2 declarations indexed from sourceView source ↗

Module documentation

Continuity and compatibility of the principal-unit quotient actions

Reduction of scalars to ZMod (p^n) makes each coordinate action continuous. Density of natural scalars then proves compatibility with quotient reduction.

Imports4

Imported by2

theorem

padicContinuousSMul

L29 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient.padicContinuousSMul

Documentation

The explicitly constructed action is jointly continuous.

Source context 6 commands

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

namespace LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
namespace DiscretePrincipalUnitQuotient
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 padicContinuousSMul (n : ℕ) :
    @ContinuousSMul ℤ_[p] (DiscretePrincipalUnitQuotient F n)
      (padicModule F p n).toSMul inferInstance inferInstance

theorem

transition_padic_smul

L45 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient.transition_padic_smul