The roots-of-unity group scheme

For a commutative ring R and a natural number n, the roots-of-unity group scheme is the diagonalizable group

mu_n = D(ULift (Multiplicative (ZMod n))).

The universe lift places the character group in the universe of R, as required by the current scheme-level diagonalizable-group API. This file synchronizes that presentation with the existing group-algebra and functor-of-points presentations:

• scheme-valued points of mu_n are the subgroup rootsOfUnity n A of the units of a value algebra A;
• the quotient of lifted character groups induced by Z -> Z/n gives a group-scheme morphism mu_n -> G_m whose action on points is the usual inclusion of roots of unity into units;
• this morphism is a closed immersion, since its coordinate map is the surjective group-algebra map induced by the quotient of character groups.

All statements include n = 0, n = 1, and the zero base and value rings. The classical quotient presentation by T ^ n - 1 and the realization as the kernel of the power map are separate constructions.

This advances Layer 4 and the worked-examples lane of the reductive-groups roadmap by keeping the Hopf-algebra, group-scheme, and functor-of-points descriptions of mu_n synchronized.

Main declarations

• TauCeti.RootsOfUnityGroup.characterGroup: the same-universe character group of mu_n.
• TauCeti.RootsOfUnityGroup.groupScheme: mu_n as a diagonalizable group scheme.
• TauCeti.RootsOfUnityGroup.schemePointsMulEquiv: scheme-valued points are nth roots of unity.
• TauCeti.RootsOfUnityGroup.characterQuotient: the lifted quotient of character groups defining mu_n -> G_m contravariantly.
• TauCeti.RootsOfUnityGroup.inclusionGroupSchemeMap: the group-scheme inclusion mu_n -> G_m.
• TauCeti.RootsOfUnityGroup.isClosedImmersion_inclusionGroupSchemeMap: the inclusion is a closed immersion.

References

Milne, Algebraic Groups, Definition 12.7 and Theorems 12.8--12.9, describes the contravariant construction D(M) and its behavior on quotients of character groups.

instance TauCeti.RootsOfUnityGroup.instFGMultiplicativeZMod (n : ℕ) : Group.FG (Multiplicative (ZMod n))

The cyclic character group Multiplicative (ZMod n) is finitely generated for every n, including n = 0, as a quotient of Multiplicative Z.

@[reducible, inline]

noncomputable abbrev TauCeti.RootsOfUnityGroup.characterGroup (n : ℕ) : FGCommGrpCat

The character group defining mu_n, lifted into the universe of the base ring.

Equations

• TauCeti.RootsOfUnityGroup.characterGroup n = TauCeti.FGCommGrpCat.of (ULift.{?u.1, 0} (Multiplicative (ZMod n)))

@[reducible, inline]

noncomputable abbrev TauCeti.RootsOfUnityGroup.groupScheme (R : Type u) [CommRing R] (n : ℕ) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))

The roots-of-unity group scheme mu_n = D(ULift (Multiplicative (ZMod n))) over Spec R.

Equations

• TauCeti.RootsOfUnityGroup.groupScheme R n = TauCeti.DiagonalizableGroup.groupScheme R (TauCeti.RootsOfUnityGroup.characterGroup n)

noncomputable def TauCeti.RootsOfUnityGroup.schemePointsMulEquiv {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (n : ℕ) : ((AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R n).X) ≃* ↥(rootsOfUnity n A)

Scheme-valued points of mu_n over Spec R are the nth roots of unity in the value algebra.

The corresponding root of unity is obtained by evaluating the character at the lifted standard generator of Multiplicative (ZMod n).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.RootsOfUnityGroup.schemePointsMulEquiv_apply_coe {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (n : ℕ) (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R n).X) : ↑↑((schemePointsMulEquiv n) p) = ((DiagonalizableGroup.groupSchemePointsMulEquiv (characterGroup n)) p).ofConv (MonoidAlgebra.single { down := generator n } 1)

A scheme-valued point of mu_n, viewed as a root of unity, is obtained by evaluating its coordinate-algebra point on the lifted standard generator.

theorem TauCeti.RootsOfUnityGroup.schemePointsMulEquiv_symm_apply_single_generator {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (n : ℕ) (ζ : ↥(rootsOfUnity n A)) : ((DiagonalizableGroup.groupSchemePointsMulEquiv (characterGroup n)) ((schemePointsMulEquiv n).symm ζ)).ofConv (MonoidAlgebra.single { down := generator n } 1) = ↑↑ζ

The scheme point associated to a root of unity evaluates the lifted standard generator at that root.

@[simp]

theorem TauCeti.RootsOfUnityGroup.schemePointsMulEquiv_symm_apply_single_generator_smul {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (n : ℕ) (ζ : ↥(rootsOfUnity n A)) (r : R) : ((DiagonalizableGroup.groupSchemePointsMulEquiv (characterGroup n)) ((schemePointsMulEquiv n).symm ζ)).ofConv (MonoidAlgebra.single { down := generator n } r) = r • ↑↑ζ

The scheme point associated to a root of unity evaluates scalar multiples of the lifted standard generator by scalar multiplication of that root.

theorem TauCeti.RootsOfUnityGroup.schemePointsMulEquiv_mapValue {R A B : Type u} [CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (n : ℕ) (phi : A →ₐ[R] B) (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R n).X) : (schemePointsMulEquiv n) (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.asOver (AlgebraicGeometry.Spec.map (CommRingCat.ofHom phi.toRingHom)) (AlgebraicGeometry.Spec ↧R)) p) = (restrictRootsOfUnity (↑phi.toRingHom) n) ((schemePointsMulEquiv n) p)

The scheme-valued roots-of-unity comparison is natural in the value algebra.

The closed inclusion into the multiplicative group scheme

noncomputable def TauCeti.RootsOfUnityGroup.characterQuotient (n : ℕ) : DiagonalizableGroup.multiplicativeCharacterGroup ⟶ characterGroup n

The quotient Multiplicative Z -> Multiplicative (ZMod n), transported between the same-universe character groups defining G_m and mu_n.

This lifted lattice map is public so later scheme-kernel constructions can reuse the exact coordinate map without reconstructing universe transports from the scheme morphism.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.RootsOfUnityGroup.characterQuotient_apply_up (n : ℕ) (x : Multiplicative ℤ) : (FGCommGrpCat.toMonoidHom (characterQuotient n)) { down := x } = { down := (toMultiplicativeZMod n) x }

The lifted character quotient sends the lift of an integer character to the lift of its residue class.

theorem TauCeti.RootsOfUnityGroup.characterQuotient_surjective (n : ℕ) : Function.Surjective ⇑(FGCommGrpCat.toMonoidHom (characterQuotient n))

The lifted character quotient defining mu_n -> G_m is surjective for every n.

noncomputable def TauCeti.RootsOfUnityGroup.inclusionGroupSchemeMap (R : Type u) [CommRing R] (n : ℕ) : groupScheme R n ⟶ DiagonalizableGroup.multiplicativeGroupScheme R

The group-scheme morphism mu_n -> G_m induced contravariantly by the lifted quotient of character groups.

Equations

• TauCeti.RootsOfUnityGroup.inclusionGroupSchemeMap R n = TauCeti.DiagonalizableGroup.groupSchemeMap R (TauCeti.RootsOfUnityGroup.characterQuotient n)

theorem TauCeti.RootsOfUnityGroup.inclusionGroupSchemeMap_def {R : Type u} [CommRing R] (n : ℕ) : inclusionGroupSchemeMap R n = DiagonalizableGroup.groupSchemeMap R (characterQuotient n)

The roots-of-unity group-scheme inclusion is the contravariant diagonalizable image of characterQuotient.

@[simp]

theorem TauCeti.RootsOfUnityGroup.multiplicativeGroupSchemePointsMulEquiv_inclusionGroupSchemeMap {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] (n : ℕ) (p : (AlgebraicGeometry.Spec ↧A).asOver (AlgebraicGeometry.Spec ↧R) ⟶ (groupScheme R n).X) : DiagonalizableGroup.multiplicativeGroupSchemePointsMulEquiv (CategoryTheory.CategoryStruct.comp p (inclusionGroupSchemeMap R n).hom.hom) = ↑((schemePointsMulEquiv n) p)

On scheme-valued points, mu_n -> G_m is the established inclusion of roots of unity into units.

instance TauCeti.RootsOfUnityGroup.isClosedImmersion_inclusionGroupSchemeMap {R : Type u} [CommRing R] (n : ℕ) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (inclusionGroupSchemeMap R n).hom.hom)

The group-scheme morphism mu_n -> G_m is a closed immersion.