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 #
- Add monoidal/braided versions of
CategoryTheory.FullSubcategory.Lift
class
CategoryTheory.MonoidalCategory.MonoidalPredicate
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
:
A property C → Prop is a monoidal predicate if it is closed under 𝟙_ and ⊗.
- prop_id : P (𝟙_ C)
- prop_tensor {X Y : C} : P X → P Y → P (tensorObj X Y)
Instances
instance
CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_whiskerRight
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
{X₁ X₂ : FullSubcategory P}
(f : X₁.obj ⟶ X₂.obj)
(Y : FullSubcategory P)
:
whiskerRight f Y = whiskerRight f Y.obj
@[simp]
theorem
CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_tensorUnit_obj
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
:
(𝟙_ (FullSubcategory P)).obj = 𝟙_ C
@[simp]
theorem
CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_rightUnitor_hom
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
(X : FullSubcategory P)
:
(rightUnitor X).hom = (rightUnitor X.obj).hom
@[simp]
theorem
CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_leftUnitor_hom
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
(X : FullSubcategory P)
:
(leftUnitor X).hom = (leftUnitor X.obj).hom
@[simp]
theorem
CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_whiskerLeft
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
(X x✝ x✝¹ : FullSubcategory P)
(f : x✝ ⟶ x✝¹)
:
whiskerLeft X f = whiskerLeft X.obj f
@[simp]
theorem
CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_associator_hom
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
(X Y Z : FullSubcategory P)
:
(associator X Y Z).hom = (associator X.obj Y.obj Z.obj).hom
@[simp]
theorem
CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_associator_inv
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
(X Y Z : FullSubcategory P)
:
(associator X Y Z).inv = (associator X.obj Y.obj Z.obj).inv
@[simp]
theorem
CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_tensorObj_obj
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
(X Y : FullSubcategory P)
:
@[simp]
theorem
CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_leftUnitor_inv
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
(X : FullSubcategory P)
:
(leftUnitor X).inv = (leftUnitor X.obj).inv
@[simp]
theorem
CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_rightUnitor_inv
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
(X : FullSubcategory P)
:
(rightUnitor X).inv = (rightUnitor X.obj).inv
@[simp]
theorem
CategoryTheory.MonoidalCategory.instMonoidalCategoryStructFullSubcategory_tensorHom
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
{X₁✝ Y₁✝ X₂✝ Y₂✝ : FullSubcategory P}
(f : X₁✝ ⟶ Y₁✝)
(g : X₂✝ ⟶ Y₂✝)
:
instance
CategoryTheory.MonoidalCategory.fullMonoidalSubcategory
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
:
When P is a monoidal predicate, 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.MonoidalCategory.fullSubcategoryInclusionMonoidal
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
:
(fullSubcategoryInclusion P).Monoidal
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.MonoidalCategory.fullSubcategoryInclusion_ε
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
:
@[simp]
theorem
CategoryTheory.MonoidalCategory.fullSubcategoryInclusion_η
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
:
@[simp]
theorem
CategoryTheory.MonoidalCategory.fullSubcategoryInclusion_μ
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
(X Y : FullSubcategory P)
:
Functor.LaxMonoidal.μ (fullSubcategoryInclusion P) X Y = CategoryStruct.id (tensorObj ((fullSubcategoryInclusion P).obj X) ((fullSubcategoryInclusion P).obj Y))
@[simp]
theorem
CategoryTheory.MonoidalCategory.fullSubcategoryInclusion_δ
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
(X Y : FullSubcategory P)
:
Functor.OplaxMonoidal.δ (fullSubcategoryInclusion P) X Y = CategoryStruct.id ((fullSubcategoryInclusion P).obj (tensorObj X Y))
instance
CategoryTheory.MonoidalCategory.instMonoidalPreadditiveFullSubcategory
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
[Preadditive C]
[MonoidalPreadditive C]
:
instance
CategoryTheory.MonoidalCategory.instMonoidalLinearFullSubcategory
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
[Preadditive C]
(R : Type u_1)
[Ring R]
[Linear R C]
[MonoidalPreadditive C]
[MonoidalLinear R C]
:
instance
CategoryTheory.MonoidalCategory.instMonoidalFullSubcategoryMap
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{P : C → Prop}
[MonoidalPredicate P]
{P' : C → Prop}
[MonoidalPredicate P']
(h : ∀ ⦃X : C⦄, P X → P' X)
:
(FullSubcategory.map h).Monoidal
An implication of predicates P → P' induces a monoidal functor between full monoidal
subcategories.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.MonoidalCategory.fullSubcategory_map_ε
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{P : C → Prop}
[MonoidalPredicate P]
{P' : C → Prop}
[MonoidalPredicate P']
(h : ∀ ⦃X : C⦄, P X → P' X)
:
@[simp]
theorem
CategoryTheory.MonoidalCategory.fullSubcategory_map_η
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{P : C → Prop}
[MonoidalPredicate P]
{P' : C → Prop}
[MonoidalPredicate P']
(h : ∀ ⦃X : C⦄, P X → P' X)
:
Functor.OplaxMonoidal.η (FullSubcategory.map h) = CategoryStruct.id ((FullSubcategory.map h).obj (𝟙_ (FullSubcategory P)))
@[simp]
theorem
CategoryTheory.MonoidalCategory.fullSubcategory_map_μ
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{P : C → Prop}
[MonoidalPredicate P]
{P' : C → Prop}
[MonoidalPredicate P']
(h : ∀ ⦃X : C⦄, P X → P' X)
(X Y : FullSubcategory P)
:
Functor.LaxMonoidal.μ (FullSubcategory.map h) X Y = CategoryStruct.id (tensorObj ((FullSubcategory.map h).obj X) ((FullSubcategory.map h).obj Y))
@[simp]
theorem
CategoryTheory.MonoidalCategory.fullSubcategory_map_δ
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{P : C → Prop}
[MonoidalPredicate P]
{P' : C → Prop}
[MonoidalPredicate P']
(h : ∀ ⦃X : C⦄, P X → P' X)
(X Y : FullSubcategory P)
:
Functor.OplaxMonoidal.δ (FullSubcategory.map h) X Y = CategoryStruct.id ((FullSubcategory.map h).obj (tensorObj X Y))
instance
CategoryTheory.MonoidalCategory.fullBraidedSubcategory
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
[BraidedCategory C]
:
The braided structure on a full subcategory inherited by the braided structure on C.
Equations
- One or more equations did not get rendered due to their size.
instance
CategoryTheory.MonoidalCategory.instBraidedFullSubcategoryFullSubcategoryInclusion
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
[BraidedCategory C]
:
(fullSubcategoryInclusion P).Braided
The forgetful braided functor from a full braided subcategory into the original category ("forgetting" the condition).
instance
CategoryTheory.MonoidalCategory.instBraidedFullSubcategoryMap
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
{P : C → Prop}
[MonoidalPredicate P]
[BraidedCategory C]
{P' : C → Prop}
[MonoidalPredicate P']
(h : ∀ ⦃X : C⦄, P X → P' X)
:
(FullSubcategory.map h).Braided
An implication of predicates P → P' induces a braided functor between full braided
subcategories.
instance
CategoryTheory.MonoidalCategory.fullSymmetricSubcategory
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
[SymmetricCategory C]
:
class
CategoryTheory.MonoidalCategory.ClosedPredicate
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalClosed C]
:
A property C → Prop is a closed predicate if it is closed under taking internal homs
- prop_ihom {X Y : C} : P X → P Y → P ((ihom X).obj Y)
Instances
instance
CategoryTheory.MonoidalCategory.fullMonoidalClosedSubcategory
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
[MonoidalClosed C]
[ClosedPredicate P]
:
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.MonoidalCategory.fullMonoidalClosedSubcategory_ihom_obj
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
[MonoidalClosed C]
[ClosedPredicate P]
(X Y : FullSubcategory P)
:
@[simp]
theorem
CategoryTheory.MonoidalCategory.fullMonoidalClosedSubcategory_ihom_map
{C : Type u}
[Category.{v, u} C]
[MonoidalCategory C]
(P : C → Prop)
[MonoidalPredicate P]
[MonoidalClosed C]
[ClosedPredicate P]
(X : FullSubcategory P)
{Y Z : FullSubcategory P}
(f : Y ⟶ Z)
: