Construct a pullback from an isomorphism

Stream: mathlib4

[Calle Sönne]

In AIM/representable, I have an object X : C in some category C. I also have an isomorphism between X and some pullback pullback f g. Is there API for immediately giving X the induced structure of a pullback of f and g? i.e. precomposing pullback.fst and pullback.snd with the isomorphism to get a new limit cone.

The files Shapes/Pullbacksand Shapes/CommSq are somewhat confusing to me as there seems to be a million options for phrasing things, and it is not clear to me which one it is I need. Once I have figured this API out, I think I will add a bunch of documentation to Shapes/Pullbacks.

[Calle Sönne]

Should I be trying to use the IsPullback API from Shapes/CommSq? Or would it be better to phrase this in a different way?

[Calle Sönne]

Okay I seem to have found cone.extend, so I guess this is what I need.

[Adam Topaz]

We should have docs#CategoryTheory.IsPullback.ofIso

[Adam Topaz]

Hmmm… maybe not?

[Calle Sönne]

Adam Topaz said:

We should have docs#CategoryTheory.IsPullback.ofIso

I ended up using docs#CategoryTheory.Limits.IsLimit.extendIso, but maybe its worth to add some API for this directly in the case of pullbacks

[Adam Topaz]

Errr it’s docs#CategoryTheory.IsPullback.of_iso_pullback because it’s a prop

[Adam Topaz]

The IsPullback api is pretty good. I would recommend using it

[Calle Sönne]

Adam Topaz said:

The IsPullback api is pretty good. I would recommend using it

but then I need to construct the projections fst and snd manually, and I would want this to be automatic

[Adam Topaz]

Can you provide a mwe with the expected workflow? I’ll be away from the computer until the evening, but I can look then if no one else responds

[Calle Sönne]

Adam Topaz said:

Can you provide a mwe with the expected workflow? I’ll be away from the computer until the evening, but I can look then if no one else responds

I think in the end I found what I needed, but I will add some docs at some point soon to maybe explain how to do this somewhere.

The following approach works for me:

import Mathlib.CategoryTheory.Limits.Shapes.Pullbacks

namespace CategoryTheory

open CategoryTheory Limits

universe v u

variable {C : Type u} [Category.{v} C] [HasLimits C]
  {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (W : C) (Φ : W ≅ pullback f g)

noncomputable def pullbackCone : PullbackCone f g :=
  (limit.cone (cospan f g)).extend Φ.hom

noncomputable def pullbackConeFst : W ⟶ X := (pullbackCone f g W Φ).fst

noncomputable def pullbackConeSnd : W ⟶ Y := (pullbackCone f g W Φ).snd

noncomputable def pullbackConeIsLimit : IsLimit (pullbackCone f g W Φ) :=
  IsLimit.extendIso _ <| limit.isLimit (cospan f g)

end CategoryTheory

So what ended up making things work nicely was when I realized that I could use Cone.extend but specify its type as PullbackCone f g, because PullbackCone is just an abbrev, and then get access to the PullbackCone API.

Possibly, it could be worth it to add an abbrev somewhere for pullbackCone in the above code (and call it something like pullback.ofIso.