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.

structure Grp_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] extends Mon_ C : Type (max u₁ v₁)

A group object in a cartesian monoidal category.

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

  The inversion operation

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

@[simp]

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

@[simp]

theorem Grp_.right_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] (self : Grp_ C) {Z : C} (h : self.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.lift (CategoryTheory.CategoryStruct.id self.X) self.inv) (CategoryTheory.CategoryStruct.comp self.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.toUnit self.X) (CategoryTheory.CategoryStruct.comp self.one h)

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

The trivial group object.

Equations

• Grp_.trivial C = { toMon_ := Mon_.trivial C, inv := CategoryTheory.CategoryStruct.id (Mon_.trivial C).X, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Grp_.trivial_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] : (trivial C).mul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (𝟙_ C)).hom

@[simp]

theorem Grp_.trivial_inv (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] : (trivial C).inv = CategoryTheory.CategoryStruct.id (𝟙_ C)

@[simp]

theorem Grp_.trivial_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] : (trivial C).one = CategoryTheory.CategoryStruct.id (𝟙_ C)

@[simp]

theorem Grp_.trivial_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] : (trivial C).X = 𝟙_ C

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

Equations

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

instance Grp_.instCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts 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.ChosenFiniteProducts 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.ChosenFiniteProducts 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.ChosenFiniteProducts C] {A B : Grp_ C} (f g : A ⟶ B) (h : f.hom = g.hom) : f = g

@[simp]

theorem Grp_.id' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts 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.ChosenFiniteProducts C] {A₁ A₂ A₃ : Grp_ C} (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f g

@[simp]

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

@[simp]

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

theorem Grp_.lift_inv_comp_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] {A B : Grp_ C} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.lift f.hom (CategoryTheory.CategoryStruct.comp A.inv f.hom)) B.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.toUnit A.X) B.one

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

@[simp]

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

@[simp]

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

theorem Grp_.lift_inv_comp_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] {A B : Grp_ C} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.lift (CategoryTheory.CategoryStruct.comp A.inv f.hom) f.hom) B.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.toUnit A.X) B.one

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

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

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

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

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

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

Morphisms of group objects preserve inverses.

@[simp]

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

def Grp_.forget₂Mon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts 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_

def Grp_.fullyFaithfulForget₂Mon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts 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.ChosenFiniteProducts C] : (forget₂Mon_ C).Full

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

@[simp]

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

@[simp]

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

@[simp]

theorem Grp_.forget₂Mon_map_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts 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.ChosenFiniteProducts 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_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] (X : Grp_ C) : (forget C).obj X = ((forget₂Mon_ C).obj X).X

@[simp]

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

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

@[simp]

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

def Grp_.mkIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] {M N : Grp_ C} (f : M.X ≅ N.X) (one_f : CategoryTheory.CategoryStruct.comp M.one f.hom = N.one := by aesop_cat) (mul_f : CategoryTheory.CategoryStruct.comp M.mul f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) N.mul := by aesop_cat) : M ≅ N

Constructor for isomorphisms in the category Grp_ C.

Equations

• Grp_.mkIso f one_f mul_f = (Grp_.fullyFaithfulForget₂Mon_ C).preimageIso (Mon_.mkIso f one_f mul_f)

@[simp]

theorem Grp_.mkIso_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] {M N : Grp_ C} (f : M.X ≅ N.X) (one_f : CategoryTheory.CategoryStruct.comp M.one f.hom = N.one := by aesop_cat) (mul_f : CategoryTheory.CategoryStruct.comp M.mul f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) N.mul := by aesop_cat) : (mkIso f one_f mul_f).hom.hom = f.hom

@[simp]

theorem Grp_.mkIso_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] {M N : Grp_ C} (f : M.X ≅ N.X) (one_f : CategoryTheory.CategoryStruct.comp M.one f.hom = N.one := by aesop_cat) (mul_f : CategoryTheory.CategoryStruct.comp M.mul f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) N.mul := by aesop_cat) : (mkIso f one_f mul_f).inv.hom = f.inv

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

Equations

• A.uniqueHomFromTrivial = A.uniqueHomFromTrivial

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

noncomputable def CategoryTheory.Functor.mapGrp {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [Limits.PreservesFiniteProducts F] : 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_one {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [Limits.PreservesFiniteProducts F] (A : Grp_ C) : (F.mapGrp.obj A).one = CategoryStruct.comp (LaxMonoidal.ε F) (F.map A.one)

@[simp]

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

@[simp]

theorem CategoryTheory.Functor.mapGrp_obj_inv {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [Limits.PreservesFiniteProducts F] (A : Grp_ C) : (F.mapGrp.obj A).inv = F.map A.inv

@[simp]

theorem CategoryTheory.Functor.mapGrp_obj_mul {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [Limits.PreservesFiniteProducts F] (A : Grp_ C) : (F.mapGrp.obj A).mul = CategoryStruct.comp (LaxMonoidal.μ F A.X A.X) (F.map A.mul)

@[simp]

theorem CategoryTheory.Functor.mapGrp_obj_X {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : Functor C D) [Limits.PreservesFiniteProducts F] (A : Grp_ C) : (F.mapGrp.obj A).X = F.obj A.X

noncomputable def CategoryTheory.Functor.mapGrpFunctor {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts 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] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts 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] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] {F G : C ⥤ₗ D} (α : F ⟶ G) (A : Grp_ C) : ((mapGrpFunctor.map α).app A).hom = α.app A.X