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.

@[reducible, inline]

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

Equations
Instances For
    @[simp]
    theorem CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} [CategoryTheory.Limits.HasPullbacks C] {U : C} {V₁ : C} {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) :
    @[simp]
    theorem CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} [CategoryTheory.Limits.HasPullbacks C] {U : C} {V₁ : C} {V₂ : C} (f : X Y) (i : U Y) (i₁ : V₁ CategoryTheory.Limits.pullback f i) (i₂ : V₂ CategoryTheory.Limits.pullback f i) :
    @[simp]
    theorem CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} [CategoryTheory.Limits.HasPullbacks C] {U : C} {V₁ : C} {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) :
    @[simp]
    theorem CategoryTheory.Limits.pullback_diagonal_map_snd_snd_fst {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : C} {Y : C} [CategoryTheory.Limits.HasPullbacks C] {U : C} {V₁ : C} {V₂ : C} (f : X Y) (i : U Y) (i₁ : V₁ CategoryTheory.Limits.pullback f i) (i₂ : V₂ CategoryTheory.Limits.pullback f 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

      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
        @[simp]
        theorem CategoryTheory.Limits.pullbackFstFstIso_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {X : C} {Y : C} {S : C} {X' : C} {Y' : C} {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₃] :

        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