English
If there are equivalences between the middle categories and a natural isomorphism between the corresponding composites, then the Guitart exactness of the vertical composition is equivalent to that of the original—and vice versa.
Русский
При наличии эквивалентностей между средними категориями и естественной изоморфией между соответствующими композициями, точность Guitart верна для вертикального композиции и обратно эквивалентны точности исходного квадрата.
LaTeX
$$$ (w.vComp w'.hom).GuitartExact \\iff w.GuitartExact $$$
Lean4
/-- If `X` is isomorphic to `X₁` and `Y` is isomorphic to `Y₁`, then
there is a natural bijection between `X ⟶ Y` and `X₁ ⟶ Y₁`. See also `Equiv.arrowCongr`. -/
@[simps]
def homCongr {X Y X₁ Y₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) : (X ⟶ Y) ≃ (X₁ ⟶ Y₁)
where
toFun f := α.inv ≫ f ≫ β.hom
invFun f := α.hom ≫ f ≫ β.inv
left_inv
f :=
show α.hom ≫ (α.inv ≫ f ≫ β.hom) ≫ β.inv = f by
rw [Category.assoc, Category.assoc, β.hom_inv_id, α.hom_inv_id_assoc, Category.comp_id]
right_inv
f :=
show α.inv ≫ (α.hom ≫ f ≫ β.inv) ≫ β.hom = f by
rw [Category.assoc, Category.assoc, β.inv_hom_id, α.inv_hom_id_assoc, Category.comp_id]
