Zulip Chat Archive

Stream: Is there code for X?

Topic: Fibered products


view this post on Zulip Adam Topaz (Sep 22 2020 at 20:24):

Does mathlib have some notation/abbreviations for fibered products (just for types)? Do I have to introduce the following?

def fibered_product {α β γ : Type*} (f : α  γ) (g : β  γ) := { x : α × β // f x.1 = g x.2 }

view this post on Zulip Patrick Massot (Sep 22 2020 at 20:24):

I don't think it's there.

view this post on Zulip Kevin Buzzard (Sep 22 2020 at 20:54):

You might find that Scott proved all limits exist in Type I guess

view this post on Zulip Adam Topaz (Sep 22 2020 at 21:07):

This doesn't seem to work.

import category_theory.types
import category_theory.limits.shapes.pullbacks
universe u
example {α β γ : Type u} (f : α  γ) (g : β  γ) : Type u := category_theory.limits.pullback f g

Lean fails to find an instance of category_theory.limits.has_pullback f g. Maybe I'm missing an import?

view this post on Zulip Bhavik Mehta (Sep 22 2020 at 21:29):

ct.limits.types iirc

view this post on Zulip Adam Topaz (Sep 22 2020 at 21:32):

Yep! That's the missing import.

view this post on Zulip Bhavik Mehta (Sep 22 2020 at 21:34):

I'm not sure if it would be useful to have a specific is_limit definition for the fibered product you gave above, so lemmas can be applied directly instead of needing to go through the canonical iso


Last updated: May 07 2021 at 22:14 UTC