Documentation

Mathlib.CategoryTheory.Monoidal.Subcategory

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) :

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)

Instances

theorem CategoryTheory.MonoidalCategory.MonoidalPredicate.prop_id {C : Type u} :

∀ {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C} {P : C → Prop} [self : CategoryTheory.MonoidalCategory.MonoidalPredicate P], P (𝟙_ C)

theorem CategoryTheory.MonoidalCategory.MonoidalPredicate.prop_tensor {C : Type u} :

∀ {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C} {P : C → Prop} [self : CategoryTheory.MonoidalCategory.MonoidalPredicate P] {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_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_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.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_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 : 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.instMonoidalCategoryStructFullSubcategory_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.instMonoidalCategoryStructFullSubcategory_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.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

@[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 : 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

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.

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.

Instances For

@[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).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] :

∀ (x x_1 : CategoryTheory.FullSubcategory P), (CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion P).μ x x_1 = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.fullSubcategoryInclusion P).obj x) ((CategoryTheory.fullSubcategoryInclusion P).obj x_1))

@[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).ε = CategoryTheory.CategoryStruct.id (𝟙_ C)

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

(CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion P).Full

Equations

⋯ = ⋯

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

(CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion P).Faithful

Equations

⋯ = ⋯

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.MonoidalCategory.fullMonoidalSubcategoryInclusion P).Additive

Equations

⋯ = ⋯

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)

Equations

⋯ = ⋯

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).toFunctor

Equations

⋯ = ⋯

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)

Equations

⋯ = ⋯

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.

Instances For

@[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).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 x_1 : CategoryTheory.FullSubcategory P), (CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map h).μ x x_1 = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.FullSubcategory.map h).obj x) ((CategoryTheory.FullSubcategory.map h).obj x_1))

@[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).ε = CategoryTheory.CategoryStruct.id (𝟙_ (CategoryTheory.FullSubcategory P'))

instance CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map_full {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).Full

Equations

⋯ = ⋯

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.MonoidalCategory.fullMonoidalSubcategory.map h).Faithful

Equations

⋯ = ⋯

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.

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 = { toMonoidalFunctor := CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion P, braided := ⋯ }

Instances For

@[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).ε = 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).obj self = self.obj

@[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 x_1 : CategoryTheory.FullSubcategory P), (CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion P).μ x x_1 = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj x.obj x_1.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).map f = f

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.MonoidalCategory.fullBraidedSubcategoryInclusion P).Full

Equations

⋯ = ⋯

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.MonoidalCategory.fullBraidedSubcategoryInclusion P).Faithful

Equations

⋯ = ⋯

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 = { toMonoidalFunctor := CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map h, braided := ⋯ }

Instances For

@[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).map f = f

@[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).obj X).obj = X.obj

@[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 x_1 : CategoryTheory.FullSubcategory P), (CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map h).μ x x_1 = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.FullSubcategory.map h).obj x) ((CategoryTheory.FullSubcategory.map h).obj x_1))

@[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).ε = CategoryTheory.CategoryStruct.id (𝟙_ (CategoryTheory.FullSubcategory P'))

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.MonoidalCategory.fullBraidedSubcategory.map h).Full

Equations

⋯ = ⋯

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.MonoidalCategory.fullBraidedSubcategory.map h).Faithful

Equations

⋯ = ⋯

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] :

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)

Instances

theorem CategoryTheory.MonoidalCategory.ClosedPredicate.prop_ihom {C : Type u} :

∀ {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C} {P : C → Prop} {inst_2 : CategoryTheory.MonoidalClosed C} [self : CategoryTheory.MonoidalCategory.ClosedPredicate P] {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 : CategoryTheory.FullSubcategory P) (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 : CategoryTheory.FullSubcategory P} {Z : CategoryTheory.FullSubcategory P} (f : Y ⟶ Z) :

(CategoryTheory.ihom X).map f = (CategoryTheory.ihom X.obj).map f