Tangent equations for a constant-form subgroup #
For the subgroup of GLₙ defined by g C gᵀ = C, the tangent equation at the identity
is X C + C Xᵀ = 0. This identifies the image of the closed-subgroup differential
without assuming that the form is nondegenerate or that the base is a field.
The coefficients may lie in any commutative algebra over the base ring.
The computation uses the counit-valued Leibniz rule and
HopfIdeal.mem_lieSubalgebra_iff_of_toIdeal_eq_span, following the same quotient
method as SpecialLinear.mem_lieSubalgebra_definingHopfIdeal_iff.
References #
- J. S. Milne, Algebraic Groups (2017), §10.a (tangent spaces of closed subgroups).
theorem
TauCeti.ConstantForm.derivation_relationMatrix
{R : Type u}
[CommRing R]
{B : Type v}
[CommRing B]
[Algebra R B]
{n : ℕ}
(C : Matrix (Fin n) (Fin n) R)
(d :
Derivation R (↑(GeneralLinear.coordinateHopfAlgebra R n))
(Bialgebra.CounitAlgebra R (↑(GeneralLinear.coordinateHopfAlgebra R n)) B))
(i j : Fin n)
:
(Bialgebra.CounitAlgebra.algEquivSelf R (↑(GeneralLinear.coordinateHopfAlgebra R n)) B) (d (relationMatrix R n C i j)) = ((GeneralLinear.tangentMatrix n) d * C.map ⇑(algebraMap R B) + C.map ⇑(algebraMap R B) * ((GeneralLinear.tangentMatrix n) d).transpose)
i j
Differentiating the constant-form relation gives X C + C Xᵀ entrywise.
theorem
TauCeti.ConstantForm.mem_lieSubalgebra_definingHopfIdeal_iff
{R : Type u}
[CommRing R]
{B : Type v}
[CommRing B]
[Algebra R B]
{n : ℕ}
(C : Matrix (Fin n) (Fin n) R)
(d :
Derivation R (↑(GeneralLinear.coordinateHopfAlgebra R n))
(Bialgebra.CounitAlgebra R (↑(GeneralLinear.coordinateHopfAlgebra R n)) B))
:
d ∈ (definingHopfIdeal R n C).lieSubalgebra ↔ (GeneralLinear.tangentMatrix n) d * C.map ⇑(algebraMap R B) + C.map ⇑(algebraMap R B) * ((GeneralLinear.tangentMatrix n) d).transpose = 0
An ambient tangent vector belongs to the Lie algebra of the constant-form subgroup exactly when its matrix satisfies the linearized form equation.