preservesLimitsOfShape_of_isZero — Mathlib

English

If G is a zero functor (takes every morphism to zero), then G preserves limits of any shape J.

Русский

Если G — нулевой функтор (отправляет каждое отображение в нуль-морфизм), то он сохраняет пределы любой формы J.

LaTeX

$$$\\text{IsZero}(G) \\Rightarrow \\forall J,\\; \\text{PreservesLimitsOfShape } J\\; G$$$

Lean4

/-- A zero functor preserves limits. -/
theorem preservesLimitsOfShape_of_isZero : PreservesLimitsOfShape J G where
  preservesLimit
    {K} :=
    ⟨fun _ =>
      ⟨by
        rw [Functor.isZero_iff] at hG
        exact IsLimit.ofIsZero _ ((K ⋙ G).isZero (fun X ↦ hG _)) (hG _)⟩⟩

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