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}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_4} D₁]
[CategoryTheory.Category.{u_10, u_5} D₂]
{T : CategoryTheory.Functor C₁ D₁}
{L : CategoryTheory.Functor C₁ C₂}
{R : CategoryTheory.Functor D₁ D₂}
{B : CategoryTheory.Functor C₂ D₂}
(w : CategoryTheory.TwoSquare T L R B)
{L' : CategoryTheory.Functor C₁ C₂}
{R' : CategoryTheory.Functor D₁ D₂}
(α : L ⟶ L')
(β : R' ⟶ R)
:
CategoryTheory.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.
Equations
- w.whiskerVertical α β = CategoryTheory.CategoryStruct.comp (CategoryTheory.whiskerLeft T β) (CategoryTheory.CategoryStruct.comp w (CategoryTheory.whiskerRight α B))
Instances For
@[simp]
theorem
CategoryTheory.TwoSquare.whiskerVertical_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_4}
{D₂ : Type u_5}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_8, u_2} C₂]
[CategoryTheory.Category.{u_9, u_4} D₁]
[CategoryTheory.Category.{u_10, u_5} D₂]
{T : CategoryTheory.Functor C₁ D₁}
{L : CategoryTheory.Functor C₁ C₂}
{R : CategoryTheory.Functor D₁ D₂}
{B : CategoryTheory.Functor C₂ D₂}
(w : CategoryTheory.TwoSquare T L R B)
{L' : CategoryTheory.Functor C₁ C₂}
{R' : CategoryTheory.Functor D₁ D₂}
(α : L ⟶ L')
(β : R' ⟶ R)
(X : C₁)
:
(w.whiskerVertical α β).app X = CategoryTheory.CategoryStruct.comp (β.app (T.obj X)) (CategoryTheory.CategoryStruct.comp (w.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}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_9, u_2} C₂]
[CategoryTheory.Category.{u_8, u_4} D₁]
[CategoryTheory.Category.{u_10, u_5} D₂]
{T : CategoryTheory.Functor C₁ D₁}
{L : CategoryTheory.Functor C₁ C₂}
{R : CategoryTheory.Functor D₁ D₂}
{B : CategoryTheory.Functor C₂ D₂}
(w : CategoryTheory.TwoSquare T L R B)
{L' : CategoryTheory.Functor C₁ C₂}
{R' : CategoryTheory.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}
[CategoryTheory.Category.{u_8, u_1} C₁]
[CategoryTheory.Category.{u_7, u_2} C₂]
[CategoryTheory.Category.{u_10, u_4} D₁]
[CategoryTheory.Category.{u_9, u_5} D₂]
{T : CategoryTheory.Functor C₁ D₁}
{L : CategoryTheory.Functor C₁ C₂}
{R : CategoryTheory.Functor D₁ D₂}
{B : CategoryTheory.Functor C₂ D₂}
(w : CategoryTheory.TwoSquare T L R B)
{L' : CategoryTheory.Functor C₁ C₂}
{R' : CategoryTheory.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}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_9, u_2} C₂]
[CategoryTheory.Category.{u_8, u_4} D₁]
[CategoryTheory.Category.{u_10, u_5} D₂]
{T : CategoryTheory.Functor C₁ D₁}
{L : CategoryTheory.Functor C₁ C₂}
{R : CategoryTheory.Functor D₁ D₂}
{B : CategoryTheory.Functor C₂ D₂}
(w : CategoryTheory.TwoSquare T L R B)
{L' : CategoryTheory.Functor C₁ C₂}
{R' : CategoryTheory.Functor D₁ D₂}
[w.GuitartExact]
(α : L ⟶ L')
(β : R' ⟶ R)
[CategoryTheory.IsIso α]
[CategoryTheory.IsIso β]
:
(w.whiskerVertical α β).GuitartExact
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}
[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} D₁]
[CategoryTheory.Category.{u_11, u_5} D₂]
[CategoryTheory.Category.{u_12, u_6} D₃]
{H₁ : CategoryTheory.Functor C₁ D₁}
{L₁ : CategoryTheory.Functor C₁ C₂}
{R₁ : CategoryTheory.Functor D₁ D₂}
{H₂ : CategoryTheory.Functor C₂ D₂}
(w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂)
{L₂ : CategoryTheory.Functor C₂ C₃}
{R₂ : CategoryTheory.Functor D₂ D₃}
{H₃ : CategoryTheory.Functor C₃ D₃}
(w' : CategoryTheory.TwoSquare H₂ L₂ R₂ H₃)
:
CategoryTheory.TwoSquare H₁ (L₁.comp L₂) (R₁.comp R₂) H₃
The vertical composition of 2-squares.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[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}
[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} D₁]
[CategoryTheory.Category.{u_11, u_5} D₂]
[CategoryTheory.Category.{u_12, u_6} D₃]
{H₁ : CategoryTheory.Functor C₁ D₁}
{L₁ : CategoryTheory.Functor C₁ C₂}
{R₁ : CategoryTheory.Functor D₁ D₂}
{H₂ : CategoryTheory.Functor C₂ D₂}
(w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂)
{L₂ : CategoryTheory.Functor C₂ C₃}
{R₂ : CategoryTheory.Functor D₂ D₃}
{H₃ : CategoryTheory.Functor C₃ D₃}
(w' : CategoryTheory.TwoSquare H₂ L₂ R₂ H₃)
(X : C₁)
:
(w.vComp w').app X = CategoryTheory.CategoryStruct.comp (R₂.map (w.app X)) (w'.app (L₁.obj X))
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}
[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} D₁]
[CategoryTheory.Category.{u_11, u_5} D₂]
[CategoryTheory.Category.{u_12, u_6} D₃]
{H₁ : CategoryTheory.Functor C₁ D₁}
{L₁ : CategoryTheory.Functor C₁ C₂}
{R₁ : CategoryTheory.Functor D₁ D₂}
{H₂ : CategoryTheory.Functor C₂ D₂}
(w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂)
{L₂ : CategoryTheory.Functor C₂ C₃}
{R₂ : CategoryTheory.Functor D₂ D₃}
{H₃ : CategoryTheory.Functor C₃ D₃}
(w' : CategoryTheory.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.vComp w').structuredArrowDownwards Y₁.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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}
[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} D₁]
[CategoryTheory.Category.{u_11, u_5} D₂]
[CategoryTheory.Category.{u_12, u_6} D₃]
{H₁ : CategoryTheory.Functor C₁ D₁}
{L₁ : CategoryTheory.Functor C₁ C₂}
{R₁ : CategoryTheory.Functor D₁ D₂}
{H₂ : CategoryTheory.Functor C₂ D₂}
(w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂)
{L₂ : CategoryTheory.Functor C₂ C₃}
{R₂ : CategoryTheory.Functor D₂ D₃}
{H₃ : CategoryTheory.Functor C₃ D₃}
(w' : CategoryTheory.TwoSquare H₂ L₂ R₂ H₃)
{L₁₂ : CategoryTheory.Functor C₁ C₃}
{R₁₂ : CategoryTheory.Functor D₁ D₃}
(eL : L₁.comp L₂ ≅ L₁₂)
(eR : R₁.comp R₂ ≅ R₁₂)
:
CategoryTheory.TwoSquare H₁ L₁₂ R₁₂ H₃
The vertical composition of 2-squares. (Variant where we allow the replacement of the vertical compositions by isomorphic functors.)
Equations
- w.vComp' w' eL eR = (w.vComp w').whiskerVertical eL.hom eR.inv
Instances For
@[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}
[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} D₁]
[CategoryTheory.Category.{u_11, u_5} D₂]
[CategoryTheory.Category.{u_12, u_6} D₃]
{H₁ : CategoryTheory.Functor C₁ D₁}
{L₁ : CategoryTheory.Functor C₁ C₂}
{R₁ : CategoryTheory.Functor D₁ D₂}
{H₂ : CategoryTheory.Functor C₂ D₂}
(w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂)
{L₂ : CategoryTheory.Functor C₂ C₃}
{R₂ : CategoryTheory.Functor D₂ D₃}
{H₃ : CategoryTheory.Functor C₃ D₃}
(w' : CategoryTheory.TwoSquare H₂ L₂ R₂ H₃)
{L₁₂ : CategoryTheory.Functor C₁ C₃}
{R₁₂ : CategoryTheory.Functor D₁ D₃}
(eL : L₁.comp L₂ ≅ L₁₂)
(eR : R₁.comp R₂ ≅ R₁₂)
(X : C₁)
:
(w.vComp' w' eL eR).app X = CategoryTheory.CategoryStruct.comp (eR.inv.app (H₁.obj X))
(CategoryTheory.CategoryStruct.comp (R₂.map (w.app X))
(CategoryTheory.CategoryStruct.comp (w'.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}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_9, u_2} C₂]
[CategoryTheory.Category.{u_11, u_3} C₃]
[CategoryTheory.Category.{u_8, u_4} D₁]
[CategoryTheory.Category.{u_10, u_5} D₂]
[CategoryTheory.Category.{u_12, u_6} D₃]
{H₁ : CategoryTheory.Functor C₁ D₁}
{L₁ : CategoryTheory.Functor C₁ C₂}
{R₁ : CategoryTheory.Functor D₁ D₂}
{H₂ : CategoryTheory.Functor C₂ D₂}
(w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂)
{L₂ : CategoryTheory.Functor C₂ C₃}
{R₂ : CategoryTheory.Functor D₂ D₃}
{H₃ : CategoryTheory.Functor C₃ D₃}
(w' : CategoryTheory.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}
[CategoryTheory.Category.{u_7, u_1} C₁]
[CategoryTheory.Category.{u_9, u_2} C₂]
[CategoryTheory.Category.{u_11, u_3} C₃]
[CategoryTheory.Category.{u_8, u_4} D₁]
[CategoryTheory.Category.{u_10, u_5} D₂]
[CategoryTheory.Category.{u_12, u_6} D₃]
{H₁ : CategoryTheory.Functor C₁ D₁}
{L₁ : CategoryTheory.Functor C₁ C₂}
{R₁ : CategoryTheory.Functor D₁ D₂}
{H₂ : CategoryTheory.Functor C₂ D₂}
(w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂)
{L₂ : CategoryTheory.Functor C₂ C₃}
{R₂ : CategoryTheory.Functor D₂ D₃}
{H₃ : CategoryTheory.Functor C₃ D₃}
(w' : CategoryTheory.TwoSquare H₂ L₂ R₂ H₃)
[w.GuitartExact]
[w'.GuitartExact]
{L₁₂ : CategoryTheory.Functor C₁ C₃}
{R₁₂ : CategoryTheory.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}
[CategoryTheory.Category.{u_11, u_1} C₁]
[CategoryTheory.Category.{u_7, u_2} C₂]
[CategoryTheory.Category.{u_8, u_3} C₃]
[CategoryTheory.Category.{u_12, u_4} D₁]
[CategoryTheory.Category.{u_9, u_5} D₂]
[CategoryTheory.Category.{u_10, u_6} D₃]
{H₁ : CategoryTheory.Functor C₁ D₁}
{L₁ : CategoryTheory.Functor C₁ C₂}
{R₁ : CategoryTheory.Functor D₁ D₂}
{H₂ : CategoryTheory.Functor C₂ D₂}
(w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂)
{H₃ : CategoryTheory.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}
[CategoryTheory.Category.{u_11, u_1} C₁]
[CategoryTheory.Category.{u_7, u_2} C₂]
[CategoryTheory.Category.{u_8, u_3} C₃]
[CategoryTheory.Category.{u_12, u_4} D₁]
[CategoryTheory.Category.{u_9, u_5} D₂]
[CategoryTheory.Category.{u_10, u_6} D₃]
{H₁ : CategoryTheory.Functor C₁ D₁}
{L₁ : CategoryTheory.Functor C₁ C₂}
{R₁ : CategoryTheory.Functor D₁ D₂}
{H₂ : CategoryTheory.Functor C₂ D₂}
(w : CategoryTheory.TwoSquare H₁ L₁ R₁ H₂)
{H₃ : CategoryTheory.Functor C₃ D₃}
(E : C₂ ≌ C₃)
(E' : D₂ ≌ D₃)
(w' : H₂.comp E'.functor ≅ E.functor.comp H₃)
{L₁₂ : CategoryTheory.Functor C₁ C₃}
{R₁₂ : CategoryTheory.Functor D₁ D₃}
(eL : L₁.comp E.functor ≅ L₁₂)
(eR : R₁.comp E'.functor ≅ R₁₂)
:
(w.vComp' w'.hom eL eR).GuitartExact ↔ w.GuitartExact