Documentation

TauCeti.CategoryTheory.Monoidal.Grp.Subobject

Group structures on subobjects #

A subobject of a group object inherits a unique group structure if the identity, multiplication, and inversion factor through it. The group axioms follow by cancellation of the monomorphism; no axioms need to be assumed for the lifted operations.

This is the categorical form of the closed-subgroup criterion for group schemes.

References #

source
@[instance_reducible]
def TauCeti.grpObjOfMono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {H G : C} [CategoryTheory.GrpObj G] (i : H ⟶ G) [CategoryTheory.Mono i] (e : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ H) (m : CategoryTheory.MonoidalCategoryStruct.tensorObj H H ⟶ H) (j : H ⟶ H) (he : CategoryTheory.CategoryStruct.comp e i = CategoryTheory.MonObj.one) (hm : CategoryTheory.CategoryStruct.comp m i = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom i i) CategoryTheory.MonObj.mul) (hj : CategoryTheory.CategoryStruct.comp j i = CategoryTheory.CategoryStruct.comp i CategoryTheory.GrpObj.inv) :
CategoryTheory.GrpObj H

The group structure induced on a subobject by lifts of identity, multiplication and inversion. Only the compatibility of the operations with the inclusion is required.

Instances For
    source
    theorem TauCeti.isMonHom_grpObjOfMono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {H G : C} [CategoryTheory.GrpObj G] (i : H ⟶ G) [CategoryTheory.Mono i] (e : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ H) (m : CategoryTheory.MonoidalCategoryStruct.tensorObj H H ⟶ H) (j : H ⟶ H) (he : CategoryTheory.CategoryStruct.comp e i = CategoryTheory.MonObj.one) (hm : CategoryTheory.CategoryStruct.comp m i = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom i i) CategoryTheory.MonObj.mul) (hj : CategoryTheory.CategoryStruct.comp j i = CategoryTheory.CategoryStruct.comp i CategoryTheory.GrpObj.inv) :
    CategoryTheory.IsMonHom i

    The inclusion of the induced group object is a homomorphism.

    source
    theorem TauCeti.grpObj_eq_of_mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {H G : C} [CategoryTheory.MonObj G] (i : H ⟶ G) [CategoryTheory.Mono i] (a b : CategoryTheory.GrpObj H) (ha : CategoryTheory.IsMonHom i) (hb : CategoryTheory.IsMonHom i) :
    a = b

    A monomorphism into a monoid object admits at most one compatible group structure.

    source
    @[simp]
    theorem TauCeti.grpObjOfMono_one {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {H G : C} [CategoryTheory.GrpObj G] (i : H ⟶ G) [CategoryTheory.Mono i] (e : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ H) (m : CategoryTheory.MonoidalCategoryStruct.tensorObj H H ⟶ H) (j : H ⟶ H) (he : CategoryTheory.CategoryStruct.comp e i = CategoryTheory.MonObj.one) (hm : CategoryTheory.CategoryStruct.comp m i = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom i i) CategoryTheory.MonObj.mul) (hj : CategoryTheory.CategoryStruct.comp j i = CategoryTheory.CategoryStruct.comp i CategoryTheory.GrpObj.inv) :
    CategoryTheory.MonObj.one = e

    The unit of the induced group object is the specified lift.

    source
    @[simp]
    theorem TauCeti.grpObjOfMono_mul {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {H G : C} [CategoryTheory.GrpObj G] (i : H ⟶ G) [CategoryTheory.Mono i] (e : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ H) (m : CategoryTheory.MonoidalCategoryStruct.tensorObj H H ⟶ H) (j : H ⟶ H) (he : CategoryTheory.CategoryStruct.comp e i = CategoryTheory.MonObj.one) (hm : CategoryTheory.CategoryStruct.comp m i = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom i i) CategoryTheory.MonObj.mul) (hj : CategoryTheory.CategoryStruct.comp j i = CategoryTheory.CategoryStruct.comp i CategoryTheory.GrpObj.inv) :
    CategoryTheory.MonObj.mul = m

    The multiplication of the induced group object is the specified lift.

    source
    @[simp]
    theorem TauCeti.grpObjOfMono_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] {H G : C} [CategoryTheory.GrpObj G] (i : H ⟶ G) [CategoryTheory.Mono i] (e : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ H) (m : CategoryTheory.MonoidalCategoryStruct.tensorObj H H ⟶ H) (j : H ⟶ H) (he : CategoryTheory.CategoryStruct.comp e i = CategoryTheory.MonObj.one) (hm : CategoryTheory.CategoryStruct.comp m i = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom i i) CategoryTheory.MonObj.mul) (hj : CategoryTheory.CategoryStruct.comp j i = CategoryTheory.CategoryStruct.comp i CategoryTheory.GrpObj.inv) :
    CategoryTheory.GrpObj.inv = j

    The inversion of the induced group object is the specified lift.