instContainsZeroMapOfPreservesZeroMorphisms

English

If P.ContainsZero, HasZero morphisms, and F preserves zero morphisms, then (P.map F) ContainsZero.

Русский

Если P содержит нуль, существуют нулевые морфизмы и F сохраняет нулевые морфизмы, то (P.map F) содержит нуль.

LaTeX

$$$$ [P.ContainsZero] \land [HasZeroMorphisms C] \land [HasZeroMorphisms D] (F: C \to D) \Rightarrow (P.map F).ContainsZero. $$$$

Lean4

instance [P.ContainsZero] [HasZeroMorphisms C] [HasZeroMorphisms D] (F : C ⥤ D) [F.PreservesZeroMorphisms] :
    (P.map F).ContainsZero where
  exists_zero := by
    obtain ⟨Z, h₁, h₂⟩ := P.exists_prop_of_containsZero
    exact ⟨F.obj Z, F.map_isZero h₁, P.prop_map_obj F h₂⟩

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