The special linear group coordinate Hopf algebra

For a commutative ring R, this file presents the coordinate Hopf algebra of SLₙ as the quotient of TauCeti.GeneralLinear.coordinateHopfAlgebra R n by the kernel Hopf ideal of the determinant coordinate morphism. The underlying ideal is the principal ideal generated by the localized generic determinant minus one:

(det - 1) ⊂ R[Xᵢⱼ][det⁻¹].

The principal-ideal calculation works over every commutative ring and in every rank. Positive integral powers use the geometric-series factorization. Negative powers are handled through the unit attached to the group-like determinant, so no cancellation, nontriviality, or domain hypothesis is needed.

The generic Hopf-ideal quotient API provides the quotient Hopf algebra. On algebra-valued points, the generic quotient-point natural isomorphism and the general-linear point equivalence identify the quotient naturally with Mathlib's Matrix.SpecialLinearGroup (Fin n) A; the induced inclusion is Matrix.SpecialLinearGroup.toGL.

This construction includes rank zero and the zero ring. It deliberately stays at the determinant-kernel boundary: no polynomial presentation, categorical pullback, smoothness, reductivity, or base-change theorem is asserted here.

Main declarations

• TauCeti.SpecialLinear.definingHopfIdeal_toIdeal: the determinant kernel ideal is generated by the localized generic determinant minus one.
• TauCeti.SpecialLinear.definingHopfIdeal_toIdeal_le_ker_of_map_determinant_eq_one: a coordinate morphism that kills det - 1 kills the defining ideal of SLₙ.
• TauCeti.SpecialLinear.coordinateHopfAlgebra: the determinant-one quotient Hopf algebra.
• TauCeti.SpecialLinear.det_map_genericMatrix_coordinateMap and TauCeti.SpecialLinear.adjoin_range_map_genericMatrix: the generic matrix of SLₙ has determinant one, and its entries generate O(SLₙ).
• TauCeti.SpecialLinear.pointsMulEquiv: the natural multiplicative equivalence between quotient Hopf points and Matrix.SpecialLinearGroup.
• TauCeti.SpecialLinear.pointsNatIso: the corresponding natural isomorphism of group-valued functors.

References

• J. S. Milne, Basic Theory of Affine Group Schemes, Part I, §1.7, pp. 49–50.
• The Stacks Project, Tag 022X, "The general linear group scheme".

The ideal calculation below is a routine direct argument through Tau Ceti's kernel-Hopf-ideal API; it is not adapted from either reference.

The determinant-one Hopf ideal and quotient

@[reducible, inline]

noncomputable abbrev TauCeti.SpecialLinear.definingHopfIdeal (R : Type u) [CommRing R] (n : ℕ) : HopfIdeal R ↑(GeneralLinear.coordinateHopfAlgebra R n)

The Hopf ideal cutting out determinant one inside the general-linear coordinate Hopf algebra. It is the kernel Hopf ideal of the determinant coordinate morphism.

Equations

• TauCeti.SpecialLinear.definingHopfIdeal R n = TauCeti.CommHopfAlgCat.kernelHopfIdeal (TauCeti.GeneralLinear.determinantCoordinateMap R n)

theorem TauCeti.SpecialLinear.definingHopfIdeal_toIdeal (R : Type u) [CommRing R] (n : ℕ) : (definingHopfIdeal R n).toIdeal = Ideal.span {↑(GeneralLinear.determinantGroupLike R n) - 1}

The determinant kernel Hopf ideal is the principal ideal generated by the localized generic determinant minus one.

theorem TauCeti.SpecialLinear.definingHopfIdeal_toIdeal_le_ker_of_map_determinant_eq_one (R : Type u) [CommRing R] (n : ℕ) {H : CommHopfAlgCat R} (f : GeneralLinear.coordinateHopfAlgebra R n ⟶ H) (hdet : (CommHopfAlgCat.Hom.hom f) ↑(GeneralLinear.determinantGroupLike R n) = 1) : (definingHopfIdeal R n).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom f)).toRingHom

A morphism from the coordinate ring of GLₙ that sends the generic determinant to one kills the defining ideal of SLₙ.

@[reducible, inline]

noncomputable abbrev TauCeti.SpecialLinear.coordinateHopfAlgebra (R : Type u) [CommRing R] (n : ℕ) : CommHopfAlgCat R

The coordinate Hopf algebra of SLₙ, obtained by imposing determinant one on the general-linear coordinate Hopf algebra.

Equations

• TauCeti.SpecialLinear.coordinateHopfAlgebra R n = TauCeti.CommHopfAlgCat.quotient (TauCeti.GeneralLinear.coordinateHopfAlgebra R n) (TauCeti.SpecialLinear.definingHopfIdeal R n)

@[reducible, inline]

noncomputable abbrev TauCeti.SpecialLinear.coordinateMap (R : Type u) [CommRing R] (n : ℕ) : GeneralLinear.coordinateHopfAlgebra R n ⟶ coordinateHopfAlgebra R n

The quotient coordinate morphism O(GLₙ) ⟶ O(SLₙ). Contravariantly, it is the closed-subgroup inclusion SLₙ ⟶ GLₙ.

Equations

• TauCeti.SpecialLinear.coordinateMap R n = TauCeti.CommHopfAlgCat.mkQuotient (TauCeti.GeneralLinear.coordinateHopfAlgebra R n) (TauCeti.SpecialLinear.definingHopfIdeal R n)

theorem TauCeti.SpecialLinear.coordinateMap_apply (R : Type u) [CommRing R] (n : ℕ) (h : ↑(GeneralLinear.coordinateHopfAlgebra R n)) : (CommHopfAlgCat.Hom.hom (coordinateMap R n)) h = (Ideal.Quotient.mkₐ R (definingHopfIdeal R n).toIdeal) h

The special-linear coordinate morphism sends an ambient coordinate to its quotient class.

@[simp]

theorem TauCeti.SpecialLinear.coordinateMap_determinantGroupLike (R : Type u) [CommRing R] (n : ℕ) : (CommHopfAlgCat.Hom.hom (coordinateMap R n)) ↑(GeneralLinear.determinantGroupLike R n) = 1

The localized generic determinant is one in the special-linear coordinate Hopf algebra.

theorem TauCeti.SpecialLinear.coordinateMap_ker (R : Type u) [CommRing R] (n : ℕ) : RingHom.ker (↑(CommHopfAlgCat.Hom.hom (coordinateMap R n))).toRingHom = Ideal.span {↑(GeneralLinear.determinantGroupLike R n) - 1}

The kernel of the special-linear coordinate morphism is the principal determinant-one ideal.

@[simp]

theorem TauCeti.SpecialLinear.det_map_genericMatrix_coordinateMap (R : Type u) [CommRing R] (n : ℕ) : ((GeneralLinear.genericMatrix R n).map ⇑(CommHopfAlgCat.Hom.hom (coordinateMap R n))).det = 1

The generic matrix of SLₙ, the image in O(SLₙ) of the generic matrix of GLₙ, has determinant one.

theorem TauCeti.SpecialLinear.adjoin_range_map_genericMatrix (R : Type u) [CommRing R] (n : ℕ) : Algebra.adjoin R (Set.range fun (ij : Fin n × Fin n) => (GeneralLinear.genericMatrix R n).map (⇑(CommHopfAlgCat.Hom.hom (coordinateMap R n))) ij.1 ij.2) = ⊤

The entries of the generic matrix of SLₙ generate O(SLₙ).

noncomputable def TauCeti.SpecialLinear.finiteTypeCoordinateHopfAlgebra (R : Type u) [CommRing R] (n : ℕ) : FiniteTypeCommHopfAlgCat R

The special-linear coordinate Hopf algebra bundled with its finite-type algebra property.

Equations

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

@[simp]

theorem TauCeti.SpecialLinear.finiteTypeCoordinateHopfAlgebra_obj (R : Type u) [CommRing R] (n : ℕ) : (finiteTypeCoordinateHopfAlgebra R n).obj = coordinateHopfAlgebra R n

The underlying commutative Hopf algebra of the finite-type object is the determinant-one quotient.

instance TauCeti.SpecialLinear.instAlgebraFiniteTypeCoordinateHopfAlgebra (R : Type u) [CommRing R] (n : ℕ) : Algebra.FiniteType R ↑(coordinateHopfAlgebra R n)

The special-linear coordinate Hopf algebra is a finite-type R-algebra, being a quotient of the finite-type general-linear coordinate Hopf algebra.

Algebra-valued points

@[simp]

theorem TauCeti.SpecialLinear.mem_definingPointsSubgroup_iff_det_eq_one (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (g : ↑(HopfAlgebra.points ↧A)) : g ∈ CommHopfAlgCat.quotientPointsSubgroup (GeneralLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n) ↧A ↔ (↑((GeneralLinear.pointsMulEquiv n) g)).det = 1

Membership in the point subgroup cut out by the determinant kernel is determinant one. This is the ambient membership criterion that further cuts consume; the determinant-one cut of the orthogonal group (TauCeti.SpecialOrthogonal) combines it with the orthogonal one.

noncomputable def TauCeti.SpecialLinear.pointsMulEquiv (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] : ↑(HopfAlgebra.points ↧A) ≃* Matrix.SpecialLinearGroup (Fin n) A

The group of algebra-valued points of the special-linear coordinate Hopf algebra is Mathlib's special linear group. The construction first applies the generic natural isomorphism from quotient points to the cut-out ambient subgroup, then reads that subgroup as determinant-one matrices through the general-linear point equivalence.

Equations

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

theorem TauCeti.SpecialLinear.pointsMulEquiv_toGL (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (f : ↑(HopfAlgebra.points ↧A)) : (GeneralLinear.pointsMulEquiv n) ((CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n) ↧A)) f) = Matrix.SpecialLinearGroup.toGL ((pointsMulEquiv R n) f)

Under the special- and general-linear point equivalences, the quotient-point inclusion is Mathlib's canonical inclusion Matrix.SpecialLinearGroup.toGL.

@[simp]

theorem TauCeti.SpecialLinear.quotientPointsHom_pointsMulEquiv_symm (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (s : Matrix.SpecialLinearGroup (Fin n) A) : (CategoryTheory.ConcreteCategory.hom (CommHopfAlgCat.quotientPointsHom (GeneralLinear.coordinateHopfAlgebra R n) (definingHopfIdeal R n) ↧A)) ((pointsMulEquiv R n).symm s) = (GeneralLinear.pointsMulEquiv n).symm (Matrix.SpecialLinearGroup.toGL s)

The ambient point attached to a special-linear matrix is the general-linear point attached to its canonical inclusion.

theorem TauCeti.SpecialLinear.pointsMulEquiv_mapValue (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] {B : Type v} [CommRing B] [Algebra R B] (phi : A →ₐ[R] B) (f : ↑(HopfAlgebra.points ↧A)) : (pointsMulEquiv R n) ((AlgHom.mapValue phi) f) = (Matrix.SpecialLinearGroup.map phi.toRingHom) ((pointsMulEquiv R n) f)

The special-linear point equivalence is natural in the value algebra: postcomposition of Hopf points agrees with entrywise mapping of determinant-one matrices.

theorem TauCeti.SpecialLinear.pointsMulEquiv_comp_pointConjugationAlgHom_symm (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (s : Matrix.SpecialLinearGroup (Fin n) R) (φ : ↑(coordinateHopfAlgebra R n) →ₐ[R] A) : Matrix.SpecialLinearGroup.toGL ((pointsMulEquiv R n) (WithConv.toConv (φ.comp (HopfAlgebra.pointConjugationAlgHom ((pointsMulEquiv R n).symm s⁻¹))))) = ((Matrix.GeneralLinearGroup.map (algebraMap R A)) (Matrix.SpecialLinearGroup.toGL s))⁻¹ * (GeneralLinear.pointsMulEquiv n) (WithConv.toConv (φ.comp ↑(CommHopfAlgCat.Hom.hom (coordinateMap R n)))) * (Matrix.GeneralLinearGroup.map (algebraMap R A)) (Matrix.SpecialLinearGroup.toGL s)

Conjugating an SLₙ point by the point attached to the inverse of s becomes ordinary matrix conjugation after extension of scalars and inclusion into GLₙ.

theorem TauCeti.SpecialLinear.pointsMulEquiv_comp_pointConjugationAlgHom_symm_toGLKerEquiv_symm (R : Type u) [CommRing R] (n : ℕ) {A : Type w} [CommRing A] [Algebra R A] (P : GL (Fin n) R) (hdet : Matrix.GeneralLinearGroup.det P = 1) (φ : ↑(coordinateHopfAlgebra R n) →ₐ[R] A) : Matrix.SpecialLinearGroup.toGL ((pointsMulEquiv R n) (WithConv.toConv (φ.comp (HopfAlgebra.pointConjugationAlgHom ((pointsMulEquiv R n).symm (Matrix.SpecialLinearGroup.toGLKerEquiv.symm ⟨P, hdet⟩)⁻¹))))) = ((Matrix.GeneralLinearGroup.map (algebraMap R A)) P)⁻¹ * (GeneralLinear.pointsMulEquiv n) (WithConv.toConv (φ.comp ↑(CommHopfAlgCat.Hom.hom (coordinateMap R n)))) * (Matrix.GeneralLinearGroup.map (algebraMap R A)) P

Conjugation by a determinant-one general-linear matrix, expressed through its corresponding special-linear point.

Naturality as an isomorphism of group-valued functors

noncomputable def TauCeti.SpecialLinear.specialLinearFunctor (R : Type u) [CommRing R] (n : ℕ) : CategoryTheory.Functor (CommAlgCat R) GrpCat

The group-valued functor sending an R-algebra to its special linear group and an algebra morphism to entrywise matrix mapping. Values are universe-lifted to match the Hopf-points functor.

Equations

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

theorem TauCeti.SpecialLinear.specialLinearFunctor_obj (R : Type u) [CommRing R] (n : ℕ) (A : CommAlgCat R) : (specialLinearFunctor R n).obj A = ↧(ULift.{u, w} (Matrix.SpecialLinearGroup (Fin n) ↑A))

The object part of specialLinearFunctor is the universe lift of the ordinary special linear group.

theorem TauCeti.SpecialLinear.specialLinearFunctor_map (R : Type u) [CommRing R] (n : ℕ) {A B : CommAlgCat R} (phi : A ⟶ B) : (specialLinearFunctor R n).map phi = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (GrpCat.ofHom (MulEquiv.ulift.symm.toMonoidHom.comp ((Matrix.SpecialLinearGroup.map (CommAlgCat.Hom.hom phi).toRingHom).comp MulEquiv.ulift.toMonoidHom))) (CategoryTheory.eqToHom ⋯))

The morphism part of specialLinearFunctor applies the value-algebra morphism entrywise.

@[simp]

theorem TauCeti.SpecialLinear.specialLinearFunctor_map_apply_apply (R : Type u) [CommRing R] (n : ℕ) {A B : CommAlgCat R} (phi : A ⟶ B) (g : ULift.{u, w} (Matrix.SpecialLinearGroup (Fin n) ↑A)) (i j : Fin n) : ↑((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom ((specialLinearFunctor R n).map phi)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) g))).down i j = (CommAlgCat.Hom.hom phi) (↑g.down i j)

Entrywise computation of the value-algebra map on the special linear functor.

noncomputable def TauCeti.SpecialLinear.pointsNatIso (R : Type u) [CommRing R] (n : ℕ) : HopfAlgebra.pointsFunctor ≅ specialLinearFunctor R n

The functor of points of the special-linear coordinate Hopf algebra is naturally isomorphic to the ordinary special linear group functor.

Equations

• TauCeti.SpecialLinear.pointsNatIso R n = CategoryTheory.NatIso.ofComponents (fun (A : CommAlgCat R) => ((TauCeti.SpecialLinear.pointsMulEquiv R n).trans MulEquiv.ulift.symm).toGrpIso) ⋯

@[simp]

theorem TauCeti.SpecialLinear.pointsNatIso_hom_app_apply (R : Type u) [CommRing R] (n : ℕ) (A : CommAlgCat R) (f : ↑(HopfAlgebra.points A)) : ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) ((CategoryTheory.ConcreteCategory.hom ((pointsNatIso R n).hom.app A)) f)).down = (pointsMulEquiv R n) f

After transport along specialLinearFunctor_obj, the forward component of pointsNatIso is the pointwise special-linear equivalence.

@[simp]

theorem TauCeti.SpecialLinear.pointsNatIso_inv_app_apply (R : Type u) [CommRing R] (n : ℕ) (A : CommAlgCat R) (g : ULift.{u, w} (Matrix.SpecialLinearGroup (Fin n) ↑A)) : (CategoryTheory.ConcreteCategory.hom ((pointsNatIso R n).inv.app A)) ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) g) = (pointsMulEquiv R n).symm g.down

After transport back along specialLinearFunctor_obj, the inverse component of pointsNatIso is the inverse pointwise special-linear equivalence.