NYLL
Module

TeichmullerLift.lean

Nyll.ValuedFieldTheory.LocalField.DiscreteValuationField.PrincipalUnits.TeichmullerLift
14 declarations indexed from sourceView source ↗

Module documentation

Teichmuller lifts

Constructs multiplicative Teichmuller representatives, and in equal characteristic the coefficient-field section of the residue map.

Imports2
Imported by3

Declarations

def

residueTeichmullerLift

L42 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueTeichmullerLift
Documentation

The Teichmuller representative lift from the finite residue field to the valuation ring: 0 lifts to 0, and nonzero residue classes lift through the root-of-unity splitting of κˣ.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
def residueTeichmullerLift [Finite F.residueField] :
    F.residueField → F.valuationSubring
theorem

residueTeichmullerLift_zero

L55 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueTeichmullerLift_zero
Documentation

Establishes the identity higherPrincipalUnitGroup.residueTeichmullerLift F 0 = 0.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem residueTeichmullerLift_zero [Finite F.residueField] :
    higherPrincipalUnitGroup.residueTeichmullerLift F 0 = 0
theorem

residueTeichmullerLift_one

L60 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueTeichmullerLift_one
Documentation

Establishes the identity higherPrincipalUnitGroup.residueTeichmullerLift F 1 = 1.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem residueTeichmullerLift_one [Finite F.residueField] :
    higherPrincipalUnitGroup.residueTeichmullerLift F 1 = 1
theorem

residueMap_residueTeichmullerLift

L77 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueMap_residueTeichmullerLift
Documentation

The Teichmuller lift reduces to the residue class it lifts.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem residueMap_residueTeichmullerLift [Finite F.residueField]
    (y : F.residueField) :
    F.residueMap (higherPrincipalUnitGroup.residueTeichmullerLift F y) = y
theorem

residueTeichmullerLift_mul

L99 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueTeichmullerLift_mul
Documentation

The Teichmuller lift is multiplicative.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem residueTeichmullerLift_mul [Finite F.residueField]
    (x y : F.residueField) :
    higherPrincipalUnitGroup.residueTeichmullerLift F (x * y) =
      higherPrincipalUnitGroup.residueTeichmullerLift F x *
        higherPrincipalUnitGroup.residueTeichmullerLift F y
theorem

residueTeichmullerLift_pow_card

L133 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueTeichmullerLift_pow_card
Documentation

Every Teichmuller representative is a root of T^q - T, where q = #κ.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem residueTeichmullerLift_pow_card [Finite F.residueField]
    (y : F.residueField) :
    higherPrincipalUnitGroup.residueTeichmullerLift F y ^
        Nat.card F.residueField =
      higherPrincipalUnitGroup.residueTeichmullerLift F y
theorem

residueTeichmullerLift_isRoot_X_pow_card_sub_X

L181 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueTeichmullerLift_isRoot_X_pow_card_sub_X
Documentation

Every residue Teichmüller lift is a root of the polynomial X^q - X, where q is the residue-field cardinality.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem residueTeichmullerLift_isRoot_X_pow_card_sub_X
    [Finite F.residueField] (y : F.residueField) :
    (Polynomial.X ^ Nat.card F.residueField - Polynomial.X :
        Polynomial F.valuationSubring).IsRoot
      (higherPrincipalUnitGroup.residueTeichmullerLift F y)
theorem

residueTeichmullerRootPolynomial_derivative_eval_isUnit_of_charP

L192 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueTeichmullerRootPolynomial_derivative_eval_isUnit_of_charP
Documentation

In equal characteristic, T^q - T has unit derivative at every Teichmuller representative.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem residueTeichmullerRootPolynomial_derivative_eval_isUnit_of_charP
    [Finite F.residueField] (p : ℕ) [Fact p.Prime]
    [CharP F.valuationSubring p] {n : ℕ+}
    (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (y : F.residueField) :
    IsUnit
      (((Polynomial.X ^ Nat.card F.residueField - Polynomial.X :
          Polynomial F.valuationSubring).derivative).eval
        (higherPrincipalUnitGroup.residueTeichmullerLift F y))
theorem

residueTeichmullerLift_add_of_charP

L219 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueTeichmullerLift_add_of_charP
Documentation

In equal characteristic, the Teichmuller lift from the finite residue field to the valuation ring is additive.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem residueTeichmullerLift_add_of_charP [Finite F.residueField]
    (p : ℕ) [Fact p.Prime] [CharP F.valuationSubring p] {n : ℕ+}
    (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (x y : F.residueField) :
    higherPrincipalUnitGroup.residueTeichmullerLift F (x + y) =
      higherPrincipalUnitGroup.residueTeichmullerLift F x +
        higherPrincipalUnitGroup.residueTeichmullerLift F y
def

residueTeichmullerRingHomOfCharP

L282 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueTeichmullerRingHomOfCharP
Documentation

In equal characteristic, the Teichmuller lift is a ring homomorphic coefficient-field section of the residue map.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · full declaration
def residueTeichmullerRingHomOfCharP
    [Finite F.residueField] (p : ℕ) [Fact p.Prime]
    [CharP F.valuationSubring p] {n : ℕ+}
    (hcard : Nat.card F.residueField = p ^ (n : ℕ)) :
    F.residueField →+* F.valuationSubring where
  toFun := higherPrincipalUnitGroup.residueTeichmullerLift F
  map_zero' := by
    exact higherPrincipalUnitGroup.residueTeichmullerLift_zero (F := F)
  map_one' := by
    exact higherPrincipalUnitGroup.residueTeichmullerLift_one (F := F)
  map_mul' := fun x y =>
    higherPrincipalUnitGroup.residueTeichmullerLift_mul (F := F) x y
  map_add' := fun x y =>
    higherPrincipalUnitGroup.residueTeichmullerLift_add_of_charP
      (F := F) p hcard x y
theorem

residueTeichmullerRingHomOfCharP_apply

L303 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueTeichmullerRingHomOfCharP_apply
Documentation

The defining evaluation formula for residueTeichmullerRingHomOfCharP is higherPrincipalUnitGroup.residueTeichmullerRingHomOfCharP (F := F) p hcard x = higherPrincipalUnitGroup.residueTeichmullerLift F x.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem residueTeichmullerRingHomOfCharP_apply
    [Finite F.residueField] (p : ℕ) [Fact p.Prime]
    [CharP F.valuationSubring p] {n : ℕ+}
    (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (x : F.residueField) :
    higherPrincipalUnitGroup.residueTeichmullerRingHomOfCharP
        (F := F) p hcard x =
      higherPrincipalUnitGroup.residueTeichmullerLift F x
theorem

residueMap_comp_residueTeichmullerRingHomOfCharP

L318 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueMap_comp_residueTeichmullerRingHomOfCharP
Documentation

Establishes the identity F.residueMap.comp (higherPrincipalUnitGroup.residueTeichmullerRingHomOfCharP (F := F) p hcard) = RingHom.id F.residueField.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem residueMap_comp_residueTeichmullerRingHomOfCharP
    [Finite F.residueField] (p : ℕ) [Fact p.Prime]
    [CharP F.valuationSubring p] {n : ℕ+}
    (hcard : Nat.card F.residueField = p ^ (n : ℕ)) :
    F.residueMap.comp
        (higherPrincipalUnitGroup.residueTeichmullerRingHomOfCharP
          (F := F) p hcard) =
      RingHom.id F.residueField
def

residueTeichmullerFieldHomOfCharP

L331 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueTeichmullerFieldHomOfCharP
Documentation

The corresponding coefficient-field embedding into the fraction field.

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
def residueTeichmullerFieldHomOfCharP
    [Finite F.residueField] (p : ℕ) [Fact p.Prime]
    [CharP F.valuationSubring p] {n : ℕ+}
    (hcard : Nat.card F.residueField = p ^ (n : ℕ)) :
    F.residueField →+* K
theorem

residueTeichmullerFieldHomOfCharP_apply

L345 ↗
LocalFieldTheory.DiscreteValuationField.CompleteDVF.higherPrincipalUnitGroup.residueTeichmullerFieldHomOfCharP_apply
Documentation

The defining evaluation formula for residueTeichmullerFieldHomOfCharP is higherPrincipalUnitGroup.residueTeichmullerFieldHomOfCharP (F := F) p hcard x = (higherPrincipalUnitGroup.residueTeichmullerLift F x : K).

Source context 11 commands

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

namespace LocalFieldTheory
open ValuationTheory
open ValuationTheory.DiscreteValuationField.ResidueField
noncomputable section
open scoped BigOperators
universe u v
namespace DiscreteValuationField
namespace CompleteDVF
variable {K : Type u} [Field K]
namespace higherPrincipalUnitGroup
variable (F : ValuationTheory.DiscreteValuationField.CompleteDVF.{u, v} K)
Lean source · statement
theorem residueTeichmullerFieldHomOfCharP_apply
    [Finite F.residueField] (p : ℕ) [Fact p.Prime]
    [CharP F.valuationSubring p] {n : ℕ+}
    (hcard : Nat.card F.residueField = p ^ (n : ℕ))
    (x : F.residueField) :
    higherPrincipalUnitGroup.residueTeichmullerFieldHomOfCharP
        (F := F) p hcard x =
      (higherPrincipalUnitGroup.residueTeichmullerLift F x : K)

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