hasExactLimitsOfShape_of_preservesEpi

English

If the limit functor lim preserves epimorphisms, then the AB* property of shape J holds in C

Русский

Если гамма-предел лимит сохраняет эпиморфизмы, то AB* свойство формы J выполняется в C

LaTeX

$$$[HasLimitsOfShape J C] \\land [PreservesEpimorphisms (lim (J := J) (C := C))] \\Rightarrow \\operatorname{HasExactLimitsOfShape}(J) C$$

Lean4

/-- If `lim` of shape `J` into an abelian category `C` preserves epimorphisms, then `C` has AB* of
shape `J`.
-/
theorem hasExactLimitsOfShape_of_preservesEpi [HasLimitsOfShape J C] [PreservesEpimorphisms (lim (J := J) (C := C))] :
    HasExactLimitsOfShape J C where
  preservesFiniteColimits :=
    by
    apply (config := { allowSynthFailures := true }) preservesFiniteColimits_of_preservesHomology
    · exact preservesHomology_of_preservesEpis_and_kernels _
    · exact additive_of_preservesBinaryBiproducts _

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