The center of the special linear group

For a field k and a positive integer n, this file identifies the center of the special linear group scheme SLₙ with the roots-of-unity group scheme μₙ. A root of unity acts by its scalar matrix. Mathlib's equivalence Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity' supplies the matrix-theoretic classification of the center; universal centrality then upgrades it to the represented center.

The natural pointwise equivalence and full faithfulness of the Hopf-algebra functor of points give an isomorphism

  k[SLₙ] / I(Z(SLₙ)) ≅ k[Multiplicative (ZMod n)]

of commutative Hopf algebras. This is the center calculation used by the standard central isogeny from SLₙ toward its adjoint form.

Main declarations

• TauCeti.SpecialLinear.rootsOfUnityScalarPoints: the scalar-matrix map from μₙ-points to SLₙ-points.
• TauCeti.SpecialLinear.rootsOfUnityScalarCenterNatIso: the natural isomorphism from μₙ-points to the represented center of SLₙ.
• TauCeti.SpecialLinear.centerCoordinateIsoGroupAlgebra: the center coordinate Hopf algebra of SLₙ is the group algebra of Multiplicative (ZMod n).

References

• J. S. Milne, Algebraic Groups (2017), Examples 2.4 and 5.49, and §18.a.

This advances Layer 6, "Reductive and semisimple groups", of the ReductiveGroups roadmap: the center and central-isogeny input for the simply connected and adjoint forms.

noncomputable def TauCeti.SpecialLinear.rootsOfUnityScalarSL (n : ℕ) {A : Type v} [CommRing A] : ↥(rootsOfUnity n A) →* Matrix.SpecialLinearGroup (Fin n) A

The scalar-matrix homomorphism from nth roots of unity to SL(Fin n, A).

Equations

• TauCeti.SpecialLinear.rootsOfUnityScalarSL n = { toFun := fun (ζ : ↥(rootsOfUnity n A)) => ⟨(Matrix.scalar (Fin n)) ↑↑ζ, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.SpecialLinear.coe_rootsOfUnityScalarSL (n : ℕ) {A : Type v} [CommRing A] (ζ : ↥(rootsOfUnity n A)) : ↑((rootsOfUnityScalarSL n) ζ) = (Matrix.scalar (Fin n)) ↑↑ζ

The underlying matrix of rootsOfUnityScalarSL is the corresponding scalar matrix.

noncomputable def TauCeti.SpecialLinear.rootsOfUnityScalarPoints (n : ℕ) {R : Type u} [CommRing R] {A : Type v} [CommRing A] [Algebra R A] : WithConv (MonoidAlgebra R (Multiplicative (ZMod n)) →ₐ[R] A) →* WithConv (↑(coordinateHopfAlgebra R n) →ₐ[R] A)

Send a roots-of-unity point to the corresponding scalar special-linear point.

Equations

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

@[simp]

theorem TauCeti.SpecialLinear.pointsMulEquiv_rootsOfUnityScalarPoints (n : ℕ) {R : Type u} [CommRing R] {A : Type v} [CommRing A] [Algebra R A] (f : WithConv (MonoidAlgebra R (Multiplicative (ZMod n)) →ₐ[R] A)) : (pointsMulEquiv R n) ((rootsOfUnityScalarPoints n) f) = (rootsOfUnityScalarSL n) ((RootsOfUnityGroup.pointsMulEquiv n) f)

Under the standard point equivalences, rootsOfUnityScalarPoints is the scalar matrix attached to a root of unity.

@[simp]

theorem TauCeti.SpecialLinear.coe_pointsMulEquiv_rootsOfUnityScalarPoints (n : ℕ) {R : Type u} [CommRing R] {A : Type v} [CommRing A] [Algebra R A] (f : WithConv (MonoidAlgebra R (Multiplicative (ZMod n)) →ₐ[R] A)) : ↑((pointsMulEquiv R n) ((rootsOfUnityScalarPoints n) f)) = (Matrix.scalar (Fin n)) ↑↑((RootsOfUnityGroup.pointsMulEquiv n) f)

The central special-linear matrix attached to a root of unity is a scalar matrix.

theorem TauCeti.SpecialLinear.rootsOfUnityScalarPoints_injective (n : ℕ) (hn : 0 < n) {R : Type u} [CommRing R] {A : Type v} [CommRing A] [Algebra R A] : Function.Injective ⇑(rootsOfUnityScalarPoints n)

For 0 < n, the scalar roots-of-unity map is injective.

theorem TauCeti.SpecialLinear.mapValue_rootsOfUnityScalarPoints (n : ℕ) {R : Type u} [CommRing R] {A : Type v} {B : Type w} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (φ : A →ₐ[R] B) (f : WithConv (MonoidAlgebra R (Multiplicative (ZMod n)) →ₐ[R] A)) : (AlgHom.mapValue φ) ((rootsOfUnityScalarPoints n) f) = (rootsOfUnityScalarPoints n) ((AlgHom.mapValue φ) f)

The scalar roots-of-unity construction is natural in the value algebra.

theorem TauCeti.SpecialLinear.isCentralPoint_rootsOfUnityScalarPoints (n : ℕ) {S : Type u} [CommRing S] {A : Type u} [CommRing A] [Algebra S A] (f : WithConv (MonoidAlgebra S (Multiplicative (ZMod n)) →ₐ[S] A)) : HopfAlgebra.IsCentralPoint ((rootsOfUnityScalarPoints n) f)

A scalar roots-of-unity point is universally central over any commutative base ring.

noncomputable def TauCeti.SpecialLinear.rootsOfUnityScalarCenterHom (n : ℕ) {S : Type u} [CommRing S] (A : Type u) [CommRing A] [Algebra S A] : WithConv (MonoidAlgebra S (Multiplicative (ZMod n)) →ₐ[S] A) →* ↥(HopfAlgebra.center S (↑(coordinateHopfAlgebra S n)) A)

The scalar roots-of-unity map with codomain restricted to the universal center.

Equations

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

@[simp]

theorem TauCeti.SpecialLinear.coe_rootsOfUnityScalarCenterHom_apply (n : ℕ) {S : Type u} [CommRing S] (A : Type u) [CommRing A] [Algebra S A] (f : WithConv (MonoidAlgebra S (Multiplicative (ZMod n)) →ₐ[S] A)) : ↑((rootsOfUnityScalarCenterHom n A) f) = (rootsOfUnityScalarPoints n) f

The value of rootsOfUnityScalarCenterHom is the underlying scalar point.

theorem TauCeti.SpecialLinear.rootsOfUnityScalarCenterHom_bijective (n : ℕ) {S : Type u} [CommRing S] (hn : 0 < n) (A : Type u) [CommRing A] [Algebra S A] : Function.Bijective ⇑(rootsOfUnityScalarCenterHom n A)

For 0 < n, scalar roots of unity give every universally central point of SLₙ.

noncomputable def TauCeti.SpecialLinear.rootsOfUnityScalarCenterMulEquiv (n : ℕ) {S : Type u} [CommRing S] (hn : 0 < n) (A : Type u) [CommRing A] [Algebra S A] : WithConv (MonoidAlgebra S (Multiplicative (ZMod n)) →ₐ[S] A) ≃* ↥(HopfAlgebra.center S (↑(coordinateHopfAlgebra S n)) A)

For 0 < n, scalar roots of unity identify μₙ with the universal center of SLₙ pointwise over any commutative base ring.

Equations

• TauCeti.SpecialLinear.rootsOfUnityScalarCenterMulEquiv n hn A = MulEquiv.ofBijective (TauCeti.SpecialLinear.rootsOfUnityScalarCenterHom n A) ⋯

@[simp]

theorem TauCeti.SpecialLinear.rootsOfUnityScalarCenterMulEquiv_apply (n : ℕ) {S : Type u} [CommRing S] (hn : 0 < n) (A : Type u) [CommRing A] [Algebra S A] (f : WithConv (MonoidAlgebra S (Multiplicative (ZMod n)) →ₐ[S] A)) : ↑((rootsOfUnityScalarCenterMulEquiv n hn A) f) = (rootsOfUnityScalarPoints n) f

The forward map of rootsOfUnityScalarCenterMulEquiv is the scalar-point map.

noncomputable def TauCeti.SpecialLinear.rootsOfUnityOfCenterPoint (n : ℕ) {S : Type u} [CommRing S] (hn : 0 < n) {A : Type u} [CommRing A] [Algebra S A] (g : ↥(HopfAlgebra.center S (↑(coordinateHopfAlgebra S n)) A)) : ↥(rootsOfUnity n A)

Read the root of unity from the upper-left entry of a universally central SLₙ-point.

Equations

• TauCeti.SpecialLinear.rootsOfUnityOfCenterPoint n hn g = (Matrix.SpecialLinearGroup.centerMulEquivRootsOfUnityFin n hn A) ⟨(TauCeti.SpecialLinear.pointsMulEquiv S n) ↑g, ⋯⟩

@[simp]

theorem TauCeti.SpecialLinear.rootsOfUnityScalarCenterMulEquiv_symm_apply (n : ℕ) {S : Type u} [CommRing S] (hn : 0 < n) (A : Type u) [CommRing A] [Algebra S A] (g : ↥(HopfAlgebra.center S (↑(coordinateHopfAlgebra S n)) A)) : (rootsOfUnityScalarCenterMulEquiv n hn A).symm g = (RootsOfUnityGroup.pointsMulEquiv n).symm (rootsOfUnityOfCenterPoint n hn g)

The inverse pointwise center equivalence reads off the root of unity from the central special-linear matrix.

theorem TauCeti.SpecialLinear.rootsOfUnityScalarPoints_mem_centerPointsSubgroup (n : ℕ) {k : Type u} [Field k] {A : Type u} [CommRing A] [Algebra k A] (f : WithConv (MonoidAlgebra k (Multiplicative (ZMod n)) →ₐ[k] A)) : (rootsOfUnityScalarPoints n) f ∈ CommHopfAlgCat.centerPointsSubgroup (coordinateHopfAlgebra k n) ↧A

Every roots-of-unity scalar point is a point of the represented center of SLₙ.

noncomputable def TauCeti.SpecialLinear.rootsOfUnityScalarCenterIso (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) (A : CommAlgCat k) : HopfAlgebra.points A ≅ ↧↥(CommHopfAlgCat.centerPointsSubgroup (coordinateHopfAlgebra k n) A)

For every value algebra, scalar roots of unity identify μₙ with the represented center of SLₙ.

Equations

• TauCeti.SpecialLinear.rootsOfUnityScalarCenterIso n hn A = ((TauCeti.SpecialLinear.rootsOfUnityScalarCenterMulEquiv n hn ↑A).trans (MulEquiv.subgroupCongr ⋯)).toGrpIso

@[simp]

theorem TauCeti.SpecialLinear.rootsOfUnityScalarCenterIso_hom_apply (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) (A : CommAlgCat k) (f : ↑(HopfAlgebra.points A)) : ↑((CategoryTheory.ConcreteCategory.hom (rootsOfUnityScalarCenterIso n hn A).hom) f) = (rootsOfUnityScalarPoints n) f

The forward component of rootsOfUnityScalarCenterIso is the scalar-matrix map.

@[simp]

theorem TauCeti.SpecialLinear.rootsOfUnityScalarCenterIso_inv_apply (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) (A : CommAlgCat k) (g : ↥(CommHopfAlgCat.centerPointsSubgroup (coordinateHopfAlgebra k n) A)) : (CategoryTheory.ConcreteCategory.hom (rootsOfUnityScalarCenterIso n hn A).inv) g = (RootsOfUnityGroup.pointsMulEquiv n).symm (rootsOfUnityOfCenterPoint n hn ⟨↑g, ⋯⟩)

The inverse represented-center equivalence reads off the root of unity from the central special-linear matrix.

noncomputable def TauCeti.SpecialLinear.rootsOfUnityScalarCenterNatIso (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) : HopfAlgebra.pointsFunctor ≅ CommHopfAlgCat.quotientPointsSubgroupFunctor (coordinateHopfAlgebra k n) (CommHopfAlgCat.centerDefiningIdeal (coordinateHopfAlgebra k n))

Scalar roots of unity identify the μₙ point functor with the represented center subfunctor of SLₙ.

Equations

• TauCeti.SpecialLinear.rootsOfUnityScalarCenterNatIso n hn = CategoryTheory.NatIso.ofComponents (TauCeti.SpecialLinear.rootsOfUnityScalarCenterIso n hn) ⋯

@[simp]

theorem TauCeti.SpecialLinear.rootsOfUnityScalarCenterNatIso_hom_app_apply (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) (A : CommAlgCat k) (f : ↑(HopfAlgebra.points A)) : ↑((CategoryTheory.ConcreteCategory.hom ((rootsOfUnityScalarCenterNatIso n hn).hom.app A)) f) = (rootsOfUnityScalarPoints n) f

The natural isomorphism sends a μₙ-point to its scalar matrix.

@[simp]

theorem TauCeti.SpecialLinear.rootsOfUnityScalarCenterNatIso_inv_app_apply (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) (A : CommAlgCat k) (g : ↥(CommHopfAlgCat.centerPointsSubgroup (coordinateHopfAlgebra k n) A)) : (CategoryTheory.ConcreteCategory.hom ((rootsOfUnityScalarCenterNatIso n hn).inv.app A)) g = (RootsOfUnityGroup.pointsMulEquiv n).symm (rootsOfUnityOfCenterPoint n hn ⟨↑g, ⋯⟩)

The inverse natural-isomorphism component reads off the root of unity from the central special-linear matrix.

noncomputable def TauCeti.SpecialLinear.rootsOfUnityScalarCenterCoordinatePointsNatIso (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) : CommHopfAlgCat.pointsFunctor.obj (Opposite.op ↧(MonoidAlgebra k (Multiplicative (ZMod n)))) ≅ CommHopfAlgCat.pointsFunctor.obj (Opposite.op (CommHopfAlgCat.quotient (coordinateHopfAlgebra k n) (CommHopfAlgCat.centerDefiningIdeal (coordinateHopfAlgebra k n))))

The point functor of μₙ is naturally isomorphic to the point functor represented by the center coordinate Hopf algebra of SLₙ.

Equations

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

noncomputable def TauCeti.SpecialLinear.centerCoordinateIsoGroupAlgebra (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) : CommHopfAlgCat.quotient (coordinateHopfAlgebra k n) (CommHopfAlgCat.centerDefiningIdeal (coordinateHopfAlgebra k n)) ≅ ↧(MonoidAlgebra k (Multiplicative (ZMod n)))

For 0 < n, the coordinate Hopf algebra of the center of SLₙ is the group algebra of Multiplicative (ZMod n), the coordinate Hopf algebra of μₙ.

Equations

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

theorem TauCeti.SpecialLinear.pointsFunctor_mapIso_centerCoordinateIsoGroupAlgebra (n : ℕ) {k : Type u} [Field k] (hn : 0 < n) : CommHopfAlgCat.pointsFunctor.mapIso (centerCoordinateIsoGroupAlgebra n hn).op = rootsOfUnityScalarCenterCoordinatePointsNatIso n hn

Applying the functor of points to centerCoordinateIsoGroupAlgebra recovers the scalar-matrix natural isomorphism used to construct it.