Module

HenselianTorsionRoots.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.HenselianTorsionRoots

4 declarations indexed from sourceView source ↗

Module documentation

Reduction of all torsion roots in residue characteristic zero

The map on all roots of unity is the restriction of the actual residue map on valuation-ring units. It is independent of any chosen exponent. Hensel uniqueness makes this map injective when the residue field has characteristic zero, so finiteness of residue-field torsion implies finiteness of field torsion.

Imports6

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.HenselianRootsOfUnity
Mathlib.GroupTheory.Torsion
Mathlib.RingTheory.Valuation.ValuationSubring
Mathlib.Algebra.Group.Subgroup.Ker
Mathlib.Algebra.Order.GroupWithZero.Basic
Mathlib.Data.Fintype.EquivFin

Imported by4

theorem

torsion_le_unitGroup

L33 ↗

ValuationTheory.DiscreteValuationField.DVF.torsion_le_unitGroup

Source context 5 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField
universe u v
variable {K : Type u} [Field K]
namespace DVF

Lean source · statement

theorem torsion_le_unitGroup (D : DVF.{u, v} K) :
    CommGroup.torsion Kˣ ≤ D.valuation.valuationSubring.unitGroup

def

torsionReduction

L47 ↗

ValuationTheory.DiscreteValuationField.DVF.torsionReduction

Documentation

A single reduction homomorphism on all torsion roots. Its underlying map is the canonical residue map on the valuation-ring unit represented by a root.

Source context 5 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField
universe u v
variable {K : Type u} [Field K]
namespace DVF

Lean source · statement

def torsionReduction (D : DVF.{u, v} K) :
    CommGroup.torsion Kˣ →* CommGroup.torsion D.residueFieldˣ

theorem

torsionReduction_injective

L64 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.torsionReduction_injective

Documentation

In residue characteristic zero the actual reduction map is injective on all torsion roots simultaneously.

Source context 6 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField
universe u v
variable {K : Type u} [Field K]
namespace HenselianDVF
variable (F : HenselianDVF.{u, v} K)

Lean source · statement

theorem torsionReduction_injective [CharZero F.residueField] :
    Function.Injective F.toDVF.torsionReduction

theorem

finite_torsion_of_finite_residueTorsion

L98 ↗

ValuationTheory.DiscreteValuationField.HenselianDVF.finite_torsion_of_finite_residueTorsion

Documentation

Finiteness of all residue-field roots of unity transfers to the base field for a Henselian DVF of residue characteristic zero.

Source context 6 commands

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

noncomputable section
namespace ValuationTheory.DiscreteValuationField
universe u v
variable {K : Type u} [Field K]
namespace HenselianDVF
variable (F : HenselianDVF.{u, v} K)

Lean source · statement

theorem finite_torsion_of_finite_residueTorsion [CharZero F.residueField]
    [Finite (CommGroup.torsion F.residueFieldˣ)] :
    Finite (CommGroup.torsion Kˣ)

Module documentation

Reduction of all torsion roots in residue characteristic zero

Declarations

torsion_le_unitGroup

torsionReduction

torsionReduction_injective

finite_torsion_of_finite_residueTorsion