Roots of unity of invertible order in a Henselian local ring

Reduction modulo the maximal ideal of a Henselian local ring R identifies the n-th roots of unity of R with those of its residue field, whenever n is invertible in R.

Surjectivity is Hensel's lemma applied to X ^ n - 1, whose roots are simple exactly because n is invertible.

Main results

• TauCeti.rootsOfUnityResidue_bijective and TauCeti.rootsOfUnityEquivResidueField: reduction is a bijection, and the resulting isomorphism with the roots of unity of the residue field.

References

• J.-P. Serre, Corps Locaux, Chapter II, §4.

theorem TauCeti.rootsOfUnityResidue_surjective {R : Type u_1} [CommRing R] [HenselianLocalRing R] {n : ℕ} (hn : IsUnit ↑n) : Function.Surjective ⇑(rootsOfUnityResidue n)

Every root of unity of invertible order in the residue field lifts, by Hensel's lemma applied to X ^ n - 1.

theorem TauCeti.rootsOfUnityResidue_bijective {R : Type u_1} [CommRing R] [HenselianLocalRing R] {n : ℕ} (hn : IsUnit ↑n) : Function.Bijective ⇑(rootsOfUnityResidue n)

Reduction is a bijection on roots of unity of invertible order.

noncomputable def TauCeti.rootsOfUnityEquivResidueField {R : Type u_1} [CommRing R] [HenselianLocalRing R] {n : ℕ} (hn : IsUnit ↑n) : ↥(rootsOfUnity n R) ≃* ↥(rootsOfUnity n (IsLocalRing.ResidueField R))

Roots of unity of invertible order lift uniquely along the residue map of a Henselian local ring: reduction is an isomorphism between the n-th roots of unity of R and those of its residue field.

Equations

• TauCeti.rootsOfUnityEquivResidueField hn = MulEquiv.ofBijective (TauCeti.rootsOfUnityResidue n) ⋯

@[simp]

theorem TauCeti.coe_rootsOfUnityEquivResidueField {R : Type u_1} [CommRing R] [HenselianLocalRing R] {n : ℕ} (hn : IsUnit ↑n) (ζ : ↥(rootsOfUnity n R)) : ↑↑((rootsOfUnityEquivResidueField hn) ζ) = (IsLocalRing.residue R) ↑↑ζ

The value of rootsOfUnityEquivResidueField is the reduction of the root of unity.