Lean4
/-- The cocone with point `P` given by `coconeOfRepresentable` is a colimit:
that is, we have exhibited an arbitrary presheaf `P` as a colimit of representables.
The result of [MM92], Chapter I, Section 5, Corollary 3.
-/
def colimitOfRepresentable (P : Cᵒᵖ ⥤ Type max w v₁) : IsColimit (coconeOfRepresentable P)
where
desc
s :=
{ app X x := uliftYonedaEquiv (s.ι.app (Opposite.op (Functor.elementsMk P X x)))
naturality X Y
f := by
ext x
have := s.w (Quiver.Hom.op (CategoryOfElements.homMk (P.elementsMk X x) (P.elementsMk Y (P.map f x)) f rfl))
dsimp at this x ⊢
rw [← this, uliftYonedaEquiv_comp]
dsimp
rw [uliftYonedaEquiv_apply, ← FunctorToTypes.naturality, uliftYonedaEquiv_uliftYoneda_map]
simp [uliftYoneda] }
fac s
j := by
ext X x
let φ : j.unop ⟶ (Functor.elementsMk P _ ((uliftYonedaEquiv.symm (unop j).snd).app X x)) := ⟨x.down.op, rfl⟩
have := s.w φ.op
dsimp [φ] at this x ⊢
rw [← this, uliftYonedaEquiv_apply]
dsimp [uliftYoneda]
rw [id_comp]
uniq s m
hm := by
ext X x
dsimp at hm ⊢
rw [← hm, uliftYonedaEquiv_comp, Equiv.apply_symm_apply]
