The category of groups in a Cartesian monoidal category

We define group objects in Cartesian monoidal categories.

We show that the associativity diagram of a group object is always Cartesian and deduce that morphisms of group objects commute with taking inverses.

We show that a finite-product-preserving functor takes group objects to group objects.

class CategoryTheory.GrpObj {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X : C) extends CategoryTheory.MonObj X : Type v₁

A group object internal to a cartesian monoidal category. Also see the bundled Grp.

• one : MonoidalCategoryStruct.tensorUnit C ⟶ X
• mul : MonoidalCategoryStruct.tensorObj X X ⟶ X
• one_mul : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight one X) mul = (MonoidalCategoryStruct.leftUnitor X).hom
• mul_one : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X one) mul = (MonoidalCategoryStruct.rightUnitor X).hom
• mul_assoc : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight mul X) mul = CategoryStruct.comp (MonoidalCategoryStruct.associator X X X).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft X mul) mul)
• inv : X ⟶ X

  The inverse in a group object

• left_inv : CategoryStruct.comp (CartesianMonoidalCategory.lift inv (CategoryStruct.id X)) MonObj.mul = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit X) MonObj.one
• right_inv : CategoryStruct.comp (CartesianMonoidalCategory.lift (CategoryStruct.id X) inv) MonObj.mul = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit X) MonObj.one

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

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

Alias of CategoryTheory.GrpObj.

---

A group object internal to a cartesian monoidal category. Also see the bundled Grp.

Equations

• @CategoryTheory.Grp_Class = @CategoryTheory.GrpObj

def CategoryTheory.MonObj.termι : Lean.ParserDescr

The inverse in a group object

Equations

• CategoryTheory.MonObj.termι = Lean.ParserDescr.node `CategoryTheory.MonObj.termι 1024 (Lean.ParserDescr.symbol "ι")

def CategoryTheory.MonObj.«termι[_]» : Lean.ParserDescr

The inverse in a group object

Equations

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

@[simp]

theorem CategoryTheory.GrpObj.left_inv_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : CartesianMonoidalCategory C} (X : C) [self : GrpObj X] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (CartesianMonoidalCategory.lift inv (CategoryStruct.id X)) (CategoryStruct.comp MonObj.mul h) = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit X) (CategoryStruct.comp MonObj.one h)

@[simp]

theorem CategoryTheory.GrpObj.right_inv_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : CartesianMonoidalCategory C} (X : C) [self : GrpObj X] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (CartesianMonoidalCategory.lift (CategoryStruct.id X) inv) (CategoryStruct.comp MonObj.mul h) = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit X) (CategoryStruct.comp MonObj.one h)

instance CategoryTheory.GrpObj.instTensorUnit {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] : GrpObj (MonoidalCategoryStruct.tensorUnit C)

Equations

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

@[simp]

theorem CategoryTheory.GrpObj.inv_def {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] : inv = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

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

A group object in a Cartesian monoidal category.

• X : C

  The underlying object in the ambient monoidal category

• grp : GrpObj self.X

@[deprecated CategoryTheory.Grp (since := "2025-10-13")]

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

Alias of CategoryTheory.Grp.

---

A group object in a Cartesian monoidal category.

Equations

• CategoryTheory.Grp_ = CategoryTheory.Grp

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

A group object is a monoid object.

Equations

• A.toMon = { X := A.X, mon := A.grp.toMonObj }

@[simp]

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

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

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

Alias of CategoryTheory.Grp.toMon.

---

A group object is a monoid object.

Equations

• @CategoryTheory.Grp.toMon_ = @CategoryTheory.Grp.toMon

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

The trivial group object.

Equations

• CategoryTheory.Grp.trivial C = { X := (CategoryTheory.Mon.trivial C).X, grp := inferInstanceAs (CategoryTheory.GrpObj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) }

@[simp]

theorem CategoryTheory.Grp.trivial_X (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] : (trivial C).X = MonoidalCategoryStruct.tensorUnit C

@[simp]

theorem CategoryTheory.Grp.trivial_grp_one (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] : MonObj.one = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.Grp.trivial_grp_inv (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] : GrpObj.inv = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CategoryTheory.Grp.trivial_grp_mul (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] : MonObj.mul = (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom

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

Equations

• CategoryTheory.Grp.instInhabited = { default := CategoryTheory.Grp.trivial C }

@[deprecated CategoryTheory.Grp.mk (since := "2025-06-15")]

def CategoryTheory.Grp.mk' {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X : C) [grp : GrpObj X] : Grp C

Alias of CategoryTheory.Grp.mk.

Equations

• @CategoryTheory.Grp.mk' = @CategoryTheory.Grp.mk

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

Equations

• CategoryTheory.Grp.instCategory = CategoryTheory.InducedCategory.category CategoryTheory.Grp.toMon

@[simp]

theorem CategoryTheory.Grp.id_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (A : Grp C) : (CategoryStruct.id A).hom = CategoryStruct.id A.X

@[simp]

theorem CategoryTheory.Grp.comp_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {R S T : Grp C} (f : R ⟶ S) (g : S ⟶ T) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

theorem CategoryTheory.Grp.hom_ext {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {A B : Grp C} (f g : A ⟶ B) (h : f.hom = g.hom) : f = g

theorem CategoryTheory.Grp.hom_ext_iff {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {A B : Grp C} {f g : A ⟶ B} : f = g ↔ f.hom = g.hom

@[simp]

theorem CategoryTheory.Grp.id' {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (A : Grp C) : CategoryStruct.id A = CategoryStruct.id A.toMon

@[simp]

theorem CategoryTheory.Grp.comp' {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {A₁ A₂ A₃ : Grp C} (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) : CategoryStruct.comp f g = CategoryStruct.comp f g

@[simp]

theorem CategoryTheory.GrpObj.lift_comp_inv_right {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {A B : C} [GrpObj B] (f : A ⟶ B) : CategoryStruct.comp (CartesianMonoidalCategory.lift f (CategoryStruct.comp f inv)) MonObj.mul = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit A) MonObj.one

@[simp]

theorem CategoryTheory.GrpObj.lift_comp_inv_right_assoc {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {A B : C} [GrpObj B] (f : A ⟶ B) {Z : C} (h : B ⟶ Z) : CategoryStruct.comp (CartesianMonoidalCategory.lift f (CategoryStruct.comp f inv)) (CategoryStruct.comp MonObj.mul h) = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit A) (CategoryStruct.comp MonObj.one h)

theorem CategoryTheory.GrpObj.lift_inv_comp_right {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {A B : C} [GrpObj A] [GrpObj B] (f : A ⟶ B) [IsMonHom f] : CategoryStruct.comp (CartesianMonoidalCategory.lift f (CategoryStruct.comp inv f)) MonObj.mul = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit A) MonObj.one

theorem CategoryTheory.GrpObj.lift_inv_comp_right_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 (CartesianMonoidalCategory.lift f (CategoryStruct.comp inv f)) (CategoryStruct.comp MonObj.mul h) = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit A) (CategoryStruct.comp MonObj.one h)

@[simp]

theorem CategoryTheory.GrpObj.lift_comp_inv_left {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {A B : C} [GrpObj B] (f : A ⟶ B) : CategoryStruct.comp (CartesianMonoidalCategory.lift (CategoryStruct.comp f inv) f) MonObj.mul = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit A) MonObj.one

@[simp]

theorem CategoryTheory.GrpObj.lift_comp_inv_left_assoc {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {A B : C} [GrpObj B] (f : A ⟶ B) {Z : C} (h : B ⟶ Z) : CategoryStruct.comp (CartesianMonoidalCategory.lift (CategoryStruct.comp f inv) f) (CategoryStruct.comp MonObj.mul h) = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit A) (CategoryStruct.comp MonObj.one h)

theorem CategoryTheory.GrpObj.lift_inv_comp_left {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {A B : C} [GrpObj A] [GrpObj B] (f : A ⟶ B) [IsMonHom f] : CategoryStruct.comp (CartesianMonoidalCategory.lift (CategoryStruct.comp inv f) f) MonObj.mul = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit A) MonObj.one

theorem CategoryTheory.GrpObj.lift_inv_comp_left_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 (CartesianMonoidalCategory.lift (CategoryStruct.comp inv f) f) (CategoryStruct.comp MonObj.mul h) = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit A) (CategoryStruct.comp MonObj.one h)

theorem CategoryTheory.GrpObj.eq_lift_inv_left {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {A B : C} [GrpObj B] (f g h : A ⟶ B) : f = CategoryStruct.comp (CartesianMonoidalCategory.lift (CategoryStruct.comp g inv) h) MonObj.mul ↔ CategoryStruct.comp (CartesianMonoidalCategory.lift g f) MonObj.mul = h

theorem CategoryTheory.GrpObj.lift_inv_left_eq {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {A B : C} [GrpObj B] (f g h : A ⟶ B) : CategoryStruct.comp (CartesianMonoidalCategory.lift (CategoryStruct.comp f inv) g) MonObj.mul = h ↔ g = CategoryStruct.comp (CartesianMonoidalCategory.lift f h) MonObj.mul

theorem CategoryTheory.GrpObj.eq_lift_inv_right {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {A B : C} [GrpObj B] (f g h : A ⟶ B) : f = CategoryStruct.comp (CartesianMonoidalCategory.lift g (CategoryStruct.comp h inv)) MonObj.mul ↔ CategoryStruct.comp (CartesianMonoidalCategory.lift f h) MonObj.mul = g

theorem CategoryTheory.GrpObj.lift_inv_right_eq {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {A B : C} [GrpObj B] (f g h : A ⟶ B) : CategoryStruct.comp (CartesianMonoidalCategory.lift f (CategoryStruct.comp g inv)) MonObj.mul = h ↔ f = CategoryStruct.comp (CartesianMonoidalCategory.lift h g) MonObj.mul

theorem CategoryTheory.GrpObj.lift_left_mul_ext {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {A B : C} [GrpObj B] {f g : A ⟶ B} (i : A ⟶ B) (h : CategoryStruct.comp (CartesianMonoidalCategory.lift f i) MonObj.mul = CategoryStruct.comp (CartesianMonoidalCategory.lift g i) MonObj.mul) : f = g

@[simp]

theorem CategoryTheory.GrpObj.inv_comp_inv {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (A : C) [GrpObj A] : CategoryStruct.comp inv inv = CategoryStruct.id A

@[simp]

theorem CategoryTheory.GrpObj.inv_comp_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (A : C) [GrpObj A] {Z : C} (h : A ⟶ Z) : CategoryStruct.comp inv (CategoryStruct.comp inv h) = h

@[reducible, inline]

abbrev CategoryTheory.GrpObj.ofIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {G X : C} [GrpObj G] (e : G ≅ X) : GrpObj X

Transfer GrpObj along an isomorphism.

Equations

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

theorem CategoryTheory.GrpObj.ofIso_mul {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {G X : C} [GrpObj G] (e : G ≅ X) : MonObj.mul = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.inv e.inv) (CategoryStruct.comp MonObj.mul e.hom)

theorem CategoryTheory.GrpObj.ofIso_one {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {G X : C} [GrpObj G] (e : G ≅ X) : MonObj.one = CategoryStruct.comp MonObj.one e.hom

theorem CategoryTheory.GrpObj.ofIso_inv {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {G X : C} [GrpObj G] (e : G ≅ X) : inv = CategoryStruct.comp e.inv (CategoryStruct.comp inv e.hom)

instance CategoryTheory.GrpObj.instIsIsoInv {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (A : C) [GrpObj A] : IsIso inv

@[simp]

theorem CategoryTheory.GrpObj.inv_inv {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (A : C) [GrpObj A] : CategoryTheory.inv inv = inv

For inv ≫ inv = 𝟙 see inv_comp_inv.

theorem CategoryTheory.GrpObj.mul_inv {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : C) [GrpObj A] : CategoryStruct.comp MonObj.mul inv = CategoryStruct.comp (β_ A A).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom inv inv) MonObj.mul)

theorem CategoryTheory.GrpObj.mul_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : C) [GrpObj A] {Z : C} (h : A ⟶ Z) : CategoryStruct.comp MonObj.mul (CategoryStruct.comp inv h) = CategoryStruct.comp (β_ A A).hom (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom inv inv) (CategoryStruct.comp MonObj.mul h))

theorem CategoryTheory.GrpObj.tensorHom_inv_inv_mul {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : C) [GrpObj A] : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom inv inv) MonObj.mul = CategoryStruct.comp (β_ A A).hom (CategoryStruct.comp MonObj.mul inv)

theorem CategoryTheory.GrpObj.tensorHom_inv_inv_mul_assoc {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : C) [GrpObj A] {Z : C} (h : A ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.tensorHom inv inv) (CategoryStruct.comp MonObj.mul h) = CategoryStruct.comp (β_ A A).hom (CategoryStruct.comp MonObj.mul (CategoryStruct.comp inv h))

theorem CategoryTheory.GrpObj.mul_inv_rev {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (G : C) [GrpObj G] : CategoryStruct.comp MonObj.mul inv = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom inv inv) (CategoryStruct.comp (β_ G G).hom MonObj.mul)

theorem CategoryTheory.GrpObj.mul_inv_rev_assoc {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (G : C) [GrpObj G] {Z : C} (h : G ⟶ Z) : CategoryStruct.comp MonObj.mul (CategoryStruct.comp inv h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom inv inv) (CategoryStruct.comp (β_ G G).hom (CategoryStruct.comp MonObj.mul h))

def CategoryTheory.GrpObj.mulRight {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {A : C} [GrpObj A] (f : MonoidalCategoryStruct.tensorUnit C ⟶ A) : A ≅ A

The map (· * f).

Equations

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

@[simp]

theorem CategoryTheory.GrpObj.mulRight_inv {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {A : C} [GrpObj A] (f : MonoidalCategoryStruct.tensorUnit C ⟶ A) : (mulRight f).inv = CategoryStruct.comp (CartesianMonoidalCategory.lift (CategoryStruct.id A) (CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit A) (CategoryStruct.comp f inv))) MonObj.mul

@[simp]

theorem CategoryTheory.GrpObj.mulRight_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {A : C} [GrpObj A] (f : MonoidalCategoryStruct.tensorUnit C ⟶ A) : (mulRight f).hom = CategoryStruct.comp (CartesianMonoidalCategory.lift (CategoryStruct.id A) (CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit A) f)) MonObj.mul

@[simp]

theorem CategoryTheory.GrpObj.mulRight_one {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (A : C) [GrpObj A] : mulRight MonObj.one = Iso.refl A

theorem CategoryTheory.GrpObj.isPullback {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (A : C) [GrpObj A] : IsPullback (MonoidalCategoryStruct.whiskerRight MonObj.mul A) (CategoryStruct.comp (MonoidalCategoryStruct.associator A A A).hom (MonoidalCategoryStruct.whiskerLeft A MonObj.mul)) MonObj.mul MonObj.mul

The associativity diagram of a group object is Cartesian.

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.

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

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

theorem CategoryTheory.GrpObj.toMonObj_injective {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {X : C} : Function.Injective (@toMonObj C inst✝ inst✝¹ X)

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

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₂

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

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.

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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)

@[simp]

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

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

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

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

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

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)

@[simp]

theorem CategoryTheory.Grp.mkIso'_inv_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 = e.inv

@[simp]

theorem CategoryTheory.Grp.mkIso'_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 = e.hom

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

@[simp]

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 = e.inv

@[simp]

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 = e.hom

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

Equations

• A.uniqueHomFromTrivial = A.toMon.uniqueHomFromTrivial

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

Grp C is cartesian-monoidal

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.

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

@[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₁✝.toMon ⟶ Y₁✝.toMon) (g : X₂✝.toMon ⟶ Y₂✝.toMon) : (MonoidalCategoryStruct.tensorHom f g).hom = MonoidalCategoryStruct.tensorHom f.hom g.hom

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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 = MonoidalCategoryStruct.whiskerRight f.hom I.X

@[simp]

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 = MonoidalCategoryStruct.whiskerLeft G.X f.hom

@[simp]

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 = (MonoidalCategoryStruct.leftUnitor G.X).hom

@[simp]

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 = (MonoidalCategoryStruct.leftUnitor G.X).inv

@[simp]

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 = (MonoidalCategoryStruct.rightUnitor G.X).hom

@[simp]

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 = (MonoidalCategoryStruct.rightUnitor G.X).inv

@[simp]

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 = (MonoidalCategoryStruct.associator G.X H.X I.X).hom

@[simp]

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 = (MonoidalCategoryStruct.associator G.X H.X I.X).inv

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.

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.

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

@[simp]

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 = SemiCartesianMonoidalCategory.fst G.X H.X

@[simp]

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 = SemiCartesianMonoidalCategory.snd G.X H.X

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.

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

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

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

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

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.

@[simp]

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 = (β_ G.X H.X).hom

@[simp]

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 = (β_ G.X H.X).inv

@[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 := ⋯ }

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

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

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.

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

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

@[simp]

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

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

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

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

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

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.

@[simp]

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

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

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

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

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

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.

@[simp]

theorem CategoryTheory.Functor.mapGrpIdIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X : Grp C) : (mapGrpIdIso.inv.app X).hom = CategoryStruct.id X.X

@[simp]

theorem CategoryTheory.Functor.mapGrpIdIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X : Grp C) : (mapGrpIdIso.hom.app X).hom = CategoryStruct.id X.X

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.

@[simp]

theorem CategoryTheory.Functor.mapGrpCompIso_hom_app_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 = CategoryStruct.id (G.obj (F.obj X.X))

@[simp]

theorem CategoryTheory.Functor.mapGrpCompIso_inv_app_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 = CategoryStruct.id (G.obj (F.obj X.X))

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

• CategoryTheory.Functor.mapGrpNatTrans f = { app := fun (X : CategoryTheory.Grp C) => CategoryTheory.Mon.Hom.mk' (f.app X.X) ⋯ ⋯, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Functor.mapGrpNatTrans_app_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 = f.app X.X

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) ⋯ ⋯) ⋯

@[simp]

theorem CategoryTheory.Functor.mapGrpNatIso_hom_app_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 = e.hom.app X.X

@[simp]

theorem CategoryTheory.Functor.mapGrpNatIso_inv_app_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 = e.inv.app X.X

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.

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

@[simp]

theorem CategoryTheory.Functor.mapGrpFunctor_map_app_hom {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).hom = α.app A.X

@[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 := ⋯ }

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

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

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

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

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

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.

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 := ⋯ }

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.

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

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

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.

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

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

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

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