Module

MixedCharPrincipalUnitLogRepresentation.lean

Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPrincipalUnitLogRepresentation

4 declarations indexed from sourceView source ↗

Module documentation

The actual principal-unit logarithm as an intertwining map

The logarithm is linear for the canonical p-adic module structures and intertwines the actual valuation-preserving automorphisms. This supplies its image as a subrepresentation without any image-stability hypothesis.

Imports4

Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharAutomorphismRepresentations
Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPrincipalUnitLogLinearity
Nyll.ValuedFieldTheory.LocalField.Analytic.MixedCharPrincipalUnitLogEquivariance
Mathlib.RepresentationTheory.Intertwining

Imported by3

def

principalUnitLogLinearMapOfMixedChar

L32 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogLinearMapOfMixedChar

Documentation

The actual logarithm is linear over the canonical p-adic integer map.

Source context 5 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u w
variable {K : Type u} [Field K] [CharZero K]
variable (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
  [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
  (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]

Lean source · statement

def principalUnitLogLinearMapOfMixedChar :
    @LinearMap ℤ_[p] ℤ_[p] _ _ (RingHom.id ℤ_[p])
      (Additive (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v) 1)) K
      _ _ (principalUnitPadicModuleOfMixedChar v p) (padicIntToFieldOfMixedChar v p).toModule

theorem

principalUnitLogLinearMapOfMixedChar_apply

L43 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogLinearMapOfMixedChar_apply

Documentation

The linear map retains the original principal-unit logarithm.

Source context 5 commands

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

noncomputable section
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
universe u w
variable {K : Type u} [Field K] [CharZero K]
variable (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
  [ValuationTheory.DiscreteValuationField.Valuation.IsCompleteDiscrete v]
  (p : ℕ) [Fact p.Prime] [CharP (IsLocalRing.ResidueField v.valuationSubring) p]

Lean source · statement

theorem principalUnitLogLinearMapOfMixedChar_apply
    (x : Additive (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v) 1)) :
    principalUnitLogLinearMapOfMixedChar v p x =
      (principalUnitLogOfMixedChar v p (Additive.toMul x)).toAdd

def

principalUnitLogIntertwinerOfMixedChar

L52 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogIntertwinerOfMixedChar

Documentation

The original logarithm intertwines the two actual automorphism actions.

Source context 6 commands

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

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

Lean source · statement

def principalUnitLogIntertwinerOfMixedChar :
    @Representation.IntertwiningMap ℤ_[p] Γ
      (Additive (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v) 1)) K
      _ _ _ _ (principalUnitPadicModuleOfMixedChar v p) (padicIntToFieldOfMixedChar v p).toModule
      (principalUnitRepresentationOfMixedChar v p σ hval)
      (fieldRepresentationOfMixedChar v p σ hval)

theorem

principalUnitLogIntertwinerOfMixedChar_apply

L70 ↗

LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.principalUnitLogIntertwinerOfMixedChar_apply

Documentation

The intertwining map has the same values as the original logarithm.

Source context 6 commands

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

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

Lean source · statement

theorem principalUnitLogIntertwinerOfMixedChar_apply
    (x : Additive (CompleteDVF.higherPrincipalUnitGroup (completeDVFOfWithZeroValuation v) 1)) :
    principalUnitLogIntertwinerOfMixedChar v p σ hval x =
      (principalUnitLogOfMixedChar v p (Additive.toMul x)).toAdd

Module documentation

The actual principal-unit logarithm as an intertwining map

Declarations

principalUnitLogLinearMapOfMixedChar

principalUnitLogLinearMapOfMixedChar_apply

principalUnitLogIntertwinerOfMixedChar

principalUnitLogIntertwinerOfMixedChar_apply