preservesLimit_comp_of_createsLimit

English

If F creates limits and G preserves limits of shape J on K, then K ⋙ F preserves limits after composition with G.

Русский

Если F создает пределы и G сохраняет пределы формы J на K, то K ⋙ F сохраняет пределы после композиции с G.

LaTeX

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

Lean4

instance preservesLimit_comp_of_createsLimit [CreatesLimit K F] [PreservesLimit K (F ⋙ G)] : PreservesLimit (K ⋙ F) G
    where
  preserves
    hc :=
    ⟨IsLimit.ofIsoLimit (isLimitOfPreserves (F ⋙ G) (liftedLimitIsLimit hc))
        ((Functor.mapConeMapCone (liftLimit hc)).symm ≪≫
          (Cones.functoriality _ _).mapIso (liftedLimitMapsToOriginal hc))⟩

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