# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: colimit of Hom

#### Kenny Lau (Aug 02 2020 at 16:54):

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

#### Kenny Lau (Aug 02 2020 at 16:55):

@Reid Barton

#### Reid Barton (Aug 02 2020 at 17:01):

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

#### Bhavik Mehta (Aug 02 2020 at 17:19):

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 (Aug 02 2020 at 17:23):

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

#### Kenny Lau (Aug 02 2020 at 17:24):

what is the integral sign in the picture?

#### Bhavik Mehta (Aug 02 2020 at 17:24):

category of elements

#### Reid Barton (Aug 02 2020 at 17:26):

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 (Aug 02 2020 at 17:39):

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

#### Reid Barton (Aug 02 2020 at 17:41):

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 (Aug 07 2020 at 16:11):

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 (Oct 10 2020 at 18:53):

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

Last updated: May 07 2021 at 23:11 UTC