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

theorem CategoryTheory.AddGrpObj.isPullback {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (A : C) [AddGrpObj A] :

IsPullback (MonoidalCategoryStruct.whiskerRight AddMonObj.add A) (CategoryStruct.comp (MonoidalCategoryStruct.associator A A A).hom (MonoidalCategoryStruct.whiskerLeft A AddMonObj.add)) AddMonObj.add AddMonObj.add

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

CategoryStruct.comp neg f = CategoryStruct.comp f neg

Morphisms of group objects preserve negations.

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

@[simp]

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

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

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

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

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

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.AddGrpObj.ext {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {X : C} (h₁ h₂ : AddGrpObj X) (H : h₁.toAddMonObj = h₂.toAddMonObj) :

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

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

h₁ = h₂ ↔ h₁.toAddMonObj = h₂.toAddMonObj

source

@[implicit_reducible]

def CategoryTheory.GrpObj.ofInvertible {C : Type u₁} [Category.{v₁, u₁} C] (G : C) [CartesianMonoidalCategory C] [MonObj G] (h : (X : C) → (f : X ⟶ G) → Invertible f) :

GrpObj G

A monoid object with invertible homs is a group object.

Equations

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

Instances For

source

@[implicit_reducible]

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

@[implicit_reducible]

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

AddGrpObj (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

@[simp]

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

neg = MonoidalCategoryStruct.tensorHom neg neg

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

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

Functor (AddGrp C) (AddMon C)

The forgetful functor from additive group objects to additive monoid objects.

Equations

CategoryTheory.AddGrp.forget₂Mon C = CategoryTheory.inducedFunctor CategoryTheory.AddGrp.toAddMon

Instances For

source

@[simp]

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

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

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

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

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

(forget₂Mon C).FullyFaithful

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

Equations

CategoryTheory.AddGrp.fullyFaithfulForget₂Mon C = CategoryTheory.fullyFaithfulInducedFunctor CategoryTheory.AddGrp.toAddMon

Instances For

source

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

(forget₂Mon C).Full

source

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

instance CategoryTheory.AddGrp.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.AddGrp.forget₂AddMon_obj_zero {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (A : AddGrp C) :

AddMonObj.zero = AddMonObj.zero

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.AddGrp.forget₂AddMon_obj_add {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (A : AddGrp C) :

AddMonObj.add = AddMonObj.add

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

@[simp]

theorem CategoryTheory.AddGrp.forget₂AddMon_map_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {A B : AddGrp 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

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

Functor (AddGrp C) C

The forgetful functor from additive group objects to the ambient category.

Equations

CategoryTheory.AddGrp.forget C = (CategoryTheory.AddGrp.forget₂Mon C).comp (CategoryTheory.AddMon.forget C)

Instances For

source

@[simp]

theorem CategoryTheory.AddGrp.forget_obj (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X : AddGrp 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

@[simp]

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

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

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

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

(forget C).Faithful

source

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

@[simp]

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

(forget₂Mon C).comp (AddMon.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

instance CategoryTheory.AddGrp.instIsIsoHomHomMon (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {G H : AddGrp 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

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

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

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

Equations

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

Instances For

source

@[simp]

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

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

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

@[simp]

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

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

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

@[reducible, inline]

abbrev CategoryTheory.AddGrp.mkIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {G H : AddGrp C} (e : G.X ≅ H.X) (zero_f : CategoryStruct.comp AddMonObj.zero e.hom = AddMonObj.zero := by cat_disch) (add_f : CategoryStruct.comp AddMonObj.add e.hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.hom e.hom) AddMonObj.add := by cat_disch) :

G ≅ H

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

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.AddGrp.mkIso_inv_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {G H : AddGrp C} (e : G.X ≅ H.X) (zero_f : CategoryStruct.comp AddMonObj.zero e.hom = AddMonObj.zero := by cat_disch) (add_f : CategoryStruct.comp AddMonObj.add e.hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.hom e.hom) AddMonObj.add := by cat_disch) :

(mkIso e zero_f add_f).inv.hom.hom = e.inv

source

@[simp]

theorem CategoryTheory.AddGrp.mkIso_hom_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {G H : AddGrp C} (e : G.X ≅ H.X) (zero_f : CategoryStruct.comp AddMonObj.zero e.hom = AddMonObj.zero := by cat_disch) (add_f : CategoryStruct.comp AddMonObj.add e.hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.hom e.hom) AddMonObj.add := by cat_disch) :

(mkIso e zero_f add_f).hom.hom.hom = e.hom

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

@[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

@[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

@[implicit_reducible]

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

@[implicit_reducible]

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

Unique (trivial C ⟶ A)

Equations

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

source

@[implicit_reducible]

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

Unique (A ⟶ trivial C)

Equations

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

source

@[implicit_reducible]

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

Unique (A ⟶ trivial C)

Equations

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

source

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

Limits.HasZeroObject (Grp C)

source

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

Limits.HasZeroObject (AddGrp C)

source

@[implicit_reducible]

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

Limits.HasZeroMorphisms (Grp C)

Equations

CategoryTheory.Grp.instHasZeroMorphisms = CategoryTheory.Limits.HasZeroObject.zeroMorphismsOfZeroObject

source

@[implicit_reducible]

noncomputable instance CategoryTheory.AddGrp.instHasZeroMorphisms {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] :

Limits.HasZeroMorphisms (AddGrp C)

Equations

CategoryTheory.AddGrp.instHasZeroMorphisms = CategoryTheory.Limits.HasZeroObject.zeroMorphismsOfZeroObject

`Grp C` is cartesian-monoidal #

source

@[implicit_reducible]

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

@[implicit_reducible]

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

MonoidalCategoryStruct (AddGrp 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.AddGrp.tensorHom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {X₁✝ Y₁✝ X₂✝ Y₂✝ : AddGrp C} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) :

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

source

@[simp]

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

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

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.AddGrp.tensorAddUnit_X {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :

(MonoidalCategoryStruct.tensorUnit (AddGrp 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.AddGrp.tensorAddUnit_zero {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :

AddMonObj.zero = AddMonObj.zero

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.AddGrp.tensorAddUnit_add {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :

AddMonObj.add = AddMonObj.add

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.AddGrp.tensorObj_zero {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (G H : AddGrp C) :

AddMonObj.zero = AddMonObj.zero

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.AddGrp.tensorObj_add {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (G H : AddGrp C) :

AddMonObj.add = AddMonObj.add

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.AddGrp.whiskerLeft_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : AddGrp C} (f : G ⟶ H) (I : AddGrp 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.AddGrp.whiskerRight_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (G : AddGrp C) {H I : AddGrp 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.AddGrp.leftUnitor_hom_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (G : AddGrp 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.AddGrp.leftUnitor_neg_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (G : AddGrp 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.AddGrp.rightUnitor_hom_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (G : AddGrp 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.AddGrp.rightUnitor_neg_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (G : AddGrp 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.AddGrp.associator_hom_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (G H I : AddGrp 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

@[simp]

theorem CategoryTheory.AddGrp.associator_neg_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (G H I : AddGrp 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

@[implicit_reducible]

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

@[implicit_reducible]

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

MonoidalCategory (AddGrp C)

Equations

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

source

@[implicit_reducible]

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

@[implicit_reducible]

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

CartesianMonoidalCategory (AddGrp 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.AddGrp.lift_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H₁ H₂ : AddGrp 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.AddGrp.fst_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (G H : AddGrp 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

@[simp]

theorem CategoryTheory.AddGrp.snd_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (G H : AddGrp 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

@[implicit_reducible]

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

@[implicit_reducible]

instance CategoryTheory.AddGrp.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.AddGrp.δ_def {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (G H : AddGrp C) :

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

source

@[simp]

theorem CategoryTheory.AddGrp.η_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 (AddGrp C)))

source

@[simp]

theorem CategoryTheory.AddGrp.μ_def {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (G H : AddGrp 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.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] :

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

source

@[simp]

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

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

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

@[implicit_reducible]

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

@[implicit_reducible]

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

BraidedCategory (AddGrp 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.AddGrp.braiding_hom_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (G H : AddGrp 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

@[simp]

theorem CategoryTheory.AddGrp.braiding_neg_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (G H : AddGrp 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

@[reducible, inline]

abbrev CategoryTheory.Functor.addGrpObjObj {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} [AddGrpObj G] :

AddGrpObj (F.obj G)

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

Equations

CategoryTheory.Functor.addGrpObjObj = { toAddMonObj := CategoryTheory.Functor.addMonObjObj G, neg := F.map CategoryTheory.AddGrpObj.neg, left_neg := ⋯, right_neg := ⋯ }

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

@[simp]

theorem CategoryTheory.Functor.obj.neg_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} [AddGrpObj G] :

AddGrpObj.neg = F.map AddGrpObj.neg

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

theorem CategoryTheory.Functor.obj.neg_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} [AddGrpObj G] {Z : D} (h : F.obj G ⟶ Z) :

CategoryStruct.comp AddGrpObj.neg h = CategoryStruct.comp (F.map AddGrpObj.neg) 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

def CategoryTheory.Functor.mapAddGrp {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 (AddGrp C) (AddGrp D)

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

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Functor.mapAddGrp_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 : AddGrp C) :

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

source

@[simp]

theorem CategoryTheory.Functor.mapAddGrp_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✝ : AddGrp C} (f : X✝ ⟶ Y✝) :

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

source

@[simp]

theorem CategoryTheory.Functor.mapAddGrp_obj_addGrp_zero {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 : AddGrp C) :

AddMonObj.zero = CategoryStruct.comp (LaxMonoidal.ε F) (F.map AddMonObj.zero)

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_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_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_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.mapAddGrp_obj_addGrp_neg {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 : AddGrp C) :

AddGrpObj.neg = F.map AddGrpObj.neg

source

@[simp]

theorem CategoryTheory.Functor.mapAddGrp_obj_addGrp_add {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 : AddGrp C) :

AddMonObj.add = CategoryStruct.comp (LaxMonoidal.μ F A.X A.X) (F.map AddMonObj.add)

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

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.Faithful.mapAddGrp {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.mapAddGrp.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 F.mapGrp : Grp C ⥤ Grp D is fully faithful too.

Equations

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

Instances For

source

def CategoryTheory.Functor.FullyFaithful.mapAddGrp {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.mapAddGrp.FullyFaithful

If F : C ⥤ D is a fully faithful monoidal functor, then F.mapAddGrp : AddGrp C ⥤ AddGrp D is fully faithful too.

Equations

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

Instances For

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

instance CategoryTheory.Functor.Full.mapAddGrp {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.mapAddGrp.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.mapAddGrp_id_zero {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (A : AddGrp C) :

AddMonObj.zero = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)) AddMonObj.zero

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.mapAddGrp_id_add {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (A : AddGrp C) :

AddMonObj.add = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorObj A.X A.X)) AddMonObj.add

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_mapAddGrp_zero {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 : AddGrp C) :

AddMonObj.zero = CategoryStruct.comp (LaxMonoidal.ε (F.comp G)) ((F.comp G).map AddMonObj.zero)

source

theorem CategoryTheory.Functor.comp_mapGrp_one_assoc {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) {Z : E} (h : ((F.comp G).mapGrp.obj A).X ⟶ Z) :

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

source

theorem CategoryTheory.Functor.comp_mapAddGrp_zero_assoc {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 : AddGrp C) {Z : E} (h : ((F.comp G).mapAddGrp.obj A).X ⟶ Z) :

CategoryStruct.comp AddMonObj.zero h = CategoryStruct.comp (CategoryStruct.comp (LaxMonoidal.ε (F.comp G)) (G.map (F.map AddMonObj.zero))) h

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

@[simp]

theorem CategoryTheory.Functor.comp_mapAddGrp_add {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 : AddGrp C) :

AddMonObj.add = CategoryStruct.comp (LaxMonoidal.μ (F.comp G) A.X A.X) ((F.comp G).map AddMonObj.add)

source

theorem CategoryTheory.Functor.comp_mapAddGrp_add_assoc {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 : AddGrp C) {Z : E} (h : ((F.comp G).mapAddGrp.obj A).X ⟶ Z) :

CategoryStruct.comp AddMonObj.add h = CategoryStruct.comp (CategoryStruct.comp (LaxMonoidal.μ (F.comp G) A.X A.X) (G.map (F.map AddMonObj.add))) h

source

theorem CategoryTheory.Functor.comp_mapGrp_mul_assoc {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) {Z : E} (h : ((F.comp G).mapGrp.obj A).X ⟶ Z) :

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

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

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

(Functor.id C).mapAddGrp ≅ Functor.id (AddGrp C)

The identity functor is also the identity on additive 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.mapAddGrpIdIso_inv_app_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X : AddGrp C) :

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

source

@[simp]

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

(mapAddGrpIdIso.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

def CategoryTheory.Functor.mapAddGrpCompIso {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).mapAddGrp ≅ F.mapAddGrp.comp G.mapAddGrp

The composition functor is also the composition on additive group objects.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Functor.mapAddGrpCompIso_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 : AddGrp C) :

(mapAddGrpCompIso.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

@[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.mapAddGrpCompIso_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 : AddGrp C) :

(mapAddGrpCompIso.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

def CategoryTheory.Functor.mapAddGrpNatTrans {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.mapAddGrp ⟶ F'.mapAddGrp

Natural transformations between functors lift to additive 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

@[simp]

theorem CategoryTheory.Functor.mapAddGrpNatTrans_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 : AddGrp C) :

((mapAddGrpNatTrans 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

def CategoryTheory.Functor.mapAddGrpNatIso {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.mapAddGrp ≅ F'.mapAddGrp

Natural isomorphisms between functors lift to additive group objects.

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Functor.mapAddGrpNatIso_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 : AddGrp C) :

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

source

@[simp]

theorem CategoryTheory.Functor.mapAddGrpNatIso_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 : AddGrp C) :

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

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

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

Functor (C ⥤ₗ D) (Functor (AddGrp C) (AddGrp D))

mapAddGrp 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.mapAddGrpFunctor_obj {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : C ⥤ₗ D) :

mapAddGrpFunctor.obj F = F.obj.mapAddGrp

source

@[simp]

theorem CategoryTheory.Functor.mapAddGrpFunctor_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 : AddGrp C) :

(mapAddGrpFunctor.map α).app A = AddGrp.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

@[reducible, inline]

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

AddGrpObj X

Pullback an additive group object along a fully faithful monoidal functor.

Equations

hF.addGrpObj X = { toAddMonObj := hF.addMonObj X, neg := hF.preimage CategoryTheory.AddGrpObj.neg, left_neg := ⋯, right_neg := ⋯ }

Instances For

source

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.addGrpObj_zero {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) [AddGrpObj (F.obj X)] :

AddMonObj.zero = hF.preimage (CategoryStruct.comp (OplaxMonoidal.η F) AddMonObj.zero)

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

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.addGrpObj_neg {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) [AddGrpObj (F.obj X)] :

AddGrpObj.neg = hF.preimage AddGrpObj.neg

source

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.addGrpObj_add {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) [AddGrpObj (F.obj X)] :

AddMonObj.add = hF.preimage (CategoryStruct.comp (OplaxMonoidal.δ F X X) AddMonObj.add)

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

@[simp]

theorem CategoryTheory.Functor.essImage_mapAddGrp {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 : AddGrp D} :

F.mapAddGrp.essImage G ↔ F.essImage G.X

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

source

@[implicit_reducible]

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

@[implicit_reducible]

noncomputable instance CategoryTheory.Functor.mapAddGrp.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.mapAddGrp.Monoidal

Equations

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

source

@[implicit_reducible]

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

@[implicit_reducible]

noncomputable instance CategoryTheory.Functor.mapAddGrp.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.mapAddGrp.Braided

Equations

CategoryTheory.Functor.mapAddGrp.instBraided F = { toMonoidal := CategoryTheory.Functor.mapAddGrp.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

def CategoryTheory.Adjunction.mapAddGrp {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.mapAddGrp ⊣ G.mapAddGrp

An adjunction of monoidal functors lifts to an adjunction of their lifts to additive 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

@[simp]

theorem CategoryTheory.Adjunction.mapAddGrp_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.mapAddGrp.counit = CategoryStruct.comp Functor.mapAddGrpCompIso.inv (CategoryStruct.comp (Functor.mapAddGrpNatTrans a.counit) Functor.mapAddGrpIdIso.hom)

source

@[simp]

theorem CategoryTheory.Adjunction.mapAddGrp_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.mapAddGrp.unit = CategoryStruct.comp Functor.mapAddGrpIdIso.inv (CategoryStruct.comp (Functor.mapAddGrpNatTrans a.unit) Functor.mapAddGrpCompIso.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

def CategoryTheory.Equivalence.mapAddGrp {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] :

AddGrp C ≌ AddGrp D

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

Equations

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

Instances For

source

@[simp]

theorem CategoryTheory.Equivalence.mapAddGrp_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.mapAddGrp.inverse = e.inverse.mapAddGrp

source

@[simp]

theorem CategoryTheory.Equivalence.mapAddGrp_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.mapAddGrp.functor = e.functor.mapAddGrp

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.mapAddGrp_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.mapAddGrp.counitIso = Functor.mapAddGrpCompIso.symm ≪≫ Functor.mapAddGrpNatIso e.counitIso ≪≫ Functor.mapAddGrpIdIso

source

@[simp]

theorem CategoryTheory.Equivalence.mapAddGrp_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.mapAddGrp.unitIso = Functor.mapAddGrpIdIso.symm ≪≫ Functor.mapAddGrpNatIso e.unitIso ≪≫ Functor.mapAddGrpCompIso

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_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_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 #