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)

@[simp]

theorem CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategoryCategory_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.instMonoidalCategoryStructFullSubcategoryCategory_associator_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] (X : CategoryTheory.FullSubcategory P) (Y : CategoryTheory.FullSubcategory P) (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.instMonoidalCategoryStructFullSubcategoryCategory_whiskerRight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] {X₁ : CategoryTheory.FullSubcategory P} {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.instMonoidalCategoryStructFullSubcategoryCategory_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.instMonoidalCategoryStructFullSubcategoryCategory_tensorObj_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] (X : CategoryTheory.FullSubcategory P) (Y : CategoryTheory.FullSubcategory P) : (CategoryTheory.MonoidalCategory.tensorObj X Y).obj = CategoryTheory.MonoidalCategory.tensorObj X.obj Y.obj

@[simp]

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

@[simp]

theorem CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategoryCategory_associator_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] (X : CategoryTheory.FullSubcategory P) (Y : CategoryTheory.FullSubcategory P) (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.instMonoidalCategoryStructFullSubcategoryCategory_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.instMonoidalCategoryStructFullSubcategoryCategory_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

@[simp]

theorem CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategoryCategory_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.instMonoidalCategoryStructFullSubcategoryCategory_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

instance CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategoryCategory {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.

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.

@[simp]

theorem CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion_toLaxMonoidalFunctor_toFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] : (CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor = CategoryTheory.fullSubcategoryInclusion P

@[simp]

theorem CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion_toLaxMonoidalFunctor_ε {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] : (CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.ε = CategoryTheory.CategoryStruct.id (𝟙_ C)

@[simp]

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

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

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.

instance CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.full {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] : CategoryTheory.Full (CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor

Equations

• CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.full P = CategoryTheory.FullSubcategory.full P

instance CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.faithful {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] : CategoryTheory.Faithful (CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor

Equations

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

instance CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion_additive {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.Preadditive C] : CategoryTheory.Functor.Additive (CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor

Equations

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

instance CategoryTheory.MonoidalCategory.instMonoidalPreadditiveFullSubcategoryCategoryFullSubcategoryFullMonoidalSubcategory {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)

Equations

• (_ : CategoryTheory.MonoidalPreadditive (CategoryTheory.FullSubcategory P)) = (_ : CategoryTheory.MonoidalPreadditive (CategoryTheory.FullSubcategory P))

instance CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion_linear {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.Functor.Linear R (CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor

Equations

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

instance CategoryTheory.MonoidalCategory.instMonoidalLinearToSemiringFullSubcategoryCategoryFullSubcategoryFullSubcategoryFullMonoidalSubcategoryInstMonoidalPreadditiveFullSubcategoryCategoryFullSubcategoryFullMonoidalSubcategory {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)

Equations

• (_ : CategoryTheory.MonoidalLinear R (CategoryTheory.FullSubcategory P)) = (_ : CategoryTheory.MonoidalLinear R (CategoryTheory.FullSubcategory P))

@[simp]

theorem CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map_toLaxMonoidalFunctor_ε {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.MonoidalCategory.fullMonoidalSubcategory.map h).toLaxMonoidalFunctor.ε = CategoryTheory.CategoryStruct.id (𝟙_ (CategoryTheory.FullSubcategory P'))

@[simp]

theorem CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map_toLaxMonoidalFunctor_toFunctor {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.MonoidalCategory.fullMonoidalSubcategory.map h).toLaxMonoidalFunctor.toFunctor = CategoryTheory.FullSubcategory.map h

@[simp]

theorem CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map_toLaxMonoidalFunctor_μ {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 : CategoryTheory.FullSubcategory P) (Y : CategoryTheory.FullSubcategory P) : (CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map h).toLaxMonoidalFunctor.μ X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.FullSubcategory.map h).toPrefunctor.obj X) ((CategoryTheory.FullSubcategory.map h).toPrefunctor.obj Y))

def CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.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.MonoidalFunctor (CategoryTheory.FullSubcategory P) (CategoryTheory.FullSubcategory P')

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.

instance CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.mapFull {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.Full (CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map h).toLaxMonoidalFunctor.toFunctor

Equations

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

instance CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map_faithful {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.Faithful (CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map h).toLaxMonoidalFunctor.toFunctor

Equations

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

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.

@[simp]

theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion_μ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.FullSubcategory P) (Y : CategoryTheory.FullSubcategory P) : (CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion P).toMonoidalFunctor.toLaxMonoidalFunctor.μ X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X.obj Y.obj)

@[simp]

theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.BraidedCategory C] : ∀ {X Y : CategoryTheory.InducedCategory C CategoryTheory.FullSubcategory.obj} (f : X ⟶ Y), (CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion P).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.toPrefunctor.map f = f

@[simp]

theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion_ε {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.BraidedCategory C] : (CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion P).toMonoidalFunctor.toLaxMonoidalFunctor.ε = CategoryTheory.CategoryStruct.id (𝟙_ C)

@[simp]

theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.BraidedCategory C] (self : CategoryTheory.FullSubcategory P) : (CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion P).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj self = self.obj

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

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

Equations

• CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion P = CategoryTheory.BraidedFunctor.mk (CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion P)

instance CategoryTheory.MonoidalCategory.fullBraidedSubcategory.full {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.BraidedCategory C] : CategoryTheory.Full (CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion P).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor

Equations

• CategoryTheory.MonoidalCategory.fullBraidedSubcategory.full P = CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.full P

instance CategoryTheory.MonoidalCategory.fullBraidedSubcategory.faithful {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.BraidedCategory C] : CategoryTheory.Faithful (CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion P).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategory.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'] [CategoryTheory.BraidedCategory C] (h : ∀ ⦃X : C⦄, P X → P' X) (X : CategoryTheory.FullSubcategory P) (Y : CategoryTheory.FullSubcategory P) : (CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map h).toMonoidalFunctor.toLaxMonoidalFunctor.μ X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.FullSubcategory.map h).toPrefunctor.obj X) ((CategoryTheory.FullSubcategory.map h).toPrefunctor.obj Y))

@[simp]

theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map_obj_obj {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'] [CategoryTheory.BraidedCategory C] (h : ∀ ⦃X : C⦄, P X → P' X) (X : CategoryTheory.FullSubcategory P) : ((CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map h).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj X).obj = X.obj

@[simp]

theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map_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'] [CategoryTheory.BraidedCategory C] (h : ∀ ⦃X : C⦄, P X → P' X) : ∀ {X Y : CategoryTheory.FullSubcategory P} (f : X ⟶ Y), (CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map h).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.toPrefunctor.map f = f

@[simp]

theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategory.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'] [CategoryTheory.BraidedCategory C] (h : ∀ ⦃X : C⦄, P X → P' X) : (CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map h).toMonoidalFunctor.toLaxMonoidalFunctor.ε = CategoryTheory.CategoryStruct.id (𝟙_ (CategoryTheory.FullSubcategory P'))

def CategoryTheory.MonoidalCategory.fullBraidedSubcategory.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'] [CategoryTheory.BraidedCategory C] (h : ∀ ⦃X : C⦄, P X → P' X) : CategoryTheory.BraidedFunctor (CategoryTheory.FullSubcategory P) (CategoryTheory.FullSubcategory P')

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

Equations

• CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map h = CategoryTheory.BraidedFunctor.mk (CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map h)

instance CategoryTheory.MonoidalCategory.fullBraidedSubcategory.mapFull {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'] [CategoryTheory.BraidedCategory C] (h : ∀ ⦃X : C⦄, P X → P' X) : CategoryTheory.Full (CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map h).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor

Equations

• CategoryTheory.MonoidalCategory.fullBraidedSubcategory.mapFull h = CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.mapFull h

instance CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map_faithful {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'] [CategoryTheory.BraidedCategory C] (h : ∀ ⦃X : C⦄, P X → P' X) : CategoryTheory.Faithful (CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map h).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor

Equations

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

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.MonoidalCategory.fullBraidedSubcategoryInclusion 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).toPrefunctor.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 : CategoryTheory.FullSubcategory P) (Y : CategoryTheory.FullSubcategory P) : ((CategoryTheory.ihom X).toPrefunctor.obj Y).obj = (CategoryTheory.ihom X.obj).toPrefunctor.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 : CategoryTheory.FullSubcategory P} {Z : CategoryTheory.FullSubcategory P} (f : Y ⟶ Z) : (CategoryTheory.ihom X).toPrefunctor.map f = (CategoryTheory.ihom X.obj).toPrefunctor.map f