English
A vertical whisker along isomorphisms preserves Guitart exactness.
Русский
Вертикальный усечение вдоль изоморфизмов сохраняет точность Гитхарта.
LaTeX
$$$(w.whiskerVertical\, \alpha\, \beta).GuitartExact \iff w.GuitartExact$$$
Lean4
/-- A 2-square stays Guitart exact if we replace the left and right functors
by isomorphic functors. See also `whiskerVertical_iff`. -/
theorem whiskerVertical [w.GuitartExact] (α : L ≅ L') (β : R ≅ R') : (w.whiskerVertical α.hom β.inv).GuitartExact :=
by
rw [guitartExact_iff_initial]
intro X₂
let e :
structuredArrowDownwards (w.whiskerVertical α.hom β.inv) X₂ ≅
w.structuredArrowDownwards X₂ ⋙ (StructuredArrow.mapIso (β.app X₂)).functor :=
NatIso.ofComponents
(fun f =>
StructuredArrow.isoMk (α.symm.app f.right)
(by
dsimp
simp only [NatTrans.naturality_assoc, assoc, ← B.map_comp, Iso.hom_inv_id_app, B.map_id, comp_id]))
rw [Functor.initial_natIso_iff e]
infer_instance
