# mathlibdocumentation

category_theory.monoidal.subcategory

# Full monoidal subcategories #

Given a monidal 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 category_theory.full_subcategory).

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

## TODO #

• Add monoidal/braided versions of category_theory.full_subcategory.lift
@[class]
structure category_theory.monoidal_category.monoidal_predicate {C : Type u} (P : C ā Prop) :
Prop
• prop_id' : P (š_ C) . "obviously"
• prop_tensor' : (ā {X Y : C}, P X ā P Y ā P (X ā Y)) . "obviously"

A property C ā Prop is a monoidal predicate if it is closed under š_ and ā.

Instances of this typeclass
theorem category_theory.monoidal_category.monoidal_predicate.prop_id {C : Type u} {P : C ā Prop}  :
P (š_ C)
theorem category_theory.monoidal_category.monoidal_predicate.prop_tensor {C : Type u} {P : C ā Prop} {X Y : C} :
P X ā P Y ā P (X ā Y)
@[protected, instance]

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

Equations

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

Equations
@[simp]
@[simp]
@[simp]
@[protected, instance]
Equations
@[protected, instance]
@[simp]
theorem category_theory.monoidal_category.full_monoidal_subcategory.map_to_lax_monoidal_functor_to_functor {C : Type u} {P : C ā Prop} {P' : C ā Prop} (h : ā ā¦X : Cā¦, P X ā P' X) :
def category_theory.monoidal_category.full_monoidal_subcategory.map {C : Type u} {P : C ā Prop} {P' : C ā Prop} (h : ā ā¦X : Cā¦, P X ā P' X) :

An implication of predicates P ā P' induces a monoidal functor between full monoidal subcategories.

Equations
@[simp]
theorem category_theory.monoidal_category.full_monoidal_subcategory.map_to_lax_monoidal_functor_Ī¼ {C : Type u} {P : C ā Prop} {P' : C ā Prop} (h : ā ā¦X : Cā¦, P X ā P' X) (X Y : category_theory.full_subcategory P) :
@[simp]
theorem category_theory.monoidal_category.full_monoidal_subcategory.map_to_lax_monoidal_functor_Īµ {C : Type u} {P : C ā Prop} {P' : C ā Prop} (h : ā ā¦X : Cā¦, P X ā P' X) :
@[protected, instance]
def category_theory.monoidal_category.full_monoidal_subcategory.map_full {C : Type u} {P : C ā Prop} {P' : C ā Prop} (h : ā ā¦X : Cā¦, P X ā P' X) :
Equations
@[protected, instance]
def category_theory.monoidal_category.full_monoidal_subcategory.map_faithful {C : Type u} {P : C ā Prop} {P' : C ā Prop} (h : ā ā¦X : Cā¦, P X ā P' X) :
@[protected, instance]

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

Equations
@[simp]

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

Equations
@[protected, instance]
Equations
@[protected, instance]
def category_theory.monoidal_category.full_braided_subcategory.map {C : Type u} {P : C ā Prop} {P' : C ā Prop} (h : ā ā¦X : Cā¦, P X ā P' X) :

An implication of predicates P ā P' induces a braided functor between full braided subcategories.

Equations
@[simp]
theorem category_theory.monoidal_category.full_braided_subcategory.map_to_monoidal_functor {C : Type u} {P : C ā Prop} {P' : C ā Prop} (h : ā ā¦X : Cā¦, P X ā P' X) :
@[protected, instance]
def category_theory.monoidal_category.full_braided_subcategory.map_full {C : Type u} {P : C ā Prop} {P' : C ā Prop} (h : ā ā¦X : Cā¦, P X ā P' X) :
Equations
@[protected, instance]
def category_theory.monoidal_category.full_braided_subcategory.map_faithful {C : Type u} {P : C ā Prop} {P' : C ā Prop} (h : ā ā¦X : Cā¦, P X ā P' X) :
@[protected, instance]
Equations
@[class]
structure category_theory.monoidal_category.closed_predicate {C : Type u} (P : C ā Prop)  :
Prop
• prop_ihom' : (ā {X Y : C}, P X ā P Y ā P .obj Y)) . "obviously"

A property C ā Prop is a closed predicate if it is closed under taking internal homs

Instances of this typeclass
theorem category_theory.monoidal_category.closed_predicate.prop_ihom {C : Type u} {P : C ā Prop} {X Y : C} :
P X ā P Y ā P .obj Y)
@[protected, instance]
Equations
@[simp]
@[simp]