Dual comodules and point representations

For a finite-projective right comodule over a commutative Hopf algebra, this file expresses the evaluation identities for dual comodule point actions through the fixed-object representation--comodule dictionary. The point action on the dual is adjoint to the original action at the inverse point, and acting by the same point on both inputs preserves evaluation.

The underlying action-level results hold at semiring generality in TauCeti.Algebra.Coalgebra.Comodule.Evaluation; the corollaries here use the dictionary's current commutative-ring and commutative-Hopf-algebra interface.

Main declarations

• TauCeti.HopfAlgebra.PointRepresentation.ofComodule_dual_action_evaluation_tmul: evaluation of a dual-action generator.
• TauCeti.HopfAlgebra.PointRepresentation.ofComodule_dual_action_evaluation: adjointness in the fixed-object dictionary.
• TauCeti.HopfAlgebra.PointRepresentation.ofComodule_dual_action_evaluation_invariant: same-point invariance of evaluation.

References

• J. S. Milne, Algebraic Groups (2017), Chapter 4(a) and the contragredient formula on p. 471.
• J. E. Humphreys, Linear Algebraic Groups, p. 60.

theorem TauCeti.HopfAlgebra.PointRepresentation.ofComodule_dual_action_evaluation_tmul {R : Type u} {H : Type v} {M : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [rho : Comodule R H M] [Module.Finite R M] [Module.Projective R M] (A : CommAlgCat R) (g : ↑(points A)) (a b : ↑A) (φ : Module.Dual R M) (m : M) : (Module.Dual.baseChangeEvaluation (↑((CategoryTheory.ConcreteCategory.hom ((ofComodule (Comodule.dual R H M)).action A)) g) (a ⊗ₜ[R] φ))) (b ⊗ₜ[R] m) = a * b * g⁻¹.ofConv (Comodule.matrixCoefficient φ m)

For the point action supplied by the representation--comodule dictionary, evaluation of a dual-action generator is inverse-point evaluation of the original matrix coefficient.

This is not a simp lemma because ofComodule_dual_action_evaluation and map_inv simplify its left-hand side first, so the simp-normal-form linter rejects the specialized orientation.

@[simp]

theorem TauCeti.HopfAlgebra.PointRepresentation.ofComodule_dual_action_evaluation {R : Type u} {H : Type v} {M : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [rho : Comodule R H M] [Module.Finite R M] [Module.Projective R M] (A : CommAlgCat R) (g : ↑(points A)) (ξ : TensorProduct R (↑A) (Module.Dual R M)) (z : TensorProduct R (↑A) M) : (Module.Dual.baseChangeEvaluation (↑((CategoryTheory.ConcreteCategory.hom ((ofComodule (Comodule.dual R H M)).action A)) g) ξ)) z = (Module.Dual.baseChangeEvaluation ξ) (↑((CategoryTheory.ConcreteCategory.hom ((ofComodule rho).action A)) g⁻¹) z)

In the fixed-object representation--comodule dictionary, the point action induced on the dual comodule is adjoint under evaluation to the original action at the inverse point.

theorem TauCeti.HopfAlgebra.PointRepresentation.ofComodule_dual_action_evaluation_invariant {R : Type u} {H : Type v} {M : Type w} [CommRing R] [CommRing H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [rho : Comodule R H M] [Module.Finite R M] [Module.Projective R M] (A : CommAlgCat R) (g : ↑(points A)) (ξ : TensorProduct R (↑A) (Module.Dual R M)) (z : TensorProduct R (↑A) M) : (Module.Dual.baseChangeEvaluation (↑((CategoryTheory.ConcreteCategory.hom ((ofComodule (Comodule.dual R H M)).action A)) g) ξ)) (↑((CategoryTheory.ConcreteCategory.hom ((ofComodule rho).action A)) g) z) = (Module.Dual.baseChangeEvaluation ξ) z

In the fixed-object representation--comodule dictionary, applying the same point to a finite-projective comodule and its dual preserves scalar-extended evaluation.

This is not a simp lemma because ofComodule_dual_action_evaluation and map_inv simplify its left-hand side first, so the simp-normal-form linter rejects the specialized orientation.