preservesLimit_of_createsLimit_and_hasLimit

English

If F creates a limit for K and K ⋙ F has a limit, then F preserves the limit of K.

Русский

Если F создаёт предел для K и K ⋙ F имеет предел, то F сохраняет предел K.

LaTeX

$$$[\text{CreatesLimit } K F] \wedge [\text{HasLimit } (K \circ F)] \Rightarrow \mathrm{PreservesLimit } K F$$$

Lean4

/-- `F` preserves the limit of `K` if it creates the limit and `K ⋙ F` has the limit. -/
instance (priority := 100) preservesLimit_of_createsLimit_and_hasLimit (K : J ⥤ C) (F : C ⥤ D) [CreatesLimit K F]
    [HasLimit (K ⋙ F)] : PreservesLimit K F where
  preserves
    t :=
    ⟨IsLimit.ofIsoLimit (limit.isLimit _)
        ((liftedLimitMapsToOriginal (limit.isLimit _)).symm ≪≫
          (Cones.functoriality K F).mapIso ((liftedLimitIsLimit (limit.isLimit _)).uniqueUpToIso t))⟩
      -- see Note [lower instance priority]

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