Categorical pullbacks along an equivalence

For functors F : A ⥤ B and G : C ⥤ B, the categorical pullback F ⊡ G has as objects the triples (a, c, F a ≅ G c). When F is an equivalence, the second projection CategoricalPullback.π₂ F G : F ⊡ G ⥤ C is an equivalence of categories: an object c of C lifts by taking for a the image of G c under an inverse of F, and any two lifts are uniquely isomorphic. This is the stability of equivalences under pullback in the (2,1)-category of categories.

The explicit form CategoricalPullback.sndEquiv transports extra structure along an equivalence: when e : A ≌ B identifies objects of A with objects of B, the category of objects of A whose image in B is equipped with a lift along G is equivalent to C.

Main declarations

• CategoryTheory.Limits.CategoricalPullback.sndEquiv: for e : A ≌ B and G : C ⥤ B, the equivalence C ≌ e.functor ⊡ G whose inverse is the second projection, with identity unit and with counit built from the structural isomorphism and the unit of e;
• CategoryTheory.Limits.CategoricalPullback.isEquivalence_π₂: the second projection out of the categorical pullback of an equivalence is an equivalence.

References

• Kerodon, Tag 032Y (categorical pullbacks).

def CategoryTheory.Limits.CategoricalPullback.sndEquiv {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (e : A ≌ B) (G : Functor C B) : C ≌ CategoricalPullback e.functor G

The categorical pullback of an equivalence e : A ≌ B along G : C ⥤ B is equivalent to C. The functor sends c to (e.inverse (G c), c) with the counit of e as structural isomorphism, the inverse is the second projection π₂, the unit is the identity, and the counit at (a, c, φ) is e.inverse (G c) ≅ e.inverse (e.functor a) ≅ a, built from φ and the unit of e.

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.sndEquiv_functor_obj_snd {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (e : A ≌ B) (G : Functor C B) (c : C) : ((sndEquiv e G).functor.obj c).snd = c

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.sndEquiv_functor_obj_fst {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (e : A ≌ B) (G : Functor C B) (c : C) : ((sndEquiv e G).functor.obj c).fst = e.inverse.obj (G.obj c)

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.sndEquiv_counitIso_hom_app_fst {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (e : A ≌ B) (G : Functor C B) (X : CategoricalPullback e.functor G) : ((sndEquiv e G).counitIso.hom.app X).fst = CategoryStruct.comp (e.inverse.map X.iso.inv) (e.unitIso.inv.app X.fst)

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.sndEquiv_unitIso_inv_app {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (e : A ≌ B) (G : Functor C B) (X : C) : (sndEquiv e G).unitIso.inv.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.sndEquiv_inverse_obj {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (e : A ≌ B) (G : Functor C B) (x : CategoricalPullback e.functor G) : (sndEquiv e G).inverse.obj x = x.snd

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.sndEquiv_counitIso_hom_app_snd {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (e : A ≌ B) (G : Functor C B) (X : CategoricalPullback e.functor G) : ((sndEquiv e G).counitIso.hom.app X).snd = CategoryStruct.id X.snd

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.sndEquiv_functor_obj_iso {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (e : A ≌ B) (G : Functor C B) (c : C) : ((sndEquiv e G).functor.obj c).iso = e.counitIso.app (G.obj c)

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.sndEquiv_functor_map_fst {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (e : A ≌ B) (G : Functor C B) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((sndEquiv e G).functor.map f).fst = e.inverse.map (G.map f)

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.sndEquiv_functor_map_snd {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (e : A ≌ B) (G : Functor C B) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((sndEquiv e G).functor.map f).snd = f

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.sndEquiv_counitIso_inv_app_fst {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (e : A ≌ B) (G : Functor C B) (X : CategoricalPullback e.functor G) : ((sndEquiv e G).counitIso.inv.app X).fst = CategoryStruct.comp (e.unitIso.hom.app X.fst) (e.inverse.map X.iso.hom)

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.sndEquiv_inverse_map {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (e : A ≌ B) (G : Functor C B) {X✝ Y✝ : CategoricalPullback e.functor G} (f : X✝ ⟶ Y✝) : (sndEquiv e G).inverse.map f = f.snd

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.sndEquiv_unitIso_hom_app {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (e : A ≌ B) (G : Functor C B) (X : C) : (sndEquiv e G).unitIso.hom.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.sndEquiv_counitIso_inv_app_snd {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (e : A ≌ B) (G : Functor C B) (X : CategoricalPullback e.functor G) : ((sndEquiv e G).counitIso.inv.app X).snd = CategoryStruct.id X.snd

theorem CategoryTheory.Limits.CategoricalPullback.sndEquiv_inverse {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (e : A ≌ B) (G : Functor C B) : (sndEquiv e G).inverse = π₂ e.functor G

The inverse of sndEquiv e G is the second projection.

instance CategoryTheory.Limits.CategoricalPullback.isEquivalence_π₂ {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (F : Functor A B) [F.IsEquivalence] (G : Functor C B) : (π₂ F G).IsEquivalence

The second projection out of the categorical pullback of an equivalence is an equivalence: an object of C lifts uniquely up to unique isomorphism.