instIsClosedUnderIsomorphismsInverseImage

English

For any functor F, the inverse image property P.inverseImage F is closed under isomorphisms if P is closed under isomorphisms.

Русский

Для любого функторa F предикат P.inverseImage F замкнут по изоморфизмам, если P замкнуто по изоморфизмам.

LaTeX

$$$$ (P.inverseImage F).IsClosedUnderIsomorphisms. $$$$

Lean4

instance (F : D ⥤ C) [P.IsClosedUnderIsomorphisms] : IsClosedUnderIsomorphisms (P.inverseImage F) where
  of_iso e hX := P.prop_of_iso (F.mapIso e) hX

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