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 isomorphisms

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_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

@[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_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

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)

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)

@[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.π₂_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

@[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

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_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

@[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

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 cat_disch) : 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 cat_disch) : (mkIso eₗ eᵣ w).inv.snd = 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 cat_disch) : (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 cat_disch) : (mkIso eₗ eᵣ w).hom.snd = eᵣ.hom

@[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 cat_disch) : (mkIso eₗ eᵣ w).inv.fst = eₗ.inv

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 isomorphism 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_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

@[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_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_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_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_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

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_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_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_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_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_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

@[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_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

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_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) ⋯) ⋯) ⋯

@[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_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_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

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 cat_disch) : 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_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 cat_disch) (X✝ : X) : ((mkNatIso e₁ e₂ coh).hom.app X✝).snd = 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 cat_disch) (X✝ : X) : ((mkNatIso e₁ e₂ coh).inv.app X✝).fst = e₁.inv.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 cat_disch) (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 cat_disch) (X✝ : X) : ((mkNatIso e₁ e₂ coh).hom.app X✝).fst = 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 cat_disch) : (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 cat_disch) : mkNatIso e₁ e₂ coh = (functorEquiv F G X).fullyFaithfulFunctor.preimageIso (mkIso e₁ e₂ ⋯)

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

def CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform {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} {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 (CatCospanTransform F G F₁ G₁) (Functor (CatCommSqOver F G X) (CatCommSqOver F₁ G₁ X))

Functorially transform a CatCommSqOver F G X by whiskering it with a CatCospanTransform.

Equations

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

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_obj_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} {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] (ψ : CatCospanTransform F G F₁ G₁) (S : CatCommSqOver F G X) : (((transform X).obj ψ).obj S).iso = S.fst.associator ψ.left F₁ ≪≫ S.fst.isoWhiskerLeft (CatCommSq.iso F ψ.left ψ.base F₁).symm ≪≫ (S.fst.associator F ψ.base).symm ≪≫ Functor.isoWhiskerRight S.iso ψ.base ≪≫ S.snd.isoWhiskerLeft (CatCommSq.iso G ψ.right ψ.base G₁) ≪≫ (S.snd.associator ψ.right G₁).symm

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_app_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} {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] {ψ ψ' : CatCospanTransform F G F₁ G₁} (η : ψ ⟶ ψ') (S : CatCommSqOver F G X) (y : X) : (((transform X).map η).app S).fst.app y = η.left.app (S.fst.obj y)

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_app_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} {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] {ψ ψ' : CatCospanTransform F G F₁ G₁} (η : ψ ⟶ ψ') (S : CatCommSqOver F G X) (y : X) : (((transform X).map η).app S).snd.app y = η.right.app (S.snd.obj y)

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_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} {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] (ψ : CatCospanTransform F G F₁ G₁) {x y : CatCommSqOver F G X} (f : x ⟶ y) : (((transform X).obj ψ).map f).fst = Functor.whiskerRight f.fst ψ.left

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_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} {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] (ψ : CatCospanTransform F G F₁ G₁) {x y : CatCommSqOver F G X} (f : x ⟶ y) : (((transform X).obj ψ).map f).snd = Functor.whiskerRight f.snd ψ.right

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_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} {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] (ψ : CatCospanTransform F G F₁ G₁) (S : CatCommSqOver F G X) : (((transform X).obj ψ).obj S).snd = S.snd.comp ψ.right

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_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} {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] (ψ : CatCospanTransform F G F₁ G₁) (S : CatCommSqOver F G X) : (((transform X).obj ψ).obj S).fst = S.fst.comp ψ.left

def CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp {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} {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₁} {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] (ψ : CatCospanTransform F G F₁ G₁) (ψ' : CatCospanTransform F₁ G₁ F₂ G₂) : (transform X).obj (ψ.comp ψ') ≅ ((transform X).obj ψ).comp ((transform X).obj ψ')

The construction CatCommSqOver.transform respects vertical composition of CatCospanTransforms.

Equations

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

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp_hom_app_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} {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₁} {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] (ψ : CatCospanTransform F G F₁ G₁) (ψ' : CatCospanTransform F₁ G₁ F₂ G₂) (X✝ : CatCommSqOver F G X) (x✝ : X) : ((transformObjComp X ψ ψ').hom.app X✝).snd.app x✝ = CategoryStruct.id (ψ'.right.obj (ψ.right.obj (X✝.snd.obj x✝)))

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp_hom_app_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} {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₁} {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] (ψ : CatCospanTransform F G F₁ G₁) (ψ' : CatCospanTransform F₁ G₁ F₂ G₂) (X✝ : CatCommSqOver F G X) (x✝ : X) : ((transformObjComp X ψ ψ').hom.app X✝).fst.app x✝ = CategoryStruct.id (ψ'.left.obj (ψ.left.obj (X✝.fst.obj x✝)))

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp_inv_app_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} {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₁} {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] (ψ : CatCospanTransform F G F₁ G₁) (ψ' : CatCospanTransform F₁ G₁ F₂ G₂) (X✝ : CatCommSqOver F G X) (x✝ : X) : ((transformObjComp X ψ ψ').inv.app X✝).fst.app x✝ = CategoryStruct.id (ψ'.left.obj (ψ.left.obj (X✝.fst.obj x✝)))

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjComp_inv_app_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} {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₁} {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] (ψ : CatCospanTransform F G F₁ G₁) (ψ' : CatCospanTransform F₁ G₁ F₂ G₂) (X✝ : CatCommSqOver F G X) (x✝ : X) : ((transformObjComp X ψ ψ').inv.app X✝).snd.app x✝ = CategoryStruct.id (ψ'.right.obj (ψ.right.obj (X✝.snd.obj x✝)))

def CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (X : Type u₄) [Category.{v₄, u₄} X] (F : Functor A B) (G : Functor C B) : (transform X).obj (CatCospanTransform.id F G) ≅ Functor.id (CatCommSqOver F G X)

The construction CatCommSqOver.transform respects the identity CatCospanTransforms.

Equations

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

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId_inv_app_snd_app {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (X : Type u₄) [Category.{v₄, u₄} X] (F : Functor A B) (G : Functor C B) (X✝ : CatCommSqOver F G X) (X✝¹ : X) : ((transformObjId X F G).inv.app X✝).snd.app X✝¹ = CategoryStruct.id (X✝.snd.obj X✝¹)

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId_hom_app_fst_app {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (X : Type u₄) [Category.{v₄, u₄} X] (F : Functor A B) (G : Functor C B) (X✝ : CatCommSqOver F G X) (X✝¹ : X) : ((transformObjId X F G).hom.app X✝).fst.app X✝¹ = CategoryStruct.id (X✝.fst.obj X✝¹)

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId_inv_app_fst_app {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (X : Type u₄) [Category.{v₄, u₄} X] (F : Functor A B) (G : Functor C B) (X✝ : CatCommSqOver F G X) (X✝¹ : X) : ((transformObjId X F G).inv.app X✝).fst.app X✝¹ = CategoryStruct.id (X✝.fst.obj X✝¹)

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId_hom_app_snd_app {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] (X : Type u₄) [Category.{v₄, u₄} X] (F : Functor A B) (G : Functor C B) (X✝ : CatCommSqOver F G X) (X✝¹ : X) : ((transformObjId X F G).hom.app X✝).snd.app X✝¹ = CategoryStruct.id (X✝.snd.obj X✝¹)

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_whiskerLeft {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} {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₁} {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] (ψ : CatCospanTransform F G F₁ G₁) {φ φ' : CatCospanTransform F₁ G₁ F₂ G₂} (α : φ ⟶ φ') : (transform X).map (CatCospanTransformMorphism.whiskerLeft ψ α) = CategoryStruct.comp (transformObjComp X ψ φ).hom (CategoryStruct.comp (((transform X).obj ψ).whiskerLeft ((transform X).map α)) (transformObjComp X ψ φ').inv)

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_whiskerRight {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} {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₁} {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] {ψ ψ' : CatCospanTransform F G F₁ G₁} (α : ψ ⟶ ψ') (φ : CatCospanTransform F₁ G₁ F₂ G₂) : (transform X).map (CatCospanTransformMorphism.whiskerRight α φ) = CategoryStruct.comp (transformObjComp X ψ φ).hom (CategoryStruct.comp (Functor.whiskerRight ((transform X).map α) ((transform X).obj φ)) (transformObjComp X ψ' φ).inv)

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_associator {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} {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₁} {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₂} {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] (ψ : CatCospanTransform F G F₁ G₁) (φ : CatCospanTransform F₁ G₁ F₂ G₂) (τ : CatCospanTransform F₂ G₂ F₃ G₃) : (transform X).map (ψ.associator φ τ).hom = CategoryStruct.comp (transformObjComp X (ψ.comp φ) τ).hom (CategoryStruct.comp (Functor.whiskerRight (transformObjComp X ψ φ).hom ((transform X).obj τ)) (CategoryStruct.comp (((transform X).obj ψ).associator ((transform X).obj φ) ((transform X).obj τ)).hom (CategoryStruct.comp (((transform X).obj ψ).whiskerLeft (transformObjComp X φ τ).inv) (transformObjComp X ψ (φ.comp τ)).inv)))

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_leftUnitor {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} {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] (ψ : CatCospanTransform F G F₁ G₁) : (transform X).map ψ.leftUnitor.hom = CategoryStruct.comp (transformObjComp X (CatCospanTransform.id F G) ψ).hom (CategoryStruct.comp (Functor.whiskerRight (transformObjId X F G).hom ((transform X).obj ψ)) ((transform X).obj ψ).leftUnitor.hom)

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_map_rightUnitor {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} {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] (ψ : CatCospanTransform F G F₁ G₁) : (transform X).map ψ.rightUnitor.hom = CategoryStruct.comp (transformObjComp X ψ (CatCospanTransform.id F₁ G₁)).hom (CategoryStruct.comp (((transform X).obj ψ).whiskerLeft (transformObjId X F₁ G₁).hom) ((transform X).obj ψ).rightUnitor.hom)

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

A functor U : X ⥤ Y (functorially) induces a functor CatCommSqOver F G Y ⥤ CatCommSqOver F G X by whiskering left the underlying categorical commutative square by U.

Equations

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

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_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₄} {Y : Type u₅} [Category.{v₄, u₄} X] [Category.{v₅, u₅} Y] (U : Functor X Y) (S : CatCommSqOver F G Y) : (((precompose F G).obj U).obj S).snd = U.comp S.snd

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_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₄} {Y : Type u₅} [Category.{v₄, u₄} X] [Category.{v₅, u₅} Y] {U V : Functor X Y} (α : U ⟶ V) (x : CatCommSqOver F G Y) : (((precompose F G).map α).app x).fst = Functor.whiskerRight α x.fst

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_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₄} {Y : Type u₅} [Category.{v₄, u₄} X] [Category.{v₅, u₅} Y] {U V : Functor X Y} (α : U ⟶ V) (x : CatCommSqOver F G Y) : (((precompose F G).map α).app x).snd = Functor.whiskerRight α x.snd

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_obj_obj_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₄} {Y : Type u₅} [Category.{v₄, u₄} X] [Category.{v₅, u₅} Y] (U : Functor X Y) (S : CatCommSqOver F G Y) : (((precompose F G).obj U).obj S).iso = U.associator S.fst F ≪≫ U.isoWhiskerLeft S.iso ≪≫ (U.associator S.snd G).symm

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_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₄} {Y : Type u₅} [Category.{v₄, u₄} X] [Category.{v₅, u₅} Y] (U : Functor X Y) {S S' : CatCommSqOver F G Y} (φ : S ⟶ S') : (((precompose F G).obj U).map φ).fst = U.whiskerLeft φ.fst

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_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₄} {Y : Type u₅} [Category.{v₄, u₄} X] [Category.{v₅, u₅} Y] (U : Functor X Y) {S S' : CatCommSqOver F G Y} (φ : S ⟶ S') : (((precompose F G).obj U).map φ).snd = U.whiskerLeft φ.snd

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_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₄} {Y : Type u₅} [Category.{v₄, u₄} X] [Category.{v₅, u₅} Y] (U : Functor X Y) (S : CatCommSqOver F G Y) : (((precompose F G).obj U).obj S).fst = U.comp S.fst

def CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId {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] : (precompose F G).obj (Functor.id X) ≅ Functor.id (CatCommSqOver F G X)

The construction precompose respects functor identities.

Equations

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

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId_hom_app_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] (X✝ : CatCommSqOver F G X) (X✝¹ : X) : ((precomposeObjId F G X).hom.app X✝).fst.app X✝¹ = CategoryStruct.id (X✝.fst.obj X✝¹)

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId_hom_app_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] (X✝ : CatCommSqOver F G X) (X✝¹ : X) : ((precomposeObjId F G X).hom.app X✝).snd.app X✝¹ = CategoryStruct.id (X✝.snd.obj X✝¹)

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId_inv_app_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] (X✝ : CatCommSqOver F G X) (X✝¹ : X) : ((precomposeObjId F G X).inv.app X✝).fst.app X✝¹ = CategoryStruct.id (X✝.fst.obj X✝¹)

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjId_inv_app_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] (X✝ : CatCommSqOver F G X) (X✝¹ : X) : ((precomposeObjId F G X).inv.app X✝).snd.app X✝¹ = CategoryStruct.id (X✝.snd.obj X✝¹)

def CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp {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₄} {Y : Type u₅} {Z : Type u₆} [Category.{v₄, u₄} X] [Category.{v₅, u₅} Y] [Category.{v₆, u₆} Z] (U : Functor X Y) (V : Functor Y Z) : (precompose F G).obj (U.comp V) ≅ ((precompose F G).obj V).comp ((precompose F G).obj U)

The construction precompose respects functor composition.

Equations

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

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp_hom_app_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₄} {Y : Type u₅} {Z : Type u₆} [Category.{v₄, u₄} X] [Category.{v₅, u₅} Y] [Category.{v₆, u₆} Z] (U : Functor X Y) (V : Functor Y Z) (X✝ : CatCommSqOver F G Z) (x✝ : X) : ((precomposeObjComp F G U V).hom.app X✝).fst.app x✝ = CategoryStruct.id (X✝.fst.obj (V.obj (U.obj x✝)))

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp_hom_app_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₄} {Y : Type u₅} {Z : Type u₆} [Category.{v₄, u₄} X] [Category.{v₅, u₅} Y] [Category.{v₆, u₆} Z] (U : Functor X Y) (V : Functor Y Z) (X✝ : CatCommSqOver F G Z) (x✝ : X) : ((precomposeObjComp F G U V).hom.app X✝).snd.app x✝ = CategoryStruct.id (X✝.snd.obj (V.obj (U.obj x✝)))

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp_inv_app_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₄} {Y : Type u₅} {Z : Type u₆} [Category.{v₄, u₄} X] [Category.{v₅, u₅} Y] [Category.{v₆, u₆} Z] (U : Functor X Y) (V : Functor Y Z) (X✝ : CatCommSqOver F G Z) (x✝ : X) : ((precomposeObjComp F G U V).inv.app X✝).snd.app x✝ = CategoryStruct.id (X✝.snd.obj (V.obj (U.obj x✝)))

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjComp_inv_app_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₄} {Y : Type u₅} {Z : Type u₆} [Category.{v₄, u₄} X] [Category.{v₅, u₅} Y] [Category.{v₆, u₆} Z] (U : Functor X Y) (V : Functor Y Z) (X✝ : CatCommSqOver F G Z) (x✝ : X) : ((precomposeObjComp F G U V).inv.app X✝).fst.app x✝ = CategoryStruct.id (X✝.fst.obj (V.obj (U.obj x✝)))

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_whiskerLeft {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₄} {Y : Type u₅} {Z : Type u₆} [Category.{v₄, u₄} X] [Category.{v₅, u₅} Y] [Category.{v₆, u₆} Z] (U : Functor X Y) {V W : Functor Y Z} (α : V ⟶ W) : (precompose F G).map (U.whiskerLeft α) = CategoryStruct.comp (precomposeObjComp F G U V).hom (CategoryStruct.comp (Functor.whiskerRight ((precompose F G).map α) ((precompose F G).obj U)) (precomposeObjComp F G U W).inv)

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_whiskerRight {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₄} {Y : Type u₅} {Z : Type u₆} [Category.{v₄, u₄} X] [Category.{v₅, u₅} Y] [Category.{v₆, u₆} Z] {U V : Functor X Y} (α : U ⟶ V) (W : Functor Y Z) : (precompose F G).map (Functor.whiskerRight α W) = CategoryStruct.comp (precomposeObjComp F G U W).hom (CategoryStruct.comp (((precompose F G).obj W).whiskerLeft ((precompose F G).map α)) (precomposeObjComp F G V W).inv)

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_associator {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₄} {Y : Type u₅} {Z : Type u₆} [Category.{v₄, u₄} X] [Category.{v₅, u₅} Y] [Category.{v₆, u₆} Z] {T : Type u₇} [Category.{v₇, u₇} T] (U : Functor X Y) (V : Functor Y Z) (W : Functor Z T) : (precompose F G).map (U.associator V W).hom = CategoryStruct.comp (precomposeObjComp F G (U.comp V) W).hom (CategoryStruct.comp (((precompose F G).obj W).whiskerLeft (precomposeObjComp F G U V).hom) (CategoryStruct.comp (((precompose F G).obj W).associator ((precompose F G).obj V) ((precompose F G).obj U)).inv (CategoryStruct.comp (Functor.whiskerRight (precomposeObjComp F G V W).inv ((precompose F G).obj U)) (precomposeObjComp F G U (V.comp W)).inv)))

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_leftUnitor {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₄} {Y : Type u₅} [Category.{v₄, u₄} X] [Category.{v₅, u₅} Y] (U : Functor X Y) : (precompose F G).map U.leftUnitor.hom = CategoryStruct.comp (precomposeObjComp F G (Functor.id X) U).hom (CategoryStruct.comp (((precompose F G).obj U).whiskerLeft (precomposeObjId F G X).hom) ((precompose F G).obj U).rightUnitor.hom)

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose_map_rightUnitor {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₄} {Y : Type u₅} [Category.{v₄, u₄} X] [Category.{v₅, u₅} Y] (U : Functor X Y) : (precompose F G).map U.rightUnitor.hom = CategoryStruct.comp (precomposeObjComp F G U (Functor.id Y)).hom (CategoryStruct.comp (Functor.whiskerRight (precomposeObjId F G Y).hom ((precompose F G).obj U)) ((precompose F G).obj U).leftUnitor.hom)

instance CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare {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} {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₇} {Y : Type u₈} [Category.{v₇, u₇} X] [Category.{v₈, u₈} Y] (ψ : CatCospanTransform F G F₁ G₁) (U : Functor X Y) : CatCommSq ((precompose F G).obj U) ((transform Y).obj ψ) ((transform X).obj ψ) ((precompose F₁ G₁).obj U)

The canonical compatibility square between (the object components of) precompose and transform. This is a "naturality square" if we think as transform _|>.obj _ as the (app component of the) map component of a pseudofunctor from the bicategory of categorical cospans with value in pseudofunctors (its value on the categorical cospan F, G being the pseudofunctor precompose F G|>.obj _).

Equations

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

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_app_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} {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₇} {Y : Type u₈} [Category.{v₇, u₇} X] [Category.{v₈, u₈} Y] (ψ : CatCospanTransform F G F₁ G₁) (U : Functor X Y) (X✝ : CatCommSqOver F G Y) (x✝ : X) : ((CatCommSq.iso ((precompose F G).obj U) ((transform Y).obj ψ) ((transform X).obj ψ) ((precompose F₁ G₁).obj U)).hom.app X✝).fst.app x✝ = CategoryStruct.id (ψ.left.obj (X✝.fst.obj (U.obj x✝)))

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_inv_app_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} {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₇} {Y : Type u₈} [Category.{v₇, u₇} X] [Category.{v₈, u₈} Y] (ψ : CatCospanTransform F G F₁ G₁) (U : Functor X Y) (X✝ : CatCommSqOver F G Y) (x✝ : X) : ((CatCommSq.iso ((precompose F G).obj U) ((transform Y).obj ψ) ((transform X).obj ψ) ((precompose F₁ G₁).obj U)).inv.app X✝).snd.app x✝ = CategoryStruct.id (ψ.right.obj (X✝.snd.obj (U.obj x✝)))

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_inv_app_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} {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₇} {Y : Type u₈} [Category.{v₇, u₇} X] [Category.{v₈, u₈} Y] (ψ : CatCospanTransform F G F₁ G₁) (U : Functor X Y) (X✝ : CatCommSqOver F G Y) (x✝ : X) : ((CatCommSq.iso ((precompose F G).obj U) ((transform Y).obj ψ) ((transform X).obj ψ) ((precompose F₁ G₁).obj U)).inv.app X✝).fst.app x✝ = CategoryStruct.id (ψ.left.obj (X✝.fst.obj (U.obj x✝)))

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_app_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} {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₇} {Y : Type u₈} [Category.{v₇, u₇} X] [Category.{v₈, u₈} Y] (ψ : CatCospanTransform F G F₁ G₁) (U : Functor X Y) (X✝ : CatCommSqOver F G Y) (x✝ : X) : ((CatCommSq.iso ((precompose F G).obj U) ((transform Y).obj ψ) ((transform X).obj ψ) ((precompose F₁ G₁).obj U)).hom.app X✝).snd.app x✝ = CategoryStruct.id (ψ.right.obj (X✝.snd.obj (U.obj x✝)))

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_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} {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₇} {Y : Type u₈} [Category.{v₇, u₇} X] [Category.{v₈, u₈} Y] (ψ : CatCospanTransform F G F₁ G₁) {U V : Functor X Y} (α : U ⟶ V) : CategoryStruct.comp (Functor.whiskerRight ((precompose F G).map α) ((transform X).obj ψ)) (CatCommSq.iso ((precompose F G).obj V) ((transform Y).obj ψ) ((transform X).obj ψ) ((precompose F₁ G₁).obj V)).hom = CategoryStruct.comp (CatCommSq.iso ((precompose F G).obj U) ((transform Y).obj ψ) ((transform X).obj ψ) ((precompose F₁ G₁).obj U)).hom (((transform Y).obj ψ).whiskerLeft ((precompose F₁ G₁).map α))

The square precomposeObjTransformObjSquare is itself natural.

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_id {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} {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₁} (ψ : CatCospanTransform F G F₁ G₁) (X : Type u₇) [Category.{v₇, u₇} X] : CategoryStruct.comp (CatCommSq.iso ((precompose F G).obj (Functor.id X)) ((transform X).obj ψ) ((transform X).obj ψ) ((precompose F₁ G₁).obj (Functor.id X))).hom (((transform X).obj ψ).whiskerLeft (precomposeObjId F₁ G₁ X).hom) = CategoryStruct.comp (Functor.whiskerRight (precomposeObjId F G X).hom ((transform X).obj ψ)) (CategoryStruct.comp ((transform X).obj ψ).leftUnitor.hom ((transform X).obj ψ).rightUnitor.inv)

The square precomposeObjTransformOBjSquare respects identities.

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precomposeObjTransformObjSquare_iso_hom_comp {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} {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₇} {Y : Type u₈} {Z : Type u₉} [Category.{v₇, u₇} X] [Category.{v₈, u₈} Y] [Category.{v₉, u₉} Z] (ψ : CatCospanTransform F G F₁ G₁) (U : Functor X Y) (V : Functor Y Z) : CategoryStruct.comp (CatCommSq.iso ((precompose F G).obj (U.comp V)) ((transform Z).obj ψ) ((transform X).obj ψ) ((precompose F₁ G₁).obj (U.comp V))).hom (((transform Z).obj ψ).whiskerLeft (precomposeObjComp F₁ G₁ U V).hom) = CategoryStruct.comp (Functor.whiskerRight (precomposeObjComp F G U V).hom ((transform X).obj ψ)) (CategoryStruct.comp (((precompose F G).obj V).associator ((precompose F G).obj U) ((transform X).obj ψ)).hom (CategoryStruct.comp (((precompose F G).obj V).whiskerLeft (CatCommSq.iso ((precompose F G).obj U) ((transform Y).obj ψ) ((transform X).obj ψ) ((precompose F₁ G₁).obj U)).hom) (CategoryStruct.comp (((precompose F G).obj V).associator ((transform Y).obj ψ) ((precompose F₁ G₁).obj U)).inv (CategoryStruct.comp (Functor.whiskerRight (CatCommSq.iso ((precompose F G).obj V) ((transform Z).obj ψ) ((transform Y).obj ψ) ((precompose F₁ G₁).obj V)).hom ((precompose F₁ G₁).obj U)) (((transform Z).obj ψ).associator ((precompose F₁ G₁).obj V) ((precompose F₁ G₁).obj U)).hom))))

The square precomposeTransformSquare respects compositions.

instance CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare {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} {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₇} {Y : Type u₈} [Category.{v₇, u₇} X] [Category.{v₈, u₈} Y] (U : Functor X Y) (ψ : CatCospanTransform F G F₁ G₁) : CatCommSq ((transform Y).obj ψ) ((precompose F G).obj U) ((precompose F₁ G₁).obj U) ((transform X).obj ψ)

The canonical compatibility square between (the object components of) transform and precompose. This is a "naturality square" if we think as precompose as the (app component of the) map component of a pseudofunctor from the opposite bicategory of categories to pseudofunctors of categorical cospans (its value on X being the pseudofunctor transform X _).

Equations

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

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_inv_app_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} {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₇} {Y : Type u₈} [Category.{v₇, u₇} X] [Category.{v₈, u₈} Y] (U : Functor X Y) (ψ : CatCospanTransform F G F₁ G₁) (X✝ : CatCommSqOver F G Y) (x✝ : X) : ((CatCommSq.iso ((transform Y).obj ψ) ((precompose F G).obj U) ((precompose F₁ G₁).obj U) ((transform X).obj ψ)).inv.app X✝).fst.app x✝ = CategoryStruct.id (ψ.left.obj (X✝.fst.obj (U.obj x✝)))

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_hom_app_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} {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₇} {Y : Type u₈} [Category.{v₇, u₇} X] [Category.{v₈, u₈} Y] (U : Functor X Y) (ψ : CatCospanTransform F G F₁ G₁) (X✝ : CatCommSqOver F G Y) (x✝ : X) : ((CatCommSq.iso ((transform Y).obj ψ) ((precompose F G).obj U) ((precompose F₁ G₁).obj U) ((transform X).obj ψ)).hom.app X✝).fst.app x✝ = CategoryStruct.id (ψ.left.obj (X✝.fst.obj (U.obj x✝)))

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_inv_app_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} {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₇} {Y : Type u₈} [Category.{v₇, u₇} X] [Category.{v₈, u₈} Y] (U : Functor X Y) (ψ : CatCospanTransform F G F₁ G₁) (X✝ : CatCommSqOver F G Y) (x✝ : X) : ((CatCommSq.iso ((transform Y).obj ψ) ((precompose F G).obj U) ((precompose F₁ G₁).obj U) ((transform X).obj ψ)).inv.app X✝).snd.app x✝ = CategoryStruct.id (ψ.right.obj (X✝.snd.obj (U.obj x✝)))

@[simp]

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_hom_app_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} {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₇} {Y : Type u₈} [Category.{v₇, u₇} X] [Category.{v₈, u₈} Y] (U : Functor X Y) (ψ : CatCospanTransform F G F₁ G₁) (X✝ : CatCommSqOver F G Y) (x✝ : X) : ((CatCommSq.iso ((transform Y).obj ψ) ((precompose F G).obj U) ((precompose F₁ G₁).obj U) ((transform X).obj ψ)).hom.app X✝).snd.app x✝ = CategoryStruct.id (ψ.right.obj (X✝.snd.obj (U.obj x✝)))

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_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} {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₇} {Y : Type u₈} [Category.{v₇, u₇} X] [Category.{v₈, u₈} Y] (U : Functor X Y) {ψ ψ' : CatCospanTransform F G F₁ G₁} (η : ψ ⟶ ψ') : CategoryStruct.comp (Functor.whiskerRight ((transform Y).map η) ((precompose F₁ G₁).obj U)) (CatCommSq.iso ((transform Y).obj ψ') ((precompose F G).obj U) ((precompose F₁ G₁).obj U) ((transform X).obj ψ')).hom = CategoryStruct.comp (CatCommSq.iso ((transform Y).obj ψ) ((precompose F G).obj U) ((precompose F₁ G₁).obj U) ((transform X).obj ψ)).hom (((precompose F G).obj U).whiskerLeft ((transform X).map η))

The square transformObjPrecomposeObjSquare is itself natural.

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_hom_id {A : Type u₁} {B : Type u₂} {C : Type u₃} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Category.{v₃, u₃} C] {X : Type u₇} {Y : Type u₈} [Category.{v₇, u₇} X] [Category.{v₈, u₈} Y] (U : Functor X Y) (F : Functor A B) (G : Functor C B) : CategoryStruct.comp (CatCommSq.iso ((transform Y).obj (CatCospanTransform.id F G)) ((precompose F G).obj U) ((precompose F G).obj U) ((transform X).obj (CatCospanTransform.id F G))).hom (((precompose F G).obj U).whiskerLeft (transformObjId X F G).hom) = CategoryStruct.comp (Functor.whiskerRight (transformObjId Y F G).hom ((precompose F G).obj U)) (CategoryStruct.comp ((precompose F G).obj U).leftUnitor.hom ((precompose F G).obj U).rightUnitor.inv)

The square transformObjPrecomposeObjSquare respects identities.

theorem CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformPrecomposeObjSquare_iso_hom_comp {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} {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₁} {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₁₀} {Y : Type u₁₁} [Category.{v₁₀, u₁₀} X] [Category.{v₁₁, u₁₁} Y] (U : Functor X Y) (ψ : CatCospanTransform F G F₁ G₁) (ψ' : CatCospanTransform F₁ G₁ F₂ G₂) : CategoryStruct.comp (CatCommSq.iso ((transform Y).obj (ψ.comp ψ')) ((precompose F G).obj U) ((precompose F₂ G₂).obj U) ((transform X).obj (ψ.comp ψ'))).hom (((precompose F G).obj U).whiskerLeft (transformObjComp X ψ ψ').hom) = CategoryStruct.comp (Functor.whiskerRight (transformObjComp Y ψ ψ').hom ((precompose F₂ G₂).obj U)) (CategoryStruct.comp (((transform Y).obj ψ).associator ((transform Y).obj ψ') ((precompose F₂ G₂).obj U)).hom (CategoryStruct.comp (((transform Y).obj ψ).whiskerLeft (CatCommSq.iso ((transform Y).obj ψ') ((precompose F₁ G₁).obj U) ((precompose F₂ G₂).obj U) ((transform X).obj ψ')).hom) (CategoryStruct.comp (((transform Y).obj ψ).associator ((precompose F₁ G₁).obj U) ((transform X).obj ψ')).inv (CategoryStruct.comp (Functor.whiskerRight (CatCommSq.iso ((transform Y).obj ψ) ((precompose F G).obj U) ((precompose F₁ G₁).obj U) ((transform X).obj ψ)).hom ((transform X).obj ψ')) (((precompose F G).obj U).associator ((transform X).obj ψ) ((transform X).obj ψ')).hom))))

The square transformPrecomposeSquare respects compositions.