Equivariance of multiplication from a normal semidirect product

Let i : N ⟶ G and j : H ⟶ G be normal subgroup objects. Ambient conjugation acts simultaneously on both factors of the semidirect product N ⋊ H: a generalized point g sends (n, h) to (gng⁻¹, ghg⁻¹). This file constructs that internal action and proves that the canonical multiplication homomorphism

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

is equivariant for simultaneous conjugation on the source and conjugation on the target.

This is the equivariance input for proving that the scheme-theoretic image of this multiplication map is normal. Together with connectedness, smoothness, and unipotence of the image, that image is the binary product used in the maximal-dimension construction of the unipotent radical.

Main declarations

• TauCeti.GrpObj.Action.normalSemidirectConjugation: simultaneous ambient conjugation on the normal semidirect product.
• TauCeti.GrpObj.Action.normalSemidirectMul_equivariant: multiplication from the normal semidirect product intertwines simultaneous conjugation with ambient conjugation.

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 simultaneous-conjugation equation needed to prove normality of the binary-product image.

noncomputable def TauCeti.GrpObj.Action.normalSemidirectConjugation {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.Normal j] : have A := normalConjugation i j; Action G (CategoryTheory.MonoidalCategoryStruct.tensorObj N H)

Simultaneous ambient conjugation on two normal subgroup objects acts on their normal semidirect product by group automorphisms.

Equations

• TauCeti.GrpObj.Action.normalSemidirectConjugation i j = { hom := TauCeti.GrpObj.Action.normalSemidirectConjugationHom✝ i j, one_act := ⋯, mul_act := ⋯, act_mul := ⋯ }

@[simp]

theorem TauCeti.GrpObj.Action.normalSemidirectConjugation_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.Normal j] (g : X ⟶ G) (x : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj N H) : have A := normalConjugation i j; act (normalSemidirectConjugation i j) g x = CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g (CategoryTheory.CategoryStruct.comp x (CategoryTheory.SemiCartesianMonoidalCategory.fst N H))) (TauCeti.normalConjugation i)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g (CategoryTheory.CategoryStruct.comp x (CategoryTheory.SemiCartesianMonoidalCategory.snd N H))) (TauCeti.normalConjugation j))

Simultaneous conjugation sends (n, h) to the pair of their ambient conjugates.

theorem TauCeti.GrpObj.Action.normalSemidirectMul_equivariant_apply {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.Normal j] (g : X ⟶ G) (x : X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj N H) : have A := normalConjugation i j; CategoryTheory.CategoryStruct.comp (act (normalSemidirectConjugation i j) g x) (normalSemidirectMul i j).hom.hom = g * CategoryTheory.CategoryStruct.comp x (normalSemidirectMul i j).hom.hom * g⁻¹

Multiplication from a normal semidirect product intertwines simultaneous ambient conjugation on the source with conjugation on the target.

theorem TauCeti.GrpObj.Action.normalSemidirectMul_equivariant {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.Normal j] : have A := normalConjugation i j; CategoryTheory.CategoryStruct.comp (normalSemidirectConjugation i j).hom (normalSemidirectMul i j).hom.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G (normalSemidirectMul i j).hom.hom) (CategoryTheory.GrpObj.conj G)

Multiplication from a normal semidirect product is equivariant for conjugation.

theorem TauCeti.GrpObj.Action.normalSemidirectMul_equivariant_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.Normal j] {Z : C} (h : G ⟶ Z) : CategoryTheory.CategoryStruct.comp (normalSemidirectConjugation i j).hom (CategoryTheory.CategoryStruct.comp (normalSemidirectMul i j).hom.hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G (normalSemidirectMul i j).hom.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrpObj.conj G) h)

Multiplication from a normal semidirect product is equivariant for conjugation.