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 CategoryTheory.GrpObj.inv_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {A B : C} [GrpObj A] [GrpObj B] (f : A ⟶ B) [IsMonHom f] :

CategoryStruct.comp inv f = CategoryStruct.comp f inv

Morphisms of group objects preserve inverses.

source

@[simp]

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

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

Morphisms of group objects preserve inverses.

source

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

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

source

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

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

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

Alias of CategoryTheory.GrpObj.toMonObj_injective.

source

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

h₁ = h₂

source

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

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

source

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

GrpObj (MonoidalCategoryStruct.tensorObj G H)

Equations

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

source

@[simp]

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

inv = MonoidalCategoryStruct.tensorHom inv inv

source

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

Functor (Grp C) (Mon C)

The forgetful functor from group objects to monoid objects.

Equations

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

Instances For

source

@[simp]

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

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

source

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

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

Functor (Grp C) (Mon C)

Alias of CategoryTheory.Grp.forget₂Mon.

The forgetful functor from group objects to monoid objects.

Equations

CategoryTheory.Grp.forget₂Mon_ = CategoryTheory.Grp.forget₂Mon

Instances For

source

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

(forget₂Mon C).FullyFaithful

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

Equations

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

Instances For

source

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

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

(forget₂Mon C).FullyFaithful

Alias of CategoryTheory.Grp.fullyFaithfulForget₂Mon.

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

Equations

CategoryTheory.Grp.fullyFaithfulForget₂Mon_ = CategoryTheory.Grp.fullyFaithfulForget₂Mon

Instances For

source

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

(forget₂Mon C).Full

source

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

(forget₂Mon C).Faithful

source

@[simp]

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

MonObj.one = MonObj.one

source

@[simp]

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

MonObj.mul = MonObj.mul

source

@[simp]

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

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

source

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

Functor (Grp C) C

The forgetful functor from group objects to the ambient category.

Equations

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

Instances For

source

@[simp]

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

(forget C).obj X = X.X

source

@[simp]

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

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

source

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

(forget C).Faithful

source

@[simp]

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

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

source

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

IsIso f.hom.hom

source

def CategoryTheory.Grp.mkIso' {C : Type u₁} [Category.{v₁, u₁} C] [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

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

Instances For

source

@[simp]

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

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

source

@[simp]

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

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

source

@[reducible, inline]

abbrev CategoryTheory.Grp.mkIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {G H : Grp C} (e : G.X ≅ H.X) (one_f : CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryStruct.comp MonObj.mul e.hom = CategoryStruct.comp (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

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

Instances For

source

@[simp]

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

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

source

@[simp]

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

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

source

@[deprecated CategoryTheory.Grp.mkIso_hom_hom_hom (since := "2025-12-18")]

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

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

Alias of CategoryTheory.Grp.mkIso_hom_hom_hom.

source

@[deprecated CategoryTheory.Grp.mkIso_inv_hom_hom (since := "2025-12-18")]

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

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

Alias of CategoryTheory.Grp.mkIso_inv_hom_hom.

source

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

Unique (trivial C ⟶ A)

Equations

A.uniqueHomFromTrivial = (have this := CategoryTheory.InducedCategory.homEquiv; this).unique

source

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

Limits.HasInitial (Grp C)

`Grp C` is cartesian-monoidal #

source

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

MonoidalCategoryStruct (Grp C)

Equations

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

MonObj.one = MonObj.one

source

@[simp]

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

MonObj.mul = MonObj.mul

source

@[simp]

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

MonObj.one = MonObj.one

source

@[simp]

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

MonObj.mul = MonObj.mul

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[deprecated CategoryTheory.Grp.whiskerLeft_hom_hom (since := "2025-12-18")]

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

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

Alias of CategoryTheory.Grp.whiskerLeft_hom_hom.

source

@[deprecated CategoryTheory.Grp.whiskerRight_hom_hom (since := "2025-12-18")]

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

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

Alias of CategoryTheory.Grp.whiskerRight_hom_hom.

source

@[deprecated CategoryTheory.Grp.leftUnitor_hom_hom_hom (since := "2025-12-18")]

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

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

Alias of CategoryTheory.Grp.leftUnitor_hom_hom_hom.

source

@[deprecated CategoryTheory.Grp.leftUnitor_inv_hom_hom (since := "2025-12-18")]

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

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

Alias of CategoryTheory.Grp.leftUnitor_inv_hom_hom.

source

@[deprecated CategoryTheory.Grp.rightUnitor_hom_hom_hom (since := "2025-12-18")]

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

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

Alias of CategoryTheory.Grp.rightUnitor_hom_hom_hom.

source

@[deprecated CategoryTheory.Grp.rightUnitor_inv_hom_hom (since := "2025-12-18")]

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

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

Alias of CategoryTheory.Grp.rightUnitor_inv_hom_hom.

source

@[deprecated CategoryTheory.Grp.associator_hom_hom_hom (since := "2025-12-18")]

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

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

Alias of CategoryTheory.Grp.associator_hom_hom_hom.

source

@[deprecated CategoryTheory.Grp.associator_inv_hom_hom (since := "2025-12-18")]

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

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

Alias of CategoryTheory.Grp.associator_inv_hom_hom.

source

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

MonoidalCategory (Grp C)

Equations

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

source

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

CartesianMonoidalCategory (Grp C)

Equations

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

source

@[simp]

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

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

source

@[simp]

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

(SemiCartesianMonoidalCategory.fst G H).hom.hom = SemiCartesianMonoidalCategory.fst G.X H.X

source

@[simp]

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

(SemiCartesianMonoidalCategory.snd G H).hom.hom = SemiCartesianMonoidalCategory.snd G.X H.X

source

@[deprecated CategoryTheory.Grp.fst_hom_hom (since := "2025-12-18")]

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

(SemiCartesianMonoidalCategory.fst G H).hom.hom = SemiCartesianMonoidalCategory.fst G.X H.X

Alias of CategoryTheory.Grp.fst_hom_hom.

source

@[deprecated CategoryTheory.Grp.snd_hom_hom (since := "2025-12-18")]

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

(SemiCartesianMonoidalCategory.snd G H).hom.hom = SemiCartesianMonoidalCategory.snd G.X H.X

Alias of CategoryTheory.Grp.snd_hom_hom.

source

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

(forget₂Mon C).Monoidal

Equations

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

BraidedCategory (Grp C)

Equations

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[deprecated CategoryTheory.Grp.braiding_hom_hom_hom (since := "2025-12-18")]

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

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

Alias of CategoryTheory.Grp.braiding_hom_hom_hom.

source

@[deprecated CategoryTheory.Grp.braiding_inv_hom_hom (since := "2025-12-18")]

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

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

Alias of CategoryTheory.Grp.braiding_inv_hom_hom.

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 CategoryTheory.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

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

Instances For

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_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_map_hom_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.hom = F.map f.hom.hom

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

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

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

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

Instances For

source

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.mapGrp_preimage {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) {X✝ Y✝ : Grp C} (f : F.mapGrp.obj X✝ ⟶ F.mapGrp.obj Y✝) :

hF.mapGrp.preimage f = Grp.homMk' (hF.mapMon.preimage f.hom)

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

@[simp]

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

MonObj.one = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)) MonObj.one

source

@[simp]

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

MonObj.mul = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorObj A.X A.X)) MonObj.mul

source

@[simp]

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

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

source

@[simp]

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

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

source

def CategoryTheory.Functor.mapGrpIdIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] :

(Functor.id C).mapGrp ≅ Functor.id (Grp C)

The identity functor is also the identity on group objects.

Equations

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

Instances For

source

@[simp]

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

(mapGrpIdIso.hom.app X).hom.hom = CategoryStruct.id X.X

source

@[simp]

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

(mapGrpIdIso.inv.app X).hom.hom = CategoryStruct.id X.X

source

def CategoryTheory.Functor.mapGrpCompIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] {F : Functor C D} {G : Functor D E} [F.Monoidal] [G.Monoidal] :

(F.comp G).mapGrp ≅ F.mapGrp.comp G.mapGrp

The composition functor is also the composition on group objects.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Functor.mapGrpCompIso_inv_app_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] {F : Functor C D} {G : Functor D E} [F.Monoidal] [G.Monoidal] (X : Grp C) :

(mapGrpCompIso.inv.app X).hom.hom = CategoryStruct.id (G.obj (F.obj X.X))

source

@[simp]

theorem CategoryTheory.Functor.mapGrpCompIso_hom_app_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] {F : Functor C D} {G : Functor D E} [F.Monoidal] [G.Monoidal] (X : Grp C) :

(mapGrpCompIso.hom.app X).hom.hom = CategoryStruct.id (G.obj (F.obj X.X))

source

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

F.mapGrp ⟶ F'.mapGrp

Natural transformations between functors lift to group objects.

Equations

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

Instances For

source

@[simp]

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

((mapGrpNatTrans f).app X).hom.hom = f.app X.X

source

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

F.mapGrp ≅ F'.mapGrp

Natural isomorphisms between functors lift to group objects.

Equations

CategoryTheory.Functor.mapGrpNatIso e = CategoryTheory.NatIso.ofComponents (fun (X : CategoryTheory.Grp C) => CategoryTheory.Grp.mkIso (e.app X.X) ⋯ ⋯) ⋯

Instances For

source

@[simp]

theorem CategoryTheory.Functor.mapGrpNatIso_hom_app_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {F F' : Functor C D} [F.Monoidal] [F'.Monoidal] (e : F ≅ F') (X : Grp C) :

((mapGrpNatIso e).hom.app X).hom.hom = e.hom.app X.X

source

@[simp]

theorem CategoryTheory.Functor.mapGrpNatIso_inv_app_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {F F' : Functor C D} [F.Monoidal] [F'.Monoidal] (e : F ≅ F') (X : Grp C) :

((mapGrpNatIso e).inv.app X).hom.hom = e.inv.app X.X

source

noncomputable def CategoryTheory.Functor.mapGrpFunctor {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] :

Functor (C ⥤ₗ D) (Functor (Grp C) (Grp D))

mapGrp is functorial in the left-exact functor.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Functor.mapGrpFunctor_map_app {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {F G : C ⥤ₗ D} (α : F ⟶ G) (A : Grp C) :

(mapGrpFunctor.map α).app A = Grp.homMk'' (α.hom.app A.X) ⋯ ⋯

source

@[simp]

theorem CategoryTheory.Functor.mapGrpFunctor_obj {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : C ⥤ₗ D) :

mapGrpFunctor.obj F = F.obj.mapGrp

source

@[reducible, inline]

abbrev CategoryTheory.Functor.FullyFaithful.grpObj {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) (X : C) [GrpObj (F.obj X)] :

GrpObj X

Pullback a group object along a fully faithful monoidal functor.

Equations

hF.grpObj X = { toMonObj := hF.monObj X, inv := hF.preimage CategoryTheory.GrpObj.inv, left_inv := ⋯, right_inv := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.grpObj_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] (hF : F.FullyFaithful) (X : C) [GrpObj (F.obj X)] :

MonObj.mul = hF.preimage (CategoryStruct.comp (OplaxMonoidal.δ F X X) MonObj.mul)

source

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.grpObj_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] (hF : F.FullyFaithful) (X : C) [GrpObj (F.obj X)] :

GrpObj.inv = hF.preimage GrpObj.inv

source

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.grpObj_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] (hF : F.FullyFaithful) (X : C) [GrpObj (F.obj X)] :

MonObj.one = hF.preimage (CategoryStruct.comp (OplaxMonoidal.η F) MonObj.one)

source

@[deprecated CategoryTheory.Functor.FullyFaithful.grpObj (since := "2025-09-13")]

def CategoryTheory.Functor.FullyFaithful.grp_Class {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) (X : C) [GrpObj (F.obj X)] :

GrpObj X

Alias of CategoryTheory.Functor.FullyFaithful.grpObj.

Pullback a group object along a fully faithful monoidal functor.

Equations

@CategoryTheory.Functor.FullyFaithful.grp_Class = @CategoryTheory.Functor.FullyFaithful.grpObj

Instances For

source

@[simp]

theorem CategoryTheory.Functor.essImage_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] {G : Grp D} :

F.mapGrp.essImage G ↔ F.essImage G.X

The essential image of a full and faithful functor between cartesian-monoidal categories is the same on group objects as on objects.

source

noncomputable instance CategoryTheory.Functor.mapGrp.instMonoidal {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory C] [BraidedCategory D] (F : Functor C D) [F.Braided] :

F.mapGrp.Monoidal

Equations

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

source

noncomputable instance CategoryTheory.Functor.mapGrp.instBraided {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory C] [BraidedCategory D] (F : Functor C D) [F.Braided] :

F.mapGrp.Braided

Equations

CategoryTheory.Functor.mapGrp.instBraided F = { toMonoidal := CategoryTheory.Functor.mapGrp.instMonoidal F, braided := ⋯ }

source

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

F.mapGrp ⊣ G.mapGrp

An adjunction of monoidal functors lifts to an adjunction of their lifts to group objects.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Adjunction.mapGrp_unit {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Monoidal] [G.Monoidal] :

a.mapGrp.unit = CategoryStruct.comp Functor.mapGrpIdIso.inv (CategoryStruct.comp (Functor.mapGrpNatTrans a.unit) Functor.mapGrpCompIso.hom)

source

@[simp]

theorem CategoryTheory.Adjunction.mapGrp_counit {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Monoidal] [G.Monoidal] :

a.mapGrp.counit = CategoryStruct.comp Functor.mapGrpCompIso.inv (CategoryStruct.comp (Functor.mapGrpNatTrans a.counit) Functor.mapGrpIdIso.hom)

source

def CategoryTheory.Equivalence.mapGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] :

Grp C ≌ Grp D

An equivalence of categories lifts to an equivalence of their group objects.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Equivalence.mapGrp_inverse {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] :

e.mapGrp.inverse = e.inverse.mapGrp

source

@[simp]

theorem CategoryTheory.Equivalence.mapGrp_functor {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] :

e.mapGrp.functor = e.functor.mapGrp

source

@[simp]

theorem CategoryTheory.Equivalence.mapGrp_counitIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] :

e.mapGrp.counitIso = Functor.mapGrpCompIso.symm ≪≫ Functor.mapGrpNatIso e.counitIso ≪≫ Functor.mapGrpIdIso

source

@[simp]

theorem CategoryTheory.Equivalence.mapGrp_unitIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] :

e.mapGrp.unitIso = Functor.mapGrpIdIso.symm ≪≫ Functor.mapGrpNatIso e.unitIso ≪≫ Functor.mapGrpCompIso

Documentation

Mathlib.CategoryTheory.Monoidal.Grp_

The category of groups in a Cartesian monoidal category #

`Grp C` is cartesian-monoidal #

The category of groups in a Cartesian monoidal category #

Grp C is cartesian-monoidal #

`Grp C` is cartesian-monoidal #