# 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

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

• prop_id : P (𝟙_ C)
• prop_tensor : ∀ {X Y : C}, P XP Y
Instances
theorem CategoryTheory.MonoidalCategory.MonoidalPredicate.prop_tensor {C : Type u} {P : CProp} {X : C} {Y : C} :
P XP Y
@[simp]
@[simp]
@[simp]
@[simp]
theorem CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_tensorHom {C : Type u} (P : CProp) :
∀ {X₁ Y₁ X₂ Y₂ : } (f : X₁ Y₁) (g : X₂ Y₂),
@[simp]
theorem CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_whiskerRight {C : Type u} (P : CProp) {X₁ : } {X₂ : } (f : X₁.obj X₂.obj) :
@[simp]
@[simp]
@[simp]
Equations
• One or more equations did not get rendered due to their size.

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]

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
Equations
• =
Equations
• =
Equations
• =
Equations
• =
Equations
• =
Equations
• =
@[simp]
theorem CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map_toLaxMonoidalFunctor_toFunctor {C : Type u} {P : CProp} {P' : CProp} (h : ∀ ⦃X : C⦄, P XP' X) :
@[simp]
theorem CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map_toLaxMonoidalFunctor_ε {C : Type u} {P : CProp} {P' : CProp} (h : ∀ ⦃X : C⦄, P XP' X) :
@[simp]
theorem CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map_toLaxMonoidalFunctor_μ {C : Type u} {P : CProp} {P' : CProp} (h : ∀ ⦃X : C⦄, P XP' X) :
def CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map {C : Type u} {P : CProp} {P' : CProp} (h : ∀ ⦃X : C⦄, P XP' X) :

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
instance CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map_full {C : Type u} {P : CProp} {P' : CProp} (h : ∀ ⦃X : C⦄, P XP' X) :
Equations
• =
instance CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map_faithful {C : Type u} {P : CProp} {P' : CProp} (h : ∀ ⦃X : C⦄, P XP' X) :
Equations
• =

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]
@[simp]
@[simp]
theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion_obj {C : Type u} (P : CProp) (self : ) :
= self.obj
@[simp]
theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion_map {C : Type u} (P : CProp) :
∀ {X Y : CategoryTheory.InducedCategory C CategoryTheory.FullSubcategory.obj} (f : X Y),

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

Equations
• = { toMonoidalFunctor := , braided := }
Instances For
Equations
• =
Equations
• =
@[simp]
theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map_obj_obj {C : Type u} {P : CProp} {P' : CProp} (h : ∀ ⦃X : C⦄, P XP' X) :
.obj = X.obj
@[simp]
theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map_μ {C : Type u} {P : CProp} {P' : CProp} (h : ∀ ⦃X : C⦄, P XP' X) :
@[simp]
theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map_map {C : Type u} {P : CProp} {P' : CProp} (h : ∀ ⦃X : C⦄, P XP' X) :
∀ {X Y : } (f : X Y),
@[simp]
theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map_ε {C : Type u} {P : CProp} {P' : CProp} (h : ∀ ⦃X : C⦄, P XP' X) :
def CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map {C : Type u} {P : CProp} {P' : CProp} (h : ∀ ⦃X : C⦄, P XP' X) :

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

Equations
• = { toMonoidalFunctor := , braided := }
Instances For
instance CategoryTheory.MonoidalCategory.fullBraidedSubcategory.mapFull {C : Type u} {P : CProp} {P' : CProp} (h : ∀ ⦃X : C⦄, P XP' X) :
Equations
• =
instance CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map_faithful {C : Type u} {P : CProp} {P' : CProp} (h : ∀ ⦃X : C⦄, P XP' X) :
Equations
• =

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

• prop_ihom : ∀ {X Y : C}, P XP YP (.obj Y)
Instances
theorem CategoryTheory.MonoidalCategory.ClosedPredicate.prop_ihom {C : Type u} {P : CProp} {X : C} {Y : C} :
P XP YP (.obj Y)
Equations
• One or more equations did not get rendered due to their size.
@[simp]
@[simp]