Orbit morphisms and translations for internal actions

An action in a cartesian monoidal category gives an orbit morphism from the acting monoid to the acted-on object for each global point. For a group object, translation by a global group point is an automorphism. The orbit morphism intertwines left translation on the group with translation on the acted-on object. Moving its base point corresponds instead to right multiplication on the group.

These constructions apply in particular to group schemes acting on schemes over a base. All identities are identities of morphisms, rather than only of global points. They use Mathlib's Hom.mulAction and the existing group-object TauCeti.leftTranslation.

def TauCeti.orbitMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (G : C) [CategoryTheory.MonObj G] {X : C} [CategoryTheory.ModObj G X] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X) : G ⟶ X

The orbit morphism of a global point, sending g to g • x.

@[simp]

theorem TauCeti.comp_orbitMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (G : C) [CategoryTheory.MonObj G] {X : C} [CategoryTheory.ModObj G X] {T : C} (g : T ⟶ G) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X) : CategoryTheory.CategoryStruct.comp g (orbitMap G x) = g • CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit T) x

Evaluation of the orbit morphism on an arbitrary test-object point.

@[simp]

theorem TauCeti.comp_orbitMap_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (G : C) [CategoryTheory.MonObj G] {X : C} [CategoryTheory.ModObj G X] {T : C} (g : T ⟶ G) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (orbitMap G x) h) = CategoryTheory.CategoryStruct.comp (g • CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit T) x) h

Evaluation of the orbit morphism on an arbitrary test-object point.

theorem TauCeti.mul_orbitMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (G : C) [CategoryTheory.MonObj G] {X : C} [CategoryTheory.ModObj G X] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (orbitMap G x) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G (orbitMap G x)) CategoryTheory.ModObj.smul

The orbit morphism intertwines multiplication with the action morphism.

theorem TauCeti.mul_orbitMap_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (G : C) [CategoryTheory.MonObj G] {X : C} [CategoryTheory.ModObj G X] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul (CategoryTheory.CategoryStruct.comp (orbitMap G x) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G (orbitMap G x)) (CategoryTheory.CategoryStruct.comp CategoryTheory.ModObj.smul h)

The orbit morphism intertwines multiplication with the action morphism.

theorem TauCeti.orbitMap_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (G : C) [CategoryTheory.MonObj G] {X Y : C} [CategoryTheory.ModObj G X] [CategoryTheory.ModObj G Y] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X) (f : X ⟶ Y) [CategoryTheory.IsModHom G f] : CategoryTheory.CategoryStruct.comp (orbitMap G x) f = orbitMap G (CategoryTheory.CategoryStruct.comp x f)

An equivariant morphism carries an orbit morphism to the orbit morphism of the image.

theorem TauCeti.orbitMap_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (G : C) [CategoryTheory.MonObj G] {X Y : C} [CategoryTheory.ModObj G X] [CategoryTheory.ModObj G Y] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X) (f : X ⟶ Y) [CategoryTheory.IsModHom G f] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (orbitMap G x) (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp (orbitMap G (CategoryTheory.CategoryStruct.comp x f)) h

An equivariant morphism carries an orbit morphism to the orbit morphism of the image.

noncomputable def TauCeti.translation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] (X : C) [CategoryTheory.ModObj G X] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ G) : X ≅ X

Translation of an acted-on object by a global group point.

@[simp]

theorem TauCeti.comp_translation_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G X : C} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] {T : C} (x : T ⟶ X) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ G) : CategoryTheory.CategoryStruct.comp x (translation X g).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit T) g • x

Translation acts on points by the native test-object action.

@[simp]

theorem TauCeti.comp_translation_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G X : C} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] {T : C} (x : T ⟶ X) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ G) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp x (CategoryTheory.CategoryStruct.comp (translation X g).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit T) g • x) h

Translation acts on points by the native test-object action.

@[simp]

theorem TauCeti.comp_translation_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G X : C} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] {T : C} (x : T ⟶ X) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ G) : CategoryTheory.CategoryStruct.comp x (translation X g).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit T) g⁻¹ • x

Inverse translation acts by the inverse group point.

@[simp]

theorem TauCeti.comp_translation_inv_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G X : C} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] {T : C} (x : T ⟶ X) (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ G) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp x (CategoryTheory.CategoryStruct.comp (translation X g).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit T) g⁻¹ • x) h

Inverse translation acts by the inverse group point.

@[simp]

theorem TauCeti.translation_one {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G X : C} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] : translation X 1 = CategoryTheory.Iso.refl X

Translation by the identity is the identity isomorphism.

@[simp]

theorem TauCeti.translation_mul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G X : C} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] (g h : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ G) : translation X (g * h) = translation X h ≪≫ translation X g

Translation by a product composes translations in action order.

@[simp]

theorem TauCeti.translation_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G X : C} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ G) : translation X g⁻¹ = (translation X g).symm

Translation by the inverse point is the inverse translation isomorphism.

theorem TauCeti.translation_hom_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G X Y : C} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] [CategoryTheory.ModObj G Y] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ G) (f : X ⟶ Y) [CategoryTheory.IsModHom G f] : CategoryTheory.CategoryStruct.comp (translation X g).hom f = CategoryTheory.CategoryStruct.comp f (translation Y g).hom

Equivariant morphisms intertwine translations.

theorem TauCeti.translation_hom_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G X Y : C} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] [CategoryTheory.ModObj G Y] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ G) (f : X ⟶ Y) [CategoryTheory.IsModHom G f] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (translation X g).hom (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (translation Y g).hom h)

Equivariant morphisms intertwine translations.

theorem TauCeti.leftTranslation_hom_orbitMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G X : C} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ G) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X) : CategoryTheory.CategoryStruct.comp (leftTranslation g).hom (orbitMap G x) = CategoryTheory.CategoryStruct.comp (orbitMap G x) (translation X g).hom

The orbit morphism intertwines left translation with the action on its target.

theorem TauCeti.leftTranslation_hom_orbitMap_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G X : C} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ G) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X) {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (leftTranslation g).hom (CategoryTheory.CategoryStruct.comp (orbitMap G x) h) = CategoryTheory.CategoryStruct.comp (orbitMap G x) (CategoryTheory.CategoryStruct.comp (translation X g).hom h)

The orbit morphism intertwines left translation with the action on its target.

theorem TauCeti.orbitMap_smul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G X : C} [CategoryTheory.GrpObj G] [CategoryTheory.ModObj G X] (g : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ G) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X) : orbitMap G (g • x) = CategoryTheory.CategoryStruct.comp (rightTranslation g).hom (orbitMap G x)

Moving the base point of an orbit morphism amounts to right multiplication on the group. The order of multiplication matters for a noncommutative group.

theorem CategoryTheory.Functor.map_orbitMap {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [CartesianMonoidalCategory C] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] (G X : C) [MonObj G] [ModObj G X] (x : MonoidalCategoryStruct.tensorUnit C ⟶ X) : F.map (TauCeti.orbitMap G x) = TauCeti.orbitMap (F.obj G) (CategoryStruct.comp (LaxMonoidal.ε F) (F.map x))

A monoidal functor between cartesian categories preserves orbit morphisms, with the base point transported by its unit comparison.