Module

TorsionReductionPrimary.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.TorsionReductionPrimary

1 declaration indexed from sourceView source ↗

Module documentation

The actual torsion-reduction kernel is primary for the residue prime

Factor a finite annihilating exponent as p^a times an integer prime to p. A kernel element is an actual principal unit. Its p^a-th power is killed by the prime-to-p factor, hence is one by the geometric-sum argument. This needs neither Henselianity nor characteristic zero of the field.

Imports5

Nyll.ValuedFieldTheory.Valuation.PrincipalUnitTorsion
Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.HenselianTorsionRoots
Mathlib.Data.Nat.Factorization.Basic
Mathlib.Algebra.CharP.Defs
Mathlib.GroupTheory.PGroup

Imported by2

theorem

torsionReduction_ker_isPGroup

L30 ↗

ValuationTheory.DiscreteValuationField.DVF.torsionReduction_ker_isPGroup

Documentation

The kernel of the canonical reduction map on all roots of unity is a p-group in residue characteristic p, for an arbitrary discrete valuation field.

Source context 3 commands

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

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

Lean source · statement

theorem torsionReduction_ker_isPGroup (D : DVF.{u, v} K)
    (p : ℕ) [Fact p.Prime] [CharP D.residueField p] :
    IsPGroup p D.torsionReduction.ker

Module documentation

The actual torsion-reduction kernel is primary for the residue prime

Declarations

torsionReduction_ker_isPGroup