English
If P.trW is a property, then P.trW respects isomorphisms: precomposition and postcomposition with an isomorphism preserve membership in P.trW.
Русский
Для свойства P.trW справедливо, что с изоморфизмами сохраняются принадлежности: пред- и пост-композиция с изоморфизмом сохраняют принадлежность к P.trW.
LaTeX
$$$P.trW \\text{ RespectsIso}$$$
Lean4
instance : P.trW.RespectsIso
where
precomp {X' X Y} e
(he : IsIso e) := by
rintro f ⟨Z, g, h, mem, mem'⟩
refine ⟨Z, g, h ≫ inv e⟦(1 : ℤ)⟧', isomorphic_distinguished _ mem _ ?_, mem'⟩
refine Triangle.isoMk _ _ (asIso e) (Iso.refl _) (Iso.refl _) (by simp) (by simp) ?_
dsimp
simp only [Functor.map_inv, assoc, IsIso.inv_hom_id, comp_id, id_comp]
postcomp {X Y Y'} e
(he : IsIso e) := by
rintro f ⟨Z, g, h, mem, mem'⟩
refine ⟨Z, inv e ≫ g, h, isomorphic_distinguished _ mem _ ?_, mem'⟩
exact Triangle.isoMk _ _ (Iso.refl _) (asIso e).symm (Iso.refl _)
