Zulip Chat Archive

Stream: Is there code for X?

Topic: colimit of Hom


view this post on Zulip Kenny Lau (Aug 02 2020 at 16:54):

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

view this post on Zulip Kenny Lau (Aug 02 2020 at 16:55):

@Reid Barton

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 02 2020 at 17:24):

what is the integral sign in the picture?

view this post on Zulip Bhavik Mehta (Aug 02 2020 at 17:24):

category of elements

view this post on Zulip 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 :=

view this post on Zulip Reid Barton (Aug 02 2020 at 17:39):

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

view this post on Zulip 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], -/

view this post on Zulip 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

view this post on Zulip 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