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 #

source
class CategoryTheory.MonoidalCategory.MonoidalPredicate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) :
Prop

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

Instances
    source
    instance CategoryTheory.MonoidalCategory.fullMonoidalSubcategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] :
    CategoryTheory.MonoidalCategory (CategoryTheory.FullSubcategory P)

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

    source
    @[simp]
    theorem CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion_toLaxMonoidalFunctor_ε {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] :
    (CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.ε = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C)
    source
    @[simp]
    theorem CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion_toLaxMonoidalFunctor_toFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] :
    (CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor = CategoryTheory.fullSubcategoryInclusion P
    source
    @[simp]
    theorem CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion_toLaxMonoidalFunctor_μ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] (X : CategoryTheory.FullSubcategory P) (Y : CategoryTheory.FullSubcategory P) :
    CategoryTheory.LaxMonoidalFunctor.μ (CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.fullSubcategoryInclusion P).obj X) ((CategoryTheory.fullSubcategoryInclusion P).obj Y))
    source
    def CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] :
    CategoryTheory.MonoidalFunctor (CategoryTheory.FullSubcategory P) C

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

    Instances For
      source
      instance CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.full {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] :
      CategoryTheory.Full (CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor
      source
      instance CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.faithful {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] :
      CategoryTheory.Faithful (CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor
      source
      instance CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion_additive {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.Preadditive C] :
      CategoryTheory.Functor.Additive (CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor
      source
      instance CategoryTheory.MonoidalCategory.instMonoidalPreadditiveFullSubcategoryCategoryFullSubcategoryFullMonoidalSubcategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.Preadditive C] [CategoryTheory.MonoidalPreadditive C] :
      CategoryTheory.MonoidalPreadditive (CategoryTheory.FullSubcategory P)
      source
      instance CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion_linear {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.Preadditive C] (R : Type u_1) [Ring R] [CategoryTheory.Linear R C] :
      CategoryTheory.Functor.Linear R (CategoryTheory.MonoidalCategory.fullMonoidalSubcategoryInclusion P).toLaxMonoidalFunctor.toFunctor
      source
      instance CategoryTheory.MonoidalCategory.instMonoidalLinearToSemiringFullSubcategoryCategoryFullSubcategoryFullSubcategoryFullMonoidalSubcategoryInstMonoidalPreadditiveFullSubcategoryCategoryFullSubcategoryFullMonoidalSubcategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.Preadditive C] (R : Type u_1) [Ring R] [CategoryTheory.Linear R C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear R C] :
      CategoryTheory.MonoidalLinear R (CategoryTheory.FullSubcategory P)
      source
      @[simp]
      theorem CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map_toLaxMonoidalFunctor_ε {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P] {P' : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P'] (h : ⦃X : C⦄ → P X → P' X) :
      (CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map h).toLaxMonoidalFunctor.ε = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.FullSubcategory P'))
      source
      @[simp]
      theorem CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map_toLaxMonoidalFunctor_toFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P] {P' : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P'] (h : ⦃X : C⦄ → P X → P' X) :
      (CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map h).toLaxMonoidalFunctor.toFunctor = CategoryTheory.FullSubcategory.map h
      source
      @[simp]
      theorem CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map_toLaxMonoidalFunctor_μ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P] {P' : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P'] (h : ⦃X : C⦄ → P X → P' X) (X : CategoryTheory.FullSubcategory P) (Y : CategoryTheory.FullSubcategory P) :
      CategoryTheory.LaxMonoidalFunctor.μ (CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map h).toLaxMonoidalFunctor X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.FullSubcategory.map h).obj X) ((CategoryTheory.FullSubcategory.map h).obj Y))
      source
      def CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P] {P' : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P'] (h : ⦃X : C⦄ → P X → P' X) :
      CategoryTheory.MonoidalFunctor (CategoryTheory.FullSubcategory P) (CategoryTheory.FullSubcategory P')

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

      Instances For
        source
        instance CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.mapFull {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P] {P' : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P'] (h : ⦃X : C⦄ → P X → P' X) :
        CategoryTheory.Full (CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map h).toLaxMonoidalFunctor.toFunctor
        source
        instance CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map_faithful {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P] {P' : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P'] (h : ⦃X : C⦄ → P X → P' X) :
        CategoryTheory.Faithful (CategoryTheory.MonoidalCategory.fullMonoidalSubcategory.map h).toLaxMonoidalFunctor.toFunctor
        source
        instance CategoryTheory.MonoidalCategory.fullBraidedSubcategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.BraidedCategory C] :
        CategoryTheory.BraidedCategory (CategoryTheory.FullSubcategory P)

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

        source
        @[simp]
        theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.BraidedCategory C] :
        ∀ {X Y : CategoryTheory.InducedCategory C CategoryTheory.FullSubcategory.obj} (f : X ⟶ Y), (CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion P).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.map f = f
        source
        @[simp]
        theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion_ε {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.BraidedCategory C] :
        (CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion P).toMonoidalFunctor.toLaxMonoidalFunctor.ε = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C)
        source
        @[simp]
        theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.BraidedCategory C] (self : CategoryTheory.FullSubcategory P) :
        (CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion P).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.obj self = self.obj
        source
        @[simp]
        theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion_μ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.BraidedCategory C] (X : CategoryTheory.FullSubcategory P) (Y : CategoryTheory.FullSubcategory P) :
        CategoryTheory.LaxMonoidalFunctor.μ (CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion P).toMonoidalFunctor.toLaxMonoidalFunctor X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X.obj Y.obj)
        source
        def CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.BraidedCategory C] :
        CategoryTheory.BraidedFunctor (CategoryTheory.FullSubcategory P) C

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

        Instances For
          source
          instance CategoryTheory.MonoidalCategory.fullBraidedSubcategory.full {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.BraidedCategory C] :
          CategoryTheory.Full (CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion P).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor
          source
          instance CategoryTheory.MonoidalCategory.fullBraidedSubcategory.faithful {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.BraidedCategory C] :
          CategoryTheory.Faithful (CategoryTheory.MonoidalCategory.fullBraidedSubcategoryInclusion P).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor
          source
          @[simp]
          theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P] {P' : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P'] [CategoryTheory.BraidedCategory C] (h : ⦃X : C⦄ → P X → P' X) :
          ∀ {X Y : CategoryTheory.FullSubcategory P} (f : X ⟶ Y), (CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map h).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.map f = f
          source
          @[simp]
          theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map_μ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P] {P' : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P'] [CategoryTheory.BraidedCategory C] (h : ⦃X : C⦄ → P X → P' X) (X : CategoryTheory.FullSubcategory P) (Y : CategoryTheory.FullSubcategory P) :
          CategoryTheory.LaxMonoidalFunctor.μ (CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map h).toMonoidalFunctor.toLaxMonoidalFunctor X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.FullSubcategory.map h).obj X) ((CategoryTheory.FullSubcategory.map h).obj Y))
          source
          @[simp]
          theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map_ε {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P] {P' : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P'] [CategoryTheory.BraidedCategory C] (h : ⦃X : C⦄ → P X → P' X) :
          (CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map h).toMonoidalFunctor.toLaxMonoidalFunctor.ε = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.FullSubcategory P'))
          source
          @[simp]
          theorem CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map_obj_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P] {P' : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P'] [CategoryTheory.BraidedCategory C] (h : ⦃X : C⦄ → P X → P' X) (X : CategoryTheory.FullSubcategory P) :
          ((CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map h).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.obj X).obj = X.obj
          source
          def CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P] {P' : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P'] [CategoryTheory.BraidedCategory C] (h : ⦃X : C⦄ → P X → P' X) :
          CategoryTheory.BraidedFunctor (CategoryTheory.FullSubcategory P) (CategoryTheory.FullSubcategory P')

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

          Instances For
            source
            instance CategoryTheory.MonoidalCategory.fullBraidedSubcategory.mapFull {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P] {P' : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P'] [CategoryTheory.BraidedCategory C] (h : ⦃X : C⦄ → P X → P' X) :
            CategoryTheory.Full (CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map h).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor
            source
            instance CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map_faithful {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P] {P' : C → Prop} [CategoryTheory.MonoidalCategory.MonoidalPredicate P'] [CategoryTheory.BraidedCategory C] (h : ⦃X : C⦄ → P X → P' X) :
            CategoryTheory.Faithful (CategoryTheory.MonoidalCategory.fullBraidedSubcategory.map h).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor
            source
            instance CategoryTheory.MonoidalCategory.fullSymmetricSubcategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.SymmetricCategory C] :
            CategoryTheory.SymmetricCategory (CategoryTheory.FullSubcategory P)
            source
            class CategoryTheory.MonoidalCategory.ClosedPredicate {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalClosed C] :
            Prop

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

            Instances
              source
              instance CategoryTheory.MonoidalCategory.fullMonoidalClosedSubcategory {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.MonoidalClosed C] [CategoryTheory.MonoidalCategory.ClosedPredicate P] :
              CategoryTheory.MonoidalClosed (CategoryTheory.FullSubcategory P)
              source
              @[simp]
              theorem CategoryTheory.MonoidalCategory.fullMonoidalClosedSubcategory_ihom_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.MonoidalClosed C] [CategoryTheory.MonoidalCategory.ClosedPredicate P] (X : CategoryTheory.FullSubcategory P) (Y : CategoryTheory.FullSubcategory P) :
              ((CategoryTheory.ihom X).obj Y).obj = (CategoryTheory.ihom X.obj).obj Y.obj
              source
              @[simp]
              theorem CategoryTheory.MonoidalCategory.fullMonoidalClosedSubcategory_ihom_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (P : C → Prop) [CategoryTheory.MonoidalCategory.MonoidalPredicate P] [CategoryTheory.MonoidalClosed C] [CategoryTheory.MonoidalCategory.ClosedPredicate P] (X : CategoryTheory.FullSubcategory P) {Y : CategoryTheory.FullSubcategory P} {Z : CategoryTheory.FullSubcategory P} (f : Y ⟶ Z) :
              (CategoryTheory.ihom X).map f = (CategoryTheory.ihom X.obj).map f