The adjoint comodule of the general linear group #
This file identifies the fixed-module adjoint comodule of GLₙ with conjugation on matrices.
It is the comodule-level adapter between the scheme-theoretic representation API and explicit
matrix subspaces.
Main declaration #
TauCeti.GeneralLinear.tangentMatrix_adjointComodule_endOfPoint: the action induced by the adjoint comodule becomesX ↦ g X g⁻¹under the tangent-matrix equivalence.
@[simp]
theorem
TauCeti.GeneralLinear.tangentMatrix_adjointComodule_endOfPoint
{k : Type u}
[Field k]
{A : Type w}
[CommRing A]
[Algebra k A]
{n : ℕ}
(g : ↑(HopfAlgebra.points ↧A))
(x : TensorProduct k A (Module.Dual k (Bialgebra.CotangentSpace k ↑(coordinateHopfAlgebra k n))))
:
(tangentMatrix n)
(Derivation.tangentScalarExtensionEquiv
((Comodule.endOfPoint (Module.Dual k (Bialgebra.CotangentSpace k ↑(coordinateHopfAlgebra k n))) g.ofConv) x)) = ↑((pointsMulEquiv n) g) * (tangentMatrix n) (Derivation.tangentScalarExtensionEquiv x) * ↑((pointsMulEquiv n) g)⁻¹
Under the tangent-matrix equivalence, the point action induced by the adjoint comodule of
GLₙ is conjugation on matrices.