μ_n is the kernel of the nth power endomorphism of 𝔾ₘ

The group scheme of nth roots of unity μ_n = D(ℤ/n) sits inside the multiplicative group 𝔾ₘ = D(ℤ) through the inclusion TauCeti.RootsOfUnityGroup.inclusion, the contravariant image of the quotient ℤ ↠ ℤ/n. On the other side, TauCeti.DiagonalizableGroup.powEnd n is the nth power endomorphism u ↦ u ^ n of 𝔾ₘ. This file identifies μ_n with the kernel of that endomorphism: on every commutative R-algebra A, the image of μ_n(A) → 𝔾ₘ(A) is exactly the set of points killed by the nth power, so μ_n is the (scheme-theoretic) kernel ker(𝔾ₘ --u ↦ uⁿ--> 𝔾ₘ).

The mechanism is the worked-example points dictionary. A point of 𝔾ₘ = D(Multiplicative ℤ) is determined by the unit it reads off on the generator Multiplicative.ofAdd 1 (DiagonalizableGroup.pointsMulEquiv_ext). The nth power endomorphism raises that unit to the nth power (DiagonalizableGroup.pointsMulEquiv_powEnd), while an included μ_n-point reads off the underlying unit of an nth root of unity (RootsOfUnityGroup.charOfPoint_inclusion_ofAdd_one), whose nth power is 1. Conversely a 𝔾ₘ-point read off as a unit u with u ^ n = 1 is u ∈ rootsOfUnity n A, hence the image of the μ_n-point attached to it.

This is a worked-example check for the reductive-groups roadmap (ReductiveGroups/README.md in TauCetiRoadmap, Layer 4: "μ_n = D(ℤ/n)", "𝔾_m = D(ℤ)", and the diagonalizable anti-equivalence M ↦ D(M)), assembling the μ_n inclusion TauCeti.RootsOfUnityGroup.inclusion and the power endomorphism TauCeti.DiagonalizableGroup.powEnd of the character/cocharacter file into the classical description of μ_n as a kernel.

Main results

• TauCeti.RootsOfUnityGroup.powEnd_comp_inclusion: the nth power endomorphism annihilates μ_n, i.e. powEnd n ∘ inclusion n is trivial.
• TauCeti.RootsOfUnityGroup.mem_range_inclusion_iff: a 𝔾ₘ-point lies in the image of the μ_n inclusion iff the nth power endomorphism kills it.
• TauCeti.RootsOfUnityGroup.range_inclusion: as subgroups of the 𝔾ₘ-points, the image of μ_n ↪ 𝔾ₘ is the kernel of the nth power endomorphism of 𝔾ₘ.

References

The μ_n inclusion and 𝔾ₘ points calculation are Tau Ceti's TauCeti.RootsOfUnityGroup.inclusion and TauCeti.RootsOfUnityGroup.pointsMulEquiv; the power endomorphism of 𝔾ₘ is TauCeti.DiagonalizableGroup.powEnd. The subgroup of nth roots of unity and mem_rootsOfUnity are Mathlib's (Mathlib.RingTheory.RootsOfUnity.Basic), and the one-generator extensionality MonoidHom.ext_mint is from Mathlib.Data.Int.Cast.Lemmas.

theorem TauCeti.RootsOfUnityGroup.powEnd_comp_inclusion {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (n : ℕ) : (DiagonalizableGroup.powEnd ↑n).comp (inclusion n) = 1

The nth power endomorphism of 𝔾ₘ annihilates μ_n. Composing the power endomorphism DiagonalizableGroup.powEnd n after the inclusion μ_n ↪ 𝔾ₘ is the trivial homomorphism of group functors: every μ_n-point maps to a root of unity, whose nth power is 1.

theorem TauCeti.RootsOfUnityGroup.powEnd_inclusion {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (n : ℕ) (f : WithConv (MonoidAlgebra R (Multiplicative (ZMod n)) →ₐ[R] A)) : (DiagonalizableGroup.powEnd ↑n) ((inclusion n) f) = 1

The nth power endomorphism annihilates every μ_n-point, in element form. This is not a simp lemma: when the power-endomorphism API is also imported, DiagonalizableGroup.powEnd_apply rewrites the left-hand side to inclusion n f ^ n, so the statement below is never in simp-normal form in that import context.

theorem TauCeti.RootsOfUnityGroup.mem_range_inclusion_iff {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (n : ℕ) {g : WithConv (MonoidAlgebra R (Multiplicative ℤ) →ₐ[R] A)} : g ∈ (inclusion n).range ↔ (DiagonalizableGroup.powEnd ↑n) g = 1

Membership in the image of μ_n ↪ 𝔾ₘ. A 𝔾ₘ-point lies in the image of the μ_n inclusion exactly when the nth power endomorphism kills it: g comes from μ_n iff gⁿ = 1.

theorem TauCeti.RootsOfUnityGroup.range_inclusion {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (n : ℕ) : (inclusion n).range = (DiagonalizableGroup.powEnd ↑n).ker

μ_n is the kernel of the nth power endomorphism of 𝔾ₘ. As subgroups of the group of 𝔾ₘ-points, the image of the inclusion μ_n ↪ 𝔾ₘ equals the kernel of the nth power endomorphism DiagonalizableGroup.powEnd n: a 𝔾ₘ-point comes from μ_n exactly when its nth power is trivial. This realizes μ_n = ker(𝔾ₘ --u ↦ uⁿ--> 𝔾ₘ) on the functor of points.