Monoidal structures on wide subcategories

Given a monoidal category C and a morphism property P : MorphismProperty C, this file introduces conditions on P ensuring that WideSubcategory P inherits additional structures.

We define stability classes under associators, unitors, and braidings, and use them to construct monoidal, braided, and symmetric structures on WideSubcategory P.

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

A morphism property stable under associator isomorphisms of a monoidal category.

• associator_hom_mem (c c' c'' : C) : P (MonoidalCategoryStruct.associator c c' c'').hom
• associator_inv_mem (c c' c'' : C) : P (MonoidalCategoryStruct.associator c c' c'').inv

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

A morphism property stable under left and right unitor isomorphisms.

• leftUnitor_hom_mem (c : C) : P (MonoidalCategoryStruct.leftUnitor c).hom
• leftUnitor_inv_mem (c : C) : P (MonoidalCategoryStruct.leftUnitor c).inv
• rightUnitor_hom_mem (c : C) : P (MonoidalCategoryStruct.rightUnitor c).hom
• rightUnitor_inv_mem (c : C) : P (MonoidalCategoryStruct.rightUnitor c).inv

class CategoryTheory.MorphismProperty.IsMonoidalStable {C : Type u_1} [Category.{v_1, u_1} C] (P : MorphismProperty C) [MonoidalCategory C] extends P.IsMonoidal, P.IsStableUnderAssociator, P.IsStableUnderUnitor : Prop

A morphism property stable under tensoring, associators, and unitors.

• id_mem (X : C) : P (CategoryStruct.id X)
• comp_mem {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : P f → P g → P (CategoryStruct.comp f g)
• whiskerLeft (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) (hg : P g) : P (MonoidalCategoryStruct.whiskerLeft X g)
• whiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (hf : P f) (Y : C) : P (MonoidalCategoryStruct.whiskerRight f Y)
• associator_hom_mem (c c' c'' : C) : P (MonoidalCategoryStruct.associator c c' c'').hom
• associator_inv_mem (c c' c'' : C) : P (MonoidalCategoryStruct.associator c c' c'').inv
• leftUnitor_hom_mem (c : C) : P (MonoidalCategoryStruct.leftUnitor c).hom
• leftUnitor_inv_mem (c : C) : P (MonoidalCategoryStruct.leftUnitor c).inv
• rightUnitor_hom_mem (c : C) : P (MonoidalCategoryStruct.rightUnitor c).hom
• rightUnitor_inv_mem (c : C) : P (MonoidalCategoryStruct.rightUnitor c).inv

class CategoryTheory.MorphismProperty.IsStableUnderBraiding {C : Type u_1} [Category.{v_1, u_1} C] [MonoidalCategory C] [BraidedCategory C] (P : MorphismProperty C) extends P.IsMonoidalStable : Prop

A monoidal-stable morphism property also stable under braiding isomorphisms.

• id_mem (X : C) : P (CategoryStruct.id X)
• comp_mem {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : P f → P g → P (CategoryStruct.comp f g)
• whiskerLeft (X : C) {Y₁ Y₂ : C} (g : Y₁ ⟶ Y₂) (hg : P g) : P (MonoidalCategoryStruct.whiskerLeft X g)
• whiskerRight {X₁ X₂ : C} (f : X₁ ⟶ X₂) (hf : P f) (Y : C) : P (MonoidalCategoryStruct.whiskerRight f Y)
• associator_hom_mem (c c' c'' : C) : P (MonoidalCategoryStruct.associator c c' c'').hom
• associator_inv_mem (c c' c'' : C) : P (MonoidalCategoryStruct.associator c c' c'').inv
• leftUnitor_hom_mem (c : C) : P (MonoidalCategoryStruct.leftUnitor c).hom
• leftUnitor_inv_mem (c : C) : P (MonoidalCategoryStruct.leftUnitor c).inv
• rightUnitor_hom_mem (c : C) : P (MonoidalCategoryStruct.rightUnitor c).hom
• rightUnitor_inv_mem (c : C) : P (MonoidalCategoryStruct.rightUnitor c).inv
• braiding_hom_mem (c c' : C) : P (β_ c c').hom
• braiding_inv_mem (c c' : C) : P (β_ c c').inv

@[implicit_reducible]

instance CategoryTheory.WideSubcategory.instMonoidalCategoryStruct {C : Type u_1} [Category.{v_1, u_1} C] (P : MorphismProperty C) [MonoidalCategory C] [P.IsMonoidalStable] : MonoidalCategoryStruct (WideSubcategory P)

@[simp]

theorem CategoryTheory.WideSubcategory.associator_def {C : Type u_1} [Category.{v_1, u_1} C] (P : MorphismProperty C) [MonoidalCategory C] [P.IsMonoidalStable] (x✝ x✝¹ x✝² : WideSubcategory P) : MonoidalCategoryStruct.associator x✝ x✝¹ x✝² = isoMk (MonoidalCategoryStruct.associator x✝.obj x✝¹.obj x✝².obj) ⋯ ⋯

@[simp]

theorem CategoryTheory.WideSubcategory.rightUnitor_def {C : Type u_1} [Category.{v_1, u_1} C] (P : MorphismProperty C) [MonoidalCategory C] [P.IsMonoidalStable] (x✝ : WideSubcategory P) : MonoidalCategoryStruct.rightUnitor x✝ = isoMk (MonoidalCategoryStruct.rightUnitor x✝.obj) ⋯ ⋯

@[simp]

theorem CategoryTheory.WideSubcategory.leftUnitor_def {C : Type u_1} [Category.{v_1, u_1} C] (P : MorphismProperty C) [MonoidalCategory C] [P.IsMonoidalStable] (x✝ : WideSubcategory P) : MonoidalCategoryStruct.leftUnitor x✝ = isoMk (MonoidalCategoryStruct.leftUnitor x✝.obj) ⋯ ⋯

@[simp]

theorem CategoryTheory.WideSubcategory.whiskerLeft_hom {C : Type u_1} [Category.{v_1, u_1} C] (P : MorphismProperty C) [MonoidalCategory C] [P.IsMonoidalStable] (c x✝ x✝¹ : WideSubcategory P) (f : x✝ ⟶ x✝¹) : (MonoidalCategoryStruct.whiskerLeft c f).hom = MonoidalCategoryStruct.whiskerLeft c.obj f.hom

@[simp]

theorem CategoryTheory.WideSubcategory.whiskerRight_hom {C : Type u_1} [Category.{v_1, u_1} C] (P : MorphismProperty C) [MonoidalCategory C] [P.IsMonoidalStable] {X₁✝ X₂✝ : WideSubcategory P} (f : X₁✝ ⟶ X₂✝) (c' : WideSubcategory P) : (MonoidalCategoryStruct.whiskerRight f c').hom = MonoidalCategoryStruct.whiskerRight f.hom c'.obj

@[simp]

theorem CategoryTheory.WideSubcategory.tensorHom_hom {C : Type u_1} [Category.{v_1, u_1} C] (P : MorphismProperty C) [MonoidalCategory C] [P.IsMonoidalStable] {X₁✝ Y₁✝ X₂✝ Y₂✝ : WideSubcategory P} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : (MonoidalCategoryStruct.tensorHom f g).hom = MonoidalCategoryStruct.tensorHom f.hom g.hom

@[simp]

theorem CategoryTheory.WideSubcategory.tensorUnit_obj {C : Type u_1} [Category.{v_1, u_1} C] (P : MorphismProperty C) [MonoidalCategory C] [P.IsMonoidalStable] : (MonoidalCategoryStruct.tensorUnit (WideSubcategory P)).obj = MonoidalCategoryStruct.tensorUnit C

@[simp]

theorem CategoryTheory.WideSubcategory.tensorObj_obj {C : Type u_1} [Category.{v_1, u_1} C] (P : MorphismProperty C) [MonoidalCategory C] [P.IsMonoidalStable] (c c' : WideSubcategory P) : (MonoidalCategoryStruct.tensorObj c c').obj = MonoidalCategoryStruct.tensorObj c.obj c'.obj

@[implicit_reducible]

instance CategoryTheory.WideSubcategory.instMonoidalCategory {C : Type u_1} [Category.{v_1, u_1} C] (P : MorphismProperty C) [MonoidalCategory C] [P.IsMonoidalStable] : MonoidalCategory (WideSubcategory P)

@[implicit_reducible]

instance CategoryTheory.WideSubcategory.instBraidedCategory {C : Type u_1} [Category.{v_1, u_1} C] (P : MorphismProperty C) [MonoidalCategory C] [BraidedCategory C] [P.IsStableUnderBraiding] : BraidedCategory (WideSubcategory P)

@[simp]

theorem CategoryTheory.WideSubcategory.tensorμ_hom {C : Type u_1} [Category.{v_1, u_1} C] {P : MorphismProperty C} [MonoidalCategory C] [BraidedCategory C] [P.IsStableUnderBraiding] (X Y Z T : WideSubcategory P) : (MonoidalCategory.tensorμ X Y Z T).hom = MonoidalCategory.tensorμ X.obj Y.obj Z.obj T.obj

@[implicit_reducible]

instance CategoryTheory.WideSubcategory.instSymmetricCategory {C : Type u_1} [Category.{v_1, u_1} C] (P : MorphismProperty C) [MonoidalCategory C] [SymmetricCategory C] [P.IsStableUnderBraiding] : SymmetricCategory (WideSubcategory P)