Full monoidal subcategories

Given a monoidal category C and a monoidal predicate on C, that is a function P : C → Prop closed under 𝟙_ and ⊗, we can put a monoidal structure on {X : C // P X} (the category structure is defined in Mathlib.CategoryTheory.FullSubcategory).

When C is also braided/symmetric, the full monoidal subcategory also inherits the braided/symmetric structure.

TODO

• Add monoidal/braided versions of CategoryTheory.FullSubcategory.Lift

class CategoryTheory.MonoidalCategory.MonoidalPredicate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) : Prop

A property C → Prop is a monoidal predicate if it is closed under 𝟙_ and ⊗.

• prop_id : P (𝟙_ C)
• prop_tensor {X Y : C} : P X → P Y → P (CategoryTheory.MonoidalCategory.tensorObj X Y)

instance CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] : CategoryTheory.MonoidalCategoryStruct (CategoryTheory.FullSubcategory P)

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_whiskerRight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] {X₁ X₂ : CategoryTheory.FullSubcategory P} (f : X₁.obj ⟶ X₂.obj) (Y : CategoryTheory.FullSubcategory P) : CategoryTheory.MonoidalCategory.whiskerRight f Y = CategoryTheory.MonoidalCategory.whiskerRight f Y.obj

@[simp]

theorem CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_tensorUnit_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] : (𝟙_ (CategoryTheory.FullSubcategory P)).obj = 𝟙_ C

@[simp]

theorem CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_rightUnitor_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] (X : CategoryTheory.FullSubcategory P) : (CategoryTheory.MonoidalCategory.rightUnitor X).hom = (CategoryTheory.MonoidalCategory.rightUnitor X.obj).hom

@[simp]

theorem CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_leftUnitor_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] (X : CategoryTheory.FullSubcategory P) : (CategoryTheory.MonoidalCategory.leftUnitor X).hom = (CategoryTheory.MonoidalCategory.leftUnitor X.obj).hom

@[simp]

theorem CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_whiskerLeft {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] (X x✝ x✝¹ : CategoryTheory.FullSubcategory P) (f : x✝ ⟶ x✝¹) : CategoryTheory.MonoidalCategory.whiskerLeft X f = CategoryTheory.MonoidalCategory.whiskerLeft X.obj f

@[simp]

theorem CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_associator_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] (X Y Z : CategoryTheory.FullSubcategory P) : (CategoryTheory.MonoidalCategory.associator X Y Z).hom = (CategoryTheory.MonoidalCategory.associator X.obj Y.obj Z.obj).hom

@[simp]

theorem CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_associator_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] (X Y Z : CategoryTheory.FullSubcategory P) : (CategoryTheory.MonoidalCategory.associator X Y Z).inv = (CategoryTheory.MonoidalCategory.associator X.obj Y.obj Z.obj).inv

@[simp]

theorem CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_tensorObj_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] (X Y : CategoryTheory.FullSubcategory P) : (CategoryTheory.MonoidalCategory.tensorObj X Y).obj = CategoryTheory.MonoidalCategory.tensorObj X.obj Y.obj

@[simp]

theorem CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_leftUnitor_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] (X : CategoryTheory.FullSubcategory P) : (CategoryTheory.MonoidalCategory.leftUnitor X).inv = (CategoryTheory.MonoidalCategory.leftUnitor X.obj).inv

@[simp]

theorem CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_rightUnitor_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] (X : CategoryTheory.FullSubcategory P) : (CategoryTheory.MonoidalCategory.rightUnitor X).inv = (CategoryTheory.MonoidalCategory.rightUnitor X.obj).inv

@[simp]

theorem CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_tensorHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] {X₁✝ Y₁✝ X₂✝ Y₂✝ : CategoryTheory.FullSubcategory P} (f : X₁✝ ⟶ Y₁✝) (g : X₂✝ ⟶ Y₂✝) : CategoryTheory.MonoidalCategory.tensorHom f g = CategoryTheory.MonoidalCategory.tensorHom f g

instance CategoryTheory.MonoidalCategory.fullMonoidalSubcategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] : CategoryTheory.MonoidalCategory (CategoryTheory.FullSubcategory P)

When P is a monoidal predicate, the full subcategory for P inherits the monoidal structure of C.

Equations

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

instance CategoryTheory.MonoidalCategory.fullSubcategoryInclusionMonoidal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] : (CategoryTheory.fullSubcategoryInclusion P).Monoidal

The forgetful monoidal functor from a full monoidal subcategory into the original category ("forgetting" the condition).

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.fullSubcategoryInclusion_ε {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] : CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.fullSubcategoryInclusion P) = CategoryTheory.CategoryStruct.id (𝟙_ C)

@[simp]

theorem CategoryTheory.MonoidalCategory.fullSubcategoryInclusion_η {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] : CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.fullSubcategoryInclusion P) = CategoryTheory.CategoryStruct.id (𝟙_ C)

@[simp]

theorem CategoryTheory.MonoidalCategory.fullSubcategoryInclusion_μ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] (X Y : CategoryTheory.FullSubcategory P) : CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.fullSubcategoryInclusion P) X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.fullSubcategoryInclusion P).obj X) ((CategoryTheory.fullSubcategoryInclusion P).obj Y))

@[simp]

theorem CategoryTheory.MonoidalCategory.fullSubcategoryInclusion_δ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] (X Y : CategoryTheory.FullSubcategory P) : CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.fullSubcategoryInclusion P) X Y = CategoryTheory.CategoryStruct.id ((CategoryTheory.fullSubcategoryInclusion P).obj (CategoryTheory.MonoidalCategory.tensorObj X Y))

instance CategoryTheory.MonoidalCategory.instMonoidalPreadditiveFullSubcategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] : CategoryTheory.MonoidalPreadditive (CategoryTheory.FullSubcategory P)

instance CategoryTheory.MonoidalCategory.instMonoidalLinearFullSubcategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.Preadditive C] (R : Type u_1) [Ring R] [CategoryTheory.Linear R C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear R C] : CategoryTheory.MonoidalLinear R (CategoryTheory.FullSubcategory P)

instance CategoryTheory.MonoidalCategory.instMonoidalFullSubcategoryMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P] {P' : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P'] (h : ∀ ⦃X : C⦄, P X → P' X) : (CategoryTheory.FullSubcategory.map h).Monoidal

An implication of predicates P → P' induces a monoidal functor between full monoidal subcategories.

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.fullSubcategory_map_ε {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P] {P' : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P'] (h : ∀ ⦃X : C⦄, P X → P' X) : CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.FullSubcategory.map h) = CategoryTheory.CategoryStruct.id (𝟙_ (CategoryTheory.FullSubcategory P'))

@[simp]

theorem CategoryTheory.MonoidalCategory.fullSubcategory_map_η {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P] {P' : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P'] (h : ∀ ⦃X : C⦄, P X → P' X) : CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.FullSubcategory.map h) = CategoryTheory.CategoryStruct.id ((CategoryTheory.FullSubcategory.map h).obj (𝟙_ (CategoryTheory.FullSubcategory P)))

@[simp]

theorem CategoryTheory.MonoidalCategory.fullSubcategory_map_μ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P] {P' : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P'] (h : ∀ ⦃X : C⦄, P X → P' X) (X Y : CategoryTheory.FullSubcategory P) : CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.FullSubcategory.map h) X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.FullSubcategory.map h).obj X) ((CategoryTheory.FullSubcategory.map h).obj Y))

@[simp]

theorem CategoryTheory.MonoidalCategory.fullSubcategory_map_δ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P] {P' : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P'] (h : ∀ ⦃X : C⦄, P X → P' X) (X Y : CategoryTheory.FullSubcategory P) : CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.FullSubcategory.map h) X Y = CategoryTheory.CategoryStruct.id ((CategoryTheory.FullSubcategory.map h).obj (CategoryTheory.MonoidalCategory.tensorObj X Y))

instance CategoryTheory.MonoidalCategory.fullBraidedSubcategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.BraidedCategory C] : CategoryTheory.BraidedCategory (CategoryTheory.FullSubcategory P)

The braided structure on a full subcategory inherited by the braided structure on C.

Equations

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

instance CategoryTheory.MonoidalCategory.instBraidedFullSubcategoryFullSubcategoryInclusion {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.BraidedCategory C] : (CategoryTheory.fullSubcategoryInclusion P).Braided

The forgetful braided functor from a full braided subcategory into the original category ("forgetting" the condition).

Equations

• CategoryTheory.MonoidalCategory.instBraidedFullSubcategoryFullSubcategoryInclusion P = CategoryTheory.Functor.Braided.mk ⋯

instance CategoryTheory.MonoidalCategory.instBraidedFullSubcategoryMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.BraidedCategory C] {P' : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P'] (h : ∀ ⦃X : C⦄, P X → P' X) : (CategoryTheory.FullSubcategory.map h).Braided

An implication of predicates P → P' induces a braided functor between full braided subcategories.

Equations

• CategoryTheory.MonoidalCategory.instBraidedFullSubcategoryMap h = CategoryTheory.Functor.Braided.mk ⋯

instance CategoryTheory.MonoidalCategory.fullSymmetricSubcategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.SymmetricCategory C] : CategoryTheory.SymmetricCategory (CategoryTheory.FullSubcategory P)

Equations

• CategoryTheory.MonoidalCategory.fullSymmetricSubcategory P = CategoryTheory.symmetricCategoryOfFaithful (CategoryTheory.fullSubcategoryInclusion P)

class CategoryTheory.MonoidalCategory.ClosedPredicate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalClosed C] : Prop

A property C → Prop is a closed predicate if it is closed under taking internal homs

• prop_ihom {X Y : C} : P X → P Y → P ((CategoryTheory.ihom X).obj Y)

instance CategoryTheory.MonoidalCategory.fullMonoidalClosedSubcategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.MonoidalClosed C] [CategoryTheory.MonoidalCategory.ClosedPredicate P] : CategoryTheory.MonoidalClosed (CategoryTheory.FullSubcategory P)

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.fullMonoidalClosedSubcategory_ihom_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.MonoidalClosed C] [CategoryTheory.MonoidalCategory.ClosedPredicate P] (X Y : CategoryTheory.FullSubcategory P) : ((CategoryTheory.ihom X).obj Y).obj = (CategoryTheory.ihom X.obj).obj Y.obj

@[simp]

theorem CategoryTheory.MonoidalCategory.fullMonoidalClosedSubcategory_ihom_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.MonoidalClosed C] [CategoryTheory.MonoidalCategory.ClosedPredicate P] (X : CategoryTheory.FullSubcategory P) {Y Z : CategoryTheory.FullSubcategory P} (f : Y ⟶ Z) : (CategoryTheory.ihom X).map f = (CategoryTheory.ihom X.obj).map f