Vertical composition of Guitart exact squares

In this file, we show that the vertical composition of Guitart exact squares is Guitart exact.

def CategoryTheory.TwoSquare.whiskerVertical {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] {T : Functor C₁ D₁} {L : Functor C₁ C₂} {R : Functor D₁ D₂} {B : Functor C₂ D₂} (w : TwoSquare T L R B) {L' : Functor C₁ C₂} {R' : Functor D₁ D₂} (α : L ⟶ L') (β : R' ⟶ R) : TwoSquare T L' R' B

Given w : TwoSquare T L R B, one may obtain a 2-square TwoSquare T L' R' B if we provide natural transformations α : L ⟶ L' and β : R' ⟶ R.

@[simp]

theorem CategoryTheory.TwoSquare.whiskerVertical_app {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] {T : Functor C₁ D₁} {L : Functor C₁ C₂} {R : Functor D₁ D₂} {B : Functor C₂ D₂} (w : TwoSquare T L R B) {L' : Functor C₁ C₂} {R' : Functor D₁ D₂} (α : L ⟶ L') (β : R' ⟶ R) (X : C₁) : (w.whiskerVertical α β).app X = CategoryStruct.comp (β.app (T.obj X)) (CategoryStruct.comp (w.natTrans.app X) (B.map (α.app X)))

theorem CategoryTheory.TwoSquare.GuitartExact.whiskerVertical {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] {T : Functor C₁ D₁} {L : Functor C₁ C₂} {R : Functor D₁ D₂} {B : Functor C₂ D₂} (w : TwoSquare T L R B) {L' : Functor C₁ C₂} {R' : Functor D₁ D₂} [w.GuitartExact] (α : L ≅ L') (β : R ≅ R') : (w.whiskerVertical α.hom β.inv).GuitartExact

A 2-square stays Guitart exact if we replace the left and right functors by isomorphic functors. See also whiskerVertical_iff.

@[simp]

theorem CategoryTheory.TwoSquare.GuitartExact.whiskerVertical_iff {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] {T : Functor C₁ D₁} {L : Functor C₁ C₂} {R : Functor D₁ D₂} {B : Functor C₂ D₂} (w : TwoSquare T L R B) {L' : Functor C₁ C₂} {R' : Functor D₁ D₂} (α : L ≅ L') (β : R ≅ R') : (w.whiskerVertical α.hom β.inv).GuitartExact ↔ w.GuitartExact

A 2-square is Guitart exact iff it is so after replacing the left and right functors by isomorphic functors.

instance CategoryTheory.TwoSquare.GuitartExact.instWhiskerVerticalOfIsIsoFunctor {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_4} {D₂ : Type u_5} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] {T : Functor C₁ D₁} {L : Functor C₁ C₂} {R : Functor D₁ D₂} {B : Functor C₂ D₂} (w : TwoSquare T L R B) {L' : Functor C₁ C₂} {R' : Functor D₁ D₂} [w.GuitartExact] (α : L ⟶ L') (β : R' ⟶ R) [IsIso α] [IsIso β] : (w.whiskerVertical α β).GuitartExact

def CategoryTheory.TwoSquare.structuredArrowDownwardsComp {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] {H₁ : Functor C₁ D₁} {L₁ : Functor C₁ C₂} {R₁ : Functor D₁ D₂} {H₂ : Functor C₂ D₂} (w : TwoSquare H₁ L₁ R₁ H₂) {L₂ : Functor C₂ C₃} {R₂ : Functor D₂ D₃} {H₃ : Functor C₃ D₃} (w' : TwoSquare H₂ L₂ R₂ H₃) (Y₁ : D₁) : (w.structuredArrowDownwards Y₁).comp (w'.structuredArrowDownwards (R₁.obj Y₁)) ≅ (w.vComp w').structuredArrowDownwards Y₁

The canonical isomorphism between w.structuredArrowDownwards Y₁ ⋙ w'.structuredArrowDownwards (R₁.obj Y₁) and (w ≫ᵥ w').structuredArrowDownwards Y₁.

def CategoryTheory.TwoSquare.vComp' {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] {H₁ : Functor C₁ D₁} {L₁ : Functor C₁ C₂} {R₁ : Functor D₁ D₂} {H₂ : Functor C₂ D₂} (w : TwoSquare H₁ L₁ R₁ H₂) {L₂ : Functor C₂ C₃} {R₂ : Functor D₂ D₃} {H₃ : Functor C₃ D₃} (w' : TwoSquare H₂ L₂ R₂ H₃) {L₁₂ : Functor C₁ C₃} {R₁₂ : Functor D₁ D₃} (eL : L₁.comp L₂ ≅ L₁₂) (eR : R₁.comp R₂ ≅ R₁₂) : TwoSquare H₁ L₁₂ R₁₂ H₃

The vertical composition of 2-squares. (Variant where we allow the replacement of the vertical compositions by isomorphic functors.)

@[simp]

theorem CategoryTheory.TwoSquare.vComp'_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] {H₁ : Functor C₁ D₁} {L₁ : Functor C₁ C₂} {R₁ : Functor D₁ D₂} {H₂ : Functor C₂ D₂} (w : TwoSquare H₁ L₁ R₁ H₂) {L₂ : Functor C₂ C₃} {R₂ : Functor D₂ D₃} {H₃ : Functor C₃ D₃} (w' : TwoSquare H₂ L₂ R₂ H₃) {L₁₂ : Functor C₁ C₃} {R₁₂ : Functor D₁ D₃} (eL : L₁.comp L₂ ≅ L₁₂) (eR : R₁.comp R₂ ≅ R₁₂) (X : C₁) : (w.vComp' w' eL eR).app X = CategoryStruct.comp (eR.inv.app (H₁.obj X)) (CategoryStruct.comp (R₂.map (w.natTrans.app X)) (CategoryStruct.comp (w'.natTrans.app (L₁.obj X)) (H₃.map (eL.hom.app X))))

instance CategoryTheory.TwoSquare.GuitartExact.vComp {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] {H₁ : Functor C₁ D₁} {L₁ : Functor C₁ C₂} {R₁ : Functor D₁ D₂} {H₂ : Functor C₂ D₂} (w : TwoSquare H₁ L₁ R₁ H₂) {L₂ : Functor C₂ C₃} {R₂ : Functor D₂ D₃} {H₃ : Functor C₃ D₃} (w' : TwoSquare H₂ L₂ R₂ H₃) [hw : w.GuitartExact] [hw' : w'.GuitartExact] : (w.vComp w').GuitartExact

instance CategoryTheory.TwoSquare.GuitartExact.vComp' {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] {H₁ : Functor C₁ D₁} {L₁ : Functor C₁ C₂} {R₁ : Functor D₁ D₂} {H₂ : Functor C₂ D₂} (w : TwoSquare H₁ L₁ R₁ H₂) {L₂ : Functor C₂ C₃} {R₂ : Functor D₂ D₃} {H₃ : Functor C₃ D₃} (w' : TwoSquare H₂ L₂ R₂ H₃) [w.GuitartExact] [w'.GuitartExact] {L₁₂ : Functor C₁ C₃} {R₁₂ : Functor D₁ D₃} (eL : L₁.comp L₂ ≅ L₁₂) (eR : R₁.comp R₂ ≅ R₁₂) : (w.vComp' w' eL eR).GuitartExact

theorem CategoryTheory.TwoSquare.GuitartExact.vComp_iff_of_equivalences {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] {H₁ : Functor C₁ D₁} {L₁ : Functor C₁ C₂} {R₁ : Functor D₁ D₂} {H₂ : Functor C₂ D₂} (w : TwoSquare H₁ L₁ R₁ H₂) {H₃ : Functor C₃ D₃} (eL : C₂ ≌ C₃) (eR : D₂ ≌ D₃) (w' : H₂.comp eR.functor ≅ eL.functor.comp H₃) : (w.vComp w'.hom).GuitartExact ↔ w.GuitartExact

theorem CategoryTheory.TwoSquare.GuitartExact.vComp'_iff_of_equivalences {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] {H₁ : Functor C₁ D₁} {L₁ : Functor C₁ C₂} {R₁ : Functor D₁ D₂} {H₂ : Functor C₂ D₂} (w : TwoSquare H₁ L₁ R₁ H₂) {H₃ : Functor C₃ D₃} (E : C₂ ≌ C₃) (E' : D₂ ≌ D₃) (w' : H₂.comp E'.functor ≅ E.functor.comp H₃) {L₁₂ : Functor C₁ C₃} {R₁₂ : Functor D₁ D₃} (eL : L₁.comp E.functor ≅ L₁₂) (eR : R₁.comp E'.functor ≅ R₁₂) : (w.vComp' w'.hom eL eR).GuitartExact ↔ w.GuitartExact