Module

MixedCharAutomorphismRepresentations.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharAutomorphismRepresentations

2 declarations indexed from sourceView source ↗

Module documentation

The actual p-adic representations of valuation-preserving automorphisms

The concrete field action restricts to principal units. Its compatibility with the constructed p-adic scalars supplies the linear representation laws.

Imports4

Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPrincipalUnitPadicEquivariance
Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPadicIntMapEquivariance
Mathlib.RepresentationTheory.Basic
Mathlib.Algebra.Module.RingHom

Imported by3

def

principalUnitRepresentationOfMixedChar

L32 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitRepresentationOfMixedChar

Documentation

The concrete automorphism action on principal units is p-adic linear.

Source context 8 commands

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

namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u w
variable {K : Type u} [Field K] {Δ : Type w} [Monoid Δ]
variable (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
variable [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
variable (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]
variable (σ : Δ →* (K ≃+* K)) (hval : ∀ (g : Δ) (x : K), v (σ g x) = v x)
open CompleteDVF.higherPrincipalUnitGroup

Lean source · statement

def principalUnitRepresentationOfMixedChar :
    @Representation ℤ_[p] Δ
      (Additive (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v) 1))
      inferInstance inferInstance inferInstance (principalUnitPadicModuleOfMixedChar v p)

def

fieldRepresentationOfMixedChar

L74 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.fieldRepresentationOfMixedChar