instContainsZeroInverseImageOfIsClosedUnderIsomorphismsOfPreservesZeroMorphismsOfHasZeroObject

English

If P.IsClosedUnderIsomorphisms, then (P.inverseImage F) is also closed under isomorphisms (assuming HasZeroObject etc.).

Русский

Если P замкнуто по изоморфизмам, то (P.inverseImage F) тоже замкнуто по изоморфизмам (при наличии нулевых объектов).

LaTeX

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

Lean4

instance [P.ContainsZero] [P.IsClosedUnderIsomorphisms] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : D ⥤ C)
    [F.PreservesZeroMorphisms] [HasZeroObject D] : (P.inverseImage F).ContainsZero where
  exists_zero := ⟨0, isZero_zero D, P.prop_of_isZero (F.map_isZero (isZero_zero D))⟩

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