Isomorphism of pullbacks

Stream: Is there code for X?

[Kenny Lau]

import Mathlib

universe v u

namespace CategoryTheory.Limits

noncomputable def pullback.iso {C : Type u} [Category.{v} C] [HasPullbacks C] {X₁ X₂ S₁ S₂ T : C}
      (f₁ : S₁ ⟶ T) (f₂ : S₂ ⟶ T) (e₁ : X₁ ≅ S₁) (e₂ : X₂ ≅ S₂) :
    pullback (e₁.hom ≫ f₁) (e₂.hom ≫ f₂) ≅ pullback f₁ f₂ where
  hom := pullback.map _ _ _ _ e₁.hom e₂.hom (𝟙 T) (Category.comp_id _) (Category.comp_id _)
  inv := pullback.map _ _ _ _ e₁.inv e₂.inv (𝟙 T) (by aesop) (by aesop)

noncomputable def pullback.iso' {C : Type u} [Category.{v} C] [HasPullbacks C] {X₁ X₂ S₁ S₂ T : C}
      {f₁ : S₁ ⟶ T} {f₂ : S₂ ⟶ T} {g₁ : X₁ ⟶ T} {g₂ : X₂ ⟶ T} (e₁ : X₁ ≅ S₁) (e₂ : X₂ ≅ S₂)
      (h₁ : e₁.hom ≫ f₁ = g₁) (h₂ : e₂.hom ≫ f₂ = g₂) :
    pullback g₁ g₂ ≅ pullback f₁ f₂ where
  hom := pullback.map _ _ _ _ e₁.hom e₂.hom (𝟙 T) (by aesop) (by aesop)
  inv := pullback.map _ _ _ _ e₁.inv e₂.inv (𝟙 T) (by aesop) (by aesop)

end CategoryTheory.Limits

[Kenny Lau]

It seems like we have pullback.map and the isIso version but not the Iso version?

[Robin Carlier]

These can be one-lined via

import Mathlib

universe v u

namespace CategoryTheory.Limits

noncomputable def pullback.iso {C : Type u} [Category.{v} C] [HasPullbacks C] {X₁ X₂ S₁ S₂ T : C}
      (f₁ : S₁ ⟶ T) (f₂ : S₂ ⟶ T) (e₁ : X₁ ≅ S₁) (e₂ : X₂ ≅ S₂) :
    pullback (e₁.hom ≫ f₁) (e₂.hom ≫ f₂) ≅ pullback f₁ f₂ :=
  HasLimit.isoOfNatIso <| cospanExt e₁ e₂ (.refl _) (by simp) (by simp)

noncomputable def pullback.iso' {C : Type u} [Category.{v} C] [HasPullbacks C] {X₁ X₂ S₁ S₂ T : C}
      {f₁ : S₁ ⟶ T} {f₂ : S₂ ⟶ T} {g₁ : X₁ ⟶ T} {g₂ : X₂ ⟶ T} (e₁ : X₁ ≅ S₁) (e₂ : X₂ ≅ S₂)
      (h₁ : e₁.hom ≫ f₁ = g₁) (h₂ : e₂.hom ≫ f₂ = g₂) :
    pullback g₁ g₂ ≅ pullback f₁ f₂ :=
  HasLimit.isoOfNatIso <| cospanExt e₁ e₂ (.refl _) (by simp [h₁]) (by simp [h₂])

end CategoryTheory.Limits

but it’s true that this is surprising that this is not here already.
Both definitions should come along lemmas that characterizes the hom and inv direction with respect to the projections.

[Joël Riou]

We should just introduce pullback.mapIso with a similar API as pullback.map (allowing three isos, not just two). It is better to define it using pullback.map as hom/inv fields, so as to allow better automation.