The monoidal point-representation--comodule equivalence

The category of finite natural point representations of an affine group has the same tensor and dual structures as the category of finite comodules over its coordinate Hopf algebra. This file transports the established monoidal structure on finite comodules across the categorical point-representation--comodule equivalence. The resulting equivalence is monoidal by construction. Commutativity of the coordinate Hopf algebra supplies the symmetric braiding, and over a field rigidity transports back along the monoidal equivalence.

Main declarations

• MonoidalCategory (TauCeti.FGPointRepresentationCat R H): the monoidal category of finite natural point representations.
• TauCeti.fgPointRepresentationCategoryEquivalence: now a monoidal equivalence with finite comodules.
• SymmetricCategory (TauCeti.FGPointRepresentationCat R H): the symmetry that exchanges tensor factors.
• RigidCategory (TauCeti.FGPointRepresentationCat k H): the rigid category of finite-dimensional point representations over a field.

References

• J. S. Milne, Basic Theory of Affine Group Schemes, Chapter VIII, §§2, 4, and 6.
• J. S. Milne, Algebraic Groups (2017), Chapter 4(a), Remark 4.1 and Proposition 9.44.

This completes the rigid monoidal refinement of the representation--comodule dictionary in Layer 1 of the ReductiveGroups roadmap.

@[instance_reducible]

noncomputable instance TauCeti.FGPointRepresentationCat.instMonoidalCategory (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : CategoryTheory.MonoidalCategory (FGPointRepresentationCat R H)

Finite natural point representations form a monoidal category. Its tensor structure is transported from the diagonal tensor product of finite comodules.

Equations

• TauCeti.FGPointRepresentationCat.instMonoidalCategory R H = CategoryTheory.Monoidal.transport (TauCeti.fgPointRepresentationCategoryEquivalence R H).symm

@[instance_reducible]

noncomputable instance TauCeti.FGPointRepresentationCat.instSymmetricCategory (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : CategoryTheory.SymmetricCategory (FGPointRepresentationCat R H)

Finite natural point representations form a symmetric monoidal category. The braiding is transported from the tensor-factor swap on finite comodules.

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.fgPointRepresentationCategoryEquivalenceFunctorMonoidal (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : (fgPointRepresentationCategoryEquivalence R H).functor.Monoidal

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.fgPointRepresentationCategoryEquivalenceInverseMonoidal (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : (fgPointRepresentationCategoryEquivalence R H).inverse.Monoidal

Equations

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

instance TauCeti.fgPointRepresentationCategoryEquivalence_isMonoidal (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : (fgPointRepresentationCategoryEquivalence R H).IsMonoidal

@[instance_reducible]

noncomputable instance TauCeti.fgPointRepresentationCategoryEquivalenceFunctorBraided (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : (fgPointRepresentationCategoryEquivalence R H).functor.Braided

The forward functor of the finite point-representation--comodule equivalence preserves the symmetric braiding.

Equations

• TauCeti.fgPointRepresentationCategoryEquivalenceFunctorBraided R H = { toMonoidal := TauCeti.fgPointRepresentationCategoryEquivalenceFunctorMonoidal R H, braided := ⋯ }

@[instance_reducible]

noncomputable instance TauCeti.fgPointRepresentationCategoryEquivalenceInverseBraided (R : Type u) [CommRing R] (H : Type v) [CommRing H] [HopfAlgebra R H] : (fgPointRepresentationCategoryEquivalence R H).inverse.Braided

The inverse functor of the finite point-representation--comodule equivalence preserves the symmetric braiding.

Equations

• TauCeti.fgPointRepresentationCategoryEquivalenceInverseBraided R H = { toMonoidal := TauCeti.fgPointRepresentationCategoryEquivalenceInverseMonoidal R H, braided := ⋯ }

@[instance_reducible]

noncomputable instance TauCeti.FGPointRepresentationCat.instRigidCategory (k : Type u) [Field k] (H : Type v) [CommRing H] [HopfAlgebra k H] : CategoryTheory.RigidCategory (FGPointRepresentationCat k H)

Finite-dimensional natural point representations over a field form a rigid monoidal category. The duals are transported from the antipode-twisted duals of finite comodules along the monoidal representation--comodule equivalence.

Equations

• TauCeti.FGPointRepresentationCat.instRigidCategory k H = CategoryTheory.rigidCategoryOfEquivalence (TauCeti.fgPointRepresentationCategoryEquivalence k H).toAdjunction