Documentation

Mathlib.CategoryTheory.CatCommSq

2-commutative squares of functors #

Similarly as CommSq.lean defines the notion of commutative squares, this file introduces the notion of 2-commutative squares of functors.

If T : C₁ ⥤ C₂, L : C₁ ⥤ C₃, R : C₂ ⥤ C₄, B : C₃ ⥤ C₄ are functors, then [CatCommSq T L R B] contains the datum of an isomorphism T ⋙ R ≅ L ⋙ B.

Future work: using this notion in the development of the localization of categories (e.g. localization of adjunctions).

theorem CategoryTheory.CatCommSq.ext_iff {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} :
∀ {inst : CategoryTheory.Category.{u_7, u_1} C₁} {inst_1 : CategoryTheory.Category.{u_8, u_2} C₂} {inst_2 : CategoryTheory.Category.{u_9, u_3} C₃} {inst_3 : CategoryTheory.Category.{u_10, u_4} C₄} {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃} {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} {x y : CategoryTheory.CatCommSq T L R B}, x = y CategoryTheory.CatCommSq.iso' = CategoryTheory.CatCommSq.iso'
theorem CategoryTheory.CatCommSq.ext {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} :
∀ {inst : CategoryTheory.Category.{u_7, u_1} C₁} {inst_1 : CategoryTheory.Category.{u_8, u_2} C₂} {inst_2 : CategoryTheory.Category.{u_9, u_3} C₃} {inst_3 : CategoryTheory.Category.{u_10, u_4} C₄} {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃} {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} {x y : CategoryTheory.CatCommSq T L R B}, CategoryTheory.CatCommSq.iso' = CategoryTheory.CatCommSq.iso'x = y

CatCommSq T L R B expresses that there is a 2-commutative square of functors, where the functors T, L, R and B are respectively the left, top, right and bottom functors of the square.

  • iso' : T.comp R L.comp B

    the isomorphism corresponding to a 2-commutative diagram

Instances

    Assuming [CatCommSq T L R B], iso T L R B is the isomorphism T ⋙ R ≅ L ⋙ B given by the 2-commutative square.

    Equations
    Instances For
      @[simp]
      theorem CategoryTheory.CatCommSq.hComp_iso'_hom_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₅ : Type u_5} {C₆ : Type u_6} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} C₃] [CategoryTheory.Category.{u_10, u_4} C₄] [CategoryTheory.Category.{u_11, u_5} C₅] [CategoryTheory.Category.{u_12, u_6} C₆] (T₁ : CategoryTheory.Functor C₁ C₂) (T₂ : CategoryTheory.Functor C₂ C₃) (V₁ : CategoryTheory.Functor C₁ C₄) (V₂ : CategoryTheory.Functor C₂ C₅) (V₃ : CategoryTheory.Functor C₃ C₆) (B₁ : CategoryTheory.Functor C₄ C₅) (B₂ : CategoryTheory.Functor C₅ C₆) [CategoryTheory.CatCommSq T₁ V₁ V₂ B₁] [CategoryTheory.CatCommSq T₂ V₂ V₃ B₂] (X : C₁) :
      CategoryTheory.CatCommSq.iso'.hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso T₂ V₂ V₃ B₂).hom.app (T₁.obj X)) (B₂.map ((CategoryTheory.CatCommSq.iso T₁ V₁ V₂ B₁).hom.app X))
      @[simp]
      theorem CategoryTheory.CatCommSq.hComp_iso'_inv_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₅ : Type u_5} {C₆ : Type u_6} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} C₃] [CategoryTheory.Category.{u_10, u_4} C₄] [CategoryTheory.Category.{u_11, u_5} C₅] [CategoryTheory.Category.{u_12, u_6} C₆] (T₁ : CategoryTheory.Functor C₁ C₂) (T₂ : CategoryTheory.Functor C₂ C₃) (V₁ : CategoryTheory.Functor C₁ C₄) (V₂ : CategoryTheory.Functor C₂ C₅) (V₃ : CategoryTheory.Functor C₃ C₆) (B₁ : CategoryTheory.Functor C₄ C₅) (B₂ : CategoryTheory.Functor C₅ C₆) [CategoryTheory.CatCommSq T₁ V₁ V₂ B₁] [CategoryTheory.CatCommSq T₂ V₂ V₃ B₂] (X : C₁) :
      CategoryTheory.CatCommSq.iso'.inv.app X = CategoryTheory.CategoryStruct.comp (B₂.map ((CategoryTheory.CatCommSq.iso T₁ V₁ V₂ B₁).inv.app X)) ((CategoryTheory.CatCommSq.iso T₂ V₂ V₃ B₂).inv.app (T₁.obj X))
      def CategoryTheory.CatCommSq.hComp {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₅ : Type u_5} {C₆ : Type u_6} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} C₃] [CategoryTheory.Category.{u_10, u_4} C₄] [CategoryTheory.Category.{u_11, u_5} C₅] [CategoryTheory.Category.{u_12, u_6} C₆] (T₁ : CategoryTheory.Functor C₁ C₂) (T₂ : CategoryTheory.Functor C₂ C₃) (V₁ : CategoryTheory.Functor C₁ C₄) (V₂ : CategoryTheory.Functor C₂ C₅) (V₃ : CategoryTheory.Functor C₃ C₆) (B₁ : CategoryTheory.Functor C₄ C₅) (B₂ : CategoryTheory.Functor C₅ C₆) [CategoryTheory.CatCommSq T₁ V₁ V₂ B₁] [CategoryTheory.CatCommSq T₂ V₂ V₃ B₂] :
      CategoryTheory.CatCommSq (T₁.comp T₂) V₁ V₃ (B₁.comp B₂)

      Horizontal composition of 2-commutative squares

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem CategoryTheory.CatCommSq.vComp_iso'_hom_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₅ : Type u_5} {C₆ : Type u_6} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} C₃] [CategoryTheory.Category.{u_10, u_4} C₄] [CategoryTheory.Category.{u_11, u_5} C₅] [CategoryTheory.Category.{u_12, u_6} C₆] (L₁ : CategoryTheory.Functor C₁ C₂) (L₂ : CategoryTheory.Functor C₂ C₃) (H₁ : CategoryTheory.Functor C₁ C₄) (H₂ : CategoryTheory.Functor C₂ C₅) (H₃ : CategoryTheory.Functor C₃ C₆) (R₁ : CategoryTheory.Functor C₄ C₅) (R₂ : CategoryTheory.Functor C₅ C₆) [CategoryTheory.CatCommSq H₁ L₁ R₁ H₂] [CategoryTheory.CatCommSq H₂ L₂ R₂ H₃] (X : C₁) :
        CategoryTheory.CatCommSq.iso'.hom.app X = CategoryTheory.CategoryStruct.comp (R₂.map ((CategoryTheory.CatCommSq.iso H₁ L₁ R₁ H₂).hom.app X)) ((CategoryTheory.CatCommSq.iso H₂ L₂ R₂ H₃).hom.app (L₁.obj X))
        @[simp]
        theorem CategoryTheory.CatCommSq.vComp_iso'_inv_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₅ : Type u_5} {C₆ : Type u_6} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} C₃] [CategoryTheory.Category.{u_10, u_4} C₄] [CategoryTheory.Category.{u_11, u_5} C₅] [CategoryTheory.Category.{u_12, u_6} C₆] (L₁ : CategoryTheory.Functor C₁ C₂) (L₂ : CategoryTheory.Functor C₂ C₃) (H₁ : CategoryTheory.Functor C₁ C₄) (H₂ : CategoryTheory.Functor C₂ C₅) (H₃ : CategoryTheory.Functor C₃ C₆) (R₁ : CategoryTheory.Functor C₄ C₅) (R₂ : CategoryTheory.Functor C₅ C₆) [CategoryTheory.CatCommSq H₁ L₁ R₁ H₂] [CategoryTheory.CatCommSq H₂ L₂ R₂ H₃] (X : C₁) :
        CategoryTheory.CatCommSq.iso'.inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.CatCommSq.iso H₂ L₂ R₂ H₃).inv.app (L₁.obj X)) (R₂.map ((CategoryTheory.CatCommSq.iso H₁ L₁ R₁ H₂).inv.app X))
        def CategoryTheory.CatCommSq.vComp {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {C₅ : Type u_5} {C₆ : Type u_6} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} C₃] [CategoryTheory.Category.{u_10, u_4} C₄] [CategoryTheory.Category.{u_11, u_5} C₅] [CategoryTheory.Category.{u_12, u_6} C₆] (L₁ : CategoryTheory.Functor C₁ C₂) (L₂ : CategoryTheory.Functor C₂ C₃) (H₁ : CategoryTheory.Functor C₁ C₄) (H₂ : CategoryTheory.Functor C₂ C₅) (H₃ : CategoryTheory.Functor C₃ C₆) (R₁ : CategoryTheory.Functor C₄ C₅) (R₂ : CategoryTheory.Functor C₅ C₆) [CategoryTheory.CatCommSq H₁ L₁ R₁ H₂] [CategoryTheory.CatCommSq H₂ L₂ R₂ H₃] :
        CategoryTheory.CatCommSq H₁ (L₁.comp L₂) (R₁.comp R₂) H₃

        Vertical composition of 2-commutative squares

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[simp]
          theorem CategoryTheory.CatCommSq.hInv_iso'_hom_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} C₃] [CategoryTheory.Category.{u_10, u_4} C₄] (T : C₁ C₂) (L : CategoryTheory.Functor C₁ C₃) (R : CategoryTheory.Functor C₂ C₄) (B : C₃ C₄) :
          ∀ (x : CategoryTheory.CatCommSq T.functor L R B.functor) (X : C₂), CategoryTheory.CatCommSq.iso'.hom.app X = CategoryTheory.CategoryStruct.comp (B.unitIso.hom.app (L.obj (T.inverse.obj X))) (CategoryTheory.CategoryStruct.comp (B.inverse.map ((CategoryTheory.CatCommSq.iso T.functor L R B.functor).inv.app (T.inverse.obj X))) (B.inverse.map (R.map (T.counitIso.hom.app X))))
          @[simp]
          theorem CategoryTheory.CatCommSq.hInv_iso'_inv_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} C₃] [CategoryTheory.Category.{u_10, u_4} C₄] (T : C₁ C₂) (L : CategoryTheory.Functor C₁ C₃) (R : CategoryTheory.Functor C₂ C₄) (B : C₃ C₄) :
          ∀ (x : CategoryTheory.CatCommSq T.functor L R B.functor) (X : C₂), CategoryTheory.CatCommSq.iso'.inv.app X = CategoryTheory.CategoryStruct.comp (B.inverse.map (R.map (T.counitIso.inv.app X))) (CategoryTheory.CategoryStruct.comp (B.inverse.map ((CategoryTheory.CatCommSq.iso T.functor L R B.functor).hom.app (T.inverse.obj X))) (B.unitIso.inv.app (L.obj (T.inverse.obj X))))
          def CategoryTheory.CatCommSq.hInv {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} C₃] [CategoryTheory.Category.{u_10, u_4} C₄] (T : C₁ C₂) (L : CategoryTheory.Functor C₁ C₃) (R : CategoryTheory.Functor C₂ C₄) (B : C₃ C₄) :
          CategoryTheory.CatCommSq T.functor L R B.functorCategoryTheory.CatCommSq T.inverse R L B.inverse

          Horizontal inverse of a 2-commutative square

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            theorem CategoryTheory.CatCommSq.hInv_hInv {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_3} C₃] [CategoryTheory.Category.{u_7, u_4} C₄] (T : C₁ C₂) (L : CategoryTheory.Functor C₁ C₃) (R : CategoryTheory.Functor C₂ C₄) (B : C₃ C₄) (h : CategoryTheory.CatCommSq T.functor L R B.functor) :
            def CategoryTheory.CatCommSq.hInvEquiv {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} C₃] [CategoryTheory.Category.{u_10, u_4} C₄] (T : C₁ C₂) (L : CategoryTheory.Functor C₁ C₃) (R : CategoryTheory.Functor C₂ C₄) (B : C₃ C₄) :
            CategoryTheory.CatCommSq T.functor L R B.functor CategoryTheory.CatCommSq T.inverse R L B.inverse

            In a square of categories, when the top and bottom functors are part of equivalence of categories, it is equivalent to show 2-commutativity for the functors of these equivalences or for their inverses.

            Equations
            Instances For
              @[simp]
              theorem CategoryTheory.CatCommSq.vInv_iso'_hom_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} C₃] [CategoryTheory.Category.{u_10, u_4} C₄] (T : CategoryTheory.Functor C₁ C₂) (L : C₁ C₃) (R : C₂ C₄) (B : CategoryTheory.Functor C₃ C₄) :
              ∀ (x : CategoryTheory.CatCommSq T L.functor R.functor B) (X : C₃), CategoryTheory.CatCommSq.iso'.hom.app X = CategoryTheory.CategoryStruct.comp (R.inverse.map (B.map (L.counitIso.inv.app X))) (CategoryTheory.CategoryStruct.comp (R.inverse.map ((CategoryTheory.CatCommSq.iso T L.functor R.functor B).inv.app (L.inverse.obj X))) (R.unitIso.inv.app (T.obj (L.inverse.obj X))))
              @[simp]
              theorem CategoryTheory.CatCommSq.vInv_iso'_inv_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} C₃] [CategoryTheory.Category.{u_10, u_4} C₄] (T : CategoryTheory.Functor C₁ C₂) (L : C₁ C₃) (R : C₂ C₄) (B : CategoryTheory.Functor C₃ C₄) :
              ∀ (x : CategoryTheory.CatCommSq T L.functor R.functor B) (X : C₃), CategoryTheory.CatCommSq.iso'.inv.app X = CategoryTheory.CategoryStruct.comp (R.unitIso.hom.app (T.obj (L.inverse.obj X))) (CategoryTheory.CategoryStruct.comp (R.inverse.map ((CategoryTheory.CatCommSq.iso T L.functor R.functor B).hom.app (L.inverse.obj X))) (R.inverse.map (B.map (L.counitIso.hom.app X))))
              def CategoryTheory.CatCommSq.vInv {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} C₃] [CategoryTheory.Category.{u_10, u_4} C₄] (T : CategoryTheory.Functor C₁ C₂) (L : C₁ C₃) (R : C₂ C₄) (B : CategoryTheory.Functor C₃ C₄) :
              CategoryTheory.CatCommSq T L.functor R.functor BCategoryTheory.CatCommSq B L.inverse R.inverse T

              Vertical inverse of a 2-commutative square

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem CategoryTheory.CatCommSq.vInv_vInv {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_8, u_1} C₁] [CategoryTheory.Category.{u_9, u_2} C₂] [CategoryTheory.Category.{u_10, u_3} C₃] [CategoryTheory.Category.{u_7, u_4} C₄] (T : CategoryTheory.Functor C₁ C₂) (L : C₁ C₃) (R : C₂ C₄) (B : CategoryTheory.Functor C₃ C₄) (h : CategoryTheory.CatCommSq T L.functor R.functor B) :
                def CategoryTheory.CatCommSq.vInvEquiv {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [CategoryTheory.Category.{u_7, u_1} C₁] [CategoryTheory.Category.{u_8, u_2} C₂] [CategoryTheory.Category.{u_9, u_3} C₃] [CategoryTheory.Category.{u_10, u_4} C₄] (T : CategoryTheory.Functor C₁ C₂) (L : C₁ C₃) (R : C₂ C₄) (B : CategoryTheory.Functor C₃ C₄) :
                CategoryTheory.CatCommSq T L.functor R.functor B CategoryTheory.CatCommSq B L.inverse R.inverse T

                In a square of categories, when the left and right functors are part of equivalence of categories, it is equivalent to show 2-commutativity for the functors of these equivalences or for their inverses.

                Equations
                Instances For