map_respectsIso — Mathlib

English

If P respects iso, then the mapped property P.map F also respects iso for any functor F.

Русский

Если P сохраняет изоморфизмы, то отображённое свойство P.map F также сохраняет изоморфизмы для любого функторa F.

LaTeX

$$$(P.map F).\\mathrm{RespectsIso}$$$

Lean4

instance map_respectsIso (P : MorphismProperty C) (F : C ⥤ D) : (P.map F).RespectsIso :=
  by
  apply RespectsIso.of_respects_arrow_iso
  intro f g e ⟨X', Y', f', hf', ⟨e'⟩⟩
  exact ⟨X', Y', f', hf', ⟨e' ≪≫ e⟩⟩

Похожие утверждения