coyoneda_preservesLimit — Mathlib

English

If F : J ⥤ C and X ∈ Cᵒᵖ with F representing, then There is a preservesLimit for F by coyoneda.obj X: PreservesLimit F (coyoneda.obj X).

Русский

Пусть F : J ⥤ C и X ∈ Cᵒᵖ так, что F представим; тогда F сохраняет пределы через coyoneda.obj X: PreservesLimit F (coyoneda.obj X).

LaTeX

$$$\\forall F:\\, J \\to C,\\; \\forall X:\\, C^{op},\\; \\mathrm{PreservesLimit}\\; F\\; (\\mathrm{coyoneda.obj} X)$$$

Lean4

instance coyoneda_preservesLimit (F : J ⥤ C) (X : Cᵒᵖ) : PreservesLimit F (coyoneda.obj X) where
  preserves {c}
    hc := by
    rw [Types.isLimit_iff]
    intro s hs
    exact
      ⟨hc.lift (Limits.coneOfSectionCompCoyoneda F X ⟨s, hs⟩), hc.fac _,
        hc.uniq (Limits.coneOfSectionCompCoyoneda F X ⟨s, hs⟩)⟩

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