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

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

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

  The inverse in a group object

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

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

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

Alias of GrpObj.

---

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

Equations

• @Grp_Class = @GrpObj

def MonObj.termι : Lean.ParserDescr

The inverse in a group object

Equations

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

def 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 GrpObj.right_inv_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.CartesianMonoidalCategory C} (X : C) [self : GrpObj X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) inv) (CategoryTheory.CategoryStruct.comp MonObj.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit X) (CategoryTheory.CategoryStruct.comp MonObj.one h)

@[simp]

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

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

Equations

• GrpObj.instTensorUnit = { toMonObj := MonObj.instTensorUnit, inv := CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C), left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

structure Grp_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.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

def Grp_.toMon_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.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 Grp_.toMon__X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Grp_ C) : A.toMon_.X = A.X

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

The trivial group object.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

• Grp_.instInhabited = { default := Grp_.trivial C }

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

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

Alias of Grp_.mk.

Equations

• @Grp_.mk' = @Grp_.mk

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

Equations

• Grp_.instCategory = CategoryTheory.InducedCategory.category Grp_.toMon_

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[reducible, inline]

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

Transfer GrpObj along an isomorphism.

Equations

• GrpObj.ofIso e = { toMonObj := MonObj.ofIso e, inv := CategoryTheory.CategoryStruct.comp e.inv (CategoryTheory.CategoryStruct.comp GrpObj.inv e.hom), left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

For inv ≫ inv = 𝟙 see inv_comp_inv.

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

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

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

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

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

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

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

The map (· * f).

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem GrpObj.isPullback {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : C) [GrpObj A] : CategoryTheory.IsPullback (CategoryTheory.MonoidalCategoryStruct.whiskerRight MonObj.mul A) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A A).hom (CategoryTheory.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 GrpObj.inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : C} [GrpObj A] [GrpObj B] (f : A ⟶ B) [IsMon_Hom f] : CategoryTheory.CategoryStruct.comp inv f = CategoryTheory.CategoryStruct.comp f inv

Morphisms of group objects preserve inverses.

@[simp]

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

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

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

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

Alias of GrpObj.toMonObj_injective.

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

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

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

Equations

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

@[simp]

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

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

The forgetful functor from group objects to monoid objects.

Equations

• Grp_.forget₂Mon_ C = CategoryTheory.inducedFunctor Grp_.toMon_

@[simp]

theorem Grp_.forget₂Mon__obj_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Grp_ C) : ((forget₂Mon_ C).obj A).X = A.X

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

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

Equations

• Grp_.fullyFaithfulForget₂Mon_ C = CategoryTheory.fullyFaithfulInducedFunctor Grp_.toMon_

instance Grp_.instFullMon_Forget₂Mon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] : (forget₂Mon_ C).Full

instance Grp_.instFaithfulMon_Forget₂Mon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] : (forget₂Mon_ C).Faithful

@[simp]

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

@[simp]

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

@[simp]

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

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

The forgetful functor from group objects to the ambient category.

Equations

• Grp_.forget C = (Grp_.forget₂Mon_ C).comp (Mon_.forget C)

@[simp]

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

@[simp]

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

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

@[simp]

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

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

def Grp_.mkIso' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : C} (e : G ≅ H) [GrpObj G] [GrpObj H] [IsMon_Hom e.hom] : { X := G, grp := inst✝ } ≅ { X := H, grp := inst✝¹ }

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

Equations

• Grp_.mkIso' e = (Grp_.fullyFaithfulForget₂Mon_ C).preimageIso (Mon_.mkIso' e)

@[simp]

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

@[simp]

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

@[reducible, inline]

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

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

Equations

• Grp_.mkIso e one_f mul_f = Grp_.mkIso' e

@[simp]

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

@[simp]

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

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

Equations

• A.uniqueHomFromTrivial = A.toMon_.uniqueHomFromTrivial

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

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_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_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_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_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 Grp(F) : Grp C ⥤ Grp D is fully faithful too.

Equations

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

@[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} [F.Monoidal] {G : Functor D E} [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} [F.Monoidal] {G : Functor D E} [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

• CategoryTheory.Functor.mapGrpIdIso = CategoryTheory.NatIso.ofComponents (fun (X : Grp_ C) => Grp_.mkIso (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id C).mapGrp.obj X).X) ⋯ ⋯) ⋯

@[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} [F.Monoidal] {G : Functor D E} [G.Monoidal] : (F.comp G).mapGrp ≅ F.mapGrp.comp G.mapGrp

The composition functor is also the composition on group objects.

Equations

• CategoryTheory.Functor.mapGrpCompIso = CategoryTheory.NatIso.ofComponents (fun (X : Grp_ C) => Grp_.mkIso (CategoryTheory.Iso.refl ((F.comp G).mapGrp.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} [F.Monoidal] {G : Functor D E} [G.Monoidal] (X : Grp_ C) : (mapGrpCompIso.inv.app X).hom = CategoryStruct.id (G.obj (F.obj X.X))

@[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} [F.Monoidal] {G : Functor D E} [G.Monoidal] (X : Grp_ C) : (mapGrpCompIso.hom.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 : Grp_ C) => Mon_.Hom.mk' (f.app X.toMon_.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 : Grp_ C) => Grp_.mkIso (e.app X.toMon_.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

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

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

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

@[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 GrpObj.inv, left_inv := ⋯, right_inv := ⋯ }

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

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

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

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

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