yonedaJointlyReflectsLimits — Mathlib

Lean4
/-- The yoneda embeddings jointly reflect limits. -/
def yonedaJointlyReflectsLimits (F : J ⥤ Cᵒᵖ) (c : Cone F) (hc : ∀ X : C, IsLimit ((yoneda.obj X).mapCone c)) :
    IsLimit c where
  lift s := ((hc s.pt.unop).lift ((yoneda.obj s.pt.unop).mapCone s) (𝟙 _)).op
  fac s
    j := Quiver.Hom.unop_inj (by simpa using congr_fun ((hc s.pt.unop).fac ((yoneda.obj s.pt.unop).mapCone s) j) (𝟙 _))
  uniq s m
    hm :=
    Quiver.Hom.unop_inj
      (by
        apply (Types.isLimitEquivSections (hc s.pt.unop)).injective
        ext j
        have eq := congr_fun ((hc s.pt.unop).fac ((yoneda.obj s.pt.unop).mapCone s) j) (𝟙 _)
        dsimp at eq
        dsimp [Types.isLimitEquivSections, Types.sectionOfCone]
        rw [eq, Category.comp_id, ← hm, unop_comp])
Похожие утверждения