Horizontal composition of Guitart exact squares #
In this file, we show that the horizontal composition of Guitart exact squares is Guitart exact.
def
CategoryTheory.TwoSquare.whiskerHorizontal
{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)
{T' : Functor C₁ D₁}
{B' : Functor C₂ D₂}
(α : T' ⟶ T)
(β : B ⟶ B')
:
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 α : T ⟶ T' and β : B' ⟶ B.
Equations
- w.whiskerHorizontal α β = (w.whiskerTop α).whiskerBottom β
Instances For
@[simp]
theorem
CategoryTheory.TwoSquare.whiskerHorizontal_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)
{T' : Functor C₁ D₁}
{B' : Functor C₂ D₂}
(α : T' ⟶ T)
(β : B ⟶ B')
(X : C₁)
:
(w.whiskerHorizontal α β).app X = CategoryStruct.comp (R.map (α.app X)) (CategoryStruct.comp (w.natTrans.app X) (β.app (L.obj X)))
theorem
CategoryTheory.TwoSquare.GuitartExact.whiskerHorizontal
{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)
{T' : Functor C₁ D₁}
{B' : Functor C₂ D₂}
[w.GuitartExact]
(α : T ≅ T')
(β : B ≅ B')
:
(w.whiskerHorizontal α.inv β.hom).GuitartExact
A 2-square stays Guitart exact if we replace the top and bottom functors
by isomorphic functors. See also whiskerHorizontal_iff.
@[simp]
theorem
CategoryTheory.TwoSquare.GuitartExact.whiskerHorizontal_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)
{T' : Functor C₁ D₁}
{B' : Functor C₂ D₂}
(α : T ≅ T')
(β : B ≅ B')
:
A 2-square is Guitart exact iff it is so after replacing the top and bottom functors by isomorphic functors.
instance
CategoryTheory.TwoSquare.GuitartExact.instWhiskerHorizontalOfIsIsoFunctor
{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)
{T' : Functor C₁ D₁}
{B' : Functor C₂ D₂}
[w.GuitartExact]
(α : T' ⟶ T)
(β : B ⟶ B')
[IsIso α]
[IsIso β]
:
(w.whiskerHorizontal α β).GuitartExact
def
CategoryTheory.TwoSquare.hComp'
{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₃]
{V₁ : Functor C₁ D₁}
{T₁ : Functor C₁ C₂}
{B₁ : Functor D₁ D₂}
{V₂ : Functor C₂ D₂}
(w : TwoSquare T₁ V₁ V₂ B₁)
{T₂ : Functor C₂ C₃}
{B₂ : Functor D₂ D₃}
{V₃ : Functor C₃ D₃}
(w' : TwoSquare T₂ V₂ V₃ B₂)
{T₁₂ : Functor C₁ C₃}
{B₁₂ : Functor D₁ D₃}
(eT : T₁.comp T₂ ≅ T₁₂)
(eB : B₁.comp B₂ ≅ B₁₂)
:
TwoSquare T₁₂ V₁ V₃ B₁₂
The horizontal composition of 2-squares. (Variant where we allow the replacement of the horizontal compositions by isomorphic functors.)
Instances For
@[simp]
theorem
CategoryTheory.TwoSquare.hComp'_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₃]
{V₁ : Functor C₁ D₁}
{T₁ : Functor C₁ C₂}
{B₁ : Functor D₁ D₂}
{V₂ : Functor C₂ D₂}
(w : TwoSquare T₁ V₁ V₂ B₁)
{T₂ : Functor C₂ C₃}
{B₂ : Functor D₂ D₃}
{V₃ : Functor C₃ D₃}
(w' : TwoSquare T₂ V₂ V₃ B₂)
{T₁₂ : Functor C₁ C₃}
{B₁₂ : Functor D₁ D₃}
(eT : T₁.comp T₂ ≅ T₁₂)
(eB : B₁.comp B₂ ≅ B₁₂)
(X : C₁)
:
instance
CategoryTheory.TwoSquare.GuitartExact.hComp
{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₃]
{V₁ : Functor C₁ D₁}
{T₁ : Functor C₁ C₂}
{B₁ : Functor D₁ D₂}
{V₂ : Functor C₂ D₂}
(w : TwoSquare T₁ V₁ V₂ B₁)
{T₂ : Functor C₂ C₃}
{B₂ : Functor D₂ D₃}
{V₃ : Functor C₃ D₃}
(w' : TwoSquare T₂ V₂ V₃ B₂)
[w.GuitartExact]
[w'.GuitartExact]
:
(w.hComp w').GuitartExact
instance
CategoryTheory.TwoSquare.GuitartExact.hComp'
{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₃]
{V₁ : Functor C₁ D₁}
{T₁ : Functor C₁ C₂}
{B₁ : Functor D₁ D₂}
{V₂ : Functor C₂ D₂}
(w : TwoSquare T₁ V₁ V₂ B₁)
{T₂ : Functor C₂ C₃}
{B₂ : Functor D₂ D₃}
{V₃ : Functor C₃ D₃}
(w' : TwoSquare T₂ V₂ V₃ B₂)
{T₁₂ : Functor C₁ C₃}
{B₁₂ : Functor D₁ D₃}
(eT : T₁.comp T₂ ≅ T₁₂)
(eB : B₁.comp B₂ ≅ B₁₂)
[w.GuitartExact]
[w'.GuitartExact]
:
(w.hComp' w' eT eB).GuitartExact
def
CategoryTheory.TwoSquare.GuitartExact.costructuredArrowRightwardsComp
{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₃]
{V₁ : Functor C₁ D₁}
{T₁ : Functor C₁ C₂}
{B₁ : Functor D₁ D₂}
{V₂ : Functor C₂ D₂}
(w : TwoSquare T₁ V₁ V₂ B₁)
{T₂ : Functor C₂ C₃}
{B₂ : Functor D₂ D₃}
{V₃ : Functor C₃ D₃}
(w' : TwoSquare T₂ V₂ V₃ B₂)
(Y₁ : D₁)
:
(w.costructuredArrowRightwards Y₁).comp (w'.costructuredArrowRightwards (B₁.obj Y₁)) ≅ (w.hComp w').costructuredArrowRightwards Y₁
The canonical isomorphism between
w.costructuredArrowRightwards Y₁ ⋙ w'.costructuredArrowRightwards (B₁.obj Y₁) and
(w ≫ₕ w').costructuredArrowRightwards Y₁.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.TwoSquare.GuitartExact.of_hComp
{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₃]
{V₁ : Functor C₁ D₁}
{T₁ : Functor C₁ C₂}
{B₁ : Functor D₁ D₂}
{V₂ : Functor C₂ D₂}
(w : TwoSquare T₁ V₁ V₂ B₁)
{T₂ : Functor C₂ C₃}
{B₂ : Functor D₂ D₃}
{V₃ : Functor C₃ D₃}
(w' : TwoSquare T₂ V₂ V₃ B₂)
[B₁.EssSurj]
[w.GuitartExact]
[(w.hComp w').GuitartExact]
:
w'.GuitartExact
theorem
CategoryTheory.TwoSquare.GuitartExact.of_hComp'
{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₃]
{V₁ : Functor C₁ D₁}
{T₁ : Functor C₁ C₂}
{B₁ : Functor D₁ D₂}
{V₂ : Functor C₂ D₂}
(w : TwoSquare T₁ V₁ V₂ B₁)
{T₂ : Functor C₂ C₃}
{B₂ : Functor D₂ D₃}
{V₃ : Functor C₃ D₃}
(w' : TwoSquare T₂ V₂ V₃ B₂)
{T₁₂ : Functor C₁ C₃}
{B₁₂ : Functor D₁ D₃}
(eT : T₁.comp T₂ ≅ T₁₂)
(eB : B₁.comp B₂ ≅ B₁₂)
[B₁.EssSurj]
[w.GuitartExact]
[h : (w.hComp' w' eT eB).GuitartExact]
:
w'.GuitartExact
theorem
CategoryTheory.TwoSquare.GuitartExact.hComp_iff_of_essSurj
{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₃]
{V₁ : Functor C₁ D₁}
{T₁ : Functor C₁ C₂}
{B₁ : Functor D₁ D₂}
{V₂ : Functor C₂ D₂}
(w : TwoSquare T₁ V₁ V₂ B₁)
{T₂ : Functor C₂ C₃}
{B₂ : Functor D₂ D₃}
{V₃ : Functor C₃ D₃}
(w' : TwoSquare T₂ V₂ V₃ B₂)
[B₁.EssSurj]
[w.GuitartExact]
:
theorem
CategoryTheory.TwoSquare.GuitartExact.hComp'_iff_of_essSurj
{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₃]
{V₁ : Functor C₁ D₁}
{T₁ : Functor C₁ C₂}
{B₁ : Functor D₁ D₂}
{V₂ : Functor C₂ D₂}
(w : TwoSquare T₁ V₁ V₂ B₁)
{T₂ : Functor C₂ C₃}
{B₂ : Functor D₂ D₃}
{V₃ : Functor C₃ D₃}
(w' : TwoSquare T₂ V₂ V₃ B₂)
{T₁₂ : Functor C₁ C₃}
{B₁₂ : Functor D₁ D₃}
(eT : T₁.comp T₂ ≅ T₁₂)
(eB : B₁.comp B₂ ≅ B₁₂)
[B₁.EssSurj]
[w.GuitartExact]
:
theorem
CategoryTheory.TwoSquare.GuitartExact.hComp_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₃]
{V₁ : Functor C₁ D₁}
{T₁ : Functor C₁ C₂}
{B₁ : Functor D₁ D₂}
{V₂ : Functor C₂ D₂}
(w : TwoSquare T₁ V₁ V₂ B₁)
{V₃ : Functor C₃ D₃}
(eT : C₂ ≌ C₃)
(eB : D₂ ≌ D₃)
(w' : eT.functor.comp V₃ ≅ V₂.comp eB.functor)
:
theorem
CategoryTheory.TwoSquare.GuitartExact.hComp'_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₃]
{V₁ : Functor C₁ D₁}
{T₁ : Functor C₁ C₂}
{B₁ : Functor D₁ D₂}
{V₂ : Functor C₂ D₂}
(w : TwoSquare T₁ V₁ V₂ B₁)
{V₃ : Functor C₃ D₃}
(E : C₂ ≌ C₃)
(E' : D₂ ≌ D₃)
(w' : E.functor.comp V₃ ≅ V₂.comp E'.functor)
{T₁₂ : Functor C₁ C₃}
{B₁₂ : Functor D₁ D₃}
(eT : T₁.comp E.functor ≅ T₁₂)
(eB : B₁.comp E'.functor ≅ B₁₂)
: