yoneda_preservesLimit — Mathlib

English

For every X in C, the Yoneda embedding yoneda.obj X preserves limits; i.e., for any diagram F, the limit of F is carried to a limit after applying yoneda.obj X.

Русский

Для каждого X ∈ C отображение Йонеда сохраняет пределы: предел диаграммы F отображается в пределе после применения yoneda.obj X.

LaTeX

$$$\\forall X:\\!C,\\; \\mathrm{PreservesLimits}(\\mathrm{yoneda.obj} X)$$$

Lean4

instance yoneda_preservesLimit (F : J ⥤ Cᵒᵖ) (X : C) : PreservesLimit F (yoneda.obj X) where
  preserves {c}
    hc := by
    rw [Types.isLimit_iff]
    intro s hs
    exact
      ⟨(hc.lift (Limits.coneOfSectionCompYoneda F X ⟨s, hs⟩)).unop, fun j =>
        Quiver.Hom.op_inj (hc.fac (Limits.coneOfSectionCompYoneda F X ⟨s, hs⟩) j), fun m hm =>
        Quiver.Hom.op_inj
          (hc.uniq (Limits.coneOfSectionCompYoneda F X ⟨s, hs⟩) _ (fun j => Quiver.Hom.unop_inj (hm j)))⟩

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