Fibered products

Stream: Is there code for X?

[Adam Topaz]

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 }

[Patrick Massot]

I don't think it's there.

[Kevin Buzzard]

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

[Adam Topaz]

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?

[Bhavik Mehta]

ct.limits.types iirc

[Adam Topaz]

Yep! That's the missing import.

[Bhavik Mehta]

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