The category of commutative groups in a cartesian monoidal category #

source

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

Type (max u₁ v₁)

A commutative group object internal to a cartesian monoidal category.

X : C
The underlying object in the ambient monoidal category
grp : Grp_Class self.X
comm : IsCommMon self.X

Instances For

source

def CommGrp_.toGrp_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp_ C) :

Grp_ C

A commutative group object is a group object.

Equations

A.toGrp_ = { X := A.X, grp := A.grp }

source

@[simp]

theorem CommGrp_.toGrp__X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp_ C) :

A.toGrp_.X = A.X

source

def CommGrp_.toCommMon_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp_ C) :

CommMon_ C

A commutative group object is a commutative monoid object.

Equations

A.toCommMon_ = { X := A.X, mon := A.grp.toMon_Class, comm := ⋯ }

source

@[simp]

theorem CommGrp_.toCommMon__X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp_ C) :

A.toCommMon_.X = A.X

source

@[reducible, inline]

abbrev CommGrp_.toMon_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp_ C) :

Mon_ C

A commutative group object is a monoid object.

Equations

A.toMon_ = A.toCommMon_.toMon_

source

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

CommGrp_ C

The trivial commutative group object.

Equations

CommGrp_.trivial C = { X := CategoryTheory.MonoidalCategoryStruct.tensorUnit C, grp := Grp_Class.instTensorUnit, comm := ⋯ }

source

@[simp]

theorem CommGrp_.trivial_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] :

(trivial C).X = CategoryTheory.MonoidalCategoryStruct.tensorUnit C

source

@[simp]

theorem CommGrp_.trivial_grp_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] :

Mon_Class.one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

source

@[simp]

theorem CommGrp_.trivial_grp_inv (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] :

Grp_Class.inv = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

source

@[simp]

theorem CommGrp_.trivial_grp_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] :

Mon_Class.mul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom

source

instance CommGrp_.instInhabited {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] :

Inhabited (CommGrp_ C)

Equations

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

source

instance CommGrp_.instCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] :

CategoryTheory.Category.{v₁, max u₁ v₁} (CommGrp_ C)

Equations

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

source

@[simp]

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

source

@[simp]

theorem CommGrp_.comp_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory 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

source

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

f = g

source

theorem CommGrp_.hom_ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {A B : CommGrp_ C} {f g : A ⟶ B} :

f = g ↔ f.hom = g.hom

source

@[simp]

theorem CommGrp_.id' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp_ C) :

CategoryTheory.CategoryStruct.id A = CategoryTheory.CategoryStruct.id A.toMon_

source

@[simp]

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

CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f g

source

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

Instances For

source

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

source

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

(forget₂Grp_ C).Full

source

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

(forget₂Grp_ C).Faithful

source

@[simp]

theorem CommGrp_.forget₂Grp_obj_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp_ C) :

Mon_Class.one = Mon_Class.one

source

@[simp]

theorem CommGrp_.forget₂Grp_obj_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp_ C) :

Mon_Class.mul = Mon_Class.mul

source

@[simp]

theorem CommGrp_.forget₂Grp_map_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {A B : CommGrp_ C} (f : A ⟶ B) :

((forget₂Grp_ C).map f).hom = f.hom

source

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

Instances For

source

def CommGrp_.fullyFaithfulForget₂CommMon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory 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_

source

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

(forget₂CommMon_ C).Full

source

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

(forget₂CommMon_ C).Faithful

source

@[simp]

theorem CommGrp_.forget₂CommMon_obj_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp_ C) :

Mon_Class.one = Mon_Class.one

source

@[simp]

theorem CommGrp_.forget₂CommMon_obj_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp_ C) :

Mon_Class.mul = Mon_Class.mul

source

@[simp]

theorem CommGrp_.forget₂CommMon_map_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {A B : CommGrp_ C} (f : A ⟶ B) :

((forget₂CommMon_ C).map f).hom = f.hom

source

def CommGrp_.forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory 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)

Instances For

CommGrp_.instFaithfulForget

source

@[simp]

theorem CommGrp_.forget_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {X✝ Y✝ : CommGrp_ C} (f : X✝ ⟶ Y✝) :

(forget C).map f = f.hom

source

@[simp]

theorem CommGrp_.forget_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CommGrp_ C) :

(forget C).obj X = ((Grp_.forget₂Mon_ C).obj ((forget₂Grp_ C).obj X)).X

source

instance CommGrp_.instFaithfulForget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] :

(forget C).Faithful

source

@[simp]

theorem CommGrp_.forget₂Grp_comp_forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] :

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

source

@[simp]

theorem CommGrp_.forget₂CommMon_comp_forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] :

(forget₂CommMon_ C).comp (CommMon_.forget C) = forget C

source

def CommGrp_.mkIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {M N : CommGrp_ C} (f : M.X ≅ N.X) (one_f : CategoryTheory.CategoryStruct.comp Mon_Class.one f.hom = Mon_Class.one := by aesop_cat) (mul_f : CategoryTheory.CategoryStruct.comp Mon_Class.mul f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) Mon_Class.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)

source

@[simp]

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

(mkIso f one_f mul_f).hom.hom = f.hom

source

@[simp]

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

(mkIso f one_f mul_f).inv.hom = f.inv

source

instance CommGrp_.uniqueHomFromTrivial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp_ C) :

Unique (trivial C ⟶ A)

Equations

A.uniqueHomFromTrivial = A.toMon_.uniqueHomFromTrivial

source

instance CommGrp_.instHasInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] :

CategoryTheory.Limits.HasInitial (CommGrp_ C)

source

noncomputable def CategoryTheory.Functor.mapCommGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.Braided] :

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.

source

@[simp]

theorem CategoryTheory.Functor.mapCommGrp_map_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.Braided] {X✝ Y✝ : CommGrp_ C} (f : X✝ ⟶ Y✝) :

(F.mapCommGrp.map f).hom = F.map f.hom

source

@[simp]

theorem CategoryTheory.Functor.mapCommGrp_obj_X {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.Braided] (A : CommGrp_ C) :

(F.mapCommGrp.obj A).X = F.obj A.X

source

@[simp]

theorem CategoryTheory.Functor.mapCommGrp_obj_grp_mul {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.Braided] (A : CommGrp_ C) :

Mon_Class.mul = CategoryStruct.comp (LaxMonoidal.μ F A.X A.X) (F.map Mon_Class.mul)

source

@[simp]

theorem CategoryTheory.Functor.mapCommGrp_obj_grp_inv {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.Braided] (A : CommGrp_ C) :

Grp_Class.inv = F.map Grp_Class.inv

source

@[simp]

theorem CategoryTheory.Functor.mapCommGrp_obj_grp_one {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.Braided] (A : CommGrp_ C) :

Mon_Class.one = CategoryStruct.comp (LaxMonoidal.ε F) (F.map Mon_Class.one)

source

@[simp]

theorem CategoryTheory.Functor.mapCommGrp_id_one {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : CommGrp_ C) :

Mon_Class.one = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)) Mon_Class.one

source

@[simp]

theorem CategoryTheory.Functor.mapCommpGrp_id_mul {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : CommGrp_ C) :

Mon_Class.mul = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorObj A.X A.X)) Mon_Class.mul

source

@[simp]

theorem CategoryTheory.Functor.comp_mapCommGrp_one {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] [BraidedCategory E] {F : Functor C D} [F.Braided] {G : Functor D E} [G.Braided] (A : CommGrp_ C) :

Mon_Class.one = CategoryStruct.comp (LaxMonoidal.ε (F.comp G)) ((F.comp G).map Mon_Class.one)

source

@[simp]

theorem CategoryTheory.Functor.comp_mapCommGrp_mul {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] [BraidedCategory E] {F : Functor C D} [F.Braided] {G : Functor D E} [G.Braided] (A : CommGrp_ C) :

Mon_Class.mul = CategoryStruct.comp (LaxMonoidal.μ (F.comp G) A.X A.X) ((F.comp G).map Mon_Class.mul)

source

noncomputable def CategoryTheory.Functor.mapCommGrpIdIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :

(Functor.id C).mapCommGrp ≅ Functor.id (CommGrp_ C)

The identity functor is also the identity on commutative group objects.

Equations

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

source

@[simp]

theorem CategoryTheory.Functor.mapCommGrpIdIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : CommGrp_ C) :

(mapCommGrpIdIso.hom.app X).hom = CategoryStruct.id X.X

source

@[simp]

theorem CategoryTheory.Functor.mapCommGrpIdIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : CommGrp_ C) :

(mapCommGrpIdIso.inv.app X).hom = CategoryStruct.id X.X

source

noncomputable def CategoryTheory.Functor.mapCommGrpCompIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] [BraidedCategory E] {F : Functor C D} [F.Braided] {G : Functor D E} [G.Braided] :

(F.comp G).mapCommGrp ≅ F.mapCommGrp.comp G.mapCommGrp

The composition functor is also the composition on commutative group objects.

Equations

CategoryTheory.Functor.mapCommGrpCompIso = CategoryTheory.NatIso.ofComponents (fun (X : CommGrp_ C) => CommGrp_.mkIso (CategoryTheory.Iso.refl ((F.comp G).mapCommGrp.obj X).X) ⋯ ⋯) ⋯

source

@[simp]

theorem CategoryTheory.Functor.mapCommGrpCompIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] [BraidedCategory E] {F : Functor C D} [F.Braided] {G : Functor D E} [G.Braided] (X : CommGrp_ C) :

(mapCommGrpCompIso.hom.app X).hom = CategoryStruct.id (G.obj (F.obj X.X))

source

@[simp]

theorem CategoryTheory.Functor.mapCommGrpCompIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] [BraidedCategory E] {F : Functor C D} [F.Braided] {G : Functor D E} [G.Braided] (X : CommGrp_ C) :

(mapCommGrpCompIso.inv.app X).hom = CategoryStruct.id (G.obj (F.obj X.X))

source

noncomputable def CategoryTheory.Functor.mapCommGrpNatTrans {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.Braided] [F'.Braided] (f : F ⟶ F') :

F.mapCommGrp ⟶ F'.mapCommGrp

Natural transformations between functors lift to commutative group objects.

Equations

CategoryTheory.Functor.mapCommGrpNatTrans f = { app := fun (X : CommGrp_ C) => Mon_.Hom.mk' (f.app X.toGrp_.toMon_.X) ⋯ ⋯, naturality := ⋯ }

source

@[simp]

theorem CategoryTheory.Functor.mapCommGrpNatTrans_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.Braided] [F'.Braided] (f : F ⟶ F') (X : CommGrp_ C) :

((mapCommGrpNatTrans f).app X).hom = f.app X.X

source

noncomputable def CategoryTheory.Functor.mapCommGrpNatIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.Braided] [F'.Braided] (e : F ≅ F') :

F.mapCommGrp ≅ F'.mapCommGrp

Natural isomorphisms between functors lift to commutative group objects.

Equations

CategoryTheory.Functor.mapCommGrpNatIso e = CategoryTheory.NatIso.ofComponents (fun (X : CommGrp_ C) => CommGrp_.mkIso (e.app X.toGrp_.toMon_.X) ⋯ ⋯) ⋯

source

@[simp]

theorem CategoryTheory.Functor.mapCommGrpNatIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.Braided] [F'.Braided] (e : F ≅ F') (X : CommGrp_ C) :

((mapCommGrpNatIso e).inv.app X).hom = e.inv.app X.X

source

@[simp]

theorem CategoryTheory.Functor.mapCommGrpNatIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.Braided] [F'.Braided] (e : F ≅ F') (X : CommGrp_ C) :

((mapCommGrpNatIso e).hom.app X).hom = e.hom.app X.X

source

noncomputable def CategoryTheory.Functor.mapCommGrpFunctor {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] :

Functor (C ⥤ₗ D) (Functor (CommGrp_ C) (CommGrp_ D))

mapCommGrp is functorial in the left-exact functor.

Equations

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

source

@[simp]

theorem CategoryTheory.Functor.mapCommGrpFunctor_obj {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : C ⥤ₗ D) :

mapCommGrpFunctor.obj F = F.obj.mapCommGrp

source

@[simp]

theorem CategoryTheory.Functor.mapCommGrpFunctor_map_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F G : C ⥤ₗ D} (α : F ⟶ G) (A : CommGrp_ C) :

((mapCommGrpFunctor.map α).app A).hom = α.app A.X

source

noncomputable def CategoryTheory.Adjunction.mapCommGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Braided] [G.Braided] :

F.mapCommGrp ⊣ G.mapCommGrp

An adjunction of braided functors lifts to an adjunction of their lifts to commutative group objects.

Equations

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

source

@[simp]

theorem CategoryTheory.Adjunction.mapCommGrp_counit {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Braided] [G.Braided] :

a.mapCommGrp.counit = CategoryStruct.comp Functor.mapCommGrpCompIso.inv (CategoryStruct.comp (Functor.mapCommGrpNatTrans a.counit) Functor.mapCommGrpIdIso.hom)

source

@[simp]

theorem CategoryTheory.Adjunction.mapCommGrp_unit {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Braided] [G.Braided] :

a.mapCommGrp.unit = CategoryStruct.comp Functor.mapCommGrpIdIso.inv (CategoryStruct.comp (Functor.mapCommGrpNatTrans a.unit) Functor.mapCommGrpCompIso.hom)

source

noncomputable def CategoryTheory.Equivalence.mapCommGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] :

CommGrp_ C ≌ CommGrp_ D

An equivalence of categories lifts to an equivalence of their commutative group objects.

Equations

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

source

@[simp]

theorem CategoryTheory.Equivalence.mapCommGrp_inverse {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] :

e.mapCommGrp.inverse = e.inverse.mapCommGrp

source

@[simp]

theorem CategoryTheory.Equivalence.mapCommGrp_functor {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] :

e.mapCommGrp.functor = e.functor.mapCommGrp

source

@[simp]

theorem CategoryTheory.Equivalence.mapCommGrp_counitIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] :

e.mapCommGrp.counitIso = Functor.mapCommGrpCompIso.symm ≪≫ Functor.mapCommGrpNatIso e.counitIso ≪≫ Functor.mapCommGrpIdIso

source

@[simp]

theorem CategoryTheory.Equivalence.mapCommGrp_unitIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] :

e.mapCommGrp.unitIso = Functor.mapCommGrpIdIso.symm ≪≫ Functor.mapCommGrpNatIso e.unitIso ≪≫ Functor.mapCommGrpCompIso

Documentation

Mathlib.CategoryTheory.Monoidal.CommGrp_

The category of commutative groups in a cartesian monoidal category #