Module

ResidueCharPrincipalUnitModule.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnitPadicAction.ResidueCharPrincipalUnitModule

1 declaration indexed from sourceView source ↗

Module documentation

P-adic scalars on the actual principal-unit group

The adic inverse-limit equivalence transports the compatible coordinate actions to U^1. No finite-residue-field assumption is used.

Imports2

Imported by3

def

principalUnitPadicModuleOfResidueChar

L24 ↗

LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitPadicModuleOfResidueChar

Documentation

The principal-unit group as a p-adic module over its residue prime.

Source context 3 commands

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

namespace LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
universe u v
variable {K : Type u} [Field K]

Lean source · statement

def principalUnitPadicModuleOfResidueChar
    (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
    (p : ℕ) [Fact p.Prime] [hres : CharP F.residueField p] :
    Module ℤ_[p] (Additive (higherPrincipalUnitGroup F 1))

Module documentation

P-adic scalars on the actual principal-unit group

Declarations

principalUnitPadicModuleOfResidueChar