English
If F preserves zero morphisms and preserves finite limits and colimits, then the inverse image of P is closed under extensions.
Русский
Если F сохраняет нулевые морфизмы и сохраняет конечные пределы и сопряжения, то P^{-1}F замкнуто по расширениям.
LaTeX
$$$\forall C,D, F:D\to C\ [F.\PreservesZeroMorphisms], [F.\PreservesFiniteLimits], [F.\PreservesFiniteColimits],\ (P^{-1}F).IsClosedUnderExtensions.$$$
Lean4
instance [P.IsClosedUnderExtensions] (F : D ⥤ C) [HasZeroMorphisms D] [F.PreservesZeroMorphisms]
[PreservesFiniteLimits F] [PreservesFiniteColimits F] : (P.inverseImage F).IsClosedUnderExtensions where
prop_X₂_of_shortExact hS h₁
h₃ := by
have := hS.mono_f
have := hS.epi_g
exact P.prop_X₂_of_shortExact (hS.map F) h₁ h₃
