English
For any morphism property P, the universally constructed P retains the RespectsIso property.
Русский
Для любого свойства морфизмов P универсальная конструкция сохраняет свойство RespectsIso.
LaTeX
$$$P^{\mathrm{universally}}.RespectsIso$$$
Lean4
instance universally_respectsIso (P : MorphismProperty C) : P.universally.RespectsIso :=
by
apply RespectsIso.mk
· intro X Y Z e f hf X' Z' i₁ i₂ f' H
have : IsPullback (𝟙 _) (i₁ ≫ e.hom) i₁ e.inv :=
IsPullback.of_horiz_isIso ⟨by rw [Category.id_comp, Category.assoc, e.hom_inv_id, Category.comp_id]⟩
exact hf _ _ _ (by simpa only [Iso.inv_hom_id_assoc, Category.id_comp] using this.paste_horiz H)
· intro X Y Z e f hf X' Z' i₁ i₂ f' H
have : IsPullback (𝟙 _) i₂ (i₂ ≫ e.inv) e.inv := IsPullback.of_horiz_isIso ⟨Category.id_comp _⟩
exact
hf _ _ _
(by simpa only [Category.assoc, Iso.hom_inv_id, Category.comp_id, Category.comp_id] using H.paste_horiz this)
