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
Instances For
    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
    Instances For
      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)
      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)
      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)
      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)
      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.
      Instances For
        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.
        Instances For
          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.
          Instances For
            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.
            Instances For
              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.
              Instances For
                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.
                Instances For
                  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₂)