Zulip Chat Archive

Stream: Is there code for X?

Topic: pullbacks in Type u


view this post on Zulip Greg Price (Mar 31 2021 at 05:39):

Is there an explicit construction in mathlib of pullbacks in the category of types? I'd like to have something like this:

import category_theory.types
open category_theory category_theory.category

universes u
variables {X Y Z : Type u}

def pullback_obj (f : X  Z) (g : Y  Z) : Type u :=
{ p : X × Y // f p.1 = g p.2 }

along with the associated cone and is_limit.

I think I see where such a construction would be -- category_theory.limits.shapes.types -- and I don't see it there. But I know I could be missing something.

view this post on Zulip Scott Morrison (Mar 31 2021 at 05:40):

Yep, it's missing. Definitely okay to add it. Make sure to add both the isomorphism to the pullback coming from has_pullbacks, and the @[simp] lemmas saying how that isomorphism commutes with pullback.fst and pullback.snd.

view this post on Zulip Greg Price (Mar 31 2021 at 05:42):

Cool. I actually have an implementation already, which I wrote the other day -- I'd be glad to send a PR. And I'll be sure to add those pieces.

Could I have an invitation to be able to push a branch?

view this post on Zulip Scott Morrison (Mar 31 2021 at 05:43):

What's your github username?

view this post on Zulip Greg Price (Mar 31 2021 at 05:43):

gnprice

view this post on Zulip Greg Price (Mar 31 2021 at 05:44):

I'm also interested in the specialization where one of the maps is mono:

def mono_pullback_obj (f : X  Z) (m : Y  Z) [mono m] : Type u :=
{ x //  y, m y = f x }

(Or perhaps the better setup would be for m to be the inclusion of a subtype too? Not sure.)

That's probably most natural to do after the more general case, though.

view this post on Zulip Scott Morrison (Mar 31 2021 at 05:44):

Sent.

view this post on Zulip Greg Price (Mar 31 2021 at 05:45):

Got it, thanks!

view this post on Zulip Greg Price (Mar 31 2021 at 07:42):

#6973


Last updated: May 07 2021 at 22:14 UTC