Module

TorsionFiniteness.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.TorsionFiniteness

2 declarations indexed from sourceView source ↗

Module documentation

Finiteness of all roots of unity in mixed characteristic

The actual torsion-reduction kernel is a p-group. Its elements inject into the finite set of p-power roots of the original field. Finiteness of the residue-field torsion then gives finiteness of all field torsion, without assuming the valuation is Henselian or complete.

Imports4

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.TorsionReductionPrimary
Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.FinitePrimePowerRoots
Mathlib.GroupTheory.Index
Mathlib.Algebra.CharP.Reduced

Imported by3

theorem

finite_torsion_of_finite_residueTorsion_mixedChar

L27 ↗

ValuationTheory.DiscreteValuationField.DVF.finite_torsion_of_finite_residueTorsion_mixedChar

Documentation

Finite residue torsion implies finite field torsion for any mixed-characteristic discrete valuation.

Source context 2 commands

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

namespace ValuationTheory.DiscreteValuationField.DVF
universe u v

Lean source · statement

theorem finite_torsion_of_finite_residueTorsion_mixedChar
    {K : Type u} [Field K] [CharZero K] (D : DVF.{u, v} K)
    (p : ℕ) [Fact p.Prime] [CharP D.residueField p]
    [Finite (CommGroup.torsion D.residueFieldˣ)] :
    Finite (CommGroup.torsion Kˣ)

theorem

finite_torsion_of_finite_residueTorsion_charP

L52 ↗

ValuationTheory.DiscreteValuationField.DVF.finite_torsion_of_finite_residueTorsion_charP