The inclusion μ_n ↪ 𝔾ₘ on points

The group scheme of nth roots of unity μ_n = D(ℤ/n) is a closed subgroup of the multiplicative group 𝔾ₘ = D(ℤ). For positive n this is the usual finite μ_n; the declarations below are polymorphic in n : ℕ and also cover the degenerate case n = 0, where ℤ/0 = ℤ and μ_0 = 𝔾ₘ. On the diagonalizable side the inclusion is contravariant to the quotient homomorphism ℤ ↠ ℤ/n: writing that quotient multiplicatively as φ : Multiplicative ℤ →* Multiplicative (ZMod n), the diagonalizable functor sends it to a homomorphism of group functors D(φ) : D(ℤ/n) → D(ℤ), i.e. μ_n → 𝔾ₘ, given on points by precomposition with the surjection R[Multiplicative ℤ] ↠ R[Multiplicative (ZMod n)] of coordinate Hopf algebras.

This file records that this points homomorphism is, under the two worked-example identifications, exactly the inclusion of nth roots of unity into the unit group: reading the image μ_n(A) → 𝔾ₘ(A) on the group-algebra generator Multiplicative.ofAdd 1 of 𝔾ₘ returns the underlying unit of the root of unity. The same statement holds against the canonical Laurent-polynomial 𝔾ₘ of TauCeti.MultiplicativeGroup, and the inclusion is injective (a monomorphism of functors) and natural in the value algebra.

Main definitions

• TauCeti.RootsOfUnityGroup.toMultiplicativeZMod: the quotient homomorphism ℤ ↠ ℤ/n written multiplicatively, Multiplicative ℤ →* Multiplicative (ZMod n).
• TauCeti.RootsOfUnityGroup.inclusion: the inclusion μ_n ↪ 𝔾ₘ on points, the contravariant image of toMultiplicativeZMod n under the diagonalizable functor.

Main results

• TauCeti.RootsOfUnityGroup.charOfPoint_inclusion: reading the character of an included point is the μ_n character precomposed with the quotient ℤ ↠ ℤ/n.
• TauCeti.RootsOfUnityGroup.charOfPoint_inclusion_ofAdd_one: reading the included point on the 𝔾ₘ generator Multiplicative.ofAdd 1 returns the underlying unit of the root of unity.
• TauCeti.RootsOfUnityGroup.multiplicativeGroup_pointEquiv_inclusion: the same identification against the canonical Laurent-polynomial 𝔾ₘ of TauCeti.MultiplicativeGroup.
• TauCeti.RootsOfUnityGroup.inclusion_injective: the inclusion is injective on points, so μ_n → 𝔾ₘ is a monomorphism of group functors.
• TauCeti.RootsOfUnityGroup.mapValue_inclusion: the inclusion is natural in the value algebra.

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 and 𝔾ₘ worked examples through the diagonalizable-group functoriality DiagonalizableGroup.pointsMap.

References

The contravariant functoriality of the diagonalizable group is Tau Ceti's TauCeti.DiagonalizableGroup.pointsMap; the μ_n and 𝔾ₘ points calculations are TauCeti.RootsOfUnityGroup.pointsMulEquiv and TauCeti.MultiplicativeGroup.pointEquiv. The multiplicative quotient ℤ ↠ ℤ/n uses Mathlib's AddMonoidHom.toMultiplicative and Int.castAddHom.

noncomputable def TauCeti.RootsOfUnityGroup.toMultiplicativeZMod (n : ℕ) : Multiplicative ℤ →* Multiplicative (ZMod n)

The quotient homomorphism ℤ ↠ ℤ/n, written multiplicatively as a homomorphism Multiplicative ℤ →* Multiplicative (ZMod n). Its diagonalizable image is the inclusion μ_n ↪ 𝔾ₘ.

Equations

• TauCeti.RootsOfUnityGroup.toMultiplicativeZMod n = AddMonoidHom.toMultiplicative (Int.castAddHom (ZMod n))

@[simp]

theorem TauCeti.RootsOfUnityGroup.toMultiplicativeZMod_ofAdd (n : ℕ) (k : ℤ) : (toMultiplicativeZMod n) (Multiplicative.ofAdd k) = Multiplicative.ofAdd ↑k

The multiplicative quotient sends ofAdd k to ofAdd (k : ℤ/n).

theorem TauCeti.RootsOfUnityGroup.toMultiplicativeZMod_ofAdd_one (n : ℕ) : (toMultiplicativeZMod n) (Multiplicative.ofAdd 1) = generator n

The multiplicative quotient sends the 𝔾ₘ generator Multiplicative.ofAdd 1 to the μ_n generator Multiplicative.ofAdd 1. This is not a simp lemma: simp already reduces the left-hand side to generator n via toMultiplicativeZMod_ofAdd and Int.cast_one.

noncomputable def TauCeti.RootsOfUnityGroup.inclusion {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (n : ℕ) : WithConv (MonoidAlgebra R (Multiplicative (ZMod n)) →ₐ[R] A) →* WithConv (MonoidAlgebra R (Multiplicative ℤ) →ₐ[R] A)

The inclusion μ_n ↪ 𝔾ₘ on points. It is the contravariant image of the quotient ℤ ↠ ℤ/n under the diagonalizable functor: precomposition with the surjection R[Multiplicative ℤ] ↠ R[Multiplicative (ZMod n)] of coordinate Hopf algebras carries a point of μ_n = D(ℤ/n) to a point of 𝔾ₘ = D(ℤ).

Equations

• TauCeti.RootsOfUnityGroup.inclusion n = TauCeti.DiagonalizableGroup.pointsMap (TauCeti.RootsOfUnityGroup.toMultiplicativeZMod n)

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

The inclusion acts by precomposition with the diagonalizable image of the quotient.

theorem TauCeti.RootsOfUnityGroup.charOfPoint_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.charOfPoint ((inclusion n) f).ofConv = (DiagonalizableGroup.charOfPoint f.ofConv).comp (toMultiplicativeZMod n)

Reading the character of an included point. The character of inclusion n f, a point of 𝔾ₘ, is the μ_n character of f precomposed with the quotient ℤ ↠ ℤ/n.

This is the general reduction; it is not a simp lemma because it would rewrite the left-hand side of the terminal evaluation lemma charOfPoint_inclusion_ofAdd_one, which is the useful simp normal form.

@[simp]

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

The inclusion is the inclusion of roots of unity. Reading the included point inclusion n f, a point of 𝔾ₘ, on the 𝔾ₘ group-algebra generator Multiplicative.ofAdd 1 returns the underlying unit of the root of unity RootsOfUnityGroup.pointsMulEquiv n f.

@[simp]

theorem TauCeti.RootsOfUnityGroup.multiplicativeGroup_pointEquiv_inclusion {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (n : ℕ) (f : WithConv (MonoidAlgebra R (Multiplicative (ZMod n)) →ₐ[R] A)) : (Units.map ↑((inclusion n) f).ofConv) (MultiplicativeGroup.unitOfPoint ↑(AddMonoidAlgebra.toMultiplicativeAlgEquiv R R ℤ)) = ↑((pointsMulEquiv n) f)

The same identification against the canonical Laurent-polynomial 𝔾ₘ of TauCeti.MultiplicativeGroup: pushing the included point along AddMonoidAlgebra.toMultiplicativeAlgEquiv and reading it with MultiplicativeGroup.pointEquiv returns the underlying unit of the root of unity.

theorem TauCeti.RootsOfUnityGroup.toMultiplicativeZMod_surjective (n : ℕ) : Function.Surjective ⇑(toMultiplicativeZMod n)

The multiplicative quotient ℤ ↠ ℤ/n is surjective.

theorem TauCeti.RootsOfUnityGroup.inclusion_injective {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] (n : ℕ) : Function.Injective ⇑(inclusion n)

The inclusion is a monomorphism of functors. The quotient ℤ ↠ ℤ/n is surjective, so precomposing characters with it is injective; since a point is determined by its character, the induced points homomorphism μ_n(A) → 𝔾ₘ(A) is injective.

theorem TauCeti.RootsOfUnityGroup.mapValue_inclusion {R : Type u} {A : Type v} [CommSemiring R] [CommSemiring A] [Algebra R A] {B : Type u_1} [CommSemiring B] [Algebra R B] (n : ℕ) (φ : A →ₐ[R] B) : (inclusion n).comp (AlgHom.mapValue φ) = (AlgHom.mapValue φ).comp (inclusion n)

Naturality in the value algebra. The inclusion μ_n → 𝔾ₘ commutes with the value-algebra functoriality AlgHom.mapValue.