Full monoidal subcategories #
Given a monidal 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 category_theory.full_subcategory
).
When C
is also braided/symmetric, the full monoidal subcategory also inherits the
braided/symmetric structure.
TODO #
- Add monoidal/braided versions of
category_theory.full_subcategory.lift
- prop_id' : P (š_ C) . "obviously"
- prop_tensor' : (ā {X Y : C}, P X ā P Y ā P (X ā Y)) . "obviously"
A property C ā Prop
is a monoidal predicate if it is closed under š_
and ā
.
Instances of this typeclass
When P
is a monoidal predicate, the full subcategory for P
inherits the monoidal structure of
C
.
Equations
- category_theory.monoidal_category.full_monoidal_subcategory P = {tensor_obj := Ī» (X Y : category_theory.full_subcategory P), {obj := X.obj ā Y.obj, property := _}, tensor_hom := Ī» (Xā Yā Xā Yā : category_theory.full_subcategory P) (f : Xā ā¶ Yā) (g : Xā ā¶ Yā), id (id (Ī» (f : Xā.obj ā¶ Yā.obj), id (Ī» (g : Xā.obj ā¶ Yā.obj), f ā g) g) f), tensor_id' := _, tensor_comp' := _, tensor_unit := {obj := š_ C _inst_2, property := _}, associator := Ī» (X Y Z : category_theory.full_subcategory P), {hom := (Ī±_ X.obj Y.obj Z.obj).hom, inv := (Ī±_ X.obj Y.obj Z.obj).inv, hom_inv_id' := _, inv_hom_id' := _}, associator_naturality' := _, left_unitor := Ī» (X : category_theory.full_subcategory P), {hom := (Ī»_ X.obj).hom, inv := (Ī»_ X.obj).inv, hom_inv_id' := _, inv_hom_id' := _}, left_unitor_naturality' := _, right_unitor := Ī» (X : category_theory.full_subcategory P), {hom := (Ļ_ X.obj).hom, inv := (Ļ_ X.obj).inv, hom_inv_id' := _, inv_hom_id' := _}, right_unitor_naturality' := _, pentagon' := _, triangle' := _}
The forgetful monoidal functor from a full monoidal subcategory into the original category ("forgetting" the condition).
Equations
- category_theory.monoidal_category.full_monoidal_subcategory_inclusion P = {to_lax_monoidal_functor := {to_functor := category_theory.full_subcategory_inclusion P, Īµ := š (š_ C), Ī¼ := Ī» (X Y : category_theory.full_subcategory P), š ((category_theory.full_subcategory_inclusion P).obj X ā (category_theory.full_subcategory_inclusion P).obj Y), Ī¼_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, Īµ_is_iso := _, Ī¼_is_iso := _}
An implication of predicates P ā P'
induces a monoidal functor between full monoidal
subcategories.
Equations
- category_theory.monoidal_category.full_monoidal_subcategory.map h = {to_lax_monoidal_functor := {to_functor := category_theory.full_subcategory.map h, Īµ := š (š_ (category_theory.full_subcategory P')), Ī¼ := Ī» (X Y : category_theory.full_subcategory P), š ((category_theory.full_subcategory.map h).obj X ā (category_theory.full_subcategory.map h).obj Y), Ī¼_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, Īµ_is_iso := _, Ī¼_is_iso := _}
Equations
- category_theory.monoidal_category.full_monoidal_subcategory.map_full h = {preimage := Ī» (X Y : category_theory.full_subcategory (Ī» (X : C), P X)) (f : (category_theory.monoidal_category.full_monoidal_subcategory.map h).to_lax_monoidal_functor.to_functor.obj X ā¶ (category_theory.monoidal_category.full_monoidal_subcategory.map h).to_lax_monoidal_functor.to_functor.obj Y), f, witness' := _}
The braided structure on a full subcategory inherited by the braided structure on C
.
Equations
- category_theory.monoidal_category.full_braided_subcategory P = category_theory.braided_category_of_faithful (category_theory.monoidal_category.full_monoidal_subcategory_inclusion P) (Ī» (X Y : category_theory.full_subcategory P), {hom := (Ī²_ X.obj Y.obj).hom, inv := (Ī²_ X.obj Y.obj).inv, hom_inv_id' := _, inv_hom_id' := _}) _
The forgetful braided functor from a full braided subcategory into the original category ("forgetting" the condition).
An implication of predicates P ā P'
induces a braided functor between full braided
subcategories.
- prop_ihom' : (ā {X Y : C}, P X ā P Y ā P ((category_theory.ihom X).obj Y)) . "obviously"
A property C ā Prop
is a closed predicate if it is closed under taking internal homs
Instances of this typeclass
Equations
- category_theory.monoidal_category.full_monoidal_closed_subcategory P = {closed' := Ī» (X : category_theory.full_subcategory P), {is_adj := {right := category_theory.full_subcategory.lift P (category_theory.full_subcategory_inclusion P ā category_theory.ihom X.obj) _, adj := category_theory.adjunction.mk_of_unit_counit {unit := {app := Ī» (Y : category_theory.full_subcategory P), (category_theory.ihom.coev X.obj).app Y.obj, naturality' := _}, counit := {app := Ī» (Y : category_theory.full_subcategory P), (category_theory.ihom.ev X.obj).app Y.obj, naturality' := _}, left_triangle' := _, right_triangle' := _}}}}