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.lean).
When C is also braided/symmetric, the full monoidal subcategory also inherits the
braided/symmetric structure.
TODO #
- Add monoidal/braided versions of
ObjectProperty.Lift
class
CategoryTheory.ObjectProperty.TensorLE
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P₁ P₂ Q : ObjectProperty C)
:
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₂)
:
Q (MonoidalCategoryStruct.tensorObj X₁ X₂)
class
CategoryTheory.ObjectProperty.ContainsUnit
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
:
This is the property that P : ObjectProperty C holds
for the unit of the monoidal category structure.
- prop_unit : P (MonoidalCategoryStruct.tensorUnit C)
Instances
theorem
CategoryTheory.ObjectProperty.prop_unit
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.ContainsUnit]
:
class
CategoryTheory.ObjectProperty.IsMonoidal
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
extends P.ContainsUnit, P.TensorLE P P :
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
class
CategoryTheory.ObjectProperty.IsMonoidalClosed
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[MonoidalClosed C]
:
A property of objects is a monoidal closed if it is closed under taking internal homs
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)
:
instance
CategoryTheory.ObjectProperty.instMonoidalCategoryStructFullSubcategory
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.ObjectProperty.tensorHom_def
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
{X₁✝ Y₁✝ X₂✝ Y₂✝ : P.FullSubcategory}
(f : X₁✝ ⟶ Y₁✝)
(g : X₂✝ ⟶ Y₂✝)
:
@[simp]
theorem
CategoryTheory.ObjectProperty.leftUnitor_def
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
(X : P.FullSubcategory)
:
@[simp]
theorem
CategoryTheory.ObjectProperty.whiskerRight_def
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
{X₁ X₂ : P.FullSubcategory}
(f : X₁.obj ⟶ X₂.obj)
(Y : P.FullSubcategory)
:
@[simp]
theorem
CategoryTheory.ObjectProperty.tensorObj_obj
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
(X Y : P.FullSubcategory)
:
@[simp]
theorem
CategoryTheory.ObjectProperty.tensorUnit_obj
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
:
@[simp]
theorem
CategoryTheory.ObjectProperty.rightUnitor_def
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
(X : P.FullSubcategory)
:
@[simp]
theorem
CategoryTheory.ObjectProperty.whiskerLeft_def
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
(X x✝ x✝¹ : P.FullSubcategory)
(f : x✝ ⟶ x✝¹)
:
@[simp]
theorem
CategoryTheory.ObjectProperty.associator_def
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
(X Y Z : P.FullSubcategory)
:
MonoidalCategoryStruct.associator X Y Z = P.isoMk (MonoidalCategoryStruct.associator X.obj Y.obj Z.obj)
instance
CategoryTheory.ObjectProperty.fullMonoidalSubcategory
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
:
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.
instance
CategoryTheory.ObjectProperty.monoidalι
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
:
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.
@[simp]
theorem
CategoryTheory.ObjectProperty.ι_ε
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
:
@[simp]
theorem
CategoryTheory.ObjectProperty.ι_η
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
:
@[simp]
theorem
CategoryTheory.ObjectProperty.ι_μ
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
(X Y : P.FullSubcategory)
:
Functor.LaxMonoidal.μ P.ι X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj (P.ι.obj X) (P.ι.obj Y))
@[simp]
theorem
CategoryTheory.ObjectProperty.ι_δ
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
(X Y : P.FullSubcategory)
:
Functor.OplaxMonoidal.δ P.ι X Y = CategoryStruct.id (P.ι.obj (MonoidalCategoryStruct.tensorObj X Y))
instance
CategoryTheory.ObjectProperty.instMonoidalPreadditiveFullSubcategory
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
[Preadditive C]
[MonoidalPreadditive C]
:
instance
CategoryTheory.ObjectProperty.instMonoidalLinearFullSubcategory
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
[Preadditive C]
(R : Type u_1)
[Ring R]
[Linear R C]
[MonoidalPreadditive C]
[MonoidalLinear R C]
:
instance
CategoryTheory.ObjectProperty.instMonoidalFullSubcategoryιOfLE
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{P : ObjectProperty C}
[P.IsMonoidal]
{P' : ObjectProperty C}
[P'.IsMonoidal]
(h : P ≤ P')
:
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.
@[simp]
theorem
CategoryTheory.ObjectProperty.ιOfLE_ε
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{P : ObjectProperty C}
[P.IsMonoidal]
{P' : ObjectProperty C}
[P'.IsMonoidal]
(h : P ≤ P')
:
@[simp]
theorem
CategoryTheory.ObjectProperty.ιOfLE_η
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{P : ObjectProperty C}
[P.IsMonoidal]
{P' : ObjectProperty C}
[P'.IsMonoidal]
(h : P ≤ P')
:
@[simp]
theorem
CategoryTheory.ObjectProperty.ιOfLE_μ
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{P : ObjectProperty C}
[P.IsMonoidal]
{P' : ObjectProperty C}
[P'.IsMonoidal]
(h : P ≤ P')
(X Y : P.FullSubcategory)
:
Functor.LaxMonoidal.μ (ιOfLE h) X Y = CategoryStruct.id (MonoidalCategoryStruct.tensorObj ((ιOfLE h).obj X) ((ιOfLE h).obj Y))
@[simp]
theorem
CategoryTheory.ObjectProperty.ιOfLE_δ
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{P : ObjectProperty C}
[P.IsMonoidal]
{P' : ObjectProperty C}
[P'.IsMonoidal]
(h : P ≤ P')
(X Y : P.FullSubcategory)
:
Functor.OplaxMonoidal.δ (ιOfLE h) X Y = CategoryStruct.id ((ιOfLE h).obj (MonoidalCategoryStruct.tensorObj X Y))
instance
CategoryTheory.ObjectProperty.fullBraidedSubcategory
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
[BraidedCategory C]
:
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)) ⋯
instance
CategoryTheory.ObjectProperty.instBraidedFullSubcategoryι
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
[BraidedCategory C]
:
The forgetful braided functor from a full braided subcategory into the original category ("forgetting" the condition).
Equations
- P.instBraidedFullSubcategoryι = { toMonoidal := P.monoidalι, braided := ⋯ }
instance
CategoryTheory.ObjectProperty.instBraidedFullSubcategoryιOfLE
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{P : ObjectProperty C}
[P.IsMonoidal]
[BraidedCategory C]
{P' : ObjectProperty C}
[P'.IsMonoidal]
(h : P ≤ P')
:
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 := ⋯ }
instance
CategoryTheory.ObjectProperty.fullSymmetricSubcategory
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
[SymmetricCategory C]
:
instance
CategoryTheory.ObjectProperty.fullMonoidalClosedSubcategory
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
[MonoidalClosed C]
[P.IsMonoidalClosed]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.ObjectProperty.ihom_obj
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
[MonoidalClosed C]
[P.IsMonoidalClosed]
(X Y : P.FullSubcategory)
:
@[simp]
theorem
CategoryTheory.ObjectProperty.ihom_map
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
[P.IsMonoidal]
[MonoidalClosed C]
[P.IsMonoidalClosed]
(X : P.FullSubcategory)
{Y Z : P.FullSubcategory}
(f : Y ⟶ Z)
:
@[deprecated CategoryTheory.ObjectProperty.IsMonoidal (since := "2025-03-05")]
def
CategoryTheory.MonoidalCategory.MonoidalPredicate
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : ObjectProperty C)
:
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.