The category of commutative groups in a cartesian monoidal category

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

A commutative group object internal to 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
• 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
• mul_comm : CategoryTheory.CategoryStruct.comp (β_ self.X self.X).hom self.mul = self.mul

@[simp]

theorem CommGrp_.mul_comm_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] (self : CommGrp_ C) {Z : C} (h : self.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (β_ self.X self.X).hom (CategoryTheory.CategoryStruct.comp self.mul h) = CategoryTheory.CategoryStruct.comp self.mul h

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

The trivial commutative group object.

Equations

• CommGrp_.trivial C = { toGrp_ := Grp_.trivial C, mul_comm := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

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

Equations

• CommGrp_.instCategory = CategoryTheory.InducedCategory.category CommGrp_.toGrp_

@[simp]

theorem CommGrp_.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 CommGrp_.comp_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] {R S T : CommGrp_ C} (f : R ⟶ S) (g : S ⟶ T) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

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

@[simp]

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

@[simp]

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

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

The forgetful functor from commutative group objects to group objects.

Equations

• CommGrp_.forget₂Grp_ C = CategoryTheory.inducedFunctor CommGrp_.toGrp_

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

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

Equations

• CommGrp_.fullyFaithfulForget₂Grp_ C = CategoryTheory.fullyFaithfulInducedFunctor CommGrp_.toGrp_

instance CommGrp_.instFullGrp_Forget₂Grp_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] : (forget₂Grp_ C).Full

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

@[simp]

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

@[simp]

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

@[simp]

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

def CommGrp_.forget₂CommMon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] : CategoryTheory.Functor (CommGrp_ C) (CommMon_ C)

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

Equations

• CommGrp_.forget₂CommMon_ C = CategoryTheory.inducedFunctor CommGrp_.toCommMon_

def CommGrp_.fullyFaithfulForget₂CommMon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] : (forget₂CommMon_ C).FullyFaithful

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

Equations

• CommGrp_.fullyFaithfulForget₂CommMon_ C = CategoryTheory.fullyFaithfulInducedFunctor CommGrp_.toCommMon_

instance CommGrp_.instFullCommMon_Forget₂CommMon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] : (forget₂CommMon_ C).Full

instance CommGrp_.instFaithfulCommMon_Forget₂CommMon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] : (forget₂CommMon_ C).Faithful

@[simp]

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

@[simp]

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

@[simp]

theorem CommGrp_.forget₂CommMon_map_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] {A B : CommGrp_ C} (f : A ⟶ B) : ((forget₂CommMon_ C).map f).hom = f.hom

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

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

Equations

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

theorem CommGrp_.forget₂CommMon_comp_forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] : (forget₂CommMon_ C).comp (CommMon_.forget C) = forget C

def CommGrp_.mkIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] {M N : CommGrp_ 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

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

@[simp]

theorem CommGrp_.mkIso_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] {M N : CommGrp_ 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 CommGrp_.mkIso_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] {M N : CommGrp_ 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 CommGrp_.uniqueHomFromTrivial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.ChosenFiniteProducts C] (A : CommGrp_ C) : Unique (trivial C ⟶ A)

Equations

• A.uniqueHomFromTrivial = A.uniqueHomFromTrivial

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

noncomputable def CategoryTheory.Functor.mapCommGrp {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 (CommGrp_ C) (CommGrp_ D)

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

Equations

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

@[simp]

theorem CategoryTheory.Functor.mapCommGrp_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 : CommGrp_ C) : (F.mapCommGrp.obj A).one = CategoryStruct.comp (LaxMonoidal.ε F) (F.map A.one)

@[simp]

theorem CategoryTheory.Functor.mapCommGrp_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 : CommGrp_ C) : (F.mapCommGrp.obj A).X = F.obj A.X

@[simp]

theorem CategoryTheory.Functor.mapCommGrp_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 : CommGrp_ C) : (F.mapCommGrp.obj A).mul = CategoryStruct.comp (LaxMonoidal.μ F A.X A.X) (F.map A.mul)

@[simp]

theorem CategoryTheory.Functor.mapCommGrp_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✝ : CommGrp_ C} (f : X✝ ⟶ Y✝) : (F.mapCommGrp.map f).hom = F.map f.hom

@[simp]

theorem CategoryTheory.Functor.mapCommGrp_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 : CommGrp_ C) : (F.mapCommGrp.obj A).inv = F.map A.inv

noncomputable def CategoryTheory.Functor.mapCommGrpFunctor {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] : Functor (C ⥤ₗ D) (Functor (CommGrp_ C) (CommGrp_ 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.mapCommGrpFunctor_obj {C : Type u₁} [Category.{v₁, u₁} C] [ChosenFiniteProducts C] {D : Type u₂} [Category.{v₂, u₂} D] [ChosenFiniteProducts D] (F : C ⥤ₗ D) : mapCommGrpFunctor.obj F = F.obj.mapCommGrp

@[simp]

theorem CategoryTheory.Functor.mapCommGrpFunctor_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 : CommGrp_ C) : ((mapCommGrpFunctor.map α).app A).hom = α.app A.X