mathlib3documentation

category_theory.monoidal.subcategory

Full monoidal subcategories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_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]
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[simp]
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]
Equations
@[protected, instance]
@[protected, instance]

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

Equations

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]
@[protected, instance]
Equations
@[protected, instance]
@[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]