Right rigidity of finite-dimensional comodules

Let H be a Hopf algebra over a field k. This file equips the monoidal category FGComoduleCat.{u,v,u} k H with right duals. The right dual of a finite-dimensional comodule is its antipode-twisted linear dual; evaluation and coevaluation are the ordinary finite-dimensional linear maps, proved colinear using the two antipode identities.

No commutativity or finite-dimensionality hypothesis is imposed on H, and the antipode need not be bijective.

Main declarations

• TauCeti.FGComoduleCat.dualEvaluation: evaluation as a finite-comodule morphism.
• TauCeti.FGComoduleCat.dualCoevaluation: coevaluation as a finite-comodule morphism.
• TauCeti.FGComoduleCat.instRightRigidCategory: finite-dimensional comodules form a right rigid monoidal category.

References

The exact-pairing packaging adapts the finite-dimensional module construction in Mathlib/Algebra/Category/FGModuleCat/Basic.lean.

See Etingof--Gelaki--Nikshych--Ostrik, Tensor Categories, Definition 2.10.1 and Remark 5.3.8; Milne, Algebraic Groups (2017), Section 9.26; and Humphreys, Linear Algebraic Groups, Section 8.2.

noncomputable def TauCeti.FGComoduleCat.dualEvaluation (k : Type u) [Field k] (H : Type v) [Semiring H] [HopfAlgebra k H] (M : FGComoduleCat k H) : CategoryTheory.MonoidalCategoryStruct.tensorObj (dual k H M) M ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGComoduleCat k H)

Evaluation of the antipode-twisted dual against a finite-dimensional comodule, as a finite-comodule morphism.

Equations

• TauCeti.FGComoduleCat.dualEvaluation k H M = TauCeti.FGComoduleCat.ofHom (let __LinearMap := contractLeft k ↑M; { toLinearMap := __LinearMap, map_coact := ⋯ })

@[simp]

theorem TauCeti.FGComoduleCat.dualEvaluation_apply (k : Type u) [Field k] (H : Type v) [Semiring H] [HopfAlgebra k H] (M : FGComoduleCat k H) (φ : ↑(dual k H M)) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (dualEvaluation k H M)) (φ ⊗ₜ[k] m) = φ m

Evaluation applies the underlying functional to the vector.

@[simp]

theorem TauCeti.FGComoduleCat.dualEvaluation_toLinearMap (k : Type u) [Field k] (H : Type v) [Semiring H] [HopfAlgebra k H] (M : FGComoduleCat k H) : (dualEvaluation k H M).hom.toLinearMap = contractLeft k ↑M

The underlying linear map of evaluation is ordinary contraction.

noncomputable def TauCeti.FGComoduleCat.dualCoevaluation (k : Type u) [Field k] (H : Type v) [Semiring H] [HopfAlgebra k H] (M : FGComoduleCat k H) : CategoryTheory.MonoidalCategoryStruct.tensorUnit (FGComoduleCat k H) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M (dual k H M)

The ordinary finite-dimensional coevaluation, as a finite-comodule morphism into the tensor product with the antipode-twisted dual.

Equations

• TauCeti.FGComoduleCat.dualCoevaluation k H M = TauCeti.FGComoduleCat.ofHom (let __LinearMap := coevaluation k ↑M; { toLinearMap := __LinearMap, map_coact := ⋯ })

theorem TauCeti.FGComoduleCat.dualCoevaluation_apply_one (k : Type u) [Field k] (H : Type v) [Semiring H] [HopfAlgebra k H] (M : FGComoduleCat k H) : (CategoryTheory.ConcreteCategory.hom (dualCoevaluation k H M)) 1 = ∑ i : ↑(Module.Basis.ofVectorSpaceIndex k ↑M), (Module.Basis.ofVectorSpace k ↑M) i ⊗ₜ[k] (Module.Basis.ofVectorSpace k ↑M).coord i

Coevaluation at one is the canonical basis-independent tensor.

@[simp]

theorem TauCeti.FGComoduleCat.dualCoevaluation_toLinearMap (k : Type u) [Field k] (H : Type v) [Semiring H] [HopfAlgebra k H] (M : FGComoduleCat k H) : (dualCoevaluation k H M).hom.toLinearMap = coevaluation k ↑M

The underlying linear map of coevaluation is ordinary finite-dimensional coevaluation.

@[instance_reducible]

noncomputable instance TauCeti.FGComoduleCat.instExactPairingDual (k : Type u) [Field k] (H : Type v) [Semiring H] [HopfAlgebra k H] (M : FGComoduleCat k H) : CategoryTheory.ExactPairing M (dual k H M)

The antipode-twisted linear dual is an exact right dual of a finite-dimensional comodule.

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.FGComoduleCat.instHasRightDual (k : Type u) [Field k] (H : Type v) [Semiring H] [HopfAlgebra k H] (M : FGComoduleCat k H) : CategoryTheory.HasRightDual M

Every finite-dimensional comodule has the antipode-twisted linear dual as a right dual.

Equations

• TauCeti.FGComoduleCat.instHasRightDual k H M = { rightDual := TauCeti.FGComoduleCat.dual k H M, exact := TauCeti.FGComoduleCat.instExactPairingDual k H M }

@[instance_reducible]

noncomputable instance TauCeti.FGComoduleCat.instRightRigidCategory (k : Type u) [Field k] (H : Type v) [Semiring H] [HopfAlgebra k H] : CategoryTheory.RightRigidCategory (FGComoduleCat k H)

Finite-dimensional comodules over a Hopf algebra form a right rigid monoidal category.

Equations

• TauCeti.FGComoduleCat.instRightRigidCategory k H = { rightDual := TauCeti.FGComoduleCat.instHasRightDual k H }