Conjugation actions on internal normal subgroups

Let φ : H ⟶ G be a normal subgroup object in a cartesian monoidal category. Mathlib's CategoryTheory.IsMonHom.Normal says that conjugation in G factors through φ. Since φ is monic, that factor is unique. This file names it as normalConjugation φ and proves the action laws directly at the level of generalized points.

Thus conjugation by the identity acts trivially, conjugation by a product is the composite of the two conjugations, and each conjugation preserves the unit, multiplication, and inverse in H. The pointwise statements avoid choosing an internal-hom object of automorphisms and are exactly the interface needed to put a semidirect-product group structure on an internal product.

Main declarations

• TauCeti.normalConjugation: the canonical factor of ambient conjugation through a normal subgroup object.
• TauCeti.normalConjugation_comp: its defining equation after inclusion in the ambient group.
• TauCeti.normalConjugation_one_left and TauCeti.normalConjugation_mul_left: the group-action laws.
• TauCeti.normalConjugation_one_right, TauCeti.normalConjugation_mul_right, and TauCeti.normalConjugation_inv_right: conjugation acts by group automorphisms.
• TauCeti.normalConjugationMulEquiv and TauCeti.normalConjugationMulAutHom: the action by automorphisms on generalized points.

References

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

This is the conjugation-action input for Layer 5, "The unipotent radical", of the ReductiveGroups roadmap. The product of two normal unipotent subgroup schemes is obtained as the image of multiplication from the semidirect product defined by this action.

noncomputable def TauCeti.normalConjugation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj H] (φ : H ⟶ G) [CategoryTheory.IsMonHom.Normal φ] : CategoryTheory.MonoidalCategoryStruct.tensorObj G H ⟶ H

The canonical conjugation action of a group object on a normal subgroup object.

For φ : H ⟶ G, the composite G ⊗ H ⟶ H ⟶ G is the ambient conjugation morphism (g, h) ↦ g * φ(h) * g⁻¹. Normality supplies a factorization and monicity of φ makes it unique.

Equations

• TauCeti.normalConjugation φ = Classical.choose ⋯

@[simp]

theorem TauCeti.normalConjugation_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj H] (φ : H ⟶ G) [CategoryTheory.IsMonHom.Normal φ] : CategoryTheory.CategoryStruct.comp (normalConjugation φ) φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G φ) (CategoryTheory.GrpObj.conj G)

Including the conjugate of a normal-subgroup element gives its ambient conjugate. This is the defining equation of normalConjugation.

theorem TauCeti.normalConjugation_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj H] (φ : H ⟶ G) [CategoryTheory.IsMonHom.Normal φ] {Z : C} (h : G ⟶ Z) : CategoryTheory.CategoryStruct.comp (normalConjugation φ) (CategoryTheory.CategoryStruct.comp φ h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G φ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.GrpObj.conj G) h)

Including the conjugate of a normal-subgroup element gives its ambient conjugate. This is the defining equation of normalConjugation.

theorem TauCeti.normalConjugation_unique {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj H] (φ : H ⟶ G) [CategoryTheory.IsMonHom.Normal φ] (ψ : CategoryTheory.MonoidalCategoryStruct.tensorObj G H ⟶ H) (hψ : CategoryTheory.CategoryStruct.comp ψ φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft G φ) (CategoryTheory.GrpObj.conj G)) : ψ = normalConjugation φ

The factorization of ambient conjugation through a normal subgroup object is unique.

theorem TauCeti.lift_normalConjugation_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H X : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj H] (φ : H ⟶ G) [CategoryTheory.IsMonHom.Normal φ] (g : X ⟶ G) (h : X ⟶ H) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g h) (CategoryTheory.CategoryStruct.comp (normalConjugation φ) φ) = g * CategoryTheory.CategoryStruct.comp h φ * g⁻¹

On generalized points, normalConjugation is ambient conjugation after applying the subgroup inclusion.

theorem TauCeti.lift_normalConjugation_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H X : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj H] (φ : H ⟶ G) [CategoryTheory.IsMonHom.Normal φ] (g : X ⟶ G) (h : X ⟶ H) {Z : C} (h✝ : G ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g h) (CategoryTheory.CategoryStruct.comp (normalConjugation φ) (CategoryTheory.CategoryStruct.comp φ h✝)) = CategoryTheory.CategoryStruct.comp (g * CategoryTheory.CategoryStruct.comp h φ * g⁻¹) h✝

On generalized points, normalConjugation is ambient conjugation after applying the subgroup inclusion.

@[simp]

theorem TauCeti.normalConjugation_one_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H X : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj H] (φ : H ⟶ G) [CategoryTheory.IsMonHom.Normal φ] (h : X ⟶ H) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift 1 h) (normalConjugation φ) = h

Conjugation by the identity fixes every generalized point of a normal subgroup object.

@[simp]

theorem TauCeti.normalConjugation_one_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H X : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj H] (φ : H ⟶ G) [CategoryTheory.IsMonHom.Normal φ] (g : X ⟶ G) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g 1) (normalConjugation φ) = 1

Conjugation fixes the identity generalized point of a normal subgroup object.

@[simp]

theorem TauCeti.normalConjugation_mul_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H X : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj H] (φ : H ⟶ G) [CategoryTheory.IsMonHom.Normal φ] (g₁ g₂ : X ⟶ G) (h : X ⟶ H) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (g₁ * g₂) h) (normalConjugation φ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g₂ h) (normalConjugation φ))) (normalConjugation φ)

Conjugation by a product is successive conjugation, with the right factor acting first.

@[simp]

theorem TauCeti.normalConjugation_mul_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H X : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj H] (φ : H ⟶ G) [CategoryTheory.IsMonHom.Normal φ] (g : X ⟶ G) (h₁ h₂ : X ⟶ H) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g (h₁ * h₂)) (normalConjugation φ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g h₁) (normalConjugation φ) * CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g h₂) (normalConjugation φ)

Conjugation preserves multiplication in a normal subgroup object.

@[simp]

theorem TauCeti.normalConjugation_inv_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H X : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj H] (φ : H ⟶ G) [CategoryTheory.IsMonHom.Normal φ] (g : X ⟶ G) (h : X ⟶ H) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g h⁻¹) (normalConjugation φ) = (CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g h) (normalConjugation φ))⁻¹

Conjugation preserves inverses in a normal subgroup object.

theorem TauCeti.comp_normalConjugation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H X : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj H] (φ : H ⟶ G) [CategoryTheory.IsMonHom.Normal φ] {Y : C} (f : Y ⟶ X) (g : X ⟶ G) (h : X ⟶ H) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g h) (normalConjugation φ)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f h)) (normalConjugation φ)

Conjugation commutes with precomposition of generalized points.

noncomputable def TauCeti.normalConjugationMulEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H X : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj H] (φ : H ⟶ G) [CategoryTheory.IsMonHom.Normal φ] (g : X ⟶ G) : (X ⟶ H) ≃* (X ⟶ H)

Conjugation by an ambient generalized point, as an automorphism of the normal subgroup's generalized-point group. Its inverse is conjugation by the inverse ambient point.

Equations

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

@[simp]

theorem TauCeti.normalConjugationMulEquiv_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H X : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj H] (φ : H ⟶ G) [CategoryTheory.IsMonHom.Normal φ] (g : X ⟶ G) (h : X ⟶ H) : (normalConjugationMulEquiv φ g) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g h) (normalConjugation φ)

Applying the conjugation automorphism is normalConjugation on the pair of generalized points.

@[simp]

theorem TauCeti.normalConjugationMulEquiv_symm_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H X : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj H] (φ : H ⟶ G) [CategoryTheory.IsMonHom.Normal φ] (g : X ⟶ G) (h : X ⟶ H) : (normalConjugationMulEquiv φ g).symm h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g⁻¹ h) (normalConjugation φ)

The inverse conjugation automorphism is conjugation by the inverse ambient point.

noncomputable def TauCeti.normalConjugationMulAutHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H X : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj H] (φ : H ⟶ G) [CategoryTheory.IsMonHom.Normal φ] : (X ⟶ G) →* MulAut (X ⟶ H)

The ambient generalized-point group acts on the normal subgroup's generalized points by conjugation. This is the action homomorphism used by the external semidirect product.

Equations

• TauCeti.normalConjugationMulAutHom φ = { toFun := TauCeti.normalConjugationMulEquiv φ, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.normalConjugationMulAutHom_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {G H X : C} [CategoryTheory.GrpObj G] [CategoryTheory.GrpObj H] (φ : H ⟶ G) [CategoryTheory.IsMonHom.Normal φ] (g : X ⟶ G) (h : X ⟶ H) : ((normalConjugationMulAutHom φ) g) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g h) (normalConjugation φ)

The action homomorphism evaluates as the canonical internal conjugation factor.