Actions in a cartesian monoidal category

If V is a cartesian monoidal category, the monoidal structure of Action V G (Mathlib's Action.instMonoidalCategory, the tensor product of the underlying objects with the diagonal action and the tensor unit with the trivial action) is cartesian: the projections of V are equivariant, and so is the map lift f g into a product for equivariant f and g. This file records the resulting CartesianMonoidalCategory (Action V G) instance, extending Mathlib's monoidal structure so that no second tensor product is introduced.

For a topological group G, the continuous actions on finite sets are closed under finite limits in Action FintypeCat G (Mathlib's Action.isContinuous), so the full subcategory ContAction FintypeCat G is cartesian monoidal as well, through Mathlib's CartesianMonoidalCategory.fullSubcategory. A group object in it is a finite group on which G acts continuously by group automorphisms; for G the absolute Galois group of a field, these correspond to the finite étale group schemes over the field (TauCeti.FiniteEtaleScheme.galoisEquivalenceGrp).

Main definitions

• Action.cartesianMonoidalCategory: the cartesian monoidal structure on Action V G, with Action.lift_hom and Action.toUnit_hom computing its maps on underlying objects.
• The instance CartesianMonoidalCategory (ContAction FintypeCat G), restricted from Action FintypeCat G, and the braiding it determines.

@[instance_reducible]

instance Action.cartesianMonoidalCategory {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.CartesianMonoidalCategory V] {G : Type u_2} [Monoid G] : CategoryTheory.CartesianMonoidalCategory (Action V G)

Actions in a cartesian monoidal category form a cartesian monoidal category. The product of two actions is the product of the underlying objects with the diagonal action, and the terminal object is the terminal object of V with the trivial action. This extends Mathlib's monoidal structure Action.instMonoidalCategory.

@[simp]

theorem Action.cartesianMonoidalCategory_fst_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.CartesianMonoidalCategory V] {G : Type u_2} [Monoid G] (X Y : Action V G) : (CategoryTheory.SemiCartesianMonoidalCategory.fst X Y).hom = CategoryTheory.SemiCartesianMonoidalCategory.fst X.V Y.V

@[simp]

theorem Action.cartesianMonoidalCategory_snd_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.CartesianMonoidalCategory V] {G : Type u_2} [Monoid G] (X Y : Action V G) : (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y).hom = CategoryTheory.SemiCartesianMonoidalCategory.snd X.V Y.V

@[simp]

theorem Action.lift_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.CartesianMonoidalCategory V] {G : Type u_2} [Monoid G] {T X Y : Action V G} (f : T ⟶ X) (g : T ⟶ Y) : (CategoryTheory.CartesianMonoidalCategory.lift f g).hom = CategoryTheory.CartesianMonoidalCategory.lift f.hom g.hom

The map into a product of actions is the map into the product of the underlying objects.

@[simp]

theorem Action.toUnit_hom {V : Type u_1} [CategoryTheory.Category.{v_1, u_1} V] [CategoryTheory.CartesianMonoidalCategory V] {G : Type u_2} [Monoid G] (X : Action V G) : (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X).hom = CategoryTheory.SemiCartesianMonoidalCategory.toUnit X.V

The map to the terminal action is the map to the terminal object of V.

@[instance_reducible]

noncomputable instance ContAction.braidedCategory (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : CategoryTheory.BraidedCategory (ContAction FintypeCat G)

The braiding of the cartesian monoidal structure on finite continuous G-sets, whose tensor product is the product of finite sets with the diagonal action.