ModuleQuotientPadicModule.lean
Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnitPadicAction.QuotientPadicModule
3 declarations indexed from sourceView source ↗ Module documentation
P-adic scalars on principal-unit quotients with arbitrary residue field
The exponent p^n of the level quotient supplies its ZMod (p^n) module. Reduction of p-adic integers then supplies the scalar action. These are explicit constructions, avoiding competing local-field instances.
Declarations
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient.zmodModule
DocumentationScalar reduction is justified by the actual prime-power exponent.
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]
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient.padicModule
DocumentationThe level quotient as a p-adic module, without finiteness assumptions.
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]
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient.padic_smul_eq_val_nsmul
DocumentationThe action is given by an ordinary power representative modulo p^n.
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]