English
Let P be a morphism property on arrows in a category C that is invariant under isomorphisms. Then for any arrows f, g with an isomorphism e: f ≅ g, the property P evaluated at the underlying morphisms is equivalent: P(hom f) ⇔ P(hom g).
Русский
Пусть P — свойство морфизмов стрел в категории C, сохраняющее инвариантность при изоморфизмах. Тогда для любых стрел f, g, если существует изоморфизм e: f ≅ g, выполняется эквиваленция P(hom(f)) ⇔ P(hom(g)).
LaTeX
$$$\\forall C\\,[\\mathcal{C}\\text{ is a category}]\,(P:\\mathrm{MorphismProperty}\,C)\,[\\mathrm{RespectsIso}\,P],\\\\{f,g:\\mathrm{Arrow}(C)\\}\\,(e:\\,f\\cong g) \\,\\Rightarrow \\, P(\\mathrm{hom}(f)) \\iff P(\\mathrm{hom}(g)).$$$
Lean4
theorem arrow_iso_iff (P : MorphismProperty C) [RespectsIso P] {f g : Arrow C} (e : f ≅ g) : P f.hom ↔ P g.hom :=
P.comma_iso_iff e
