Counit-valued points of the special linear group

A point of SLₙ valued in the counit algebra determines a determinant-one matrix. Its image under the closed-subgroup inclusion is the corresponding counit-valued point of GLₙ.

Main declarations

• TauCeti.SpecialLinear.counitPointsMulEquiv: the determinant-one matrix of a counit-valued point.
• TauCeti.SpecialLinear.toGL_counitPointsMulEquiv: compatibility with the inclusion into GLₙ.

noncomputable def TauCeti.SpecialLinear.counitPointsMulEquiv {R : Type u_1} [CommRing R] {B : Type u_2} [CommRing B] [Algebra R B] (n : ℕ) : WithConv (↑(coordinateHopfAlgebra R n) →ₐ[R] Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B) ≃* Matrix.SpecialLinearGroup (Fin n) B

The determinant-one matrix of a point of SLₙ valued in its counit algebra.

Equations

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

theorem TauCeti.SpecialLinear.counitPointsMulEquiv_eq_pointsMulEquiv {R : Type u_1} [CommRing R] {B : Type u_2} [CommRing B] [Algebra R B] (n : ℕ) (g : WithConv (↑(coordinateHopfAlgebra R n) →ₐ[R] Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B)) : (counitPointsMulEquiv n) g = (pointsMulEquiv R n) ((Bialgebra.CounitAlgebra.pointsMulEquiv R (↑(coordinateHopfAlgebra R n)) B) g)

The determinant-one matrix of a counit-valued point is the matrix of its transported ordinary point.

@[simp]

theorem TauCeti.SpecialLinear.toGL_counitPointsMulEquiv {R : Type u_1} [CommRing R] {B : Type u_2} [CommRing B] [Algebra R B] (n : ℕ) (g : WithConv (↑(coordinateHopfAlgebra R n) →ₐ[R] Bialgebra.CounitAlgebra R (↑(coordinateHopfAlgebra R n)) B)) : Matrix.SpecialLinearGroup.toGL ((counitPointsMulEquiv n) g) = (GeneralLinear.counitPointsMulEquiv n) ((AlgHom.mapDomain (CommHopfAlgCat.Hom.hom (coordinateMap R n))) g)

The image in GLₙ of a counit-valued SLₙ point is its canonical inclusion.