coyonedaJointlyReflectsLimits — Mathlib

Lean4

/-- The coyoneda embeddings jointly reflect limits. -/
def coyonedaJointlyReflectsLimits (F : J ⥤ C) (c : Cone F) (hc : ∀ X : Cᵒᵖ, IsLimit ((coyoneda.obj X).mapCone c)) :
    IsLimit c where
  lift s := (hc (op s.pt)).lift ((coyoneda.obj (op s.pt)).mapCone s) (𝟙 _)
  fac s j := by simpa using congr_fun ((hc (op s.pt)).fac ((coyoneda.obj (op s.pt)).mapCone s) j) (𝟙 _)
  uniq s m
    hm := by
    apply (Types.isLimitEquivSections (hc (op s.pt))).injective
    ext j
    dsimp [Types.isLimitEquivSections, Types.sectionOfCone]
    have eq := congr_fun ((hc (op s.pt)).fac ((coyoneda.obj (op s.pt)).mapCone s) j) (𝟙 _)
    dsimp at eq
    rw [eq, Category.id_comp, ← hm]

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