Roots of unity do not leave an integrally closed subring

If R is integrally closed in A, then R and A have the same n-th roots of unity for every n ≠ 0: an n-th root of unity x of A satisfies x ^ n = 1, so it is integral over R and therefore comes from R, and its inverse x ^ (n - 1) comes from R as well.

The typical use is R a valuation ring and A its fraction field, where it says that all roots of unity of the field are already units of the valuation ring.

Main results

• TauCeti.restrictRootsOfUnity_bijective: the inclusion R → A induces a bijection on n-th roots of unity.
• TauCeti.rootsOfUnityMulEquiv: the inclusion R → A restricts to an isomorphism μ_n(R) ≃* μ_n(A).

theorem TauCeti.restrictRootsOfUnity_bijective (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] [IsIntegrallyClosedIn R A] (n : ℕ) [NeZero n] : Function.Bijective ⇑(restrictRootsOfUnity (algebraMap R A) n)

If R is integrally closed in A and n ≠ 0, restricting the inclusion R → A to n-th roots of unity is a bijection: it is injective because R → A is, and surjective because an n-th root of unity of A is integral over R, hence comes from R.

noncomputable def TauCeti.rootsOfUnityMulEquiv (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] [IsIntegrallyClosedIn R A] (n : ℕ) [NeZero n] : ↥(rootsOfUnity n R) ≃* ↥(rootsOfUnity n A)

If R is integrally closed in A, the inclusion R → A identifies the n-th roots of unity of R with those of A.

Equations

• TauCeti.rootsOfUnityMulEquiv R A n = MulEquiv.ofBijective (restrictRootsOfUnity (algebraMap R A) n) ⋯

@[simp]

theorem TauCeti.coe_rootsOfUnityMulEquiv (R : Type u_1) (A : Type u_2) [CommRing R] [CommRing A] [Algebra R A] [IsIntegrallyClosedIn R A] (n : ℕ) [NeZero n] (x : ↥(rootsOfUnity n R)) : ↑↑((rootsOfUnityMulEquiv R A n) x) = (algebraMap R A) ↑↑x