instIsClosedUnderIsomorphismsMap — Mathlib

English

For any functor F, the mapped property P.map F is closed under isomorphisms if P is closed under isomorphisms.

Русский

Для любого функторов F свойство P.map F сохраняет замыкание по изоморфизмам, если P замкнуто по изоморфизмам.

LaTeX

$$$$ \text{If } P.IsClosedUnderIsomorphisms, \ (P.map F).IsClosedUnderIsomorphisms. $$$$

Lean4

instance (F : C ⥤ D) : IsClosedUnderIsomorphisms (P.map F) where
  of_iso := by
    rintro _ _ e ⟨X, hX, ⟨e'⟩⟩
    exact ⟨X, hX, ⟨e' ≪≫ e⟩⟩

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