# Documentation

Mathlib.CategoryTheory.Monoidal.Subcategory

# 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
• prop_id :
• prop_tensor : ∀ {X Y : C}, P XP Y

A property C → Prop is a monoidal predicate if it is closed under 𝟙_ and ⊗.

Instances

When P is a monoidal predicate, the full subcategory for P inherits the monoidal structure of C.

@[simp]
@[simp]

The forgetful monoidal functor from a full monoidal subcategory into the original category ("forgetting" the condition).

Instances For
instance CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.full {C : Type u} (P : CProp) :
CategoryTheory.Full ().toLaxMonoidalFunctor.toFunctor
instance CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion_linear {C : Type u} (P : CProp) (R : Type u_1) [Ring R] [] :
CategoryTheory.Functor.Linear R ().toLaxMonoidalFunctor.toFunctor
@[simp]
theorem CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map_toLaxMonoidalFunctor_ε {C : Type u} {P : CProp} {P' : CProp} (h : X : C⦄ → P XP' X) :
@[simp]
theorem CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map_toLaxMonoidalFunctor_toFunctor {C : Type u} {P : CProp} {P' : CProp} (h : X : C⦄ → P XP' X) :
().toLaxMonoidalFunctor.toFunctor =
@[simp]
theorem CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map_toLaxMonoidalFunctor_μ {C : Type u} {P : CProp} {P' : CProp} (h : X : C⦄ → P XP' X) :
CategoryTheory.LaxMonoidalFunctor.μ ().toLaxMonoidalFunctor X Y =
def CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map {C : Type u} {P : CProp} {P' : CProp} (h : X : C⦄ → P XP' X) :

An implication of predicates P → P' induces a monoidal functor between full monoidal subcategories.

Instances For
instance CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.mapFull {C : Type u} {P : CProp} {P' : CProp} (h : X : C⦄ → P XP' X) :
CategoryTheory.Full ().toLaxMonoidalFunctor.toFunctor
instance CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map_faithful {C : Type u} {P : CProp} {P' : CProp} (h : X : C⦄ → P XP' X) :
CategoryTheory.Faithful ().toLaxMonoidalFunctor.toFunctor

The braided structure on a full subcategory inherited by the braided structure on C.

@[simp]
theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion_map {C : Type u} (P : CProp) :
∀ {X Y : CategoryTheory.InducedCategory C CategoryTheory.FullSubcategory.obj} (f : X Y), ().toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.map f = f
@[simp]
theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion_ε {C : Type u} (P : CProp) :
().toMonoidalFunctor.toLaxMonoidalFunctor =
@[simp]
theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion_obj {C : Type u} (P : CProp) (self : ) :
().toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.obj self = self.obj
@[simp]
theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion_μ {C : Type u} (P : CProp) :
CategoryTheory.LaxMonoidalFunctor.μ ().toMonoidalFunctor.toLaxMonoidalFunctor X Y =

The forgetful braided functor from a full braided subcategory into the original category ("forgetting" the condition).

Instances For
instance CategoryTheory.MonoidalCategory.fullBraidedSubcategory.full {C : Type u} (P : CProp) :
CategoryTheory.Full ().toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor
instance CategoryTheory.MonoidalCategory.fullBraidedSubcategory.faithful {C : Type u} (P : CProp) :
CategoryTheory.Faithful ().toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor
@[simp]
theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map_map {C : Type u} {P : CProp} {P' : CProp} (h : X : C⦄ → P XP' X) :
∀ {X Y : } (f : X Y), ().toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.map f = f
@[simp]
theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map_μ {C : Type u} {P : CProp} {P' : CProp} (h : X : C⦄ → P XP' X) :
CategoryTheory.LaxMonoidalFunctor.μ ().toMonoidalFunctor.toLaxMonoidalFunctor X Y =
@[simp]
theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map_ε {C : Type u} {P : CProp} {P' : CProp} (h : X : C⦄ → P XP' X) :
().toMonoidalFunctor.toLaxMonoidalFunctor =
@[simp]
theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map_obj_obj {C : Type u} {P : CProp} {P' : CProp} (h : X : C⦄ → P XP' X) :
(().toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.obj X).obj = X.obj
def CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map {C : Type u} {P : CProp} {P' : CProp} (h : X : C⦄ → P XP' X) :

An implication of predicates P → P' induces a braided functor between full braided subcategories.

Instances For
instance CategoryTheory.MonoidalCategory.fullBraidedSubcategory.mapFull {C : Type u} {P : CProp} {P' : CProp} (h : X : C⦄ → P XP' X) :
CategoryTheory.Full ().toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor
instance CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map_faithful {C : Type u} {P : CProp} {P' : CProp} (h : X : C⦄ → P XP' X) :
CategoryTheory.Faithful ().toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor
• prop_ihom : ∀ {X Y : C}, P XP YP (().obj Y)

A property C → Prop is a closed predicate if it is closed under taking internal homs

Instances
@[simp]
theorem CategoryTheory.MonoidalCategory.fullMonoidalClosedSubcategory_ihom_obj {C : Type u} (P : CProp) :
(().obj Y).obj = (CategoryTheory.ihom X.obj).obj Y.obj
@[simp]