NYLL
Module

Core.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnitPadicAction.Core
4 declarations indexed from sourceView source ↗

Module documentation

Assembles the inverse-limit and topological models used to define the ℤ_[p]-module structure on principal units.

Imports8
Imported by3

Declarations

theorem

principalUnitPadic_natCast_smul

L43 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitPadic_natCast_smul
Documentation

Natural p-adic scalars act by the ordinary group powers.

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 principalUnitPadic_natCast_smul
    (F : LocalField.{u, v} K) (n : ℕ)
    (x : (LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
      F.toCompleteDVF) 1) :
    (n : ℤ_[F.residueCharacteristic]) • Additive.ofMul x =
      Additive.ofMul (x ^ n)
theorem

principalUnitPadic_nsmul_eq_pow

L57 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitPadic_nsmul_eq_pow
Documentation

Equivalent multiplicative reading of principalUnitPadic_natCast_smul.

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 principalUnitPadic_nsmul_eq_pow
    (F : LocalField.{u, v} K) (n : ℕ)
    (x : (LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup
      F.toCompleteDVF) 1) :
    Additive.toMul
        ((n : ℤ_[F.residueCharacteristic]) • Additive.ofMul x) = x ^ n
theorem

principalUnitPadic_smul_mem_higher

L71 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitPadic_smul_mem_higher
Documentation

Every U^r, for r >= 1, is stable under the canonical p-adic action on U^1.

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
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · statement
theorem principalUnitPadic_smul_mem_higher
    (F : LocalField.{u, v} K) {r : ℕ} (hr : 1 ≤ r)
    (a : ℤ_[F.residueCharacteristic])
    (x : (higherPrincipalUnitGroup F.toCompleteDVF) 1)
    (hx : (x : F.valuationSubringˣ) ∈
      (higherPrincipalUnitGroup F.toCompleteDVF) r) :
    ((Additive.toMul (a • Additive.ofMul x) :
        (higherPrincipalUnitGroup F.toCompleteDVF) 1) :
      F.valuationSubringˣ) ∈
        (higherPrincipalUnitGroup F.toCompleteDVF) r
theorem

principalUnitPadic_residueCharacteristic_mul_smul_mem_succ

L147 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.principalUnitPadic_residueCharacteristic_mul_smul_mem_succ
Documentation

A p-adic scalar divisible by the residue characteristic kills the leading graded class: on U^r it lands in U^(r+1).

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
open _root_.LocalFieldTheory.DiscreteValuationField.CompleteDVF (
  higherPrincipalUnitGroup
) in
Lean source · statement
theorem principalUnitPadic_residueCharacteristic_mul_smul_mem_succ
    (F : LocalField.{u, v} K) {r : ℕ} (hr : 1 ≤ r)
    (b : ℤ_[F.residueCharacteristic])
    (x : (higherPrincipalUnitGroup F.toCompleteDVF) 1)
    (hx : (x : F.valuationSubringˣ) ∈
      (higherPrincipalUnitGroup F.toCompleteDVF) r) :
    ((Additive.toMul
        (((F.residueCharacteristic : ℤ_[F.residueCharacteristic]) * b) •
          Additive.ofMul x) :
        (higherPrincipalUnitGroup F.toCompleteDVF) 1) :
      F.valuationSubringˣ) ∈
        (higherPrincipalUnitGroup F.toCompleteDVF) (r + 1)

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