Copy-discard structures on wide subcategories

Given a monoidal category C, a morphism property P : MorphismProperty C satisfying P.IsMonoidalStable and a comonoid object c : C, we introduce a condition P. IsStableUnderComonoid c saying that c inherits a comonoid object structure in the category of WideSubcategory P. If C is a copy-discard category, if P is also stable under braiding and that this condition P. IsStableUnderComonoid holds for all objects c : C, we show that WideSubcategory P is also a copy-discard category.

class CategoryTheory.MorphismProperty.IsStableUnderComonoid {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] (P : MorphismProperty C) (c : C) [ComonObj c] : Prop

A braided-stable morphism property stable under comonoid counit and comultiplication.

• counit_mem : P ComonObj.counit
• comul_mem : P ComonObj.comul

@[implicit_reducible]

instance CategoryTheory.MorphismProperty.instComonObjWideSubcategoryOfIsStableUnderComonoidObj {C : Type u_1} [Category.{v_1, u_1} C] (P : MorphismProperty C) [MonoidalCategory C] [P.IsMonoidalStable] (c : WideSubcategory P) [ComonObj c.obj] [P.IsStableUnderComonoid c.obj] : ComonObj c

@[simp]

theorem CategoryTheory.MorphismProperty.counit_hom {C : Type u_1} [Category.{v_1, u_1} C] (P : MorphismProperty C) [MonoidalCategory C] [P.IsMonoidalStable] (c : WideSubcategory P) [ComonObj c.obj] [P.IsStableUnderComonoid c.obj] : ComonObj.counit.hom = ComonObj.counit

@[simp]

theorem CategoryTheory.MorphismProperty.comul_hom {C : Type u_1} [Category.{v_1, u_1} C] (P : MorphismProperty C) [MonoidalCategory C] [P.IsMonoidalStable] (c : WideSubcategory P) [ComonObj c.obj] [P.IsStableUnderComonoid c.obj] : ComonObj.comul.hom = ComonObj.comul

instance CategoryTheory.MorphismProperty.instIsCommComonObjWideSubcategoryOfObj {C : Type u_1} [Category.{v_1, u_1} C] (P : MorphismProperty C) [MonoidalCategory C] [BraidedCategory C] [P.IsStableUnderBraiding] (c : WideSubcategory P) [ComonObj c.obj] [IsCommComonObj c.obj] [P.IsStableUnderComonoid c.obj] : IsCommComonObj c

@[implicit_reducible]

instance CategoryTheory.MorphismProperty.instCopyDiscardCategoryWideSubcategoryOfIsStableUnderComonoid {C : Type u_1} [Category.{v_1, u_1} C] (P : MorphismProperty C) [MonoidalCategory C] [CopyDiscardCategory C] [P.IsStableUnderBraiding] [∀ (c : C), P.IsStableUnderComonoid c] : CopyDiscardCategory (WideSubcategory P)