Documentation

Mathlib.CategoryTheory.Monoidal.Subcategory

Full monoidal subcategories #

Given a monoidal category C and a property of objects P : ObjectProperty C that is monoidal (i.e. it holds for the unit and is stable by ), we can put a monoidal structure on P.FullSubcategory (the category structure is defined in Mathlib.CategoryTheory.ObjectProperty.FullSubcategory).

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

TODO #

Given three properties of objects P₁, P₂, and Q in a monoidal category C, we say TensorLE P₁ P₂ Q holds if the tensor product of an object in P₁ and an object P₂ is necessary in Q, see also ObjectProperty.IsMonoidal.

Instances
    theorem CategoryTheory.ObjectProperty.prop_tensor {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {P₁ P₂ Q : ObjectProperty C} [P₁.TensorLE P₂ Q] {X₁ X₂ : C} (h₁ : P₁ X₁) (h₂ : P₂ X₂) :

    This is the property that P : ObjectProperty C holds for the unit of the monoidal category structure.

    Instances

      If C is a monoidal category, we say that P : ObjectProperty C is monoidal if it is stable by tensor product and holds for the unit.

      Instances

        A property of objects is a monoidal closed if it is closed under taking internal homs

        • prop_ihom (X Y : C) : P XP YP ((ihom X).obj Y)
        Instances
          theorem CategoryTheory.ObjectProperty.prop_ihom {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (P : ObjectProperty C) [MonoidalClosed C] [P.IsMonoidalClosed] {X Y : C} (hX : P X) (hY : P Y) :
          P ((ihom X).obj Y)
          Equations
          • One or more equations did not get rendered due to their size.

          When P : ObjectProperty C is monoidal, the full subcategory for P inherits the monoidal structure of C.

          Equations
          • One or more equations did not get rendered due to their size.

          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.

          An inequality P ≤ P' between monoidal properties of objects induces a monoidal functor between full monoidal subcategories.

          Equations
          • One or more equations did not get rendered due to their size.

          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

          An inequality P ≤ P' between monoidal properties of objects induces a braided functor between full braided subcategories.

          Equations
          Equations
          • One or more equations did not get rendered due to their size.
          @[deprecated CategoryTheory.ObjectProperty.IsMonoidal (since := "2025-03-05")]

          Alias of CategoryTheory.ObjectProperty.IsMonoidal.


          If C is a monoidal category, we say that P : ObjectProperty C is monoidal if it is stable by tensor product and holds for the unit.

          Equations
          Instances For