Roots of unity in a local ring and its residue field

Reduction modulo the maximal ideal maps the roots of unity of a local ring to those of its residue field. This map is injective when the order is invertible in the ring.

Main results

• TauCeti.rootsOfUnityResidue: the reduction homomorphism on roots of unity.
• TauCeti.rootsOfUnityResidue_injective: reduction is injective on roots of unity of invertible order.
• TauCeti.eq_of_residue_eq_of_pow_eq_one, IsPrimitiveRoot.map_residue: the same statement for elements of the ring, and its consequence that reduction preserves primitive roots of unity of invertible order.
• TauCeti.aeval_minpoly_eq_zero_of_aeval_residue_eq_zero: a root of unity of invertible order whose residue is a root of the minimal polynomial of an integral root of unity is itself a root of that minimal polynomial.

def TauCeti.rootsOfUnityResidue {R : Type u_1} [CommRing R] [IsLocalRing R] (n : ℕ) : ↥(rootsOfUnity n R) →* ↥(rootsOfUnity n (IsLocalRing.ResidueField R))

Reduction modulo the maximal ideal, as a homomorphism between the groups of n-th roots of unity of a local ring and of its residue field.

Equations

• TauCeti.rootsOfUnityResidue n = restrictRootsOfUnity (IsLocalRing.residue R) n

@[simp]

theorem TauCeti.coe_rootsOfUnityResidue {R : Type u_1} [CommRing R] [IsLocalRing R] (n : ℕ) (ζ : ↥(rootsOfUnity n R)) : ↑↑((rootsOfUnityResidue n) ζ) = (IsLocalRing.residue R) ↑↑ζ

The value of the reduction homomorphism on roots of unity.

theorem TauCeti.rootsOfUnityResidue_injective {R : Type u_1} [CommRing R] [IsLocalRing R] {n : ℕ} (hn : IsUnit ↑n) : Function.Injective ⇑(rootsOfUnityResidue n)

Distinct roots of unity of invertible order have distinct reductions.

theorem TauCeti.eq_of_residue_eq_of_pow_eq_one {R : Type u_1} [CommRing R] [IsLocalRing R] {n : ℕ} (hn : IsUnit ↑n) {x y : R} (hx : x ^ n = 1) (hy : y ^ n = 1) (h : (IsLocalRing.residue R) x = (IsLocalRing.residue R) y) : x = y

Two n-th roots of unity with the same residue are equal, when n is invertible.

theorem TauCeti.aeval_minpoly_eq_zero_of_aeval_residue_eq_zero {R : Type u_1} [CommRing R] [IsLocalRing R] {A : Type u_2} {S : Type u_3} [CommRing A] [IsDomain A] [IsIntegrallyClosed A] [CommRing S] [IsDomain S] [Algebra A S] [Module.IsTorsionFree A S] [IsDomain R] [Algebra A R] {n : ℕ} (hn : IsUnit ↑n) {ζ : S} (hζA : IsIntegral A ζ) (hζ : ζ ^ n = 1) {ξ : R} (hξ : ξ ^ n = 1) (hres : (Polynomial.aeval ((IsLocalRing.residue R) ξ)) (minpoly A ζ) = 0) : (Polynomial.aeval ξ) (minpoly A ζ) = 0

Let A be an integrally closed domain, let ζ be an n-th root of unity of a domain S over A such that ζ is integral over A, and let R be a local domain over A in which n is invertible. An n-th root of unity ξ of R whose residue is a root of the minimal polynomial of ζ over A is itself a root of that minimal polynomial.

theorem IsPrimitiveRoot.map_residue {R : Type u_1} [CommRing R] [IsLocalRing R] {n : ℕ} (hn : IsUnit ↑n) {ζ : R} (hζ : IsPrimitiveRoot ζ n) : IsPrimitiveRoot ((IsLocalRing.residue R) ζ) n

Reduction preserves primitive roots of unity of invertible order.