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 #
- Add monoidal/braided versions of
ObjectProperty.Lift
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
This is the property that P : ObjectProperty C
holds
for the unit of the monoidal category structure.
- prop_unit : P (MonoidalCategoryStruct.tensorUnit C)
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
Instances
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
- P.fullBraidedSubcategory = CategoryTheory.braidedCategoryOfFaithful P.ι (fun (X Y : P.FullSubcategory) => P.isoMk (β_ X.obj Y.obj)) ⋯
The forgetful braided functor from a full braided subcategory into the original category ("forgetting" the condition).
Equations
- P.instBraidedFullSubcategoryι = { toMonoidal := P.monoidalι, braided := ⋯ }
An inequality P ≤ P'
between monoidal properties of objects induces
a braided functor between full braided subcategories.
Equations
- CategoryTheory.ObjectProperty.instBraidedFullSubcategoryιOfLE h = { toMonoidal := CategoryTheory.ObjectProperty.instMonoidalFullSubcategoryιOfLE h, braided := ⋯ }
Equations
- One or more equations did not get rendered due to their size.
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.