Evaluation and dual point actions

For a finite-projective right comodule M over a Hopf algebra, this file relates the point action on its antipode-twisted dual comodule to the original point action. The canonical A-valued pairing between A ⊗[R] Module.Dual R M and A ⊗[R] M satisfies

⟨g · ξ, z⟩ = ⟨ξ, g⁻¹ · z⟩.

Equivalently, acting by the same point on both inputs preserves evaluation. On pure tensors, both sides are the inverse point evaluated at the existing matrix coefficient, multiplied by the two scalar factors. The basis-free proof uses the characteristic equation for Comodule.dualCoact; it does not identify the scalar extension of the dual with the full dual of the scalar extension.

The action-level results hold for a possibly noncommutative Hopf algebra over a commutative semiring.

Main declarations

• TauCeti.Comodule.baseChangeEvaluation_endOfPoint_tmul: evaluation after a point acts on a pure tensor.
• TauCeti.Comodule.baseChangeEvaluation_dual_endOfPoint: adjointness of the dual point action and the inverse original point action.
• TauCeti.Comodule.baseChangeEvaluation_dual_endOfPoint_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.

@[simp]

theorem TauCeti.Comodule.baseChangeEvaluation_endOfPoint_tmul {R : Type u} {H : Type v} {M : Type w} {A : Type x} [CommSemiring R] [Semiring H] [Algebra R H] [Coalgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [CommSemiring A] [Algebra R A] (g : H →ₐ[R] A) (a b : A) (φ : Module.Dual R M) (m : M) : (Module.Dual.baseChangeEvaluation (a ⊗ₜ[R] φ)) ((endOfPoint M g) (b ⊗ₜ[R] m)) = a * b * g (matrixCoefficient φ m)

Pairing a scalar-extended functional with a point acting on a pure tensor evaluates the point at the corresponding matrix coefficient.

@[simp]

theorem TauCeti.Comodule.baseChangeEvaluation_dual_endOfPoint_tmul {R : Type u} {H : Type v} {M : Type w} {A : Type x} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [Module.Finite R M] [Module.Projective R M] [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) (a b : A) (φ : Module.Dual R M) (m : M) : (Module.Dual.baseChangeEvaluation ((endOfPoint (Module.Dual R M) g.ofConv) (a ⊗ₜ[R] φ))) (b ⊗ₜ[R] m) = a * b * g⁻¹.ofConv (matrixCoefficient φ m)

On pure tensors, acting on the dual leg and then evaluating gives the inverse point applied to the original matrix coefficient, together with the two scalar factors.

@[simp]

theorem TauCeti.Comodule.baseChangeEvaluation_dual_endOfPoint {R : Type u} {H : Type v} {M : Type w} {A : Type x} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [Module.Finite R M] [Module.Projective R M] [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) (ξ : TensorProduct R A (Module.Dual R M)) (z : TensorProduct R A M) : (Module.Dual.baseChangeEvaluation ((endOfPoint (Module.Dual R M) g.ofConv) ξ)) z = (Module.Dual.baseChangeEvaluation ξ) ((endOfPoint M g⁻¹.ofConv) z)

The point action on the antipode-twisted dual comodule is adjoint, under canonical scalar-extended evaluation, to the original point action at the inverse point.

@[simp]

theorem TauCeti.Comodule.baseChangeEvaluation_dual_endOfPoint_invariant {R : Type u} {H : Type v} {M : Type w} {A : Type x} [CommSemiring R] [Semiring H] [HopfAlgebra R H] [AddCommMonoid M] [Module R M] [Comodule R H M] [Module.Finite R M] [Module.Projective R M] [CommSemiring A] [Algebra R A] (g : WithConv (H →ₐ[R] A)) (ξ : TensorProduct R A (Module.Dual R M)) (z : TensorProduct R A M) : (Module.Dual.baseChangeEvaluation ((endOfPoint (Module.Dual R M) g.ofConv) ξ)) ((endOfPoint M g.ofConv) z) = (Module.Dual.baseChangeEvaluation ξ) z

Acting by the same point on a finite-projective comodule and its antipode-twisted dual preserves the canonical scalar-extended evaluation pairing.