Multiplication from semidirect products of internal subgroups

Let i : N ⟶ G be a normal subgroup object and let j : H ⟶ G be another internal-group homomorphism. Conjugation through j gives an action of H on N. This file constructs that action and the canonical internal-group homomorphism

N ⋊ H ⟶ G,    (n, h) ↦ i(n) * j(h).

The construction is characterized on generalized points and on the two canonical inclusions. For two normal closed subgroup schemes, its scheme-theoretic image is their product. This is the binary-product map used in the maximal-dimension construction of the unipotent radical.

Main declarations

• TauCeti.GrpObj.Action.normalConjugation: conjugation along a map into the ambient group.
• TauCeti.GrpObj.Action.normalSemidirectMul: multiplication from the resulting semidirect product into the ambient group.

References

• J. S. Milne, Algebraic Groups (2017), Proposition 6.42 and §6.a.
• A. Borel, Linear Algebraic Groups, Proposition 14.4.

This advances Layer 5, "The unipotent radical", of the ReductiveGroups roadmap. It supplies the group-scheme multiplication homomorphism whose scheme-theoretic image is the product of two normal connected smooth unipotent closed subgroups.

noncomputable def TauCeti.GrpObj.Action.normalConjugation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N H : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] [CategoryTheory.GrpObj H] (i : N ⟶ G) [CategoryTheory.IsMonHom.Normal i] (j : H ⟶ G) [CategoryTheory.IsMonHom j] : Action H N

Conjugation by an internal group mapping to G acts on a normal subgroup object of G.

If i : N ⟶ G is normal and j : H ⟶ G is an internal-group homomorphism, the action sends (h, n) to the unique element of N whose image in G is j(h) * i(n) * j(h)⁻¹.

Equations

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

@[simp]

theorem TauCeti.GrpObj.Action.normalConjugation_act {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N H X : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] [CategoryTheory.GrpObj H] (i : N ⟶ G) [CategoryTheory.IsMonHom.Normal i] (j : H ⟶ G) [CategoryTheory.IsMonHom j] (h : X ⟶ H) (n : X ⟶ N) : (normalConjugation i j).act h n = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp h j) n) (TauCeti.normalConjugation i)

The action by conjugation along j evaluates as ambient conjugation through j.

noncomputable def TauCeti.GrpObj.Action.normalSemidirectMul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N H : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] [CategoryTheory.GrpObj H] (i : N ⟶ G) [CategoryTheory.IsMonHom.Normal i] (j : H ⟶ G) [CategoryTheory.IsMonHom j] : have A := normalConjugation i j; A.semidirectProduct ⟶ { X := G, grp := inst✝ }

Multiplication from the semidirect product determined by a normal subgroup map.

On generalized points this sends (n, h) to i(n) * j(h).

Equations

• TauCeti.GrpObj.Action.normalSemidirectMul i j = CategoryTheory.yonedaGrpFullyFaithful.preimage (TauCeti.GrpObj.Action.normalSemidirectMulNatTrans✝ i j)

@[simp]

theorem TauCeti.GrpObj.Action.comp_normalSemidirectMul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N H X : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] [CategoryTheory.GrpObj H] (i : N ⟶ G) [CategoryTheory.IsMonHom.Normal i] (j : H ⟶ G) [CategoryTheory.IsMonHom j] (x : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj N H) : have A := normalConjugation i j; CategoryTheory.CategoryStruct.comp x (normalSemidirectMul i j).hom.hom = CategoryTheory.CategoryStruct.comp x (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.fst N H) i) * CategoryTheory.CategoryStruct.comp x (CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.snd N H) j)

Normal semidirect multiplication sends a generalized point to the product of its two ambient components.

@[simp]

theorem TauCeti.GrpObj.Action.inl_comp_normalSemidirectMul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N H : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] [CategoryTheory.GrpObj H] (i : N ⟶ G) [CategoryTheory.IsMonHom.Normal i] (j : H ⟶ G) [CategoryTheory.IsMonHom j] : let A := normalConjugation i j; CategoryTheory.CategoryStruct.comp A.inl (normalSemidirectMul i j) = CategoryTheory.Grp.ofHom i

Normal semidirect multiplication restricts to the normal subgroup map on the first canonical factor.

theorem TauCeti.GrpObj.Action.inl_comp_normalSemidirectMul_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N H : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] [CategoryTheory.GrpObj H] (i : N ⟶ G) [CategoryTheory.IsMonHom.Normal i] (j : H ⟶ G) [CategoryTheory.IsMonHom j] {Z : CategoryTheory.Grp C} (h : { X := G, grp := inst✝ } ⟶ Z) : CategoryTheory.CategoryStruct.comp (normalConjugation i j).inl (CategoryTheory.CategoryStruct.comp (normalSemidirectMul i j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Grp.ofHom i) h

Normal semidirect multiplication restricts to the normal subgroup map on the first canonical factor.

@[simp]

theorem TauCeti.GrpObj.Action.inr_comp_normalSemidirectMul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N H : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] [CategoryTheory.GrpObj H] (i : N ⟶ G) [CategoryTheory.IsMonHom.Normal i] (j : H ⟶ G) [CategoryTheory.IsMonHom j] : let A := normalConjugation i j; CategoryTheory.CategoryStruct.comp A.inr (normalSemidirectMul i j) = CategoryTheory.Grp.ofHom j

Normal semidirect multiplication restricts to the second ambient map on the second canonical factor.

theorem TauCeti.GrpObj.Action.inr_comp_normalSemidirectMul_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G N H : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj N] [CategoryTheory.GrpObj H] (i : N ⟶ G) [CategoryTheory.IsMonHom.Normal i] (j : H ⟶ G) [CategoryTheory.IsMonHom j] {Z : CategoryTheory.Grp C} (h : { X := G, grp := inst✝ } ⟶ Z) : CategoryTheory.CategoryStruct.comp (normalConjugation i j).inr (CategoryTheory.CategoryStruct.comp (normalSemidirectMul i j) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Grp.ofHom j) h

Normal semidirect multiplication restricts to the second ambient map on the second canonical factor.