unknown declaration `CategoryTheory.Limits.pullback`

Stream: mathlib4

[Anthony Bordg]

The piece of code below,

def restriction_map {X' : C} (f : X' ⟶ XS.1) :
    (yoneda.obj X' ⟶ P) → ((pullback (XS.2.functorInclusion) (yoneda.map f)) ⟶ P) :=
    fun α => (pullback.snd (f := XS.2.functorInclusion) (g := yoneda.map f)) ≫ α

where XS : (X : C) × Sieve X and P : Cᵒᵖ ⥤ Type v₁, attempts to formalize the restriction map $(S\times_{Y(X)}Y(X')) \rightarrow Y(X') \xrightarrow{\alpha} P$.
I got an unknown declaration 'CategoryTheory.Limits.pullback' error, although I import Mathlib.CategoryTheory.Limits.Shapes.Pullbacks and the scope Limits is opened, moreover, I can Ctrl-click on pullback and open the corresponding file Pullbacks. Also, the code

def restriction_map {X' : C} (f : X' ⟶ XS.1) :
    (yoneda.obj X' ⟶ P) → ((pullback (XS.2.functorInclusion) (yoneda.map f)) ⟶ P) := sorry

doesn't return an error, suggesting that the error comes from the body of the function. Some suggestion?

PS: in the Documentation, pullback is located inHasPullback. Is the documentation outdated?

[Kim Morrison]

Why do you think something is outdated?

[Kim Morrison]

Could you post a #mwe showing the unknown declaration error you're seeing?

[Anthony Bordg]

Here is a mwe.

import Mathlib.CategoryTheory.Sites.Sheaf
import Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback

open CategoryTheory

universe u₁ v₁

variable {C : Type u₁} [Category.{v₁} C]
variable (XS : (X : C) × Sieve X)
variable (P : Cᵒᵖ ⥤ Type v₁)

open Limits

def restriction_map {X' : C} (f : X' ⟶ XS.1) :
    (yoneda.obj X' ⟶ P) → ((pullback (XS.2.functorInclusion) (yoneda.map f)) ⟶ P) :=
    /-
    compiler IR check failed at 'restriction_map._rarg', error: unknown declaration 'CategoryTheory.Limits.pullback'
    -/
    fun α => (pullback.snd (f := XS.2.functorInclusion) (g := yoneda.map f)) ≫ α

[Christian Merten]

Adding noncomputable in front of the def fixes this.

[Kevin Buzzard]

lean4#1785