# 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 : } {inst_1 : } {inst_2 : } {inst_3 : } {T : } {L : } {R : } {B : } (x y : ), 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 : } {inst_1 : } {inst_2 : } {inst_3 : } {T : } {L : } {R : } {B : } (x y : ), CategoryTheory.CatCommSq.iso' = CategoryTheory.CatCommSq.iso'x = y
class CategoryTheory.CatCommSq {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [] [] [] [] (T : ) (L : ) (R : ) (B : ) :
Type (max u_1 u_10)
• iso' :

the isomorphism corresponding to a 2-commutative diagram

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.

Instances
def CategoryTheory.CatCommSq.iso {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [] [] [] [] (T : ) (L : ) (R : ) (B : ) [h : ] :

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

Instances For
@[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} [] [] [] [] [] [] (T₁ : ) (T₂ : ) (V₁ : ) (V₂ : ) (V₃ : ) (B₁ : ) (B₂ : ) [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))
@[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} [] [] [] [] [] [] (T₁ : ) (T₂ : ) (V₁ : ) (V₂ : ) (V₃ : ) (B₁ : ) (B₂ : ) [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))
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} [] [] [] [] [] [] (T₁ : ) (T₂ : ) (V₁ : ) (V₂ : ) (V₃ : ) (B₁ : ) (B₂ : ) [CategoryTheory.CatCommSq T₁ V₁ V₂ B₁] [CategoryTheory.CatCommSq T₂ V₂ V₃ B₂] :
CategoryTheory.CatCommSq () V₁ V₃ ()

Horizontal composition of 2-commutative squares

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} [] [] [] [] [] [] (L₁ : ) (L₂ : ) (H₁ : ) (H₂ : ) (H₃ : ) (R₁ : ) (R₂ : ) [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} [] [] [] [] [] [] (L₁ : ) (L₂ : ) (H₁ : ) (H₂ : ) (H₃ : ) (R₁ : ) (R₂ : ) [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} [] [] [] [] [] [] (L₁ : ) (L₂ : ) (H₁ : ) (H₂ : ) (H₃ : ) (R₁ : ) (R₂ : ) [CategoryTheory.CatCommSq H₁ L₁ R₁ H₂] [CategoryTheory.CatCommSq H₂ L₂ R₂ H₃] :
CategoryTheory.CatCommSq H₁ () () H₃

Vertical composition of 2-commutative squares

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} [] [] [] [] (T : C₁ C₂) (L : ) (R : ) (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} [] [] [] [] (T : C₁ C₂) (L : ) (R : ) (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} [] [] [] [] (T : C₁ C₂) (L : ) (R : ) (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

Instances For
theorem CategoryTheory.CatCommSq.hInv_hInv {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [] [] [] [] (T : C₁ C₂) (L : ) (R : ) (B : C₃ C₄) (h : CategoryTheory.CatCommSq T.functor L R B.functor) :
CategoryTheory.CatCommSq.hInv T.symm R L B.symm () = h
def CategoryTheory.CatCommSq.hInvEquiv {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [] [] [] [] (T : C₁ C₂) (L : ) (R : ) (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 categorires, it is equivalent to show 2-commutativity for the functors of these equivalences or for their inverses.

Instances For
instance CategoryTheory.CatCommSq.hInv' {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} [] [] [] [] (T : ) (L : ) (R : ) (B : ) [h : ] :