Differentiating a comodule representation

A right comodule over a commutative bialgebra carries a representation of its tangent Lie algebra at the identity. A counit-valued derivation acts by contraction of the coaction. This is the infinitesimal part of the existing action on dual-number points, and comodule morphisms intertwine the differentiated actions, and subcomodules are stable under them. Pairing the differentiated action with a functional recovers the tangent vector applied to the corresponding matrix coefficient.

The construction works over any commutative ring, for comodules of arbitrary rank, without smoothness or an antipode. For coordinate Hopf algebras it differentiates rational group representations, providing the passage to Lie-algebra representations used in complete reducibility arguments.

References

• J. C. Jantzen, Representations of Algebraic Groups, I.7.
• W. C. Waterhouse, Introduction to Affine Group Schemes, §§3 and 12.

noncomputable def TauCeti.Comodule.differential {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommRing H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] : Derivation R H (Bialgebra.CounitAlgebra R H R) →ₗ⁅R⁆ Module.End R M

The differentiated representation of a comodule: contract its coaction against a counit-valued derivation.

Equations

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

@[simp]

theorem TauCeti.Comodule.differential_apply {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommRing H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] (d : Derivation R H (Bialgebra.CounitAlgebra R H R)) (m : M) : (differential d) m = ((Bialgebra.CounitAlgebra.algEquivSelf R H R).toLinearMap ∘ₗ ↑d).tensorComponent (coact m)

The action of a tangent vector is contraction of the coaction by its underlying functional.

@[simp]

theorem TauCeti.Comodule.Hom.map_differential {R : Type u_1} {H : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CommRing H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] [AddCommGroup N] [Module R N] [Comodule R H N] (f : Hom R H M N) (d : Derivation R H (Bialgebra.CounitAlgebra R H R)) (m : M) : f ((differential d) m) = (differential d) (f m)

Every comodule morphism intertwines the differentiated representations.

theorem TauCeti.Comodule.snd_endOfPoint_derivationToDualNumberEquivLift {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommRing H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] (d : Derivation R H (Bialgebra.CounitAlgebra R H R)) (m : M) : (TensorProduct.lid R M) ((LinearMap.rTensor M ((Bialgebra.CounitAlgebra.algEquivSelf R H R).toLinearMap ∘ₗ ↑R (TrivSqZeroExt.sndHom (Bialgebra.CounitAlgebra R H R) (Bialgebra.CounitAlgebra R H R)))) ((endOfPoint M ↑((derivationToDualNumberEquivLift R H (Bialgebra.CounitAlgebra R H R)) d)) (1 ⊗ₜ[R] m))) = (differential d) m

The coefficient of ε in the action of a tangent dual-number point on 1 ⊗ m is the differentiated action on m. The counit coefficient algebra is identified with R by its canonical algebra equivalence.

theorem Derivation.apply_matrixCoefficient {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommRing H] [Bialgebra R H] [AddCommGroup M] [Module R M] [TauCeti.Comodule R H M] (d : Derivation R H (TauCeti.Bialgebra.CounitAlgebra R H R)) (φ : Module.Dual R M) (m : M) : (TauCeti.Bialgebra.CounitAlgebra.algEquivSelf R H R) (d (TauCeti.Comodule.matrixCoefficient φ m)) = φ ((TauCeti.Comodule.differential d) m)

A tangent vector at the identity, applied to a matrix coefficient c(φ, m), is the functional φ applied to the differentiated action of the tangent vector on m.

theorem TauCeti.Subcomodule.differential_mem {R : Type u_1} {H : Type u_2} {M : Type u_3} [CommRing R] [CommRing H] [Bialgebra R H] [AddCommGroup M] [Module R M] [Comodule R H M] (N : Subcomodule R H M) (d : Derivation R H (Bialgebra.CounitAlgebra R H R)) {m : M} (hm : m ∈ N) : (Comodule.differential d) m ∈ N

A subcomodule is stable under the differentiated action of every tangent vector.