Translation by a point of a group object

Let G be a group object in a cartesian monoidal category C. A global point x : 𝟙_ C ⟶ G acts on G by left translation y ↦ x * y. In terms of points with values in an object Y, the translation sends f : Y ⟶ G to the product of the constant point toUnit Y ≫ x and f. It is an automorphism of G, with inverse the translation by x⁻¹, and a homomorphism of group objects i : H ⟶ G intertwines translation by x on H with translation by x ≫ i on G.

For a group scheme G over S, these are the translations of G by its S-points, which move closed subschemes of G around; a closed subgroup scheme is stable under translation by its own points.

More generally, a point φ : Y ⟶ G with values in an object Y acts on G ⊗ Y, the base change of G to Y, by (g, y) ↦ (φ y * g, y). For a group scheme G over S and a scheme Y over S, this is left translation of G ×_S Y over Y by the Y-point of G ×_S Y given by φ; it moves points of G that are not defined over the base, such as the tautological point Y = G, φ = 𝟙 G.

Main definitions

• TauCeti.rightTranslation x: right translation by a global point, as an isomorphism.
• TauCeti.leftTranslation x: left translation by x, as an isomorphism G ≅ G.
• TauCeti.leftTranslationProd φ: left translation by a point φ : Y ⟶ G, as an isomorphism G ⊗ Y ≅ G ⊗ Y.

Main results

• TauCeti.comp_leftTranslation_hom: translation by x sends a point f to x * f.
• TauCeti.leftTranslation_hom_comp: a homomorphism i intertwines translation by x with translation by x ≫ i.
• TauCeti.lift_comp_leftTranslationProd_hom: translation by φ sends a point (a, b) of G ⊗ Y to ((b ≫ φ) * a, b).
• TauCeti.leftTranslationProd_hom_comp_whiskerRight: a homomorphism i intertwines translation by φ with translation by φ ≫ i.

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

Left translation y ↦ x * y on a group object G by a global point x : 𝟙_ C ⟶ G, as an automorphism of G. Its inverse is the translation by x⁻¹.

theorem TauCeti.leftTranslation_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ G) : (leftTranslation x).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit G) x * CategoryTheory.CategoryStruct.id G

Translation by x is the product of the constant point x and the identity of G.

@[simp]

theorem TauCeti.leftTranslation_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ G) : (leftTranslation x).inv = (leftTranslation x⁻¹).hom

The inverse of translation by x is translation by x⁻¹.

@[simp]

theorem TauCeti.comp_leftTranslation_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] {Y : C} (f : Y ⟶ G) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ G) : CategoryTheory.CategoryStruct.comp f (leftTranslation x).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit Y) x * f

Translation by x sends a point f : Y ⟶ G to x * f.

@[simp]

theorem TauCeti.comp_leftTranslation_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] {Y : C} (f : Y ⟶ G) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ G) {Z : C} (h : G ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (leftTranslation x).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit Y) x * f) h

Translation by x sends a point f : Y ⟶ G to x * f.

theorem TauCeti.leftTranslation_hom_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] {H : C} [CategoryTheory.GrpObj H] (i : H ⟶ G) [CategoryTheory.IsMonHom i] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ H) : CategoryTheory.CategoryStruct.comp (leftTranslation x).hom i = CategoryTheory.CategoryStruct.comp i (leftTranslation (CategoryTheory.CategoryStruct.comp x i)).hom

A homomorphism of group objects i : H ⟶ G intertwines translation by a point x of H with translation by its image x ≫ i.

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

Right translation y ↦ y * x by a global group point, with inverse given by x⁻¹.

theorem TauCeti.rightTranslation_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ G) : (rightTranslation x).hom = CategoryTheory.CategoryStruct.id G * CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit G) x

The morphism underlying right translation is right multiplication by the constant point.

@[simp]

theorem TauCeti.rightTranslation_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ G) : (rightTranslation x).inv = (rightTranslation x⁻¹).hom

The inverse of right translation is right translation by the inverse point.

@[simp]

theorem TauCeti.comp_rightTranslation_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] {Y : C} (f : Y ⟶ G) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ G) : CategoryTheory.CategoryStruct.comp f (rightTranslation x).hom = f * CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit Y) x

Right translation acts on every test-object point by right multiplication.

@[simp]

theorem TauCeti.comp_rightTranslation_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] {Y : C} (f : Y ⟶ G) (x : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ G) {Z : C} (h : G ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (rightTranslation x).hom h) = CategoryTheory.CategoryStruct.comp (f * CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit Y) x) h

Right translation acts on every test-object point by right multiplication.

Translation by a point with values in an object

noncomputable def TauCeti.leftTranslationProd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] {Y : C} (φ : Y ⟶ G) : CategoryTheory.MonoidalCategoryStruct.tensorObj G Y ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj G Y

Left translation by a point with values in Y. For a point φ : Y ⟶ G, the automorphism (g, y) ↦ (φ y * g, y) of G ⊗ Y, the base change of G to Y. Its inverse is the translation by φ⁻¹.

theorem TauCeti.leftTranslationProd_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] {Y : C} (φ : Y ⟶ G) : (leftTranslationProd φ).hom = CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd G Y) φ * CategoryTheory.SemiCartesianMonoidalCategory.fst G Y) (CategoryTheory.SemiCartesianMonoidalCategory.snd G Y)

Translation by φ is (g, y) ↦ (φ y * g, y).

@[simp]

theorem TauCeti.leftTranslationProd_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] {Y : C} (φ : Y ⟶ G) : (leftTranslationProd φ).inv = (leftTranslationProd φ⁻¹).hom

The inverse of translation by φ is translation by φ⁻¹.

@[simp]

theorem TauCeti.lift_comp_leftTranslationProd_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] {Y Z : C} (a : Z ⟶ G) (b : Z ⟶ Y) (φ : Y ⟶ G) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift a b) (leftTranslationProd φ).hom = CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp b φ * a) b

Translation by φ sends a point (a, b) of G ⊗ Y to ((b ≫ φ) * a, b).

@[simp]

theorem TauCeti.lift_comp_leftTranslationProd_hom_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] {Y Z : C} (a : Z ⟶ G) (b : Z ⟶ Y) (φ : Y ⟶ G) {Z✝ : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj G Y ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift a b) (CategoryTheory.CategoryStruct.comp (leftTranslationProd φ).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp b φ * a) b) h

Translation by φ sends a point (a, b) of G ⊗ Y to ((b ≫ φ) * a, b).

@[simp]

theorem TauCeti.leftTranslationProd_hom_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] {Y : C} (φ : Y ⟶ G) : CategoryTheory.CategoryStruct.comp (leftTranslationProd φ).hom (CategoryTheory.SemiCartesianMonoidalCategory.fst G Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd G Y) φ * CategoryTheory.SemiCartesianMonoidalCategory.fst G Y

The first component of the translate of (g, y) by φ is φ y * g.

@[simp]

theorem TauCeti.leftTranslationProd_hom_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] {Y : C} (φ : Y ⟶ G) {Z : C} (h : G ⟶ Z) : CategoryTheory.CategoryStruct.comp (leftTranslationProd φ).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst G Y) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd G Y) φ * CategoryTheory.SemiCartesianMonoidalCategory.fst G Y) h

The first component of the translate of (g, y) by φ is φ y * g.

@[simp]

theorem TauCeti.leftTranslationProd_hom_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] {Y : C} (φ : Y ⟶ G) : CategoryTheory.CategoryStruct.comp (leftTranslationProd φ).hom (CategoryTheory.SemiCartesianMonoidalCategory.snd G Y) = CategoryTheory.SemiCartesianMonoidalCategory.snd G Y

Translation by φ lies over Y.

@[simp]

theorem TauCeti.leftTranslationProd_hom_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] {Y : C} (φ : Y ⟶ G) {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (leftTranslationProd φ).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd G Y) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd G Y) h

Translation by φ lies over Y.

theorem TauCeti.leftTranslationProd_hom_comp_whiskerRight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] {Y H : C} [CategoryTheory.GrpObj H] (i : G ⟶ H) [CategoryTheory.IsMonHom i] (φ : Y ⟶ G) : CategoryTheory.CategoryStruct.comp (leftTranslationProd φ).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight i Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight i Y) (leftTranslationProd (CategoryTheory.CategoryStruct.comp φ i)).hom

A homomorphism of group objects i : G ⟶ H intertwines translation by a point φ of G with translation by its image φ ≫ i.

theorem TauCeti.leftTranslationProd_hom_comp_whiskerRight_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G : C} [CategoryTheory.GrpObj G] {Y H : C} [CategoryTheory.GrpObj H] (i : G ⟶ H) [CategoryTheory.IsMonHom i] (φ : Y ⟶ G) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj H Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (leftTranslationProd φ).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight i Y) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight i Y) (CategoryTheory.CategoryStruct.comp (leftTranslationProd (CategoryTheory.CategoryStruct.comp φ i)).hom h)

A homomorphism of group objects i : G ⟶ H intertwines translation by a point φ of G with translation by its image φ ≫ i.