Categorical pullbacks

This file defines the basic properties of categorical pullbacks.

Given a pair of functors (F : A ⥤ B, G : C ⥤ B), we define the category CategoricalPullback F G as the category of triples (a : A, c : C, e : F.obj a ≅ G.obj b).

The category CategoricalPullback F G sits in a canonical CatCommSq, and we formalize that this square is a "limit" in the following sense: functors X ⥤ CategoricalPullback F G are equivalent to pairs of functors (L : X ⥤ A, R : X ⥤ C) equipped with a natural isomorphism L ⋙ F ≅ R ⋙ G.

We formalize this by introducing a category CatCommSqOver F G X that encodes exactly this data, and we prove that the category of functors X ⥤ CategoricalPullback F G is equivalent to CatCommSqOver F G X.

Main declarations

• CategoricalPullback F G: the type of the categorical pullback.
• π₁ F G : CategoricalPullback F G and π₂ F G : CategoricalPullback F G: the canonical projections.
• CategoricalPullback.catCommSq: the canonical CatCommSq (π₁ F G) (π₂ F G) F G which exhibits CategoricalPullback F G as the pullback (in the (2,1)-categorical sense) of the cospan of F and G.
• CategoricalPullback.functorEquiv F G X: the equivalence of categories between functors X ⥤ CategoricalPullback F G and CatCommSqOver F G X, where the latter is an abbrev for CategoricalPullback (whiskeringRight X A B|>.obj F) (whiskeringRight X C B|>.obj G).

References

• Kerodon: section 1.4.5.2
• Niles Johnson, Donald Yau, 2-Dimensional Categories, example 5.3.9, although we take a slightly different (equivalent) model of the object.

TODOs:

• 2-functoriality of the construction with respect to "transformation of categorical cospans".
• Full equivalence-invariance of the notion (follows from suitable 2-functoriality).
• Define a CatPullbackSquare typeclass extending CatCommSqthat encodes the fact that a given CatCommSq defines an equivalence between the top left corner and the categorical pullback of its legs.
• Define a IsCatPullbackSquare propclass.
• Define the "categorical fiber" of a functor at an object of the target category.
• Pasting calculus for categorical pullback squares.
• Categorical pullback squares attached to Grothendieck constructions of pseudofunctors.
• Stability of (co)fibered categories under categorical pullbacks.

structure CategoryTheory.Limits.CategoricalPullback {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) (G : Functor C B) : Type (max (max u₁ u₃) v₂)

The CategoricalPullback F G is the category of triples (a : A, c : C, F a ≅ G c). Morphisms (a, c, e) ⟶ (a', c', e') are pairs of morphisms (f₁ : a ⟶ a', f₂ : c ⟶ c') compatible with the specified isomorphisms.

• fst : A

  the first component element

• snd : C

  the second component element

• iso : F.obj self.fst ≅ G.obj self.snd

  the structural isomorphism F.obj fst ≅ G.obj snd

def CategoryTheory.Limits.CategoricalPullback.«term_⊡_» : Lean.TrailingParserDescr

A notation for the categorical pullback.

Equations

• One or more equations did not get rendered due to their size.

structure CategoryTheory.Limits.CategoricalPullback.Hom {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} {G : Functor C B} (x y : CategoricalPullback F G) : Type (max v₁ v₃)

The Hom types for the categorical pullback are given by pairs of maps compatible with the structural isomorphisms.

• fst : x.fst ⟶ y.fst

  the first component of f : Hom x y is a morphism x.fst ⟶ y.fst

• snd : x.snd ⟶ y.snd

  the second component of f : Hom x y is a morphism x.snd ⟶ y.snd

• w : CategoryStruct.comp (F.map self.fst) y.iso.hom = CategoryStruct.comp x.iso.hom (G.map self.snd)

  the compatibility condition on fst and snd with respect to the structure isompophisms

theorem CategoryTheory.Limits.CategoricalPullback.Hom.ext_iff {A : Type u₁} {B : Type u₂} {C : Type u₃} {inst✝ : Category.{v₁, u₁} A} {inst✝¹ : Category.{v₂, u₂} B} {inst✝² : Category.{v₃, u₃} C} {F : Functor A B} {G : Functor C B} {x y : CategoricalPullback F G} {x✝ y✝ : x.Hom y} : x✝ = y✝ ↔ x✝.fst = y✝.fst ∧ x✝.snd = y✝.snd

theorem CategoryTheory.Limits.CategoricalPullback.Hom.ext {A : Type u₁} {B : Type u₂} {C : Type u₃} {inst✝ : Category.{v₁, u₁} A} {inst✝¹ : Category.{v₂, u₂} B} {inst✝² : Category.{v₃, u₃} C} {F : Functor A B} {G : Functor C B} {x y : CategoricalPullback F G} {x✝ y✝ : x.Hom y} (fst : x✝.fst = y✝.fst) (snd : x✝.snd = y✝.snd) : x✝ = y✝

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.Hom.w_assoc {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} {G : Functor C B} {x y : CategoricalPullback F G} (self : x.Hom y) {Z : B} (h : G.obj y.snd ⟶ Z) : CategoryStruct.comp (F.map self.fst) (CategoryStruct.comp y.iso.hom h) = CategoryStruct.comp x.iso.hom (CategoryStruct.comp (G.map self.snd) h)

instance CategoryTheory.Limits.CategoricalPullback.instCategory {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} {G : Functor C B} : Category.{max v₃ v₁, max (max u₃ u₁) v₂} (CategoricalPullback F G)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.comp_fst {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} {G : Functor C B} {X✝ Y✝ Z✝ : CategoricalPullback F G} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryStruct.comp f g).fst = CategoryStruct.comp f.fst g.fst

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.id_fst {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} {G : Functor C B} (x : CategoricalPullback F G) : (CategoryStruct.id x).fst = CategoryStruct.id x.fst

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.comp_snd {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} {G : Functor C B} {X✝ Y✝ Z✝ : CategoricalPullback F G} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryStruct.comp f g).snd = CategoryStruct.comp f.snd g.snd

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.id_snd {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} {G : Functor C B} (x : CategoricalPullback F G) : (CategoryStruct.id x).snd = CategoryStruct.id x.snd

theorem CategoryTheory.Limits.CategoricalPullback.comp_fst_assoc {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} {G : Functor C B} {X✝ Y✝ Z✝ : CategoricalPullback F G} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) {Z : A} (h : Z✝.fst ⟶ Z) : CategoryStruct.comp (CategoryStruct.comp f g).fst h = CategoryStruct.comp f.fst (CategoryStruct.comp g.fst h)

theorem CategoryTheory.Limits.CategoricalPullback.comp_snd_assoc {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} {G : Functor C B} {X✝ Y✝ Z✝ : CategoricalPullback F G} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) {Z : C} (h : Z✝.snd ⟶ Z) : CategoryStruct.comp (CategoryStruct.comp f g).snd h = CategoryStruct.comp f.snd (CategoryStruct.comp g.snd h)

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.Hom.w' {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} {G : Functor C B} {x y : CategoricalPullback F G} (f : x ⟶ y) : CategoryStruct.comp (G.map f.snd) y.iso.inv = CategoryStruct.comp x.iso.inv (F.map f.fst)

Naturality square for morphisms in the inverse direction.

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.Hom.w'_assoc {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} {G : Functor C B} {x y : CategoricalPullback F G} (f : x ⟶ y) {Z : B} (h : F.obj y.fst ⟶ Z) : CategoryStruct.comp (G.map f.snd) (CategoryStruct.comp y.iso.inv h) = CategoryStruct.comp x.iso.inv (CategoryStruct.comp (F.map f.fst) h)

theorem CategoryTheory.Limits.CategoricalPullback.hom_ext {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} {G : Functor C B} {x y : CategoricalPullback F G} {f g : x ⟶ y} (hₗ : f.fst = g.fst) (hᵣ : f.snd = g.snd) : f = g

Extensionnality principle for morphisms in CategoricalPullback F G.

theorem CategoryTheory.Limits.CategoricalPullback.hom_ext_iff {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} {G : Functor C B} {x y : CategoricalPullback F G} {f g : x ⟶ y} : f = g ↔ f.fst = g.fst ∧ f.snd = g.snd

def CategoryTheory.Limits.CategoricalPullback.π₁ {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) (G : Functor C B) : Functor (CategoricalPullback F G) A

CategoricalPullback.π₁ F G is the first projection CategoricalPullback F G ⥤ A.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.π₁_obj {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) (G : Functor C B) (x : CategoricalPullback F G) : (π₁ F G).obj x = x.fst

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.π₁_map {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) (G : Functor C B) {X✝ Y✝ : CategoricalPullback F G} (f : X✝ ⟶ Y✝) : (π₁ F G).map f = f.fst

def CategoryTheory.Limits.CategoricalPullback.π₂ {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) (G : Functor C B) : Functor (CategoricalPullback F G) C

CategoricalPullback.π₂ F G is the second projection CategoricalPullback F G ⥤ C.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.π₂_obj {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) (G : Functor C B) (x : CategoricalPullback F G) : (π₂ F G).obj x = x.snd

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.π₂_map {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) (G : Functor C B) {X✝ Y✝ : CategoricalPullback F G} (f : X✝ ⟶ Y✝) : (π₂ F G).map f = f.snd

instance CategoryTheory.Limits.CategoricalPullback.catCommSq {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) (G : Functor C B) : CatCommSq (π₁ F G) (π₂ F G) F G

The canonical categorical commutative square in which CategoricalPullback F G sits.

Equations

• CategoryTheory.Limits.CategoricalPullback.catCommSq F G = { iso := CategoryTheory.NatIso.ofComponents (fun (x : CategoryTheory.Limits.CategoricalPullback F G) => x.iso) ⋯ }

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.catCommSq_iso_hom_app {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) (G : Functor C B) (X : CategoricalPullback F G) : (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom.app X = X.iso.hom

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.catCommSq_iso_inv_app {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) (G : Functor C B) (X : CategoricalPullback F G) : (CatCommSq.iso (π₁ F G) (π₂ F G) F G).inv.app X = X.iso.inv

def CategoryTheory.Limits.CategoricalPullback.mkIso {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} {G : Functor C B} {x y : CategoricalPullback F G} (eₗ : x.fst ≅ y.fst) (eᵣ : x.snd ≅ y.snd) (w : CategoryStruct.comp (F.map eₗ.hom) y.iso.hom = CategoryStruct.comp x.iso.hom (G.map eᵣ.hom) := by aesop_cat) : x ≅ y

Constructor for isomorphisms in CategoricalPullback F G.

Equations

• CategoryTheory.Limits.CategoricalPullback.mkIso eₗ eᵣ w = { hom := { fst := eₗ.hom, snd := eᵣ.hom, w := w }, inv := { fst := eₗ.inv, snd := eᵣ.inv, w := ⋯ }, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.mkIso_inv_snd {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} {G : Functor C B} {x y : CategoricalPullback F G} (eₗ : x.fst ≅ y.fst) (eᵣ : x.snd ≅ y.snd) (w : CategoryStruct.comp (F.map eₗ.hom) y.iso.hom = CategoryStruct.comp x.iso.hom (G.map eᵣ.hom) := by aesop_cat) : (mkIso eₗ eᵣ w).inv.snd = eᵣ.inv

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.mkIso_inv_fst {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} {G : Functor C B} {x y : CategoricalPullback F G} (eₗ : x.fst ≅ y.fst) (eᵣ : x.snd ≅ y.snd) (w : CategoryStruct.comp (F.map eₗ.hom) y.iso.hom = CategoryStruct.comp x.iso.hom (G.map eᵣ.hom) := by aesop_cat) : (mkIso eₗ eᵣ w).inv.fst = eₗ.inv

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.mkIso_hom_fst {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} {G : Functor C B} {x y : CategoricalPullback F G} (eₗ : x.fst ≅ y.fst) (eᵣ : x.snd ≅ y.snd) (w : CategoryStruct.comp (F.map eₗ.hom) y.iso.hom = CategoryStruct.comp x.iso.hom (G.map eᵣ.hom) := by aesop_cat) : (mkIso eₗ eᵣ w).hom.fst = eₗ.hom

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.mkIso_hom_snd {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} {G : Functor C B} {x y : CategoricalPullback F G} (eₗ : x.fst ≅ y.fst) (eᵣ : x.snd ≅ y.snd) (w : CategoryStruct.comp (F.map eₗ.hom) y.iso.hom = CategoryStruct.comp x.iso.hom (G.map eᵣ.hom) := by aesop_cat) : (mkIso eₗ eᵣ w).hom.snd = eᵣ.hom

instance CategoryTheory.Limits.CategoricalPullback.instIsIsoFst {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) (G : Functor C B) {x y : CategoricalPullback F G} (f : x ⟶ y) [IsIso f] : IsIso f.fst

instance CategoryTheory.Limits.CategoricalPullback.instIsIsoSnd {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) (G : Functor C B) {x y : CategoricalPullback F G} (f : x ⟶ y) [IsIso f] : IsIso f.snd

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.inv_fst {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) (G : Functor C B) {x y : CategoricalPullback F G} (f : x ⟶ y) [IsIso f] : (inv f).fst = inv f.fst

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.inv_snd {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) (G : Functor C B) {x y : CategoricalPullback F G} (f : x ⟶ y) [IsIso f] : (inv f).snd = inv f.snd

theorem CategoryTheory.Limits.CategoricalPullback.isIso_iff {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) (G : Functor C B) {x y : CategoricalPullback F G} (f : x ⟶ y) : IsIso f ↔ IsIso f.fst ∧ IsIso f.snd

@[reducible, inline]

abbrev CategoryTheory.Limits.CategoricalPullback.CatCommSqOver {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] : Type (max (max (max (max (max u₁ u₄) v₁) v₄) (max (max u₃ u₄) v₃) v₄) u₄ v₂)

The data of a categorical commutative square over a cospan F, G with cone point X is that of a functor T : X ⥤ A, a functor L : X ⥤ C, and a CatCommSqOver T L F G. Note that this is exactly what an object of ((whiskeringRight X A B).obj F) ⊡ ((whiskeringRight X C B).obj G) is, so CatCommSqOver F G X is in fact an abbreviation for ((whiskeringRight X A B).obj F) ⊡ ((whiskeringRight X C B).obj G).

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.asSquare {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} {G : Functor C B} (X : Type u₄) [Category.{v₄, u₄} X] (S : CatCommSqOver F G X) : CatCommSq S.fst S.snd F G

Interpret a CatCommSqOver F G X X as a CatCommSq.

Equations

• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.asSquare X S = { iso := S.iso }

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.asSquare_iso {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} {G : Functor C B} (X : Type u₄) [Category.{v₄, u₄} X] (S : CatCommSqOver F G X) : CatCommSq.iso S.fst S.snd F G = S.iso

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.iso_hom_naturality {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} {G : Functor C B} (X : Type u₄) [Category.{v₄, u₄} X] (S : CatCommSqOver F G X) {x x' : X} (f : x ⟶ x') : CategoryStruct.comp (F.map (S.fst.map f)) (S.iso.hom.app x') = CategoryStruct.comp (S.iso.hom.app x) (G.map (S.snd.map f))

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.iso_hom_naturality_assoc {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} {G : Functor C B} (X : Type u₄) [Category.{v₄, u₄} X] (S : CatCommSqOver F G X) {x x' : X} (f : x ⟶ x') {Z : B} (h : (((Functor.whiskeringRight X C B).obj G).obj S.snd).obj x' ⟶ Z) : CategoryStruct.comp (F.map (S.fst.map f)) (CategoryStruct.comp (S.iso.hom.app x') h) = CategoryStruct.comp (S.iso.hom.app x) (CategoryStruct.comp (G.map (S.snd.map f)) h)

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.w_app {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} {G : Functor C B} (X : Type u₄) [Category.{v₄, u₄} X] {S S' : CatCommSqOver F G X} (φ : S ⟶ S') (x : X) : CategoryStruct.comp (F.map (φ.fst.app x)) (S'.iso.hom.app x) = CategoryStruct.comp (S.iso.hom.app x) (G.map (φ.snd.app x))

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.w_app_assoc {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} {G : Functor C B} (X : Type u₄) [Category.{v₄, u₄} X] {S S' : CatCommSqOver F G X} (φ : S ⟶ S') (x : X) {Z : B} (h : (((Functor.whiskeringRight X C B).obj G).obj S'.snd).obj x ⟶ Z) : CategoryStruct.comp (F.map (φ.fst.app x)) (CategoryStruct.comp (S'.iso.hom.app x) h) = CategoryStruct.comp (S.iso.hom.app x) (CategoryStruct.comp (G.map (φ.snd.app x)) h)

@[reducible, inline]

abbrev CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.fstFunctor {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] : Functor (CatCommSqOver F G X) (Functor X A)

The "first projection" of a CatCommSqOver as a functor.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.sndFunctor {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] : Functor (CatCommSqOver F G X) (Functor X C)

The "second projection" of a CatCommSqOver as a functor.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.e {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] : (fstFunctor F G X).comp ((Functor.whiskeringRight X A B).obj F) ≅ (sndFunctor F G X).comp ((Functor.whiskeringRight X C B).obj G)

The structure isompophism of a CatCommSqOver as a natural transformation.

Equations

• CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.e F G X = CategoryTheory.NatIso.ofComponents (fun (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) => S.iso) ⋯

def CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] : Functor (Functor X (CategoricalPullback F G)) (CatCommSqOver F G X)

Interpret a functor to the categorical pullback as a CatCommSqOver.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_obj_snd_obj {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] (J : Functor X (CategoricalPullback F G)) (X✝ : X) : ((toCatCommSqOver F G X).obj J).snd.obj X✝ = (J.obj X✝).snd

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_obj_iso_inv_app {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] (J : Functor X (CategoricalPullback F G)) (X✝ : X) : ((toCatCommSqOver F G X).obj J).iso.inv.app X✝ = (J.obj X✝).iso.inv

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_obj_iso_hom_app {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] (J : Functor X (CategoricalPullback F G)) (X✝ : X) : ((toCatCommSqOver F G X).obj J).iso.hom.app X✝ = (J.obj X✝).iso.hom

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_obj_fst_map {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] (J : Functor X (CategoricalPullback F G)) {X✝ Y✝ : X} (f : X✝ ⟶ Y✝) : ((toCatCommSqOver F G X).obj J).fst.map f = (J.map f).fst

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_map_snd_app {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] {J J' : Functor X (CategoricalPullback F G)} (F✝ : J ⟶ J') (X✝ : X) : ((toCatCommSqOver F G X).map F✝).snd.app X✝ = (F✝.app X✝).snd

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_obj_snd_map {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] (J : Functor X (CategoricalPullback F G)) {X✝ Y✝ : X} (f : X✝ ⟶ Y✝) : ((toCatCommSqOver F G X).obj J).snd.map f = (J.map f).snd

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_map_fst_app {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] {J J' : Functor X (CategoricalPullback F G)} (F✝ : J ⟶ J') (X✝ : X) : ((toCatCommSqOver F G X).map F✝).fst.app X✝ = (F✝.app X✝).fst

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_obj_fst_obj {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] (J : Functor X (CategoricalPullback F G)) (X✝ : X) : ((toCatCommSqOver F G X).obj J).fst.obj X✝ = (J.obj X✝).fst

def CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] : Functor (CatCommSqOver F G X) (Functor X (CategoricalPullback F G))

Interpret a CatCommSqOver as a functor to the categorical pullback.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_map_app_snd {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] {S S' : CatCommSqOver F G X} (φ : S ⟶ S') (x : X) : (((toFunctorToCategoricalPullback F G X).map φ).app x).snd = φ.snd.app x

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_obj_obj_iso_hom {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] (S : CatCommSqOver F G X) (x : X) : (((toFunctorToCategoricalPullback F G X).obj S).obj x).iso.hom = S.iso.hom.app x

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_obj_obj_fst {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] (S : CatCommSqOver F G X) (x : X) : (((toFunctorToCategoricalPullback F G X).obj S).obj x).fst = S.fst.obj x

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_obj_obj_iso_inv {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] (S : CatCommSqOver F G X) (x : X) : (((toFunctorToCategoricalPullback F G X).obj S).obj x).iso.inv = S.iso.inv.app x

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_obj_map_fst {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] (S : CatCommSqOver F G X) {x y : X} (f : x ⟶ y) : (((toFunctorToCategoricalPullback F G X).obj S).map f).fst = S.fst.map f

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_obj_map_snd {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] (S : CatCommSqOver F G X) {x y : X} (f : x ⟶ y) : (((toFunctorToCategoricalPullback F G X).obj S).map f).snd = S.snd.map f

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_map_app_fst {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] {S S' : CatCommSqOver F G X} (φ : S ⟶ S') (x : X) : (((toFunctorToCategoricalPullback F G X).map φ).app x).fst = φ.fst.app x

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.toFunctorToCategoricalPullback_obj_obj_snd {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] (S : CatCommSqOver F G X) (x : X) : (((toFunctorToCategoricalPullback F G X).obj S).obj x).snd = S.snd.obj x

def CategoryTheory.Limits.CategoricalPullback.functorEquiv {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] : Functor X (CategoricalPullback F G) ≌ CatCommSqOver F G X

The universal property of categorical pullbacks, stated as an equivalence of categories between functors X ⥤ (F ⊡ G) and categorical commutative squares over X.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] : (functorEquiv F G X).functor = toCatCommSqOver F G X

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.functorEquiv_inverse {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] : (functorEquiv F G X).inverse = CatCommSqOver.toFunctorToCategoricalPullback F G X

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.functorEquiv_counitIso {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] : (functorEquiv F G X).counitIso = NatIso.ofComponents (fun (x : CatCommSqOver F G X) => mkIso (NatIso.ofComponents (fun (x_1 : X) => Iso.refl ((((CatCommSqOver.toFunctorToCategoricalPullback F G X).comp (toCatCommSqOver F G X)).obj x).fst.obj x_1)) ⋯) (NatIso.ofComponents (fun (x_1 : X) => Iso.refl ((((CatCommSqOver.toFunctorToCategoricalPullback F G X).comp (toCatCommSqOver F G X)).obj x).snd.obj x_1)) ⋯) ⋯) ⋯

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.functorEquiv_unitIso {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) (G : Functor C B) (X : Type u₄) [Category.{v₄, u₄} X] : (functorEquiv F G X).unitIso = NatIso.ofComponents (fun (x : Functor X (CategoricalPullback F G)) => NatIso.ofComponents (fun (x_1 : X) => mkIso (Iso.refl (((Functor.id (Functor X (CategoricalPullback F G))).obj x).obj x_1).fst) (Iso.refl (((Functor.id (Functor X (CategoricalPullback F G))).obj x).obj x_1).snd) ⋯) ⋯) ⋯

def CategoryTheory.Limits.CategoricalPullback.mkNatIso {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} {G : Functor C B} {X : Type u₄} [Category.{v₄, u₄} X] {J K : Functor X (CategoricalPullback F G)} (e₁ : J.comp (π₁ F G) ≅ K.comp (π₁ F G)) (e₂ : J.comp (π₂ F G) ≅ K.comp (π₂ F G)) (coh : CategoryStruct.comp (Functor.whiskerRight e₁.hom F) (CategoryStruct.comp (K.associator (π₁ F G) F).hom (CategoryStruct.comp (K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom) (K.associator (π₂ F G) G).inv)) = CategoryStruct.comp (J.associator (π₁ F G) F).hom (CategoryStruct.comp (J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom) (CategoryStruct.comp (J.associator (π₂ F G) G).inv (Functor.whiskerRight e₂.hom G))) := by aesop_cat) : J ≅ K

A constructor for natural isomorphisms of functors X ⥤ CategoricalPullback: to construct such an isomorphism, it suffices to produce isomorphisms after whiskering with the projections, and compatible with the canonical 2-commutative square .

Equations

• CategoryTheory.Limits.CategoricalPullback.mkNatIso e₁ e₂ coh = CategoryTheory.NatIso.ofComponents (fun (x : X) => CategoryTheory.Limits.CategoricalPullback.mkIso (e₁.app x) (e₂.app x) ⋯) ⋯

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.mkNatIso_inv_app_snd {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} {G : Functor C B} {X : Type u₄} [Category.{v₄, u₄} X] {J K : Functor X (CategoricalPullback F G)} (e₁ : J.comp (π₁ F G) ≅ K.comp (π₁ F G)) (e₂ : J.comp (π₂ F G) ≅ K.comp (π₂ F G)) (coh : CategoryStruct.comp (Functor.whiskerRight e₁.hom F) (CategoryStruct.comp (K.associator (π₁ F G) F).hom (CategoryStruct.comp (K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom) (K.associator (π₂ F G) G).inv)) = CategoryStruct.comp (J.associator (π₁ F G) F).hom (CategoryStruct.comp (J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom) (CategoryStruct.comp (J.associator (π₂ F G) G).inv (Functor.whiskerRight e₂.hom G))) := by aesop_cat) (X✝ : X) : ((mkNatIso e₁ e₂ coh).inv.app X✝).snd = e₂.inv.app X✝

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.mkNatIso_hom_app_fst {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} {G : Functor C B} {X : Type u₄} [Category.{v₄, u₄} X] {J K : Functor X (CategoricalPullback F G)} (e₁ : J.comp (π₁ F G) ≅ K.comp (π₁ F G)) (e₂ : J.comp (π₂ F G) ≅ K.comp (π₂ F G)) (coh : CategoryStruct.comp (Functor.whiskerRight e₁.hom F) (CategoryStruct.comp (K.associator (π₁ F G) F).hom (CategoryStruct.comp (K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom) (K.associator (π₂ F G) G).inv)) = CategoryStruct.comp (J.associator (π₁ F G) F).hom (CategoryStruct.comp (J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom) (CategoryStruct.comp (J.associator (π₂ F G) G).inv (Functor.whiskerRight e₂.hom G))) := by aesop_cat) (X✝ : X) : ((mkNatIso e₁ e₂ coh).hom.app X✝).fst = e₁.hom.app X✝

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.mkNatIso_inv_app_fst {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} {G : Functor C B} {X : Type u₄} [Category.{v₄, u₄} X] {J K : Functor X (CategoricalPullback F G)} (e₁ : J.comp (π₁ F G) ≅ K.comp (π₁ F G)) (e₂ : J.comp (π₂ F G) ≅ K.comp (π₂ F G)) (coh : CategoryStruct.comp (Functor.whiskerRight e₁.hom F) (CategoryStruct.comp (K.associator (π₁ F G) F).hom (CategoryStruct.comp (K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom) (K.associator (π₂ F G) G).inv)) = CategoryStruct.comp (J.associator (π₁ F G) F).hom (CategoryStruct.comp (J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom) (CategoryStruct.comp (J.associator (π₂ F G) G).inv (Functor.whiskerRight e₂.hom G))) := by aesop_cat) (X✝ : X) : ((mkNatIso e₁ e₂ coh).inv.app X✝).fst = e₁.inv.app X✝

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.mkNatIso_hom_app_snd {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} {G : Functor C B} {X : Type u₄} [Category.{v₄, u₄} X] {J K : Functor X (CategoricalPullback F G)} (e₁ : J.comp (π₁ F G) ≅ K.comp (π₁ F G)) (e₂ : J.comp (π₂ F G) ≅ K.comp (π₂ F G)) (coh : CategoryStruct.comp (Functor.whiskerRight e₁.hom F) (CategoryStruct.comp (K.associator (π₁ F G) F).hom (CategoryStruct.comp (K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom) (K.associator (π₂ F G) G).inv)) = CategoryStruct.comp (J.associator (π₁ F G) F).hom (CategoryStruct.comp (J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom) (CategoryStruct.comp (J.associator (π₂ F G) G).inv (Functor.whiskerRight e₂.hom G))) := by aesop_cat) (X✝ : X) : ((mkNatIso e₁ e₂ coh).hom.app X✝).snd = e₂.hom.app X✝

theorem CategoryTheory.Limits.CategoricalPullback.natTrans_ext {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} {G : Functor C B} {X : Type u₄} [Category.{v₄, u₄} X] {J K : Functor X (CategoricalPullback F G)} {α β : J ⟶ K} (e₁ : Functor.whiskerRight α (π₁ F G) = Functor.whiskerRight β (π₁ F G)) (e₂ : Functor.whiskerRight α (π₂ F G) = Functor.whiskerRight β (π₂ F G)) : α = β

To check equality of two natural transformations of functors to a CategoricalPullback, it suffices to do so after whiskering with the projections.

theorem CategoryTheory.Limits.CategoricalPullback.natTrans_ext_iff {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} {G : Functor C B} {X : Type u₄} [Category.{v₄, u₄} X] {J K : Functor X (CategoricalPullback F G)} {α β : J ⟶ K} : α = β ↔ Functor.whiskerRight α (π₁ F G) = Functor.whiskerRight β (π₁ F G) ∧ Functor.whiskerRight α (π₂ F G) = Functor.whiskerRight β (π₂ F G)

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.toCatCommSqOver_mapIso_mkNatIso_eq_mkIso {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} {G : Functor C B} {X : Type u₄} [Category.{v₄, u₄} X] {J K : Functor X (CategoricalPullback F G)} (e₁ : J.comp (π₁ F G) ≅ K.comp (π₁ F G)) (e₂ : J.comp (π₂ F G) ≅ K.comp (π₂ F G)) (coh : CategoryStruct.comp (Functor.whiskerRight e₁.hom F) (CategoryStruct.comp (K.associator (π₁ F G) F).hom (CategoryStruct.comp (K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom) (K.associator (π₂ F G) G).inv)) = CategoryStruct.comp (J.associator (π₁ F G) F).hom (CategoryStruct.comp (J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom) (CategoryStruct.comp (J.associator (π₂ F G) G).inv (Functor.whiskerRight e₂.hom G))) := by aesop_cat) : (toCatCommSqOver F G X).mapIso (mkNatIso e₁ e₂ coh) = mkIso e₁ e₂ ⋯

theorem CategoryTheory.Limits.CategoricalPullback.mkNatIso_eq {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} {G : Functor C B} {X : Type u₄} [Category.{v₄, u₄} X] {J K : Functor X (CategoricalPullback F G)} (e₁ : J.comp (π₁ F G) ≅ K.comp (π₁ F G)) (e₂ : J.comp (π₂ F G) ≅ K.comp (π₂ F G)) (coh : CategoryStruct.comp (Functor.whiskerRight e₁.hom F) (CategoryStruct.comp (K.associator (π₁ F G) F).hom (CategoryStruct.comp (K.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom) (K.associator (π₂ F G) G).inv)) = CategoryStruct.comp (J.associator (π₁ F G) F).hom (CategoryStruct.comp (J.whiskerLeft (CatCommSq.iso (π₁ F G) (π₂ F G) F G).hom) (CategoryStruct.comp (J.associator (π₂ F G) G).inv (Functor.whiskerRight e₂.hom G))) := by aesop_cat) : mkNatIso e₁ e₂ coh = (functorEquiv F G X).fullyFaithfulFunctor.preimageIso (mkIso e₁ e₂ ⋯)

Comparing mkNatIso with the corresponding construction one can deduce from functorEquiv.