## Stream: Is there code for X?

### Topic: Fibered products

#### 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 }


#### Patrick Massot (Sep 22 2020 at 20:24):

I don't think it's there.

#### Kevin Buzzard (Sep 22 2020 at 20:54):

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

#### 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?

#### Bhavik Mehta (Sep 22 2020 at 21:29):

ct.limits.types iirc

#### Adam Topaz (Sep 22 2020 at 21:32):

Yep! That's the missing import.

#### 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