NYLL
Module

FiniteQuotientPadicModule.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnitPadicAction.FiniteQuotientPadicModule
20 declarations indexed from sourceView source ↗

Module documentation

P-adic modules on finite principal-unit quotients

Finite principal-unit quotients have the expected residue-characteristic exponent. Reduction of p-adic integers therefore supplies canonical module structures, compatible with the transition maps.

The finite-coordinate p-adic actions

Imports8
Imported by3

Declarations

def

principalUnitResidueDegree

L49 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitResidueDegree
Documentation

The residue degree f, chosen from the finite-field identity q = p^f.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
def principalUnitResidueDegree
    (F : LocalField.{u, v} K) : ℕ+
theorem

residueCharacteristic_prime_and_card_eq_pow_residueDegree

L59 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueCharacteristic_prime_and_card_eq_pow_residueDegree
Documentation

Establishes the identity F.residueCharacteristic.Prime ∧ Nat.card F.residueField = F.residueCharacteristic ^ (principalUnitResidueDegree F : ℕ).

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
theorem residueCharacteristic_prime_and_card_eq_pow_residueDegree
    (F : LocalField.{u, v} K) :
    F.residueCharacteristic.Prime ∧
      Nat.card F.residueField =
        F.residueCharacteristic ^ (principalUnitResidueDegree F : ℕ)
theorem

principalUnitResidueDegree_unique

L72 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitResidueDegree_unique
Documentation

The finite-field cardinality identity uniquely determines the residue degree selected above.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
theorem principalUnitResidueDegree_unique
    (F : LocalField.{u, v} K) (d : ℕ+)
    (hcard :
      Nat.card F.residueField =
        F.residueCharacteristic ^ (d : ℕ)) :
    d = principalUnitResidueDegree F
instance

principalUnitQuotientCarrier_finite

L85 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitQuotientCarrier_finite
Documentation

The type in Finite (Internal.principalUnitQuotientCarrier F.toCompleteDVF n) is finite.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
instance Internal.principalUnitQuotientCarrier_finite
    (F : LocalField.{u, v} K) (n : ℕ) :
    Finite (Internal.principalUnitQuotientCarrier F.toCompleteDVF n)
theorem

card_principalUnitQuotientCarrier_eq_residueCharacteristic_pow

L99 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.card_principalUnitQuotientCarrier_eq_residueCharacteristic_pow
Documentation

The n-th first-principal-unit quotient has cardinality p^(f*n).

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
theorem Internal.card_principalUnitQuotientCarrier_eq_residueCharacteristic_pow
    (F : LocalField.{u, v} K) (n : ℕ) :
    Nat.card (Internal.principalUnitQuotientCarrier F.toCompleteDVF n) =
      F.residueCharacteristic ^ ((principalUnitResidueDegree F : ℕ) * n)
instance

discretePrincipalUnitQuotientFinite

L151 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.discretePrincipalUnitQuotientFinite
Documentation

The type in Finite (DiscretePrincipalUnitQuotient F.toCompleteDVF n) is finite.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
instance discretePrincipalUnitQuotientFinite
    (F : LocalField.{u, v} K) (n : ℕ) :
    Finite (DiscretePrincipalUnitQuotient F.toCompleteDVF n)
theorem

card_discretePrincipalUnitQuotient_eq_residueCharacteristic_pow

L160 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.card_discretePrincipalUnitQuotient_eq_residueCharacteristic_pow
Documentation

A wrapped level quotient has the expected local-field cardinality p^(f*n).

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
theorem card_discretePrincipalUnitQuotient_eq_residueCharacteristic_pow
    (F : LocalField.{u, v} K) (n : ℕ) :
    Nat.card (DiscretePrincipalUnitQuotient F.toCompleteDVF n) =
      F.residueCharacteristic ^ ((principalUnitResidueDegree F : ℕ) * n)
theorem

principalUnitQuotientCarrier_pow_residueCharacteristic_pow_eq_one

L183 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitQuotientCarrier_pow_residueCharacteristic_pow_eq_one
Documentation

Lagrange's theorem gives the exact exponent bound needed to reduce a p-adic scalar modulo p^(f*n).

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
theorem Internal.principalUnitQuotientCarrier_pow_residueCharacteristic_pow_eq_one
    (F : LocalField.{u, v} K) (n : ℕ)
    (x : Internal.principalUnitQuotientCarrier F.toCompleteDVF n) :
    x ^ (F.residueCharacteristic ^
        ((principalUnitResidueDegree F : ℕ) * n)) = 1
theorem

principalUnitQuotientCarrier_nsmul_residueCharacteristic_pow_eq_zero

L195 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitQuotientCarrier_nsmul_residueCharacteristic_pow_eq_zero
Documentation

Establishes the identity (F.residueCharacteristic ^ ((principalUnitResidueDegree F : ℕ) * n)) • x = 0.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
theorem Internal.principalUnitQuotientCarrier_nsmul_residueCharacteristic_pow_eq_zero
    (F : LocalField.{u, v} K) (n : ℕ)
    (x : Additive (Internal.principalUnitQuotientCarrier F.toCompleteDVF n)) :
    (F.residueCharacteristic ^
        ((principalUnitResidueDegree F : ℕ) * n)) • x = 0
theorem

discretePrincipalUnitQuotient_nsmul_residueCharacteristic_pow_eq_zero

L206 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.discretePrincipalUnitQuotient_nsmul_residueCharacteristic_pow_eq_zero
Documentation

The exact exponent bound, stated on the canonical discrete wrapper.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
theorem discretePrincipalUnitQuotient_nsmul_residueCharacteristic_pow_eq_zero
    (F : LocalField.{u, v} K) (n : ℕ)
    (x : DiscretePrincipalUnitQuotient F.toCompleteDVF n) :
    (F.residueCharacteristic ^
        ((principalUnitResidueDegree F : ℕ) * n)) • x = 0
def

principalUnitQuotientCarrierZModModule

L219 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitQuotientCarrierZModModule
Documentation

The canonical ZMod (p^(f*n))-module on the n-th finite coordinate.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
def Internal.principalUnitQuotientCarrierZModModule
    (F : LocalField.{u, v} K) (n : ℕ) :
    Module
      (ZMod (F.residueCharacteristic ^
        ((principalUnitResidueDegree F : ℕ) * n)))
      (Additive (Internal.principalUnitQuotientCarrier F.toCompleteDVF n))
instance

principalUnitQuotientCarrierPadicModule

L232 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitQuotientCarrierPadicModule
Documentation

Restriction of scalars along Z_p -> ZMod (p^(f*n)).

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
instance Internal.principalUnitQuotientCarrierPadicModule
    (F : LocalField.{u, v} K) (n : ℕ) :
    Module ℤ_[F.residueCharacteristic]
      (Additive (Internal.principalUnitQuotientCarrier F.toCompleteDVF n))
instance

discretePrincipalUnitQuotientPadicModule

L244 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.discretePrincipalUnitQuotientPadicModule
Documentation

Equips the target in Module ℤ_[F.residueCharacteristic] (DiscretePrincipalUnitQuotient F.toCompleteDVF n) with the indicated module structure.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
instance discretePrincipalUnitQuotientPadicModule
    (F : LocalField.{u, v} K) (n : ℕ) :
    Module ℤ_[F.residueCharacteristic]
      (DiscretePrincipalUnitQuotient F.toCompleteDVF n)
theorem

addEquiv_map_smul

L258 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient.addEquiv_map_smul
Documentation

Establishes the identity DiscretePrincipalUnitQuotient.addEquiv F.toCompleteDVF n (a • x) = a • DiscretePrincipalUnitQuotient.addEquiv F.toCompleteDVF n x.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
theorem DiscretePrincipalUnitQuotient.addEquiv_map_smul
    (F : LocalField.{u, v} K) (n : ℕ)
    (a : ℤ_[F.residueCharacteristic])
    (x : DiscretePrincipalUnitQuotient F.toCompleteDVF n) :
    DiscretePrincipalUnitQuotient.addEquiv F.toCompleteDVF n (a • x) =
      a • DiscretePrincipalUnitQuotient.addEquiv F.toCompleteDVF n x
def

principalUnitQuotientCarrierPadicScalar

L268 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitQuotientCarrierPadicScalar
Documentation

The finite-coordinate scalar written explicitly through reduction of a p-adic integer modulo p^(f*n).

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
def Internal.principalUnitQuotientCarrierPadicScalar
    (F : LocalField.{u, v} K) (n : ℕ)
    (a : ℤ_[F.residueCharacteristic])
    (x : Additive (Internal.principalUnitQuotientCarrier F.toCompleteDVF n)) :
    Additive (Internal.principalUnitQuotientCarrier F.toCompleteDVF n)
theorem

principalUnitQuotientCarrierPadicScalar_eq_smul

L278 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitQuotientCarrierPadicScalar_eq_smul
Documentation

Establishes the identity principalUnitQuotientCarrierPadicScalar F n a x = a • x.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
theorem Internal.principalUnitQuotientCarrierPadicScalar_eq_smul
    (F : LocalField.{u, v} K) (n : ℕ)
    (a : ℤ_[F.residueCharacteristic])
    (x : Additive (Internal.principalUnitQuotientCarrier F.toCompleteDVF n)) :
    principalUnitQuotientCarrierPadicScalar F n a x = a • x
theorem

continuous_principalUnitQuotientCarrierPadicScalar

L287 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.continuous_principalUnitQuotientCarrierPadicScalar
Documentation

Joint continuity of the p-adic scalar action on one finite discrete coordinate.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · full declaration
theorem Internal.continuous_principalUnitQuotientCarrierPadicScalar
    (F : LocalField.{u, v} K) (n : ℕ) :
    letI : TopologicalSpace
        (Internal.principalUnitQuotientCarrier F.toCompleteDVF n) := ⊥
    Continuous fun z : ℤ_[F.residueCharacteristic] ×
        Additive (Internal.principalUnitQuotientCarrier F.toCompleteDVF n) =>
      principalUnitQuotientCarrierPadicScalar F n z.1 z.2 := by
  let p := F.residueCharacteristic
  let f : ℕ := principalUnitResidueDegree F
  let : TopologicalSpace
      (Internal.principalUnitQuotientCarrier F.toCompleteDVF n) := ⊥
  let : DiscreteTopology
      (Internal.principalUnitQuotientCarrier F.toCompleteDVF n) := ⟨rfl⟩
  let : TopologicalSpace (ZMod (p ^ (f * n))) := ⊥
  let : DiscreteTopology (ZMod (p ^ (f * n))) := ⟨rfl⟩
  let : Module (ZMod (p ^ (f * n)))
      (Additive (Internal.principalUnitQuotientCarrier F.toCompleteDVF n)) := by
    simpa [p, f] using principalUnitQuotientCarrierZModModule F n
  have hred : Continuous fun z : ℤ_[F.residueCharacteristic] ×
      Additive (Internal.principalUnitQuotientCarrier F.toCompleteDVF n) =>
      PadicInt.toZModPow (f * n) z.1 :=
    (Internal.continuous_padicIntToZModPow p (f * n)).comp continuous_fst
  have hact : Continuous fun z : ZMod (p ^ (f * n)) ×
      Additive (Internal.principalUnitQuotientCarrier F.toCompleteDVF n) =>
      z.1 • z.2 :=
    continuous_of_discreteTopology
  change Continuous fun z : ℤ_[F.residueCharacteristic] ×
      Additive (Internal.principalUnitQuotientCarrier F.toCompleteDVF n) =>
    PadicInt.toZModPow (f * n) z.1 • z.2
  exact hact.comp (hred.prodMk continuous_snd)
theorem

continuous_discretePrincipalUnitQuotientPadic_smul

L322 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.continuous_discretePrincipalUnitQuotientPadic_smul
Documentation

The specified map is continuous: Continuous fun z : ℤ_[F.residueCharacteristic] × DiscretePrincipalUnitQuotient F.toCompleteDVF n => z.1 • z.2.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · full declaration
theorem continuous_discretePrincipalUnitQuotientPadic_smul
    (F : LocalField.{u, v} K) (n : ℕ) :
    Continuous fun z : ℤ_[F.residueCharacteristic] ×
        DiscretePrincipalUnitQuotient F.toCompleteDVF n =>
      z.1 • z.2 := by
  let : TopologicalSpace
      (Additive (Internal.principalUnitQuotientCarrier F.toCompleteDVF n)) := ⊥
  let : DiscreteTopology
      (Additive (Internal.principalUnitQuotientCarrier F.toCompleteDVF n)) := ⟨rfl⟩
  let e : DiscretePrincipalUnitQuotient F.toCompleteDVF n ≃ₜ
      Additive (Internal.principalUnitQuotientCarrier F.toCompleteDVF n) :=
    { toEquiv := DiscretePrincipalUnitQuotient.equiv F.toCompleteDVF n
      continuous_toFun := continuous_of_discreteTopology
      continuous_invFun := continuous_of_discreteTopology }
  have hpair : Continuous fun z : ℤ_[F.residueCharacteristic] ×
      DiscretePrincipalUnitQuotient F.toCompleteDVF n =>
      (z.1, e z.2) :=
    continuous_fst.prodMk (e.continuous.comp continuous_snd)
  have h := e.continuous_symm.comp
    ((Internal.continuous_principalUnitQuotientCarrierPadicScalar F n).comp hpair)
  refine h.congr fun z => ?_
  apply e.injective
  simp only [Function.comp_apply, e.apply_symm_apply]
  change
    Internal.principalUnitQuotientCarrierPadicScalar F n z.1
        (DiscretePrincipalUnitQuotient.addEquiv F.toCompleteDVF n z.2) =
      DiscretePrincipalUnitQuotient.addEquiv F.toCompleteDVF n (z.1 • z.2)
  rw [Internal.principalUnitQuotientCarrierPadicScalar_eq_smul,
    DiscretePrincipalUnitQuotient.addEquiv_map_smul]
theorem

principalUnitQuotientCarrierTransitionAdd_map_smul

L355 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.Internal.principalUnitQuotientCarrierTransitionAdd_map_smul
Documentation

Reduction between finite principal-unit quotients is Z_p-linear. The key point is compatibility of toZModPow with the cast from level f*n to level f*m.

Source context 13 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
Lean source · statement
theorem Internal.principalUnitQuotientCarrierTransitionAdd_map_smul
    (F : LocalField.{u, v} K) {m n : ℕ} (hmn : m ≤ n)
    (a : ℤ_[F.residueCharacteristic])
    (x : Additive (Internal.principalUnitQuotientCarrier F.toCompleteDVF n)) :
    principalUnitQuotientCarrierTransitionAdd F.toCompleteDVF hmn (a • x) =
      a • principalUnitQuotientCarrierTransitionAdd F.toCompleteDVF hmn x
def

transitionLinear

L396 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.DiscretePrincipalUnitQuotient.transitionLinear
Documentation

Wrapped coordinate reduction is Z_p-linear.

Source context 14 commands

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

noncomputable section
open scoped BigOperators
universe u v
namespace LocalFieldTheory.DiscreteValuationField
open LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
namespace CompleteDVF
open LocalFieldTheory.DiscreteValuationField.CompleteDVF
namespace higherPrincipalUnitGroup
open LubinTate
open LubinTate.Valuations
variable {K : Type u} [Field K]
open Internal
namespace DiscretePrincipalUnitQuotient
Lean source · full declaration
def transitionLinear
    (F : LocalField.{u, v} K) {m n : ℕ} (hmn : m ≤ n) :
    DiscretePrincipalUnitQuotient F.toCompleteDVF n →ₗ[
      ℤ_[F.residueCharacteristic]]
      DiscretePrincipalUnitQuotient F.toCompleteDVF m where
  toFun := transition F.toCompleteDVF hmn
  map_add' := fun x y => (transition F.toCompleteDVF hmn).map_add x y
  map_smul' a x := by
    have hx : (a • x).val = a • x.val := by
      simpa only [addEquiv_apply] using
        addEquiv_map_smul F n a x
    have hy :
        (a • transition F.toCompleteDVF hmn x).val =
          a • (transition F.toCompleteDVF hmn x).val := by
      simpa only [addEquiv_apply] using
        addEquiv_map_smul F m a (transition F.toCompleteDVF hmn x)
    apply (addEquiv F.toCompleteDVF m).injective
    simpa only [addEquiv_apply, val_transition, RingHom.id_apply, hx, hy] using
      Internal.principalUnitQuotientCarrierTransitionAdd_map_smul
        F hmn a x.val

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.