NYLL
Module

ParameterCongruence.lean

Nyll.ClassFieldTheory.LubinTate.FiniteLevel.ParameterCongruence
5 declarations indexed from sourceView source ↗

Module documentation

Parameter congruences for standard Lubin--Tate polynomials

The standard polynomial

f_π(X) = X ^ q + π * X

depends polynomially on its parameter. Hence two parameters which become equal after applying a ring homomorphism give the same polynomial, all the same compositional iterates, and the same primitive quotient polynomial.

The final theorem records the corresponding ideal-congruence statement for evaluations. It is the algebraic input needed when comparing primitive levels attached to two sufficiently close uniformizers; it is independent of the characteristic and does not assume an equivalence between the two levels.

Imports1
Imported by2

Declarations

theorem

standardLubinTatePolynomial_map_eq_of_parameter_eq

L43 ↗
LubinTate.standardLubinTatePolynomial_map_eq_of_parameter_eq
Documentation

Equal images of two parameters give equal images of their standard Lubin--Tate polynomials.

Source context 6 commands

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

noncomputable section
open scoped Polynomial
universe u v w
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTatePolynomial_map_eq_of_parameter_eq
    (F : LocalField.{u, v} K)
    {R : Type w} [CommRing R]
    (f : F.valuationSubring →+* R)
    {π ϖ : F.valuationSubring} (h : f π = f ϖ) :
    (standardLubinTatePolynomial F π).map f =
      (standardLubinTatePolynomial F ϖ).map f
theorem

standardLubinTatePolynomialIterate_map_eq_of_parameter_eq

L54 ↗
LubinTate.standardLubinTatePolynomialIterate_map_eq_of_parameter_eq
Documentation

Equal images of two parameters give equal images of every compositional iterate of the corresponding standard polynomials.

Source context 6 commands

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

noncomputable section
open scoped Polynomial
universe u v w
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTatePolynomialIterate_map_eq_of_parameter_eq
    (F : LocalField.{u, v} K)
    {R : Type w} [CommRing R]
    (f : F.valuationSubring →+* R)
    {π ϖ : F.valuationSubring} (h : f π = f ϖ) (n : ℕ) :
    (standardLubinTatePolynomialIterate F π n).map f =
      (standardLubinTatePolynomialIterate F ϖ n).map f
theorem

standardLubinTatePrimitivePolynomial_map_eq_of_parameter_eq

L72 ↗
LubinTate.standardLubinTatePrimitivePolynomial_map_eq_of_parameter_eq
Documentation

Equal images of two parameters give equal images of their primitive quotient polynomials at every finite level.

Source context 6 commands

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

noncomputable section
open scoped Polynomial
universe u v w
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTatePrimitivePolynomial_map_eq_of_parameter_eq
    (F : LocalField.{u, v} K)
    {R : Type w} [CommRing R]
    (f : F.valuationSubring →+* R)
    {π ϖ : F.valuationSubring} (h : f π = f ϖ) (n : ℕ) :
    (standardLubinTatePrimitivePolynomial F π n).map f =
      (standardLubinTatePrimitivePolynomial F ϖ n).map f
theorem

standardLubinTatePrimitivePolynomial_eval₂_eq_of_parameter_eq

L85 ↗
LubinTate.standardLubinTatePrimitivePolynomial_eval₂_eq_of_parameter_eq
Documentation

Equal parameter images make the two primitive polynomials have equal evaluations at every point of the target ring.

Source context 6 commands

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

noncomputable section
open scoped Polynomial
universe u v w
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTatePrimitivePolynomial_eval₂_eq_of_parameter_eq
    (F : LocalField.{u, v} K)
    {R : Type w} [CommRing R]
    (f : F.valuationSubring →+* R)
    {π ϖ : F.valuationSubring} (h : f π = f ϖ)
    (n : ℕ) (x : R) :
    Polynomial.eval₂ f x
        (standardLubinTatePrimitivePolynomial F π n) =
      Polynomial.eval₂ f x
        (standardLubinTatePrimitivePolynomial F ϖ n)
theorem

standardLubinTatePrimitivePolynomial_eval₂_sub_mem_of_parameter_sub_mem

L104 ↗
LubinTate.standardLubinTatePrimitivePolynomial_eval₂_sub_mem_of_parameter_sub_mem
Documentation

If two parameters are congruent modulo an ideal after mapping into a commutative ring, then the evaluations of their primitive quotient polynomials at the same point are congruent modulo that ideal.

Source context 6 commands

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

noncomputable section
open scoped Polynomial
universe u v w
namespace LubinTate
open LocalFieldTheory.DiscreteValuationField
variable {K : Type u} [Field K]
Lean source · statement
theorem standardLubinTatePrimitivePolynomial_eval₂_sub_mem_of_parameter_sub_mem
    (F : LocalField.{u, v} K)
    {R : Type w} [CommRing R]
    (f : F.valuationSubring →+* R) (I : Ideal R)
    {π ϖ : F.valuationSubring} (h : f π - f ϖ ∈ I)
    (n : ℕ) (x : R) :
    Polynomial.eval₂ f x
          (standardLubinTatePrimitivePolynomial F π n) -
        Polynomial.eval₂ f x
          (standardLubinTatePrimitivePolynomial F ϖ n) ∈ I

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