colimit of Hom

Stream: Is there code for X?

[Kenny Lau]

Every functor $\mathscr{C}^{op} \implies \mathsf{Set}$ is a colimit of functors of the form $\operatorname{Hom}_{\mathscr{C}}(-, X)$

[Kenny Lau]

@Reid Barton

[Reid Barton]

I think I proved it in a branch at some point but I don't know the current status

[Bhavik Mehta]

I'd also like to see this in mathlib, and I haven't seen it done anywhere. I'd particularly like to see the more general version image.png, from which the original follows nicely (just set A=yoneda)

[Reid Barton]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/adjunctions/near/147503855 but I don't know what happened to the branch

[Kenny Lau]

what is the integral sign in the picture?

[Bhavik Mehta]

category of elements

[Reid Barton]

I found the branch locally, but obviously it's super old.

+def cocontinuous_equiv : (C ⥤ D) ≌ cocontinuous_functor.{(v+1) u₂ v} (presheaf C) D :=

[Reid Barton]

https://github.com/leanprover-community/mathlib/tree/old-adjunctions in case it's of interest

[Reid Barton]

Haha I forgot about this proof

/-
    dsimp [canonical_diagram.cocone, canonical_diagram,
      canonical_diagram.colimit_cocone, id_iso_yoneda_extension_yoneda,
      adjunction.nat_iso_equiv, adjunction.nat_trans_equiv,
      equiv.refl, equiv.symm, equiv.trans, iso.hom_equiv_of_isos,
      adjunction.mate, adjunction.nat_equiv, adjunction.nat_equiv',
      adjunction.hom_equiv, adjunction.id, adjunction.adjunction_of_equiv_left,
      adjunction.adjunction_of_equiv, adjunction.left_adjoint_of_equiv,
      yoneda_extension_adj, yoneda_extension_e,
      equiv.subtype_equiv_subtype, equiv.subtype_equiv_of_subtype, equiv.Pi_congr_right,
      equiv.arrow_congr,
      is_colimit.equiv,
      restricted_yoneda, yoneda_extension, yoneda_extension_obj,
      restricted_yoneda_yoneda_iso_id,
      nat_iso.of_components, iso_of_equiv, yoneda_equiv], -/

[Bhavik Mehta]

I've chucked together a quick version of this (both the theorem I posted and the original result): https://github.com/b-mehta/topos/blob/master/src/category/colimits.lean if people are interested - I'll PR it to mathlib hopefully soon

[Bhavik Mehta]

Soon finally came :) https://github.com/leanprover-community/mathlib/pull/4401