The category of groups in a Cartesian monoidal category #

In fact, any monoid object whose associativity diagram is Cartesian can be made into a group object (we do not prove this in this file), so we should expect that many properties of group objects follow from this result.

source

@[simp]

theorem GrpObj.inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [GrpObj A] [GrpObj B] (f : A ⟶ B) [IsMonHom f] :

CategoryTheory.CategoryStruct.comp inv f = CategoryTheory.CategoryStruct.comp f inv

Morphisms of group objects preserve inverses.

source

@[simp]

theorem GrpObj.inv_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [GrpObj A] [GrpObj B] (f : A ⟶ B) [IsMonHom f] {Z : C} (h : B ⟶ Z) :

CategoryTheory.CategoryStruct.comp inv (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp inv h)

source

theorem GrpObj.toMonObj_injective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {X : C} :

Function.Injective (@toMonObj C inst✝ inst✝¹ X)

source

@[deprecated GrpObj.toMonObj_injective (since := "2025-09-09")]

theorem GrpObj.toMon_Class_injective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {X : C} :

Function.Injective (@toMonObj C inst✝ inst✝¹ X)

Alias of GrpObj.toMonObj_injective.

source

theorem GrpObj.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {X : C} (h₁ h₂ : GrpObj X) (H : h₁.toMonObj = h₂.toMonObj) :

h₁ = h₂

source

theorem GrpObj.ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {X : C} {h₁ h₂ : GrpObj X} :

h₁ = h₂ ↔ h₁.toMonObj = h₂.toMonObj

source

instance GrpObj.tensorObj.instTensorObj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H : C} [GrpObj G] [GrpObj H] :

GrpObj (CategoryTheory.MonoidalCategoryStruct.tensorObj G H)

Equations

GrpObj.tensorObj.instTensorObj = { toMonObj := Mon.instMonObjTensorObj, inv := CategoryTheory.MonoidalCategoryStruct.tensorHom GrpObj.inv GrpObj.inv, left_inv := ⋯, right_inv := ⋯ }

source

@[simp]

theorem GrpObj.tensorObj.inv_def {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H : C} [GrpObj G] [GrpObj H] :

inv = CategoryTheory.MonoidalCategoryStruct.tensorHom inv inv

source

def Grp.forget₂Mon (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] :

CategoryTheory.Functor (Grp C) (Mon C)

The forgetful functor from group objects to monoid objects.

Equations

Grp.forget₂Mon C = CategoryTheory.inducedFunctor Grp.toMon

Instances For

source

@[simp]

theorem Grp.forget₂Mon_obj_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Grp C) :

((forget₂Mon C).obj A).X = A.X

source

@[deprecated Grp.forget₂Mon (since := "2025-09-15")]

def Grp.forget₂Mon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] :

CategoryTheory.Functor (Grp C) (Mon C)

Alias of Grp.forget₂Mon.

The forgetful functor from group objects to monoid objects.

Equations

Grp.forget₂Mon_ = Grp.forget₂Mon

Instances For

source

def Grp.fullyFaithfulForget₂Mon (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] :

(forget₂Mon C).FullyFaithful

The forgetful functor from group objects to monoid objects is fully faithful.

Equations

Grp.fullyFaithfulForget₂Mon C = CategoryTheory.fullyFaithfulInducedFunctor Grp.toMon

Instances For

source

@[deprecated Grp.fullyFaithfulForget₂Mon (since := "2025-09-15")]

def Grp.fullyFaithfulForget₂Mon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] :

(forget₂Mon C).FullyFaithful

Alias of Grp.fullyFaithfulForget₂Mon.

The forgetful functor from group objects to monoid objects is fully faithful.

Equations

Grp.fullyFaithfulForget₂Mon_ = Grp.fullyFaithfulForget₂Mon

Instances For

source

instance Grp.instFullMonForget₂Mon (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] :

(forget₂Mon C).Full

source

instance Grp.instFaithfulMonForget₂Mon (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] :

(forget₂Mon C).Faithful

source

@[simp]

theorem Grp.forget₂Mon_obj_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Grp C) :

MonObj.one = MonObj.one

source

@[simp]

theorem Grp.forget₂Mon_obj_mul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Grp C) :

MonObj.mul = MonObj.mul

source

@[simp]

theorem Grp.forget₂Mon_map_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : Grp C} (f : A ⟶ B) :

((forget₂Mon C).map f).hom = f.hom

source

def Grp.forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] :

CategoryTheory.Functor (Grp C) C

The forgetful functor from group objects to the ambient category.

Equations

Grp.forget C = (Grp.forget₂Mon C).comp (Mon.forget C)

Instances For

source

@[simp]

theorem Grp.forget_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {X✝ Y✝ : Grp C} (f : X✝ ⟶ Y✝) :

(forget C).map f = f.hom

source

@[simp]

theorem Grp.forget_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (X : Grp C) :

(forget C).obj X = X.X

source

instance Grp.instFaithfulForget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] :

(forget C).Faithful

source

@[simp]

theorem Grp.forget₂Mon_comp_forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] :

(forget₂Mon C).comp (Mon.forget C) = forget C

source

instance Grp.instIsIsoHom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : Grp C} {f : G ⟶ H} [CategoryTheory.IsIso f] :

CategoryTheory.IsIso f.hom

source

def Grp.mkIso' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : C} (e : G ≅ H) [GrpObj G] [GrpObj H] [IsMonHom e.hom] :

{ X := G, grp := inst✝ } ≅ { X := H, grp := inst✝¹ }

Construct an isomorphism of group objects by giving a monoid isomorphism between the underlying objects.

Equations

Grp.mkIso' e = (Grp.fullyFaithfulForget₂Mon C).preimageIso (Mon.mkIso' e)

Instances For

source

@[simp]

theorem Grp.mkIso'_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : C} (e : G ≅ H) [GrpObj G] [GrpObj H] [IsMonHom e.hom] :

(mkIso' e).hom.hom = e.hom

source

@[simp]

theorem Grp.mkIso'_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : C} (e : G ≅ H) [GrpObj G] [GrpObj H] [IsMonHom e.hom] :

(mkIso' e).inv.hom = e.inv

source

@[reducible, inline]

abbrev Grp.mkIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : Grp C} (e : G.X ≅ H.X) (one_f : CategoryTheory.CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryTheory.CategoryStruct.comp MonObj.mul e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) :

G ≅ H

Construct an isomorphism of group objects by giving an isomorphism between the underlying objects and checking compatibility with unit and multiplication only in the forward direction.

Equations

Grp.mkIso e one_f mul_f = Grp.mkIso' e

Instances For

source

@[simp]

theorem Grp.mkIso_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : Grp C} (e : G.X ≅ H.X) (one_f : CategoryTheory.CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryTheory.CategoryStruct.comp MonObj.mul e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) :

(mkIso e one_f mul_f).inv.hom = e.inv

source

@[simp]

theorem Grp.mkIso_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : Grp C} (e : G.X ≅ H.X) (one_f : CategoryTheory.CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryTheory.CategoryStruct.comp MonObj.mul e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) :

(mkIso e one_f mul_f).hom.hom = e.hom

source

instance Grp.uniqueHomFromTrivial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Grp C) :

Unique (trivial C ⟶ A)

Equations

A.uniqueHomFromTrivial = A.toMon.uniqueHomFromTrivial

source

instance Grp.instHasInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] :

CategoryTheory.Limits.HasInitial (Grp C)

`Grp C` is cartesian-monoidal #

source

instance Grp.instMonoidalCategoryStruct {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] :

CategoryTheory.MonoidalCategoryStruct (Grp C)

Equations

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

source

@[simp]

theorem Grp.tensorHom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {X₁✝ Y₁✝ X₂✝ Y₂✝ : Grp C} (f : X₁✝.toMon ⟶ Y₁✝.toMon) (g : X₂✝.toMon ⟶ Y₂✝.toMon) :

(CategoryTheory.MonoidalCategoryStruct.tensorHom f g).hom = CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom

source

@[simp]

theorem Grp.tensorObj_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H : Grp C) :

(CategoryTheory.MonoidalCategoryStruct.tensorObj G H).X = CategoryTheory.MonoidalCategoryStruct.tensorObj G.X H.X

source

@[simp]

theorem Grp.tensorUnit_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] :

(CategoryTheory.MonoidalCategoryStruct.tensorUnit (Grp C)).X = CategoryTheory.MonoidalCategoryStruct.tensorUnit C

source

@[simp]

theorem Grp.tensorUnit_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] :

MonObj.one = MonObj.one

source

@[simp]

theorem Grp.tensorUnit_mul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] :

MonObj.mul = MonObj.mul

source

@[simp]

theorem Grp.tensorObj_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H : Grp C) :

MonObj.one = MonObj.one

source

@[simp]

theorem Grp.tensorObj_mul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H : Grp C) :

MonObj.mul = MonObj.mul

source

@[simp]

theorem Grp.whiskerLeft_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H : Grp C} (f : G ⟶ H) (I : Grp C) :

(CategoryTheory.MonoidalCategoryStruct.whiskerRight f I).hom = CategoryTheory.MonoidalCategoryStruct.whiskerRight f.hom I.X

source

@[simp]

theorem Grp.whiskerRight_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G : Grp C) {H I : Grp C} (f : H ⟶ I) :

(CategoryTheory.MonoidalCategoryStruct.whiskerLeft G f).hom = CategoryTheory.MonoidalCategoryStruct.whiskerLeft G.X f.hom

source

@[simp]

theorem Grp.leftUnitor_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G : Grp C) :

(CategoryTheory.MonoidalCategoryStruct.leftUnitor G).hom.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor G.X).hom

source

@[simp]

theorem Grp.leftUnitor_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G : Grp C) :

(CategoryTheory.MonoidalCategoryStruct.leftUnitor G).inv.hom = (CategoryTheory.MonoidalCategoryStruct.leftUnitor G.X).inv

source

@[simp]

theorem Grp.rightUnitor_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G : Grp C) :

(CategoryTheory.MonoidalCategoryStruct.rightUnitor G).hom.hom = (CategoryTheory.MonoidalCategoryStruct.rightUnitor G.X).hom

source

@[simp]

theorem Grp.rightUnitor_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G : Grp C) :

(CategoryTheory.MonoidalCategoryStruct.rightUnitor G).inv.hom = (CategoryTheory.MonoidalCategoryStruct.rightUnitor G.X).inv

source

@[simp]

theorem Grp.associator_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H I : Grp C) :

(CategoryTheory.MonoidalCategoryStruct.associator G H I).hom.hom = (CategoryTheory.MonoidalCategoryStruct.associator G.X H.X I.X).hom

source

@[simp]

theorem Grp.associator_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H I : Grp C) :

(CategoryTheory.MonoidalCategoryStruct.associator G H I).inv.hom = (CategoryTheory.MonoidalCategoryStruct.associator G.X H.X I.X).inv

source

instance Grp.instMonoidalCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] :

CategoryTheory.MonoidalCategory (Grp C)

Equations

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

source

instance Grp.instCartesianMonoidalCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] :

CategoryTheory.CartesianMonoidalCategory (Grp C)

Equations

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

source

@[simp]

theorem Grp.lift_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H₁ H₂ : Grp C} (f : G ⟶ H₁) (g : G ⟶ H₂) :

(CategoryTheory.CartesianMonoidalCategory.lift f g).hom = CategoryTheory.CartesianMonoidalCategory.lift f.hom g.hom

source

@[simp]

theorem Grp.fst_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H : Grp C) :

(CategoryTheory.CartesianMonoidalCategory.fst G H).hom = CategoryTheory.CartesianMonoidalCategory.fst G.X H.X

source

@[simp]

theorem Grp.snd_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H : Grp C) :

(CategoryTheory.CartesianMonoidalCategory.snd G H).hom = CategoryTheory.CartesianMonoidalCategory.snd G.X H.X

source

instance Grp.instMonoidalMonForget₂Mon {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] :

(forget₂Mon C).Monoidal

Equations

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

source

@[simp]

theorem Grp.ε_def {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] :

CategoryTheory.Functor.LaxMonoidal.ε (forget₂Mon C) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Mon C))

source

@[simp]

theorem Grp.δ_def {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H : Grp C) :

CategoryTheory.Functor.OplaxMonoidal.δ (forget₂Mon C) G H = CategoryTheory.CategoryStruct.id ((forget₂Mon C).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj G H))

source

@[simp]

theorem Grp.μ_def {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H : Grp C) :

CategoryTheory.Functor.LaxMonoidal.μ (forget₂Mon C) G H = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj ((forget₂Mon C).obj G) ((forget₂Mon C).obj H))

source

@[simp]

theorem Grp.η_def {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] :

CategoryTheory.Functor.OplaxMonoidal.η (forget₂Mon C) = CategoryTheory.CategoryStruct.id ((forget₂Mon C).obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit (Grp C)))

source

instance Grp.instBraidedCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] :

CategoryTheory.BraidedCategory (Grp C)

Equations

Grp.instBraidedCategory = CategoryTheory.BraidedCategory.ofFaithful (Grp.forget₂Mon C) (fun (G H : Grp C) => Grp.mkIso (β_ G.X H.X) ⋯ ⋯) ⋯

source

@[simp]

theorem Grp.braiding_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H : Grp C) :

(β_ G H).hom.hom = (β_ G.X H.X).hom

source

@[simp]

theorem Grp.braiding_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (G H : Grp C) :

(β_ G H).inv.hom = (β_ G.X H.X).inv

source

@[reducible, inline]

abbrev CategoryTheory.Functor.grpObjObj {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {F : Functor C D} [F.Monoidal] {G : C} [GrpObj G] :

GrpObj (F.obj G)

The image of a group object under a monoidal functor is a group object.

Equations

CategoryTheory.Functor.grpObjObj = { toMonObj := CategoryTheory.Functor.monObjObj G, inv := F.map GrpObj.inv, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.Functor.obj.ι_def {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {F : Functor C D} [F.Monoidal] {G : C} [GrpObj G] :

GrpObj.inv = F.map GrpObj.inv

source

theorem CategoryTheory.Functor.obj.ι_def_assoc {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {F : Functor C D} [F.Monoidal] {G : C} [GrpObj G] {Z : D} (h : F.obj G ⟶ Z) :

CategoryStruct.comp GrpObj.inv h = CategoryStruct.comp (F.map GrpObj.inv) h

source

def CategoryTheory.Functor.mapGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] :

Functor (Grp C) (Grp D)

A finite-product-preserving functor takes group objects to group objects.

Equations

F.mapGrp = { obj := fun (A : Grp C) => { X := F.obj A.X, grp := CategoryTheory.Functor.grpObjObj }, map := fun {X Y : Grp C} (f : X ⟶ Y) => F.mapMon.map f, map_id := ⋯, map_comp := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.Functor.mapGrp_obj_grp_one {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] (A : Grp C) :

MonObj.one = CategoryStruct.comp (LaxMonoidal.ε F) (F.map MonObj.one)

source

@[simp]

theorem CategoryTheory.Functor.mapGrp_obj_X {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] (A : Grp C) :

(F.mapGrp.obj A).X = F.obj A.X

source

@[simp]

theorem CategoryTheory.Functor.mapGrp_obj_grp_inv {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] (A : Grp C) :

GrpObj.inv = F.map GrpObj.inv

source

@[simp]

theorem CategoryTheory.Functor.mapGrp_obj_grp_mul {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] (A : Grp C) :

MonObj.mul = CategoryStruct.comp (LaxMonoidal.μ F A.X A.X) (F.map MonObj.mul)

source

@[simp]

theorem CategoryTheory.Functor.mapGrp_map_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] {X✝ Y✝ : Grp C} (f : X✝ ⟶ Y✝) :

(F.mapGrp.map f).hom = F.map f.hom

source

instance CategoryTheory.Functor.Faithful.mapGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {F : Functor C D} [F.Monoidal] [F.Faithful] :

F.mapGrp.Faithful

source

instance CategoryTheory.Functor.Full.mapGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {F : Functor C D} [F.Monoidal] [F.Full] [F.Faithful] :

F.mapGrp.Full

source

def CategoryTheory.Functor.FullyFaithful.mapGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {F : Functor C D} [F.Monoidal] (hF : F.FullyFaithful) :

F.mapGrp.FullyFaithful

If F : C ⥤ D is a fully faithful monoidal functor, then GrpCat(F) : GrpCat C ⥤ GrpCat D is fully faithful too.

Equations

hF.mapGrp = { preimage := fun {X Y : Grp C} (f : F.mapGrp.obj X ⟶ F.mapGrp.obj Y) => { hom := hF.preimage f.hom, isMonHom_hom := ⋯ }, map_preimage := ⋯, preimage_map := ⋯ }