English
If the vertical composition of two squares is formed using equivalences on the middle columns/rows, then the Guitart exactness is equivalent to that of the first square.
Русский
Если вертикальная композиция строится с использованием эквивалентностей между средними столбцами/строками, то точность Guitart эквивалентна точности первого квадрата.
LaTeX
$$$ (w \\vComp w').GuitartExact \\iff w.GuitartExact $$$
Lean4
theorem vComp_iff_of_equivalences (eL : C₂ ≌ C₃) (eR : D₂ ≌ D₃) (w' : H₂ ⋙ eR.functor ≅ eL.functor ⋙ H₃) :
(w ≫ᵥ w'.hom).GuitartExact ↔ w.GuitartExact := by
constructor
· intro hww'
letI : CatCommSq H₂ eL.functor eR.functor H₃ := ⟨w'⟩
have hw' : CatCommSq.iso H₂ eL.functor eR.functor H₃ = w' := rfl
letI : CatCommSq H₃ eL.inverse eR.inverse H₂ := CatCommSq.vInvEquiv _ _ _ _ inferInstance
let w'' := CatCommSq.iso H₃ eL.inverse eR.inverse H₂
let α : (L₁ ⋙ eL.functor) ⋙ eL.inverse ≅ L₁ :=
Functor.associator _ _ _ ≪≫ Functor.isoWhiskerLeft L₁ eL.unitIso.symm ≪≫ L₁.rightUnitor
let β : (R₁ ⋙ eR.functor) ⋙ eR.inverse ≅ R₁ :=
Functor.associator _ _ _ ≪≫ Functor.isoWhiskerLeft R₁ eR.unitIso.symm ≪≫ R₁.rightUnitor
have : w = (w ≫ᵥ w'.hom).vComp' w''.hom α β := by
ext X₁
simp? [w'', α, β] says
simp only [Functor.comp_obj, vComp'_app, Iso.trans_inv, Functor.isoWhiskerLeft_inv, Iso.symm_inv, assoc,
NatTrans.comp_app, Functor.id_obj, Functor.rightUnitor_inv_app, Functor.whiskerLeft_app,
Functor.associator_inv_app, comp_id, id_comp, vComp_app, Functor.map_comp, Equivalence.inv_fun_map,
CatCommSq.vInv_iso_hom_app, Iso.trans_hom, Functor.isoWhiskerLeft_hom, Iso.symm_hom,
Functor.associator_hom_app, Functor.rightUnitor_hom_app, Iso.hom_inv_id_app_assoc, w'', α, β]
simp only [hw', ← eR.inverse.map_comp_assoc]
rw [Equivalence.counitInv_app_functor, ← Functor.comp_map, ← NatTrans.naturality_assoc]
simp [← H₂.map_comp]
rw [this]
infer_instance
· intro
exact vComp w w'.hom
