comp_preservesLimit — Mathlib

English

If G preserves a limit and F is initial, then F ⋙ G preserves the limit.

Русский

Если G сохраняет предел, и F — начальный, то F ⋙ G сохраняет предел.

LaTeX

$$$\\text{PreservesLimit}(G,H) \\Rightarrow \\text{PreservesLimit}(F \\circ G,H).$$$

Lean4

instance (priority := 100) comp_preservesLimit {B : Type u₄} [Category.{v₄} B] {H : E ⥤ B} [PreservesLimit G H] :
    PreservesLimit (F ⋙ G) H where
  preserves {c}
    hc := by
    refine ⟨isLimitExtendConeEquiv (G := G ⋙ H) F (H.mapCone c) ?_⟩
    let hc' := isLimitOfPreserves H ((isLimitExtendConeEquiv F c).symm hc)
    exact IsLimit.ofIsoLimit hc' (Cones.ext (Iso.refl _) (by simp))

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