Documentation

Mathlib.CategoryTheory.Limits.Shapes.Diagonal

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.

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

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

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

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

Equations
source
@[simp]
theorem CategoryTheory.Limits.pullback.diagonal_fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullback f f] :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.fst f f) = CategoryTheory.CategoryStruct.id X
source
@[simp]
theorem CategoryTheory.Limits.pullback.diagonal_fst_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullback f f] {Z : C} (h : X ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f f) h) = h
source
@[simp]
theorem CategoryTheory.Limits.pullback.diagonal_snd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullback f f] :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.snd f f) = CategoryTheory.CategoryStruct.id X
source
@[simp]
theorem CategoryTheory.Limits.pullback.diagonal_snd_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullback f f] {Z : C} (h : X ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f f) h) = h
source
instance CategoryTheory.Limits.pullback.instIsSplitMonoDiagonal {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullback f f] :
CategoryTheory.IsSplitMono (CategoryTheory.Limits.pullback.diagonal f)
Equations
  • ⋯ = ⋯
source
instance CategoryTheory.Limits.pullback.instIsSplitEpiFst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullback f f] :
CategoryTheory.IsSplitEpi (CategoryTheory.Limits.pullback.fst f f)
Equations
  • ⋯ = ⋯
source
instance CategoryTheory.Limits.pullback.instIsSplitEpiSnd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullback f f] :
CategoryTheory.IsSplitEpi (CategoryTheory.Limits.pullback.snd f f)
Equations
  • ⋯ = ⋯
source
instance CategoryTheory.Limits.pullback.instIsIsoDiagonalOfMono {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullback f f] [CategoryTheory.Mono f] :
CategoryTheory.IsIso (CategoryTheory.Limits.pullback.diagonal f)
Equations
  • ⋯ = ⋯
source
theorem CategoryTheory.Limits.pullback.isIso_diagonal_iff {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullback f f] :
CategoryTheory.IsIso (CategoryTheory.Limits.pullback.diagonal f) ↔ CategoryTheory.Mono f
source
theorem CategoryTheory.Limits.pullback.diagonal_isKernelPair {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Limits.HasPullback f f] :
CategoryTheory.IsKernelPair f (CategoryTheory.Limits.pullback.fst f f) (CategoryTheory.Limits.pullback.snd f f)

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

source
@[simp]
theorem CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i) (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i))) (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))) = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)
source
@[simp]
theorem CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i) (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) {Z : C} (h : X ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i))) (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f i) h))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)) h
source
@[simp]
theorem CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i) (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i))) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i))) = CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)
source
@[simp]
theorem CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i) (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) {Z : C} (h : X ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i))) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f i) h))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)) h
source
@[reducible, inline]
abbrev CategoryTheory.Limits.pullbackDiagonalMapIso.hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i) (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [CategoryTheory.Limits.HasPullback i₁ i₂] :
CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯) ⟶ CategoryTheory.Limits.pullback i₁ i₂

The underlying map of pullbackDiagonalIso

Equations
  • One or more equations did not get rendered due to their size.
source
@[reducible, inline]
abbrev CategoryTheory.Limits.pullbackDiagonalMapIso.inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i) (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [CategoryTheory.Limits.HasPullback i₁ i₂] :
CategoryTheory.Limits.pullback i₁ i₂ ⟶ CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)

The underlying inverse of pullbackDiagonalIso

Equations
  • One or more equations did not get rendered due to their size.
source
def CategoryTheory.Limits.pullbackDiagonalMapIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i) (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [CategoryTheory.Limits.HasPullback i₁ i₂] :
CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯) ≅ CategoryTheory.Limits.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.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i) (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [CategoryTheory.Limits.HasPullback i₁ i₂] :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).hom (CategoryTheory.Limits.pullback.fst i₁ i₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)))
source
@[simp]
theorem CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i) (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [CategoryTheory.Limits.HasPullback i₁ i₂] {Z : C} (h : V₁ ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst i₁ i₂) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i))) h)
source
@[simp]
theorem CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i) (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [CategoryTheory.Limits.HasPullback i₁ i₂] :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).hom (CategoryTheory.Limits.pullback.snd i₁ i₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)))
source
@[simp]
theorem CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i) (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [CategoryTheory.Limits.HasPullback i₁ i₂] {Z : C} (h : V₂ ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd i₁ i₂) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i))) h)
source
@[simp]
theorem CategoryTheory.Limits.pullbackDiagonalMapIso.inv_fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i) (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [CategoryTheory.Limits.HasPullback i₁ i₂] :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).inv (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst i₁ i₂) (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))
source
@[simp]
theorem CategoryTheory.Limits.pullbackDiagonalMapIso.inv_fst_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i) (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [CategoryTheory.Limits.HasPullback i₁ i₂] {Z : C} (h : X ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst i₁ i₂) (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f i) h))
source
@[simp]
theorem CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i) (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [CategoryTheory.Limits.HasPullback i₁ i₂] :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)))) = CategoryTheory.Limits.pullback.fst i₁ i₂
source
@[simp]
theorem CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_fst_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i) (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [CategoryTheory.Limits.HasPullback i₁ i₂] {Z : C} (h : V₁ ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i))) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst i₁ i₂) h
source
@[simp]
theorem CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i) (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [CategoryTheory.Limits.HasPullback i₁ i₂] :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)))) = CategoryTheory.Limits.pullback.snd i₁ i₂
source
@[simp]
theorem CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i) (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [CategoryTheory.Limits.HasPullback i₁ i₂] {Z : C} (h : V₂ ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIso f i i₁ i₂).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i))) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd i₁ i₂) h
source
theorem CategoryTheory.Limits.pullback_fst_map_snd_isPullback {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ CategoryTheory.Limits.pullback f i) (i₂ : V₂ ⟶ CategoryTheory.Limits.pullback f i) [CategoryTheory.Limits.HasPullback i₁ i₂] :
CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst i₁ i₂) (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i))) (CategoryTheory.Limits.pullback.map i₁ i₂ (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.id V₁) (CategoryTheory.CategoryStruct.id V₂) (CategoryTheory.Limits.pullback.snd f i) ⋯ ⋯) (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.snd f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.snd f i)) f f (CategoryTheory.CategoryStruct.comp i₁ (CategoryTheory.Limits.pullback.fst f i)) (CategoryTheory.CategoryStruct.comp i₂ (CategoryTheory.Limits.pullback.fst f i)) i ⋯ ⋯)
source
def CategoryTheory.Limits.pullbackDiagonalMapIdIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [CategoryTheory.Limits.HasPullback i i] [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)] [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)] :
CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) ≅ CategoryTheory.Limits.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.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [CategoryTheory.Limits.HasPullback i i] [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)] [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)] :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).hom (CategoryTheory.Limits.pullback.fst f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i))
source
@[simp]
theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_fst_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [CategoryTheory.Limits.HasPullback i i] [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)] [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)] {Z : C} (h : X ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)) h)
source
@[simp]
theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_snd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [CategoryTheory.Limits.HasPullback i i] [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)] [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)] :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).hom (CategoryTheory.Limits.pullback.snd f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i))
source
@[simp]
theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_hom_snd_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [CategoryTheory.Limits.HasPullback i i] [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)] [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)] {Z : C} (h : Y ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)) h)
source
@[simp]
theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [CategoryTheory.Limits.HasPullback i i] [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)] [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)] :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) f
source
@[simp]
theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_fst_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [CategoryTheory.Limits.HasPullback i i] [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)] [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)] {Z : C} (h : T ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.CategoryStruct.comp f h)
source
@[simp]
theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [CategoryTheory.Limits.HasPullback i i] [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)] [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)] :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i))) = CategoryTheory.Limits.pullback.fst f g
source
@[simp]
theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [CategoryTheory.Limits.HasPullback i i] [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)] [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)] {Z : C} (h : X ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h
source
@[simp]
theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_snd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [CategoryTheory.Limits.HasPullback i i] [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)] [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)] :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i))) = CategoryTheory.Limits.pullback.snd f g
source
@[simp]
theorem CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_snd_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [CategoryTheory.Limits.HasPullback i i] [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)] [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)] {Z : C} (h : Y ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h
source
theorem CategoryTheory.Limits.pullback.diagonal_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y Z : C} [CategoryTheory.Limits.HasPullbacks C] (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.Limits.HasPullback f f] [CategoryTheory.Limits.HasPullback g g] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f g)] :
CategoryTheory.Limits.pullback.diagonal (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackDiagonalMapIdIso f f g).inv (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.diagonal g) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp f g) g g f f (CategoryTheory.CategoryStruct.id Z) ⋯ ⋯)))
source
theorem CategoryTheory.Limits.pullback_map_diagonal_isPullback {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [CategoryTheory.Limits.HasPullback i i] [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)] [CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)] :
CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) f) (CategoryTheory.Limits.pullback.map f g (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id Y) i ⋯ ⋯) (CategoryTheory.Limits.pullback.diagonal i) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
source
def CategoryTheory.Limits.diagonalObjPullbackFstIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
CategoryTheory.Limits.pullback.diagonalObj (CategoryTheory.Limits.pullback.fst f g) ≅ CategoryTheory.Limits.pullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f

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

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f) (CategoryTheory.Limits.pullback.fst g g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.Limits.pullback.snd f g)
source
@[simp]
theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_fst_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z✝ : C} (h : Y ⟶ Z✝) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g g) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h)
source
@[simp]
theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_snd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f) (CategoryTheory.Limits.pullback.snd g g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.Limits.pullback.snd f g)
source
@[simp]
theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_fst_snd_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z✝ : C} (h : Y ⟶ Z✝) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h)
source
@[simp]
theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_snd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).hom (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.Limits.pullback.fst f g)
source
@[simp]
theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_hom_snd_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z✝ : C} (h : X ⟶ Z✝) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h)
source
@[simp]
theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.Limits.pullback.fst f g)) = CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f
source
@[simp]
theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_fst_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z✝ : C} (h : X ⟶ Z✝) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f) h
source
@[simp]
theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_snd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.Limits.pullback.snd f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f) (CategoryTheory.Limits.pullback.fst g g)
source
@[simp]
theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_fst_snd_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z✝ : C} (h : Y ⟶ Z✝) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst g g) h)
source
@[simp]
theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.Limits.pullback.fst f g)) = CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f
source
@[simp]
theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_fst_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z✝ : C} (h : X ⟶ Z✝) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f g) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f) h
source
@[simp]
theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_snd {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.Limits.pullback.snd f g)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f) (CategoryTheory.Limits.pullback.snd g g)
source
@[simp]
theorem CategoryTheory.Limits.diagonalObjPullbackFstIso_inv_snd_snd_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {Z✝ : C} (h : Y ⟶ Z✝) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.fst f g)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) g) f) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd g g) h)
source
theorem CategoryTheory.Limits.diagonal_pullback_fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
CategoryTheory.Limits.pullback.diagonal (CategoryTheory.Limits.pullback.fst f g) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackSymmetry f (CategoryTheory.Over.mk g).hom).hom (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.pullback f).map (CategoryTheory.Over.homMk (CategoryTheory.Limits.pullback.diagonal g) ⋯)).left (CategoryTheory.Limits.diagonalObjPullbackFstIso f g).inv)
source
theorem CategoryTheory.Limits.pullback_lift_diagonal_isPullback {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y : C} [CategoryTheory.Limits.HasPullbacks C] {S : C} (g : Y ⟶ X) (f : X ⟶ S) :
CategoryTheory.IsPullback g (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.id Y) g ⋯) (CategoryTheory.Limits.pullback.diagonal f) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp g f) f f f g (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)

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

source
def CategoryTheory.Limits.pullbackFstFstIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.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₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f') (e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g') [CategoryTheory.Mono i₃] :
CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f' g') i₁) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f' g') i₂) ≅ CategoryTheory.Limits.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.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem CategoryTheory.Limits.pullbackFstFstIso_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.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₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f') (e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g') [CategoryTheory.Mono i₃] :
(CategoryTheory.Limits.pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).hom = CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f' g') i₁) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f' g') i₂)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst f' g') i₁)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f' g') i₁) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f' g') i₂)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd f' g') i₂)) ⋯
source
@[simp]
theorem CategoryTheory.Limits.pullbackFstFstIso_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.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₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f') (e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g') [CategoryTheory.Mono i₃] :
(CategoryTheory.Limits.pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).inv = CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) (CategoryTheory.Limits.pullback.fst f g) ⋯) (CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) (CategoryTheory.Limits.pullback.snd f g) ⋯) ⋯
source
theorem CategoryTheory.Limits.pullback_map_eq_pullbackFstFstIso_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.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₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f') (e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g') [CategoryTheory.Mono i₃] :
CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f' g') i₁) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f' g') i₂)) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f' g') i₂))
source
theorem CategoryTheory.Limits.pullback_lift_map_isPullback {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.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₁ : CategoryTheory.CategoryStruct.comp f i₃ = CategoryTheory.CategoryStruct.comp i₁ f') (e₂ : CategoryTheory.CategoryStruct.comp g i₃ = CategoryTheory.CategoryStruct.comp i₂ g') [CategoryTheory.Mono i₃] :
CategoryTheory.IsPullback (CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) (CategoryTheory.Limits.pullback.fst f g) ⋯) (CategoryTheory.Limits.pullback.lift (CategoryTheory.Limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) (CategoryTheory.Limits.pullback.snd f g) ⋯) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst f' g') i₁) (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.snd f' g') i₂)