Module

RootsOfUnity.lean

Nyll.ValuedFieldTheory.Valuation.Henselian.RootsOfUnity

3 declarations indexed from sourceView source ↗

Module documentation

Roots of unity in valuation rings

Reduction on roots of unity of order invertible in the residue field is injective and, for a Henselian valuation ring, surjective. Roots of nonzero order in the field also belong to the valuation ring.

Imports4

Mathlib.RingTheory.Valuation.ValuationSubring
Mathlib.RingTheory.Henselian
Mathlib.RingTheory.RootsOfUnity.Basic
Mathlib.Algebra.Order.GroupWithZero.Basic

Imported by3

theorem

rootsOfUnityReduction_injective

L26 ↗

ValuationSubring.rootsOfUnityReduction_injective

Documentation

Reduction is injective on roots with order invertible in the residue field.

Source context 2 commands

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

namespace ValuationSubring
variable {K : Type*} [Field K] (A : ValuationSubring K)

Lean source · statement

theorem rootsOfUnityReduction_injective
    (n : ℕ) [NeZero (n : IsLocalRing.ResidueField A)] :
    Function.Injective (restrictRootsOfUnity (IsLocalRing.residue A) n)

theorem

rootsOfUnityReduction_surjective

L51 ↗

ValuationSubring.rootsOfUnityReduction_surjective

Documentation

Hensel's lemma lifts every prime-to-residue-characteristic root of unity.

Source context 2 commands

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

namespace ValuationSubring
variable {K : Type*} [Field K] (A : ValuationSubring K)

Lean source · statement

theorem rootsOfUnityReduction_surjective
    [HenselianRing A (IsLocalRing.maximalIdeal A)]
    (n : ℕ) [NeZero (n : IsLocalRing.ResidueField A)] :
    Function.Surjective (restrictRootsOfUnity (IsLocalRing.residue A) n)

theorem

rootsOfUnity_toField_bijective

L89 ↗

ValuationSubring.rootsOfUnity_toField_bijective

Documentation

All field roots of nonzero order belong to a valuation ring.

Source context 2 commands

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

namespace ValuationSubring
variable {K : Type*} [Field K] (A : ValuationSubring K)

Lean source · statement

theorem rootsOfUnity_toField_bijective (n : ℕ) [NeZero n] :
    Function.Bijective (restrictRootsOfUnity (algebraMap A K) n)

Module documentation

Roots of unity in valuation rings

Declarations

rootsOfUnityReduction_injective

rootsOfUnityReduction_surjective

rootsOfUnity_toField_bijective