Guitart exact squares and quotient categories #
Consider a commutative square of categories given by a natural isomorphism
e : T ⋙ R ≅ L ⋙ B:
T
C₀ ----> H₀
| |
L| |R
v v
C ----> H
B
If both T and B are full and T is essentially surjective, we show
that the 2-square above is Guitart exact if, whenever two morphisms
f₀ and f₁ in L.obj X₀ ⟶ Y (for X₀ : C₀ and Y : C) become equal
after applying B, there exists a precylinder object P of X₀
such that T.map P.i₀ = T.map i₁ and there exists a left homotopy
between f₀ and f₁ for P.map L. The dual result is also obtained.
This result shall be applied in the situation where C₀ is a suitable
full subcategory of a category C of homological complexes, and H₀ and H
are the corresponding homotopy categories (TODO @joelriou).
theorem
CategoryTheory.TwoSquare.GuitartExact.quotient_of_nonempty_leftHomotopy
{C₀ : Type u_1}
{C : Type u_2}
{H₀ : Type u_3}
{H : Type u_4}
[Category.{v_1, u_1} C₀]
[Category.{v_2, u_2} C]
[Category.{v_3, u_3} H₀]
[Category.{v_4, u_4} H]
{T : Functor C₀ H₀}
{L : Functor C₀ C}
{R : Functor H₀ H}
{B : Functor C H}
[T.EssSurj]
[T.Full]
[B.Full]
(e : T.comp R ≅ L.comp B)
(he :
∀ ⦃X₀ : C₀⦄ ⦃Y : C⦄ (f₀ f₁ : L.obj X₀ ⟶ Y),
B.map f₀ = B.map f₁ →
∃ (P : HomotopicalAlgebra.Precylinder X₀), T.map P.i₀ = T.map P.i₁ ∧ Nonempty ((P.map L).LeftHomotopy f₀ f₁))
:
theorem
CategoryTheory.TwoSquare.GuitartExact.quotient_of_nonempty_rightHomotopy
{C₀ : Type u_1}
{C : Type u_2}
{H₀ : Type u_3}
{H : Type u_4}
[Category.{v_1, u_1} C₀]
[Category.{v_2, u_2} C]
[Category.{v_3, u_3} H₀]
[Category.{v_4, u_4} H]
{T : Functor C₀ H₀}
{L : Functor C₀ C}
{R : Functor H₀ H}
{B : Functor C H}
[T.EssSurj]
[T.Full]
[B.Full]
(e : T.comp R ≅ L.comp B)
(he :
∀ ⦃X : C⦄ ⦃Y₀ : C₀⦄ (f₀ f₁ : X ⟶ L.obj Y₀),
B.map f₀ = B.map f₁ →
∃ (P : HomotopicalAlgebra.PrepathObject Y₀), T.map P.p₀ = T.map P.p₁ ∧ Nonempty ((P.map L).RightHomotopy f₀ f₁))
: