Semidirect products of internal groups

Let G and N be group objects in a cartesian monoidal category. An internal left action of G on N is a morphism G ⊗ N ⟶ N whose action on generalized points is unital, multiplicative in G, and by group automorphisms of N. This file packages those three laws and constructs the internal semidirect product N ⋊ G on the product object N ⊗ G.

The construction is characterized on every generalized-point group. The points of the internal semidirect product are naturally the ordinary SemidirectProduct of the point groups. This gives the group-object laws without choosing elements of the ambient category and exposes the familiar component formulas to downstream constructions.

Main declarations

• TauCeti.GrpObj.Action: an internal action by group automorphisms.
• TauCeti.GrpObj.Action.toMulAutHom: the induced action on generalized points.
• TauCeti.GrpObj.Action.semidirectProduct: the internal semidirect-product group object.
• TauCeti.GrpObj.Action.pointMulEquiv: its generalized points are an ordinary semidirect product.

References

• W. C. Waterhouse, Introduction to Affine Group Schemes, §§15--16.
• J. S. Milne, Algebraic Groups (2017), §6.a.

This is a prerequisite for Layer 5, "The unipotent radical", of the ReductiveGroups roadmap. For two normal closed subgroup schemes, conjugation supplies the action below; multiplication from their semidirect product is then a group-scheme morphism whose image is their product.

structure TauCeti.GrpObj.Action {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] (G N : C) [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] : Type v

An action of the internal group G on the internal group N.

The morphism hom : G ⊗ N ⟶ N is required to induce a left group action on generalized points, and each element of G(X) must act multiplicatively on N(X). The latter condition makes the action one by group automorphisms; its inverse is the action of the inverse generalized point.

• hom : CategoryTheory.MonoidalCategoryStruct.tensorObj G N ⟶ N

  The action morphism G ⊗ N ⟶ N.

• one_act (X : C) (n : X ⟶ N) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift 1 n) self.hom = n

  The identity generalized point acts trivially.

• mul_act (X : C) (g h : X ⟶ G) (n : X ⟶ N) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (g * h) n) self.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g (CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift h n) self.hom)) self.hom

  Multiplication of generalized points acts by composition, in left-action order.

• act_mul (X : C) (g : X ⟶ G) (n m : X ⟶ N) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g (n * m)) self.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g n) self.hom * CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g m) self.hom

  Every generalized point acts multiplicatively on the point group of N.

theorem TauCeti.GrpObj.Action.ext {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A B : Action G N) (h : A.hom = B.hom) : A = B

Internal actions are determined by their action morphisms.

theorem TauCeti.GrpObj.Action.ext_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] {A B : Action G N} : A = B ↔ A.hom = B.hom

def TauCeti.GrpObj.Action.act {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) {X : C} (g : X ⟶ G) (n : X ⟶ N) : X ⟶ N

The action of a generalized point of G on a generalized point of N.

Equations

• A.act g n = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g n) A.hom

theorem TauCeti.GrpObj.Action.act_def {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) {X : C} (g : X ⟶ G) (n : X ⟶ N) : A.act g n = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g n) A.hom

The action on generalized points is induced by the action morphism.

@[simp]

theorem TauCeti.GrpObj.Action.one_act_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) {X : C} (n : X ⟶ N) : A.act 1 n = n

@[simp]

theorem TauCeti.GrpObj.Action.mul_act_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) {X : C} (g h : X ⟶ G) (n : X ⟶ N) : A.act (g * h) n = A.act g (A.act h n)

@[simp]

theorem TauCeti.GrpObj.Action.act_mul_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) {X : C} (g : X ⟶ G) (n m : X ⟶ N) : A.act g (n * m) = A.act g n * A.act g m

theorem TauCeti.GrpObj.Action.comp_act {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) {X Y : C} (f : X ⟶ Y) (g : Y ⟶ G) (n : Y ⟶ N) : CategoryTheory.CategoryStruct.comp f (A.act g n) = A.act (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f n)

Internal actions commute with precomposition of generalized points.

theorem TauCeti.GrpObj.Action.comp_act_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) {X Y : C} (f : X ⟶ Y) (g : Y ⟶ G) (n : Y ⟶ N) {Z : C} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (A.act g n) h) = CategoryTheory.CategoryStruct.comp (A.act (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f n)) h

Internal actions commute with precomposition of generalized points.

def TauCeti.GrpObj.Action.toMulAut {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) {X : C} (g : X ⟶ G) : MulAut (X ⟶ N)

A generalized point of G acts as an automorphism of the generalized-point group of N.

Equations

• A.toMulAut g = { toFun := A.act g, invFun := A.act g⁻¹, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.GrpObj.Action.toMulAut_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) {X : C} (g : X ⟶ G) (n : X ⟶ N) : (A.toMulAut g) n = A.act g n

@[simp]

theorem TauCeti.GrpObj.Action.act_one_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) {X : C} (g : X ⟶ G) : A.act g 1 = 1

def TauCeti.GrpObj.Action.toMulAutHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) (X : C) : (X ⟶ G) →* MulAut (X ⟶ N)

The action homomorphism from generalized points of G to automorphisms of the generalized points of N.

Equations

• A.toMulAutHom X = { toFun := A.toMulAut, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.GrpObj.Action.toMulAutHom_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) {X : C} (g : X ⟶ G) (n : X ⟶ N) : ((A.toMulAutHom X) g) n = A.act g n

@[instance_reducible]

noncomputable def TauCeti.GrpObj.Action.semidirectProductGrpObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) : CategoryTheory.GrpObj (CategoryTheory.MonoidalCategoryStruct.tensorObj N G)

The group-object structure on N ⊗ G representing the pointwise semidirect product.

Equations

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

@[reducible, inline]

noncomputable abbrev TauCeti.GrpObj.Action.semidirectProduct {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) : CategoryTheory.Grp C

The internal semidirect product associated to an internal action. Its underlying object is the categorical product N ⊗ G.

Equations

• A.semidirectProduct = { X := CategoryTheory.MonoidalCategoryStruct.tensorObj N G, grp := A.semidirectProductGrpObj }

noncomputable def TauCeti.GrpObj.Action.pointMulEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) (X : C) : (X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj N G) ≃* (X ⟶ N) ⋊[A.toMulAutHom X] (X ⟶ G)

Generalized points of the internal semidirect product are naturally the ordinary semidirect product of the generalized-point groups.

Equations

• A.pointMulEquiv X = ((TauCeti.GrpObj.Action.pointIso✝ A).app (Opposite.op X)).groupIsoToMulEquiv

@[simp]

theorem TauCeti.GrpObj.Action.pointMulEquiv_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) {X : C} (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj N G) : ((A.pointMulEquiv X) f).left = CategoryTheory.CategoryStruct.comp f (CategoryTheory.SemiCartesianMonoidalCategory.fst N G)

@[simp]

theorem TauCeti.GrpObj.Action.pointMulEquiv_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) {X : C} (f : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj N G) : ((A.pointMulEquiv X) f).right = CategoryTheory.CategoryStruct.comp f (CategoryTheory.SemiCartesianMonoidalCategory.snd N G)

@[simp]

theorem TauCeti.GrpObj.Action.pointMulEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) {X : C} (f : (X ⟶ N) ⋊[A.toMulAutHom X] (X ⟶ G)) : (A.pointMulEquiv X).symm f = CategoryTheory.CartesianMonoidalCategory.lift f.left f.right

noncomputable def TauCeti.GrpObj.Action.inl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) : { X := N, grp := inst✝ } ⟶ A.semidirectProduct

The canonical inclusion N ⟶ N ⋊ G of internal groups.

Equations

• A.inl = CategoryTheory.yonedaGrpFullyFaithful.preimage (CategoryTheory.CategoryStruct.comp (TauCeti.GrpObj.Action.inlNatTrans✝ A) (TauCeti.GrpObj.Action.pointIso✝ A).inv)

noncomputable def TauCeti.GrpObj.Action.inr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) : { X := G, grp := inst✝ } ⟶ A.semidirectProduct

The canonical inclusion G ⟶ N ⋊ G of internal groups.

Equations

• A.inr = CategoryTheory.yonedaGrpFullyFaithful.preimage (CategoryTheory.CategoryStruct.comp (TauCeti.GrpObj.Action.inrNatTrans✝ A) (TauCeti.GrpObj.Action.pointIso✝ A).inv)

noncomputable def TauCeti.GrpObj.Action.rightHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) : A.semidirectProduct ⟶ { X := G, grp := inst✝ }

The canonical projection N ⋊ G ⟶ G of internal groups.

Equations

• A.rightHom = CategoryTheory.yonedaGrpFullyFaithful.preimage (CategoryTheory.CategoryStruct.comp (TauCeti.GrpObj.Action.pointIso✝ A).hom (TauCeti.GrpObj.Action.rightHomNatTrans✝ A))

@[simp]

theorem TauCeti.GrpObj.Action.pointMulEquiv_comp_inl {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) {X : C} (n : X ⟶ N) : (A.pointMulEquiv X) (CategoryTheory.CategoryStruct.comp n A.inl.hom.hom) = SemidirectProduct.inl n

On generalized points, the first canonical inclusion is SemidirectProduct.inl.

@[simp]

theorem TauCeti.GrpObj.Action.pointMulEquiv_comp_inr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) {X : C} (g : X ⟶ G) : (A.pointMulEquiv X) (CategoryTheory.CategoryStruct.comp g A.inr.hom.hom) = SemidirectProduct.inr g

On generalized points, the second canonical inclusion is SemidirectProduct.inr.

@[simp]

theorem TauCeti.GrpObj.Action.inl_hom_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) : CategoryTheory.CategoryStruct.comp A.inl.hom.hom (CategoryTheory.SemiCartesianMonoidalCategory.fst N G) = CategoryTheory.CategoryStruct.id N

The first projection of the canonical inclusion of the normal factor is the identity.

theorem TauCeti.GrpObj.Action.inl_hom_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) {Z : C} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp A.inl.hom.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst N G) h) = h

The first projection of the canonical inclusion of the normal factor is the identity.

@[simp]

theorem TauCeti.GrpObj.Action.inl_hom_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) : CategoryTheory.CategoryStruct.comp A.inl.hom.hom (CategoryTheory.SemiCartesianMonoidalCategory.snd N G) = 1

The second projection of the canonical inclusion of the normal factor is the unit.

theorem TauCeti.GrpObj.Action.inl_hom_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) {Z : C} (h : G ⟶ Z) : CategoryTheory.CategoryStruct.comp A.inl.hom.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd N G) h) = CategoryTheory.CategoryStruct.comp 1 h

The second projection of the canonical inclusion of the normal factor is the unit.

@[simp]

theorem TauCeti.GrpObj.Action.inr_hom_fst {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) : CategoryTheory.CategoryStruct.comp A.inr.hom.hom (CategoryTheory.SemiCartesianMonoidalCategory.fst N G) = 1

The first projection of the canonical inclusion of the acting factor is the unit.

theorem TauCeti.GrpObj.Action.inr_hom_fst_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) {Z : C} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp A.inr.hom.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst N G) h) = CategoryTheory.CategoryStruct.comp 1 h

The first projection of the canonical inclusion of the acting factor is the unit.

@[simp]

theorem TauCeti.GrpObj.Action.inr_hom_snd {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) : CategoryTheory.CategoryStruct.comp A.inr.hom.hom (CategoryTheory.SemiCartesianMonoidalCategory.snd N G) = CategoryTheory.CategoryStruct.id G

The second projection of the canonical inclusion of the acting factor is the identity.

theorem TauCeti.GrpObj.Action.inr_hom_snd_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) {Z : C} (h : G ⟶ Z) : CategoryTheory.CategoryStruct.comp A.inr.hom.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd N G) h) = h

The second projection of the canonical inclusion of the acting factor is the identity.

@[simp]

theorem TauCeti.GrpObj.Action.comp_rightHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] (A : Action G N) {X : C} (x : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj N G) : CategoryTheory.CategoryStruct.comp x A.rightHom.hom.hom = SemidirectProduct.rightHom ((A.pointMulEquiv X) x)

On generalized points, the canonical projection is SemidirectProduct.rightHom.