The category of groups in a cartesian monoidal category #

In fact, any monoid object whose associativity diagram is cartesian can be made into a group object (we do not prove this in this file), so we should expect that many properties of group objects follow from this result.

source

@[simp]

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

source

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

source

theorem IsMon_Hom.inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] {X Y : C} [Grp_Class X] [Grp_Class Y] (f : X ⟶ Y) [IsMon_Hom f] :

CategoryTheory.CategoryStruct.comp Grp_Class.inv f = CategoryTheory.CategoryStruct.comp f Grp_Class.inv

source

theorem IsMon_Hom.inv_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] {X Y : C} [Grp_Class X] [Grp_Class Y] (f : X ⟶ Y) [IsMon_Hom f] {Z : C} (h : Y ⟶ Z) :

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

source

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

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

source

theorem Grp_Class.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] {X : C} (h₁ h₂ : Grp_Class X) (H : toMon_Class = toMon_Class) :

h₁ = h₂

source

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

h₁ = h₂ ↔ toMon_Class = toMon_Class

source

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_

Instances For

source

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_

Instances For

source

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

(forget₂Mon_ C).Full

source

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

(forget₂Mon_ C).Faithful

source

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

source

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

source

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

source

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)

Instances For

source

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

source

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

source

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

(forget C).Faithful

source

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

source

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)

Instances For

source

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

source

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

source

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

source

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

CategoryTheory.Limits.HasInitial (Grp_ C)

source

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.

Instances For

source

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

source

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

source

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

source

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

source

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

source

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.

Instances For

source

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

source

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

Documentation

Mathlib.CategoryTheory.Monoidal.Grp_

The category of groups in a cartesian monoidal category #