Normal subgroup objects #
In this file we define normal subgroups of group objects in a cartesian monoidal category as
a predicate on morphisms. A morphism φ : H ⟶ G of group objects is normal if it is mono, a
monoid morphism and the conjugation map (g, h) ↦ g * h * g⁻¹ factors through φ.
This is applied in the study of group schemes.
Main declarations #
CategoryTheory.IsMonHom.Normal: The predicate on morphisms to be a normal monoid morphism.CategoryTheory.IsMonHom.normal_iff_normal_monoidHom: A monoid morphismH ⟶ Gthat is mono is normal if and only if for everyX, the image ofH(X)inG(X)is a normal subgroup.
References #
- In the context of group schemes: Görtz, Wedhorn, Algebraic Geometry II, Definition 27.3
class
CategoryTheory.IsAddMonHom.Normal
{C : Type u_1}
[Category.{v_1, u_1} C]
[CartesianMonoidalCategory C]
{G H : C}
[AddGrpObj G]
[AddGrpObj H]
(φ : H ⟶ G)
:
A morphism φ : H ⟶ G of additive group objects is a normal monoid homomorphism if it is a
monoid homomorphism that is mono and such that the conjugation map (g, h) ↦ g + h - g
factors through φ.
- mono : Mono φ
- isAddMonHom : IsAddMonHom φ
- exists_comp_eq_addConj : ∃ (ψ : MonoidalCategoryStruct.tensorObj G H ⟶ H), CategoryStruct.comp ψ φ = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft G φ) (AddGrpObj.addConj G)
Instances
class
CategoryTheory.IsMonHom.Normal
{C : Type u_1}
[Category.{v_1, u_1} C]
[CartesianMonoidalCategory C]
{G H : C}
[GrpObj G]
[GrpObj H]
(φ : H ⟶ G)
:
A morphism φ : H ⟶ G of group objects is a normal monoid homomorphism if it is a
monoid homomorphism that is mono and such that the conjugation map (g, h) ↦ g * h * g⁻¹
factors through φ.
- mono : Mono φ
- isMonHom : IsMonHom φ
- exists_comp_eq_conj : ∃ (ψ : MonoidalCategoryStruct.tensorObj G H ⟶ H), CategoryStruct.comp ψ φ = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft G φ) (GrpObj.conj G)
Instances
instance
CategoryTheory.IsMonHom.instNormalId
{C : Type u_1}
[Category.{v_1, u_1} C]
[CartesianMonoidalCategory C]
{G : C}
[GrpObj G]
:
instance
CategoryTheory.IsAddMonHom.instNormalId
{C : Type u_1}
[Category.{v_1, u_1} C]
[CartesianMonoidalCategory C]
{G : C}
[AddGrpObj G]
:
instance
CategoryTheory.IsMonHom.instNormalOne
{C : Type u_1}
[Category.{v_1, u_1} C]
[CartesianMonoidalCategory C]
{G : C}
[GrpObj G]
:
instance
CategoryTheory.IsAddMonHom.instNormalZero
{C : Type u_1}
[Category.{v_1, u_1} C]
[CartesianMonoidalCategory C]
{G : C}
[AddGrpObj G]
:
theorem
CategoryTheory.IsMonHom.isNormalHom_iff
{C : Type u_1}
[Category.{v_1, u_1} C]
[CartesianMonoidalCategory C]
{G H : C}
[GrpObj G]
[GrpObj H]
{φ : H ⟶ G}
[IsMonHom φ]
[Mono φ]
:
Normal φ ↔ ∃ (ψ : MonoidalCategoryStruct.tensorObj G H ⟶ H),
CategoryStruct.comp ψ φ = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft G φ) (GrpObj.conj G)
theorem
CategoryTheory.IsAddMonHom.isNormalHom_iff
{C : Type u_1}
[Category.{v_1, u_1} C]
[CartesianMonoidalCategory C]
{G H : C}
[AddGrpObj G]
[AddGrpObj H]
{φ : H ⟶ G}
[IsAddMonHom φ]
[Mono φ]
:
Normal φ ↔ ∃ (ψ : MonoidalCategoryStruct.tensorObj G H ⟶ H),
CategoryStruct.comp ψ φ = CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft G φ) (AddGrpObj.addConj G)
theorem
CategoryTheory.IsMonHom.normal_iff_normal_monoidHom
{C : Type u_1}
[Category.{v_1, u_1} C]
[CartesianMonoidalCategory C]
{G H : C}
[GrpObj G]
[GrpObj H]
{φ : H ⟶ G}
[IsMonHom φ]
[Mono φ]
:
If φ is mono, it is a normal group homomorphism if and only if for all X the image of
H(X) in G(X) is a normal subgroup.
theorem
CategoryTheory.IsAddMonHom.normal_iff_normal_addMonoidHom
{C : Type u_1}
[Category.{v_1, u_1} C]
[CartesianMonoidalCategory C]
{G H : C}
[AddGrpObj G]
[AddGrpObj H]
{φ : H ⟶ G}
[IsAddMonHom φ]
[Mono φ]
:
@[instance 100]
instance
CategoryTheory.IsMonHom.instNormalOfIsCommMonObjOfMono
{C : Type u_1}
[Category.{v_1, u_1} C]
[CartesianMonoidalCategory C]
{G H : C}
[GrpObj G]
[GrpObj H]
{φ : H ⟶ G}
[BraidedCategory C]
[IsCommMonObj G]
[IsMonHom φ]
[Mono φ]
:
Normal φ
@[instance 100]
instance
CategoryTheory.IsAddMonHom.instNormalOfIsCommAddMonObjOfMono
{C : Type u_1}
[Category.{v_1, u_1} C]
[CartesianMonoidalCategory C]
{G H : C}
[AddGrpObj G]
[AddGrpObj H]
{φ : H ⟶ G}
[BraidedCategory C]
[IsCommAddMonObj G]
[IsAddMonHom φ]
[Mono φ]
:
Normal φ
theorem
CategoryTheory.IsMonHom.Normal.of_isPullback_η
{C : Type u_1}
[Category.{v_1, u_1} C]
[CartesianMonoidalCategory C]
{G H : C}
[GrpObj G]
[GrpObj H]
{φ : H ⟶ G}
[IsMonHom φ]
{P : C}
(p : G ⟶ P)
[GrpObj P]
[IsMonHom p]
(h : IsPullback φ (SemiCartesianMonoidalCategory.toUnit H) p MonObj.one)
:
Normal φ
theorem
CategoryTheory.IsAddMonHom.Normal.of_isPullback_η
{C : Type u_1}
[Category.{v_1, u_1} C]
[CartesianMonoidalCategory C]
{G H : C}
[AddGrpObj G]
[AddGrpObj H]
{φ : H ⟶ G}
[IsAddMonHom φ]
{P : C}
(p : G ⟶ P)
[AddGrpObj P]
[IsAddMonHom p]
(h : IsPullback φ (SemiCartesianMonoidalCategory.toUnit H) p AddMonObj.zero)
:
Normal φ