Full monoidal subcategories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
@[class]
structure
category_theory.monoidal_category.monoidal_predicate
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(P : C → Prop) :
Prop
A property C → Prop is a monoidal predicate if it is closed under 𝟙_ and ⊗.
Instances of this typeclass
theorem
category_theory.monoidal_category.monoidal_predicate.prop_id
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{P : C → Prop}
[self : category_theory.monoidal_category.monoidal_predicate P] :
P (𝟙_ C)
theorem
category_theory.monoidal_category.monoidal_predicate.prop_tensor
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{P : C → Prop}
[self : category_theory.monoidal_category.monoidal_predicate P]
{X Y : C} :
@[protected, instance]
def
category_theory.monoidal_category.full_monoidal_subcategory
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(P : C → Prop)
[category_theory.monoidal_category.monoidal_predicate P] :
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' := _}
def
category_theory.monoidal_category.full_monoidal_subcategory_inclusion
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(P : C → Prop)
[category_theory.monoidal_category.monoidal_predicate P] :
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 := _}
@[simp]
@[simp]
theorem
category_theory.monoidal_category.full_monoidal_subcategory_inclusion_to_lax_monoidal_functor_μ
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(P : C → Prop)
[category_theory.monoidal_category.monoidal_predicate P]
(X Y : category_theory.full_subcategory P) :
@[simp]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
def
category_theory.monoidal_category.category_theory.full_subcategory.category_theory.monoidal_preadditive
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(P : C → Prop)
[category_theory.monoidal_category.monoidal_predicate P]
[category_theory.preadditive C]
[category_theory.monoidal_preadditive C] :
@[protected, instance]
def
category_theory.monoidal_category.full_monoidal_subcategory_inclusion_linear
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(P : C → Prop)
[category_theory.monoidal_category.monoidal_predicate P]
[category_theory.preadditive C]
(R : Type u_1)
[ring R]
[category_theory.linear R C] :
@[protected, instance]
def
category_theory.monoidal_category.category_theory.full_subcategory.category_theory.monoidal_linear
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(P : C → Prop)
[category_theory.monoidal_category.monoidal_predicate P]
[category_theory.preadditive C]
(R : Type u_1)
[ring R]
[category_theory.linear R C]
[category_theory.monoidal_preadditive C]
[category_theory.monoidal_linear R C] :
@[simp]
theorem
category_theory.monoidal_category.full_monoidal_subcategory.map_to_lax_monoidal_functor_to_functor
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{P : C → Prop}
[category_theory.monoidal_category.monoidal_predicate P]
{P' : C → Prop}
[category_theory.monoidal_category.monoidal_predicate P']
(h : ∀ ⦃X : C⦄, P X → P' X) :
def
category_theory.monoidal_category.full_monoidal_subcategory.map
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{P : C → Prop}
[category_theory.monoidal_category.monoidal_predicate P]
{P' : C → Prop}
[category_theory.monoidal_category.monoidal_predicate P']
(h : ∀ ⦃X : C⦄, P X → P' X) :
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 := _}
@[simp]
theorem
category_theory.monoidal_category.full_monoidal_subcategory.map_to_lax_monoidal_functor_μ
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{P : C → Prop}
[category_theory.monoidal_category.monoidal_predicate P]
{P' : C → Prop}
[category_theory.monoidal_category.monoidal_predicate P']
(h : ∀ ⦃X : C⦄, P X → P' X)
(X Y : category_theory.full_subcategory P) :
@[simp]
theorem
category_theory.monoidal_category.full_monoidal_subcategory.map_to_lax_monoidal_functor_ε
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{P : C → Prop}
[category_theory.monoidal_category.monoidal_predicate P]
{P' : C → Prop}
[category_theory.monoidal_category.monoidal_predicate P']
(h : ∀ ⦃X : C⦄, P X → P' X) :
@[protected, instance]
def
category_theory.monoidal_category.full_monoidal_subcategory.map_full
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{P : C → Prop}
[category_theory.monoidal_category.monoidal_predicate P]
{P' : C → Prop}
[category_theory.monoidal_category.monoidal_predicate P']
(h : ∀ ⦃X : C⦄, P X → P' X) :
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' := _}
@[protected, instance]
def
category_theory.monoidal_category.full_monoidal_subcategory.map_faithful
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{P : C → Prop}
[category_theory.monoidal_category.monoidal_predicate P]
{P' : C → Prop}
[category_theory.monoidal_category.monoidal_predicate P']
(h : ∀ ⦃X : C⦄, P X → P' X) :
@[protected, instance]
def
category_theory.monoidal_category.full_braided_subcategory
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(P : C → Prop)
[category_theory.monoidal_category.monoidal_predicate P]
[category_theory.braided_category C] :
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' := _}) _
@[simp]
def
category_theory.monoidal_category.full_braided_subcategory_inclusion
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(P : C → Prop)
[category_theory.monoidal_category.monoidal_predicate P]
[category_theory.braided_category C] :
The forgetful braided functor from a full braided subcategory into the original category ("forgetting" the condition).
@[protected, instance]
@[protected, instance]
def
category_theory.monoidal_category.full_braided_subcategory.map
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{P : C → Prop}
[category_theory.monoidal_category.monoidal_predicate P]
{P' : C → Prop}
[category_theory.monoidal_category.monoidal_predicate P']
[category_theory.braided_category C]
(h : ∀ ⦃X : C⦄, P X → P' X) :
An implication of predicates P → P' induces a braided functor between full braided
subcategories.
@[simp]
theorem
category_theory.monoidal_category.full_braided_subcategory.map_to_monoidal_functor
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{P : C → Prop}
[category_theory.monoidal_category.monoidal_predicate P]
{P' : C → Prop}
[category_theory.monoidal_category.monoidal_predicate P']
[category_theory.braided_category C]
(h : ∀ ⦃X : C⦄, P X → P' X) :
@[protected, instance]
def
category_theory.monoidal_category.full_braided_subcategory.map_full
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{P : C → Prop}
[category_theory.monoidal_category.monoidal_predicate P]
{P' : C → Prop}
[category_theory.monoidal_category.monoidal_predicate P']
[category_theory.braided_category C]
(h : ∀ ⦃X : C⦄, P X → P' X) :
@[protected, instance]
def
category_theory.monoidal_category.full_braided_subcategory.map_faithful
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{P : C → Prop}
[category_theory.monoidal_category.monoidal_predicate P]
{P' : C → Prop}
[category_theory.monoidal_category.monoidal_predicate P']
[category_theory.braided_category C]
(h : ∀ ⦃X : C⦄, P X → P' X) :
@[protected, instance]
@[class]
structure
category_theory.monoidal_category.closed_predicate
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(P : C → Prop)
[category_theory.monoidal_category.monoidal_predicate P]
[category_theory.monoidal_closed C] :
Prop
A property C → Prop is a closed predicate if it is closed under taking internal homs
Instances of this typeclass
theorem
category_theory.monoidal_category.closed_predicate.prop_ihom
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{P : C → Prop}
[category_theory.monoidal_category.monoidal_predicate P]
[category_theory.monoidal_closed C]
[self : category_theory.monoidal_category.closed_predicate P]
{X Y : C} :
P X → P Y → P ((category_theory.ihom X).obj Y)
@[protected, instance]
def
category_theory.monoidal_category.full_monoidal_closed_subcategory
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(P : C → Prop)
[category_theory.monoidal_category.monoidal_predicate P]
[category_theory.monoidal_closed C]
[category_theory.monoidal_category.closed_predicate P] :
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' := _}}}}
@[simp]
theorem
category_theory.monoidal_category.full_monoidal_closed_subcategory_ihom_obj
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(P : C → Prop)
[category_theory.monoidal_category.monoidal_predicate P]
[category_theory.monoidal_closed C]
[category_theory.monoidal_category.closed_predicate P]
(X Y : category_theory.full_subcategory P) :
((category_theory.ihom X).obj Y).obj = (category_theory.ihom X.obj).obj Y.obj
@[simp]
theorem
category_theory.monoidal_category.full_monoidal_closed_subcategory_ihom_map
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(P : C → Prop)
[category_theory.monoidal_category.monoidal_predicate P]
[category_theory.monoidal_closed C]
[category_theory.monoidal_category.closed_predicate P]
(X : category_theory.full_subcategory P)
{Y Z : category_theory.full_subcategory P}
(f : Y ⟶ Z) :
(category_theory.ihom X).map f = (category_theory.ihom X.obj).map f