English
If left and right functors are equivalences and the square is an isomorphism, then the square is Guitart exact.
Русский
Если левый и правый функторы являются эквивалентностями, а квадрат является изоморфизмом, то квадрат точен по Гитхарту.
LaTeX
$$$[L\text{ IsEquivalence}] \ [R\text{ IsEquivalence}] \ [\text{IsIso } w] \Rightarrow w.GuitartExact$$$
Lean4
/-- When the left and right functors of a 2-square are equivalences, and the natural
transformation of the 2-square is an isomorphism, then the 2-square is Guitart exact. -/
instance (priority := 100) guitartExact_of_isEquivalence_of_isIso [L.IsEquivalence] [R.IsEquivalence] [IsIso w] :
GuitartExact w := by
rw [guitartExact_iff_initial]
intro X₂
have := StructuredArrow.isEquivalence_post X₂ T R
have : (Comma.mapRight _ w : StructuredArrow (R.obj X₂) _ ⥤ _).IsEquivalence :=
(Comma.mapRightIso _ (asIso w)).isEquivalence_functor
have := StructuredArrow.isEquivalence_pre (R.obj X₂) L B
dsimp only [structuredArrowDownwards]
infer_instance
