preservesLimit_of_comp — Mathlib

English

Final restatement: preserves limits with whisker equivalence for an initial F and composed G.

Русский

Финальное переформулирование: сохранение пределов с эквивалентностью whisker для начального F и композиции G.

LaTeX

$$$$ \text{preservesLimit_of_comp } \Rightarrow \text{PreservesLimit } G H $$$$

Lean4

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

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