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 #

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

Instances

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

    Instances For

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

      Instances For

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

        Instances For

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

          Instances