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.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_4} D₁]
[Category.{u_10, 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.
Equations
- w.whiskerVertical α β = (w.whiskerLeft α).whiskerRight β
Instances For
@[simp]
theorem
CategoryTheory.TwoSquare.whiskerVertical_app
{C₁ : Type u_1}
{C₂ : Type u_2}
{D₁ : Type u_4}
{D₂ : Type u_5}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_4} D₁]
[Category.{u_10, 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.{u_7, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_8, u_4} D₁]
[Category.{u_10, 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.{u_8, u_1} C₁]
[Category.{u_7, u_2} C₂]
[Category.{u_10, u_4} D₁]
[Category.{u_9, 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')
:
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.{u_7, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_8, u_4} D₁]
[Category.{u_10, 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.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} C₃]
[Category.{u_10, u_4} D₁]
[Category.{u_11, u_5} D₂]
[Category.{u_12, 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₁.
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}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} C₃]
[Category.{u_10, u_4} D₁]
[Category.{u_11, u_5} D₂]
[Category.{u_12, 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.)
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}
[Category.{u_7, u_1} C₁]
[Category.{u_8, u_2} C₂]
[Category.{u_9, u_3} C₃]
[Category.{u_10, u_4} D₁]
[Category.{u_11, u_5} D₂]
[Category.{u_12, 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₁)
:
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.{u_7, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_11, u_3} C₃]
[Category.{u_8, u_4} D₁]
[Category.{u_10, u_5} D₂]
[Category.{u_12, 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.{u_7, u_1} C₁]
[Category.{u_9, u_2} C₂]
[Category.{u_11, u_3} C₃]
[Category.{u_8, u_4} D₁]
[Category.{u_10, u_5} D₂]
[Category.{u_12, 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.{u_11, u_1} C₁]
[Category.{u_7, u_2} C₂]
[Category.{u_8, u_3} C₃]
[Category.{u_12, u_4} D₁]
[Category.{u_9, u_5} D₂]
[Category.{u_10, 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₃)
:
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.{u_11, u_1} C₁]
[Category.{u_7, u_2} C₂]
[Category.{u_8, u_3} C₃]
[Category.{u_12, u_4} D₁]
[Category.{u_9, u_5} D₂]
[Category.{u_10, 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₁₂)
: