The diagonal object of a morphism.

We provide various API and isomorphisms considering the diagonal object Δ_{Y/X} := pullback f f of a morphism f : X ⟶ Y.

@[reducible, inline]

abbrev CategoryTheory.Limits.pullback.diagonalObj {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) [HasPullback f f] : C

The diagonal object of a morphism f : X ⟶ Y is Δ_{X/Y} := pullback f f.

def CategoryTheory.Limits.pullback.diagonal {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) [HasPullback f f] : X ⟶ diagonalObj f

The diagonal morphism X ⟶ Δ_{X/Y} for a morphism f : X ⟶ Y.

@[simp]

theorem CategoryTheory.Limits.pullback.diagonal_fst {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) [HasPullback f f] : CategoryStruct.comp (diagonal f) (fst f f) = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.pullback.diagonal_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) [HasPullback f f] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (diagonal f) (CategoryStruct.comp (fst f f) h) = h

@[simp]

theorem CategoryTheory.Limits.pullback.diagonal_snd {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) [HasPullback f f] : CategoryStruct.comp (diagonal f) (snd f f) = CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.pullback.diagonal_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) [HasPullback f f] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (diagonal f) (CategoryStruct.comp (snd f f) h) = h

instance CategoryTheory.Limits.pullback.instIsSplitMonoDiagonal {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) [HasPullback f f] : IsSplitMono (diagonal f)

instance CategoryTheory.Limits.pullback.instIsSplitEpiFst {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) [HasPullback f f] : IsSplitEpi (fst f f)

instance CategoryTheory.Limits.pullback.instIsSplitEpiSnd {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) [HasPullback f f] : IsSplitEpi (snd f f)

instance CategoryTheory.Limits.pullback.instIsIsoDiagonalOfMono {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) [HasPullback f f] [Mono f] : IsIso (diagonal f)

theorem CategoryTheory.Limits.pullback.isIso_diagonal_iff {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) [HasPullback f f] : IsIso (diagonal f) ↔ Mono f

theorem CategoryTheory.Limits.pullback.diagonal_isKernelPair {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) [HasPullback f f] : IsKernelPair f (fst f f) (snd f f)

The two projections Δ_{X/Y} ⟶ X form a kernel pair for f : X ⟶ Y.

@[simp]

theorem CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ pullback f i) (i₂ : V₂ ⟶ pullback f i) : CategoryStruct.comp (pullback.snd (pullback.diagonal f) (pullback.map (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) f f (CategoryStruct.comp i₁ (pullback.fst f i)) (CategoryStruct.comp i₂ (pullback.fst f i)) i ⋯ ⋯)) (CategoryStruct.comp (pullback.fst (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i))) (CategoryStruct.comp i₁ (pullback.fst f i))) = pullback.fst (pullback.diagonal f) (pullback.map (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) f f (CategoryStruct.comp i₁ (pullback.fst f i)) (CategoryStruct.comp i₂ (pullback.fst f i)) i ⋯ ⋯)

@[simp]

theorem CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ pullback f i) (i₂ : V₂ ⟶ pullback f i) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (pullback.snd (pullback.diagonal f) (pullback.map (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) f f (CategoryStruct.comp i₁ (pullback.fst f i)) (CategoryStruct.comp i₂ (pullback.fst f i)) i ⋯ ⋯)) (CategoryStruct.comp (pullback.fst (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i))) (CategoryStruct.comp i₁ (CategoryStruct.comp (pullback.fst f i) h))) = CategoryStruct.comp (pullback.fst (pullback.diagonal f) (pullback.map (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) f f (CategoryStruct.comp i₁ (pullback.fst f i)) (CategoryStruct.comp i₂ (pullback.fst f i)) i ⋯ ⋯)) h

@[simp]

theorem CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ pullback f i) (i₂ : V₂ ⟶ pullback f i) : CategoryStruct.comp (pullback.snd (pullback.diagonal f) (pullback.map (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) f f (CategoryStruct.comp i₁ (pullback.fst f i)) (CategoryStruct.comp i₂ (pullback.fst f i)) i ⋯ ⋯)) (CategoryStruct.comp (pullback.snd (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i))) (CategoryStruct.comp i₂ (pullback.fst f i))) = pullback.fst (pullback.diagonal f) (pullback.map (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) f f (CategoryStruct.comp i₁ (pullback.fst f i)) (CategoryStruct.comp i₂ (pullback.fst f i)) i ⋯ ⋯)

@[simp]

theorem CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ pullback f i) (i₂ : V₂ ⟶ pullback f i) {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (pullback.snd (pullback.diagonal f) (pullback.map (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) f f (CategoryStruct.comp i₁ (pullback.fst f i)) (CategoryStruct.comp i₂ (pullback.fst f i)) i ⋯ ⋯)) (CategoryStruct.comp (pullback.snd (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i))) (CategoryStruct.comp i₂ (CategoryStruct.comp (pullback.fst f i) h))) = CategoryStruct.comp (pullback.fst (pullback.diagonal f) (pullback.map (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) f f (CategoryStruct.comp i₁ (pullback.fst f i)) (CategoryStruct.comp i₂ (pullback.fst f i)) i ⋯ ⋯)) h

@[reducible, inline]

abbrev CategoryTheory.Limits.pullbackDiagonalMapIso.hom {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ pullback f i) (i₂ : V₂ ⟶ pullback f i) [HasPullback i₁ i₂] : pullback (pullback.diagonal f) (pullback.map (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) f f (CategoryStruct.comp i₁ (pullback.fst f i)) (CategoryStruct.comp i₂ (pullback.fst f i)) i ⋯ ⋯) ⟶ pullback i₁ i₂

The underlying map of pullbackDiagonalIso

@[reducible, inline]

abbrev CategoryTheory.Limits.pullbackDiagonalMapIso.inv {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ pullback f i) (i₂ : V₂ ⟶ pullback f i) [HasPullback i₁ i₂] : pullback i₁ i₂ ⟶ pullback (pullback.diagonal f) (pullback.map (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) f f (CategoryStruct.comp i₁ (pullback.fst f i)) (CategoryStruct.comp i₂ (pullback.fst f i)) i ⋯ ⋯)

The underlying inverse of pullbackDiagonalIso

def CategoryTheory.Limits.pullbackDiagonalMapIso {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ pullback f i) (i₂ : V₂ ⟶ pullback f i) [HasPullback i₁ i₂] : pullback (pullback.diagonal f) (pullback.map (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) f f (CategoryStruct.comp i₁ (pullback.fst f i)) (CategoryStruct.comp i₂ (pullback.fst f i)) i ⋯ ⋯) ≅ pullback i₁ i₂

This iso witnesses the fact that given f : X ⟶ Y, i : U ⟶ Y, and i₁ : V₁ ⟶ X ×[Y] U, i₂ : V₂ ⟶ X ×[Y] U, the diagram

V₁ ×[X ×[Y] U] V₂ ⟶ V₁ ×[U] V₂
        |                 |
        |                 |
        ↓                 ↓
        X         ⟶   X ×[Y] X

is a pullback square. Also see pullback_fst_map_snd_isPullback.

@[simp]

theorem CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ pullback f i) (i₂ : V₂ ⟶ pullback f i) [HasPullback i₁ i₂] : CategoryStruct.comp (pullbackDiagonalMapIso f i i₁ i₂).hom (pullback.fst i₁ i₂) = CategoryStruct.comp (pullback.snd (pullback.diagonal f) (pullback.map (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) f f (CategoryStruct.comp i₁ (pullback.fst f i)) (CategoryStruct.comp i₂ (pullback.fst f i)) i ⋯ ⋯)) (pullback.fst (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)))

@[simp]

theorem CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ pullback f i) (i₂ : V₂ ⟶ pullback f i) [HasPullback i₁ i₂] {Z : C} (h : V₁ ⟶ Z) : CategoryStruct.comp (pullbackDiagonalMapIso f i i₁ i₂).hom (CategoryStruct.comp (pullback.fst i₁ i₂) h) = CategoryStruct.comp (pullback.snd (pullback.diagonal f) (pullback.map (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) f f (CategoryStruct.comp i₁ (pullback.fst f i)) (CategoryStruct.comp i₂ (pullback.fst f i)) i ⋯ ⋯)) (CategoryStruct.comp (pullback.fst (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i))) h)

@[simp]

theorem CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ pullback f i) (i₂ : V₂ ⟶ pullback f i) [HasPullback i₁ i₂] : CategoryStruct.comp (pullbackDiagonalMapIso f i i₁ i₂).hom (pullback.snd i₁ i₂) = CategoryStruct.comp (pullback.snd (pullback.diagonal f) (pullback.map (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) f f (CategoryStruct.comp i₁ (pullback.fst f i)) (CategoryStruct.comp i₂ (pullback.fst f i)) i ⋯ ⋯)) (pullback.snd (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)))

@[simp]

theorem CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ pullback f i) (i₂ : V₂ ⟶ pullback f i) [HasPullback i₁ i₂] {Z : C} (h : V₂ ⟶ Z) : CategoryStruct.comp (pullbackDiagonalMapIso f i i₁ i₂).hom (CategoryStruct.comp (pullback.snd i₁ i₂) h) = CategoryStruct.comp (pullback.snd (pullback.diagonal f) (pullback.map (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) f f (CategoryStruct.comp i₁ (pullback.fst f i)) (CategoryStruct.comp i₂ (pullback.fst f i)) i ⋯ ⋯)) (CategoryStruct.comp (pullback.snd (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i))) h)

@[simp]

theorem CategoryTheory.Limits.pullbackDiagonalMapIso.inv_fst {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ pullback f i) (i₂ : V₂ ⟶ pullback f i) [HasPullback i₁ i₂] : CategoryStruct.comp (pullbackDiagonalMapIso f i i₁ i₂).inv (pullback.fst (pullback.diagonal f) (pullback.map (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) f f (CategoryStruct.comp i₁ (pullback.fst f i)) (CategoryStruct.comp i₂ (pullback.fst f i)) i ⋯ ⋯)) = CategoryStruct.comp (pullback.fst i₁ i₂) (CategoryStruct.comp i₁ (pullback.fst f i))

@[simp]

theorem CategoryTheory.Limits.pullbackDiagonalMapIso.inv_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ pullback f i) (i₂ : V₂ ⟶ pullback f i) [HasPullback i₁ i₂] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (pullbackDiagonalMapIso f i i₁ i₂).inv (CategoryStruct.comp (pullback.fst (pullback.diagonal f) (pullback.map (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) f f (CategoryStruct.comp i₁ (pullback.fst f i)) (CategoryStruct.comp i₂ (pullback.fst f i)) i ⋯ ⋯)) h) = CategoryStruct.comp (pullback.fst i₁ i₂) (CategoryStruct.comp i₁ (CategoryStruct.comp (pullback.fst f i) h))

@[simp]

theorem CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_fst {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ pullback f i) (i₂ : V₂ ⟶ pullback f i) [HasPullback i₁ i₂] : CategoryStruct.comp (pullbackDiagonalMapIso f i i₁ i₂).inv (CategoryStruct.comp (pullback.snd (pullback.diagonal f) (pullback.map (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) f f (CategoryStruct.comp i₁ (pullback.fst f i)) (CategoryStruct.comp i₂ (pullback.fst f i)) i ⋯ ⋯)) (pullback.fst (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)))) = pullback.fst i₁ i₂

@[simp]

theorem CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ pullback f i) (i₂ : V₂ ⟶ pullback f i) [HasPullback i₁ i₂] {Z : C} (h : V₁ ⟶ Z) : CategoryStruct.comp (pullbackDiagonalMapIso f i i₁ i₂).inv (CategoryStruct.comp (pullback.snd (pullback.diagonal f) (pullback.map (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) f f (CategoryStruct.comp i₁ (pullback.fst f i)) (CategoryStruct.comp i₂ (pullback.fst f i)) i ⋯ ⋯)) (CategoryStruct.comp (pullback.fst (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i))) h)) = CategoryStruct.comp (pullback.fst i₁ i₂) h

@[simp]

theorem CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ pullback f i) (i₂ : V₂ ⟶ pullback f i) [HasPullback i₁ i₂] : CategoryStruct.comp (pullbackDiagonalMapIso f i i₁ i₂).inv (CategoryStruct.comp (pullback.snd (pullback.diagonal f) (pullback.map (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) f f (CategoryStruct.comp i₁ (pullback.fst f i)) (CategoryStruct.comp i₂ (pullback.fst f i)) i ⋯ ⋯)) (pullback.snd (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)))) = pullback.snd i₁ i₂

@[simp]

theorem CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ pullback f i) (i₂ : V₂ ⟶ pullback f i) [HasPullback i₁ i₂] {Z : C} (h : V₂ ⟶ Z) : CategoryStruct.comp (pullbackDiagonalMapIso f i i₁ i₂).inv (CategoryStruct.comp (pullback.snd (pullback.diagonal f) (pullback.map (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) f f (CategoryStruct.comp i₁ (pullback.fst f i)) (CategoryStruct.comp i₂ (pullback.fst f i)) i ⋯ ⋯)) (CategoryStruct.comp (pullback.snd (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i))) h)) = CategoryStruct.comp (pullback.snd i₁ i₂) h

theorem CategoryTheory.Limits.pullback_fst_map_snd_isPullback {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ pullback f i) (i₂ : V₂ ⟶ pullback f i) [HasPullback i₁ i₂] : IsPullback (CategoryStruct.comp (pullback.fst i₁ i₂) (CategoryStruct.comp i₁ (pullback.fst f i))) (pullback.map i₁ i₂ (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) (CategoryStruct.id V₁) (CategoryStruct.id V₂) (pullback.snd f i) ⋯ ⋯) (pullback.diagonal f) (pullback.map (CategoryStruct.comp i₁ (pullback.snd f i)) (CategoryStruct.comp i₂ (pullback.snd f i)) f f (CategoryStruct.comp i₁ (pullback.fst f i)) (CategoryStruct.comp i₂ (pullback.fst f i)) i ⋯ ⋯)

def CategoryTheory.Limits.pullbackDiagonalMapIdIso {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [HasPullback i i] [HasPullback f g] [HasPullback (CategoryStruct.comp f i) (CategoryStruct.comp g i)] [HasPullback (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)] : pullback (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯) ≅ pullback f g

This iso witnesses the fact that given f : X ⟶ T, g : Y ⟶ T, and i : T ⟶ S, the diagram

X ×ₜ Y ⟶ X ×ₛ Y
  |         |
  |         |
  ↓         ↓
  T    ⟶  T ×ₛ T

is a pullback square. Also see pullback_map_diagonal_isPullback.

@[simp]

theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_fst {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [HasPullback i i] [HasPullback f g] [HasPullback (CategoryStruct.comp f i) (CategoryStruct.comp g i)] [HasPullback (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)] : CategoryStruct.comp (pullbackDiagonalMapIdIso f g i).hom (pullback.fst f g) = CategoryStruct.comp (pullback.snd (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)) (pullback.fst (CategoryStruct.comp f i) (CategoryStruct.comp g i))

@[simp]

theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [HasPullback i i] [HasPullback f g] [HasPullback (CategoryStruct.comp f i) (CategoryStruct.comp g i)] [HasPullback (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (pullbackDiagonalMapIdIso f g i).hom (CategoryStruct.comp (pullback.fst f g) h) = CategoryStruct.comp (pullback.snd (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)) (CategoryStruct.comp (pullback.fst (CategoryStruct.comp f i) (CategoryStruct.comp g i)) h)

@[simp]

theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_snd {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [HasPullback i i] [HasPullback f g] [HasPullback (CategoryStruct.comp f i) (CategoryStruct.comp g i)] [HasPullback (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)] : CategoryStruct.comp (pullbackDiagonalMapIdIso f g i).hom (pullback.snd f g) = CategoryStruct.comp (pullback.snd (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)) (pullback.snd (CategoryStruct.comp f i) (CategoryStruct.comp g i))

@[simp]

theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [HasPullback i i] [HasPullback f g] [HasPullback (CategoryStruct.comp f i) (CategoryStruct.comp g i)] [HasPullback (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (pullbackDiagonalMapIdIso f g i).hom (CategoryStruct.comp (pullback.snd f g) h) = CategoryStruct.comp (pullback.snd (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)) (CategoryStruct.comp (pullback.snd (CategoryStruct.comp f i) (CategoryStruct.comp g i)) h)

@[simp]

theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_fst {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [HasPullback i i] [HasPullback f g] [HasPullback (CategoryStruct.comp f i) (CategoryStruct.comp g i)] [HasPullback (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)] : CategoryStruct.comp (pullbackDiagonalMapIdIso f g i).inv (pullback.fst (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)) = CategoryStruct.comp (pullback.fst f g) f

@[simp]

theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [HasPullback i i] [HasPullback f g] [HasPullback (CategoryStruct.comp f i) (CategoryStruct.comp g i)] [HasPullback (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)] {Z : C} (h : T ⟶ Z) : CategoryStruct.comp (pullbackDiagonalMapIdIso f g i).inv (CategoryStruct.comp (pullback.fst (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)) h) = CategoryStruct.comp (pullback.fst f g) (CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [HasPullback i i] [HasPullback f g] [HasPullback (CategoryStruct.comp f i) (CategoryStruct.comp g i)] [HasPullback (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)] : CategoryStruct.comp (pullbackDiagonalMapIdIso f g i).inv (CategoryStruct.comp (pullback.snd (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)) (pullback.fst (CategoryStruct.comp f i) (CategoryStruct.comp g i))) = pullback.fst f g

@[simp]

theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [HasPullback i i] [HasPullback f g] [HasPullback (CategoryStruct.comp f i) (CategoryStruct.comp g i)] [HasPullback (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)] {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (pullbackDiagonalMapIdIso f g i).inv (CategoryStruct.comp (pullback.snd (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)) (CategoryStruct.comp (pullback.fst (CategoryStruct.comp f i) (CategoryStruct.comp g i)) h)) = CategoryStruct.comp (pullback.fst f g) h

@[simp]

theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_snd {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [HasPullback i i] [HasPullback f g] [HasPullback (CategoryStruct.comp f i) (CategoryStruct.comp g i)] [HasPullback (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)] : CategoryStruct.comp (pullbackDiagonalMapIdIso f g i).inv (CategoryStruct.comp (pullback.snd (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)) (pullback.snd (CategoryStruct.comp f i) (CategoryStruct.comp g i))) = pullback.snd f g

@[simp]

theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [HasPullback i i] [HasPullback f g] [HasPullback (CategoryStruct.comp f i) (CategoryStruct.comp g i)] [HasPullback (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)] {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp (pullbackDiagonalMapIdIso f g i).inv (CategoryStruct.comp (pullback.snd (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)) (CategoryStruct.comp (pullback.snd (CategoryStruct.comp f i) (CategoryStruct.comp g i)) h)) = CategoryStruct.comp (pullback.snd f g) h

theorem CategoryTheory.Limits.pullback.diagonal_comp {C : Type u_1} [Category.{u_2, u_1} C] {X Y Z : C} [HasPullbacks C] (f : X ⟶ Y) (g : Y ⟶ Z) : diagonal (CategoryStruct.comp f g) = CategoryStruct.comp (diagonal f) (CategoryStruct.comp (pullbackDiagonalMapIdIso f f g).inv (snd (diagonal g) (map (CategoryStruct.comp f g) (CategoryStruct.comp f g) g g f f (CategoryStruct.id Z) ⋯ ⋯)))

theorem CategoryTheory.Limits.pullback.comp_diagonal {C : Type u_1} [Category.{u_2, u_1} C] {X Y Z : C} [HasPullbacks C] (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryStruct.comp f (diagonal g) = CategoryStruct.comp (diagonal (CategoryStruct.comp f g)) (map (CategoryStruct.comp f g) (CategoryStruct.comp f g) g g f f (CategoryStruct.id Z) ⋯ ⋯)

theorem CategoryTheory.Limits.pullback.comp_diagonal_assoc {C : Type u_1} [Category.{u_2, u_1} C] {X Y Z : C} [HasPullbacks C] (f : X ⟶ Y) (g : Y ⟶ Z) {Z✝ : C} (h : diagonalObj g ⟶ Z✝) : CategoryStruct.comp f (CategoryStruct.comp (diagonal g) h) = CategoryStruct.comp (diagonal (CategoryStruct.comp f g)) (CategoryStruct.comp (map (CategoryStruct.comp f g) (CategoryStruct.comp f g) g g f f (CategoryStruct.id Z) ⋯ ⋯) h)

theorem CategoryTheory.Limits.pullback_map_diagonal_isPullback {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [HasPullback i i] [HasPullback f g] [HasPullback (CategoryStruct.comp f i) (CategoryStruct.comp g i)] [HasPullback (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)] : IsPullback (CategoryStruct.comp (pullback.fst f g) f) (pullback.map f g (CategoryStruct.comp f i) (CategoryStruct.comp g i) (CategoryStruct.id X) (CategoryStruct.id Y) i ⋯ ⋯) (pullback.diagonal i) (pullback.map (CategoryStruct.comp f i) (CategoryStruct.comp g i) i i f g (CategoryStruct.id S) ⋯ ⋯)

def CategoryTheory.Limits.diagonalObjPullbackFstIso {C : Type u_1} [Category.{u_2, u_1} C] [HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : pullback.diagonalObj (pullback.fst f g) ≅ pullback (CategoryStruct.comp (pullback.snd g g) g) f

The diagonal object of X ×[Z] Y ⟶ X is isomorphic to Δ_{Y/Z} ×[Z] X.

@[simp]

theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_fst {C : Type u_1} [Category.{u_2, u_1} C] [HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryStruct.comp (diagonalObjPullbackFstIso f g).hom (CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd g g) g) f) (pullback.fst g g)) = CategoryStruct.comp (pullback.fst (pullback.fst f g) (pullback.fst f g)) (pullback.snd f g)

@[simp]

theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] [HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z✝ : C} (h : Y ⟶ Z✝) : CategoryStruct.comp (diagonalObjPullbackFstIso f g).hom (CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd g g) g) f) (CategoryStruct.comp (pullback.fst g g) h)) = CategoryStruct.comp (pullback.fst (pullback.fst f g) (pullback.fst f g)) (CategoryStruct.comp (pullback.snd f g) h)

@[simp]

theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_snd {C : Type u_1} [Category.{u_2, u_1} C] [HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryStruct.comp (diagonalObjPullbackFstIso f g).hom (CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd g g) g) f) (pullback.snd g g)) = CategoryStruct.comp (pullback.snd (pullback.fst f g) (pullback.fst f g)) (pullback.snd f g)

@[simp]

theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z✝ : C} (h : Y ⟶ Z✝) : CategoryStruct.comp (diagonalObjPullbackFstIso f g).hom (CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd g g) g) f) (CategoryStruct.comp (pullback.snd g g) h)) = CategoryStruct.comp (pullback.snd (pullback.fst f g) (pullback.fst f g)) (CategoryStruct.comp (pullback.snd f g) h)

@[simp]

theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_snd {C : Type u_1} [Category.{u_2, u_1} C] [HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryStruct.comp (diagonalObjPullbackFstIso f g).hom (pullback.snd (CategoryStruct.comp (pullback.snd g g) g) f) = CategoryStruct.comp (pullback.fst (pullback.fst f g) (pullback.fst f g)) (pullback.fst f g)

@[simp]

theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z✝ : C} (h : X ⟶ Z✝) : CategoryStruct.comp (diagonalObjPullbackFstIso f g).hom (CategoryStruct.comp (pullback.snd (CategoryStruct.comp (pullback.snd g g) g) f) h) = CategoryStruct.comp (pullback.fst (pullback.fst f g) (pullback.fst f g)) (CategoryStruct.comp (pullback.fst f g) h)

@[simp]

theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_fst {C : Type u_1} [Category.{u_2, u_1} C] [HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryStruct.comp (diagonalObjPullbackFstIso f g).inv (CategoryStruct.comp (pullback.fst (pullback.fst f g) (pullback.fst f g)) (pullback.fst f g)) = pullback.snd (CategoryStruct.comp (pullback.snd g g) g) f

@[simp]

theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] [HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z✝ : C} (h : X ⟶ Z✝) : CategoryStruct.comp (diagonalObjPullbackFstIso f g).inv (CategoryStruct.comp (pullback.fst (pullback.fst f g) (pullback.fst f g)) (CategoryStruct.comp (pullback.fst f g) h)) = CategoryStruct.comp (pullback.snd (CategoryStruct.comp (pullback.snd g g) g) f) h

@[simp]

theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_snd {C : Type u_1} [Category.{u_2, u_1} C] [HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryStruct.comp (diagonalObjPullbackFstIso f g).inv (CategoryStruct.comp (pullback.fst (pullback.fst f g) (pullback.fst f g)) (pullback.snd f g)) = CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd g g) g) f) (pullback.fst g g)

@[simp]

theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z✝ : C} (h : Y ⟶ Z✝) : CategoryStruct.comp (diagonalObjPullbackFstIso f g).inv (CategoryStruct.comp (pullback.fst (pullback.fst f g) (pullback.fst f g)) (CategoryStruct.comp (pullback.snd f g) h)) = CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd g g) g) f) (CategoryStruct.comp (pullback.fst g g) h)

@[simp]

theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_fst {C : Type u_1} [Category.{u_2, u_1} C] [HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryStruct.comp (diagonalObjPullbackFstIso f g).inv (CategoryStruct.comp (pullback.snd (pullback.fst f g) (pullback.fst f g)) (pullback.fst f g)) = pullback.snd (CategoryStruct.comp (pullback.snd g g) g) f

@[simp]

theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_fst_assoc {C : Type u_1} [Category.{u_2, u_1} C] [HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z✝ : C} (h : X ⟶ Z✝) : CategoryStruct.comp (diagonalObjPullbackFstIso f g).inv (CategoryStruct.comp (pullback.snd (pullback.fst f g) (pullback.fst f g)) (CategoryStruct.comp (pullback.fst f g) h)) = CategoryStruct.comp (pullback.snd (CategoryStruct.comp (pullback.snd g g) g) f) h

@[simp]

theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_snd {C : Type u_1} [Category.{u_2, u_1} C] [HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : CategoryStruct.comp (diagonalObjPullbackFstIso f g).inv (CategoryStruct.comp (pullback.snd (pullback.fst f g) (pullback.fst f g)) (pullback.snd f g)) = CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd g g) g) f) (pullback.snd g g)

@[simp]

theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_snd_assoc {C : Type u_1} [Category.{u_2, u_1} C] [HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z✝ : C} (h : Y ⟶ Z✝) : CategoryStruct.comp (diagonalObjPullbackFstIso f g).inv (CategoryStruct.comp (pullback.snd (pullback.fst f g) (pullback.fst f g)) (CategoryStruct.comp (pullback.snd f g) h)) = CategoryStruct.comp (pullback.fst (CategoryStruct.comp (pullback.snd g g) g) f) (CategoryStruct.comp (pullback.snd g g) h)

theorem CategoryTheory.Limits.diagonal_pullback_fst {C : Type u_1} [Category.{u_2, u_1} C] [HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) : pullback.diagonal (pullback.fst f g) = CategoryStruct.comp (pullbackSymmetry f (Over.mk g).hom).hom (CategoryStruct.comp ((Over.pullback f).map (Over.homMk (pullback.diagonal g) ⋯)).left (diagonalObjPullbackFstIso f g).inv)

theorem CategoryTheory.Limits.pullback_lift_diagonal_isPullback {C : Type u_1} [Category.{u_2, u_1} C] {X Y : C} [HasPullbacks C] {S : C} (g : Y ⟶ X) (f : X ⟶ S) : IsPullback g (pullback.lift (CategoryStruct.id Y) g ⋯) (pullback.diagonal f) (pullback.map (CategoryStruct.comp g f) f f f g (CategoryStruct.id X) (CategoryStruct.id S) ⋯ ⋯)

Informally, this is a special case of pullback_map_diagonal_isPullback for T = X.

def CategoryTheory.Limits.pullbackFstFstIso {C : Type u_1} [Category.{u_2, u_1} C] [HasPullbacks C] {X Y S X' Y' S' : C} (f : X ⟶ S) (g : Y ⟶ S) (f' : X' ⟶ S') (g' : Y' ⟶ S') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : S ⟶ S') (e₁ : CategoryStruct.comp f i₃ = CategoryStruct.comp i₁ f') (e₂ : CategoryStruct.comp g i₃ = CategoryStruct.comp i₂ g') [Mono i₃] : pullback (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂) ≅ pullback f g

Given the following diagram with S ⟶ S' a monomorphism,

    X ⟶ X'
      ↘      ↘
        S ⟶ S'
      ↗      ↗
    Y ⟶ Y'

This iso witnesses the fact that

      X ×[S] Y ⟶ (X' ×[S'] Y') ×[Y'] Y
          |                  |
          |                  |
          ↓                  ↓
(X' ×[S'] Y') ×[X'] X ⟶ X' ×[S'] Y'

is a pullback square. The diagonal map of this square is pullback.map. Also see pullback_lift_map_is_pullback.

@[simp]

theorem CategoryTheory.Limits.pullbackFstFstIso_inv {C : Type u_1} [Category.{u_2, u_1} C] [HasPullbacks C] {X Y S X' Y' S' : C} (f : X ⟶ S) (g : Y ⟶ S) (f' : X' ⟶ S') (g' : Y' ⟶ S') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : S ⟶ S') (e₁ : CategoryStruct.comp f i₃ = CategoryStruct.comp i₁ f') (e₂ : CategoryStruct.comp g i₃ = CategoryStruct.comp i₂ g') [Mono i₃] : (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).inv = pullback.lift (pullback.lift (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) (pullback.fst f g) ⋯) (pullback.lift (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) (pullback.snd f g) ⋯) ⋯

@[simp]

theorem CategoryTheory.Limits.pullbackFstFstIso_hom {C : Type u_1} [Category.{u_2, u_1} C] [HasPullbacks C] {X Y S X' Y' S' : C} (f : X ⟶ S) (g : Y ⟶ S) (f' : X' ⟶ S') (g' : Y' ⟶ S') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : S ⟶ S') (e₁ : CategoryStruct.comp f i₃ = CategoryStruct.comp i₁ f') (e₂ : CategoryStruct.comp g i₃ = CategoryStruct.comp i₂ g') [Mono i₃] : (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).hom = pullback.lift (CategoryStruct.comp (pullback.fst (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂)) (pullback.snd (pullback.fst f' g') i₁)) (CategoryStruct.comp (pullback.snd (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂)) (pullback.snd (pullback.snd f' g') i₂)) ⋯

theorem CategoryTheory.Limits.pullback_map_eq_pullbackFstFstIso_inv {C : Type u_1} [Category.{u_2, u_1} C] [HasPullbacks C] {X Y S X' Y' S' : C} (f : X ⟶ S) (g : Y ⟶ S) (f' : X' ⟶ S') (g' : Y' ⟶ S') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : S ⟶ S') (e₁ : CategoryStruct.comp f i₃ = CategoryStruct.comp i₁ f') (e₂ : CategoryStruct.comp g i₃ = CategoryStruct.comp i₂ g') [Mono i₃] : pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂ = CategoryStruct.comp (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).inv (CategoryStruct.comp (pullback.snd (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂)) (pullback.fst (pullback.snd f' g') i₂))

theorem CategoryTheory.Limits.pullback_lift_map_isPullback {C : Type u_1} [Category.{u_2, u_1} C] [HasPullbacks C] {X Y S X' Y' S' : C} (f : X ⟶ S) (g : Y ⟶ S) (f' : X' ⟶ S') (g' : Y' ⟶ S') (i₁ : X ⟶ X') (i₂ : Y ⟶ Y') (i₃ : S ⟶ S') (e₁ : CategoryStruct.comp f i₃ = CategoryStruct.comp i₁ f') (e₂ : CategoryStruct.comp g i₃ = CategoryStruct.comp i₂ g') [Mono i₃] : IsPullback (pullback.lift (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) (pullback.fst f g) ⋯) (pullback.lift (pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) (pullback.snd f g) ⋯) (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂)