mathlib3 documentation

category_theory.limits.shapes.diagonal

The diagonal object of a morphism. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

source
@[reducible]
noncomputable def category_theory.limits.pullback.diagonal_obj {C : Type u_1} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_pullback f f] :
C

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

source
noncomputable def category_theory.limits.pullback.diagonal {C : Type u_1} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_pullback f f] :
X ⟶ category_theory.limits.pullback.diagonal_obj f

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

Equations
Instances for category_theory.limits.pullback.diagonal
source
@[simp]
theorem category_theory.limits.pullback.diagonal_fst {C : Type u_1} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_pullback f f] :
category_theory.limits.pullback.diagonal f ≫ category_theory.limits.pullback.fst = 𝟙 X
source
@[simp]
theorem category_theory.limits.pullback.diagonal_fst_assoc {C : Type u_1} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_pullback f f] {X' : C} (f' : X ⟶ X') :
category_theory.limits.pullback.diagonal f ≫ category_theory.limits.pullback.fst ≫ f' = f'
source
@[simp]
theorem category_theory.limits.pullback.diagonal_snd {C : Type u_1} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_pullback f f] :
category_theory.limits.pullback.diagonal f ≫ category_theory.limits.pullback.snd = 𝟙 X
source
@[simp]
theorem category_theory.limits.pullback.diagonal_snd_assoc {C : Type u_1} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_pullback f f] {X' : C} (f' : X ⟶ X') :
category_theory.limits.pullback.diagonal f ≫ category_theory.limits.pullback.snd ≫ f' = f'
source
@[protected, instance]
def category_theory.limits.pullback.diagonal.category_theory.is_split_mono {C : Type u_1} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_pullback f f] :
category_theory.is_split_mono (category_theory.limits.pullback.diagonal f)
source
@[protected, instance]
def category_theory.limits.pullback.fst.category_theory.is_split_epi {C : Type u_1} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_pullback f f] :
category_theory.is_split_epi category_theory.limits.pullback.fst
source
@[protected, instance]
def category_theory.limits.pullback.snd.category_theory.is_split_epi {C : Type u_1} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_pullback f f] :
category_theory.is_split_epi category_theory.limits.pullback.snd
source
@[protected, instance]
def category_theory.limits.pullback.diagonal.category_theory.is_iso {C : Type u_1} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_pullback f f] [category_theory.mono f] :
category_theory.is_iso (category_theory.limits.pullback.diagonal f)
source
theorem category_theory.limits.pullback.diagonal_is_kernel_pair {C : Type u_1} [category_theory.category C] {X Y : C} (f : X ⟶ Y) [category_theory.limits.has_pullback f f] :
category_theory.is_kernel_pair f category_theory.limits.pullback.fst category_theory.limits.pullback.snd

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

source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_snd_fst_fst_assoc {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ category_theory.limits.pullback f i) (i₂ : V₂ ⟶ category_theory.limits.pullback f i) {X' : C} (f' : X ⟶ X') :
category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst ≫ i₁ ≫ category_theory.limits.pullback.fst ≫ f' = category_theory.limits.pullback.fst ≫ f'
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_snd_fst_fst {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ category_theory.limits.pullback f i) (i₂ : V₂ ⟶ category_theory.limits.pullback f i) :
category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst ≫ i₁ ≫ category_theory.limits.pullback.fst = category_theory.limits.pullback.fst
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_snd_snd_fst_assoc {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ category_theory.limits.pullback f i) (i₂ : V₂ ⟶ category_theory.limits.pullback f i) {X' : C} (f' : X ⟶ X') :
category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd ≫ i₂ ≫ category_theory.limits.pullback.fst ≫ f' = category_theory.limits.pullback.fst ≫ f'
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_snd_snd_fst {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ category_theory.limits.pullback f i) (i₂ : V₂ ⟶ category_theory.limits.pullback f i) :
category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd ≫ i₂ ≫ category_theory.limits.pullback.fst = category_theory.limits.pullback.fst
source
noncomputable def category_theory.limits.pullback_diagonal_map_iso {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ category_theory.limits.pullback f i) (i₂ : V₂ ⟶ category_theory.limits.pullback f i) [category_theory.limits.has_pullback i₁ i₂] :
category_theory.limits.pullback (category_theory.limits.pullback.diagonal f) (category_theory.limits.pullback.map (i₁ ≫ category_theory.limits.pullback.snd) (i₂ ≫ category_theory.limits.pullback.snd) f f (i₁ ≫ category_theory.limits.pullback.fst) (i₂ ≫ category_theory.limits.pullback.fst) i _ _) ≅ category_theory.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_is_pullback.

Equations
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_iso_hom_fst {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ category_theory.limits.pullback f i) (i₂ : V₂ ⟶ category_theory.limits.pullback f i) [category_theory.limits.has_pullback i₁ i₂] :
(category_theory.limits.pullback_diagonal_map_iso f i i₁ i₂).hom ≫ category_theory.limits.pullback.fst = category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_iso_hom_fst_assoc {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ category_theory.limits.pullback f i) (i₂ : V₂ ⟶ category_theory.limits.pullback f i) [category_theory.limits.has_pullback i₁ i₂] {X' : C} (f' : V₁ ⟶ X') :
(category_theory.limits.pullback_diagonal_map_iso f i i₁ i₂).hom ≫ category_theory.limits.pullback.fst ≫ f' = category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst ≫ f'
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_iso_hom_snd {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ category_theory.limits.pullback f i) (i₂ : V₂ ⟶ category_theory.limits.pullback f i) [category_theory.limits.has_pullback i₁ i₂] :
(category_theory.limits.pullback_diagonal_map_iso f i i₁ i₂).hom ≫ category_theory.limits.pullback.snd = category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_iso_hom_snd_assoc {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ category_theory.limits.pullback f i) (i₂ : V₂ ⟶ category_theory.limits.pullback f i) [category_theory.limits.has_pullback i₁ i₂] {X' : C} (f' : V₂ ⟶ X') :
(category_theory.limits.pullback_diagonal_map_iso f i i₁ i₂).hom ≫ category_theory.limits.pullback.snd ≫ f' = category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd ≫ f'
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_iso_inv_fst_assoc {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ category_theory.limits.pullback f i) (i₂ : V₂ ⟶ category_theory.limits.pullback f i) [category_theory.limits.has_pullback i₁ i₂] {X' : C} (f' : X ⟶ X') :
(category_theory.limits.pullback_diagonal_map_iso f i i₁ i₂).inv ≫ category_theory.limits.pullback.fst ≫ f' = category_theory.limits.pullback.fst ≫ i₁ ≫ category_theory.limits.pullback.fst ≫ f'
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_iso_inv_fst {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ category_theory.limits.pullback f i) (i₂ : V₂ ⟶ category_theory.limits.pullback f i) [category_theory.limits.has_pullback i₁ i₂] :
(category_theory.limits.pullback_diagonal_map_iso f i i₁ i₂).inv ≫ category_theory.limits.pullback.fst = category_theory.limits.pullback.fst ≫ i₁ ≫ category_theory.limits.pullback.fst
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_iso_inv_snd_fst_assoc {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ category_theory.limits.pullback f i) (i₂ : V₂ ⟶ category_theory.limits.pullback f i) [category_theory.limits.has_pullback i₁ i₂] {X' : C} (f' : V₁ ⟶ X') :
(category_theory.limits.pullback_diagonal_map_iso f i i₁ i₂).inv ≫ category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst ≫ f' = category_theory.limits.pullback.fst ≫ f'
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_iso_inv_snd_fst {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ category_theory.limits.pullback f i) (i₂ : V₂ ⟶ category_theory.limits.pullback f i) [category_theory.limits.has_pullback i₁ i₂] :
(category_theory.limits.pullback_diagonal_map_iso f i i₁ i₂).inv ≫ category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst = category_theory.limits.pullback.fst
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_iso_inv_snd_snd {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ category_theory.limits.pullback f i) (i₂ : V₂ ⟶ category_theory.limits.pullback f i) [category_theory.limits.has_pullback i₁ i₂] :
(category_theory.limits.pullback_diagonal_map_iso f i i₁ i₂).inv ≫ category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd = category_theory.limits.pullback.snd
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_iso_inv_snd_snd_assoc {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ category_theory.limits.pullback f i) (i₂ : V₂ ⟶ category_theory.limits.pullback f i) [category_theory.limits.has_pullback i₁ i₂] {X' : C} (f' : V₂ ⟶ X') :
(category_theory.limits.pullback_diagonal_map_iso f i i₁ i₂).inv ≫ category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd ≫ f' = category_theory.limits.pullback.snd ≫ f'
source
theorem category_theory.limits.pullback_fst_map_snd_is_pullback {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {U V₁ V₂ : C} (f : X ⟶ Y) (i : U ⟶ Y) (i₁ : V₁ ⟶ category_theory.limits.pullback f i) (i₂ : V₂ ⟶ category_theory.limits.pullback f i) [category_theory.limits.has_pullback i₁ i₂] :
category_theory.is_pullback (category_theory.limits.pullback.fst ≫ i₁ ≫ category_theory.limits.pullback.fst) (category_theory.limits.pullback.map i₁ i₂ (i₁ ≫ category_theory.limits.pullback.snd) (i₂ ≫ category_theory.limits.pullback.snd) (𝟙 V₁) (𝟙 V₂) category_theory.limits.pullback.snd _ _) (category_theory.limits.pullback.diagonal f) (category_theory.limits.pullback.map (i₁ ≫ category_theory.limits.pullback.snd) (i₂ ≫ category_theory.limits.pullback.snd) f f (i₁ ≫ category_theory.limits.pullback.fst) (i₂ ≫ category_theory.limits.pullback.fst) i _ _)
source
noncomputable def category_theory.limits.pullback_diagonal_map_id_iso {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [category_theory.limits.has_pullback i i] [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (f ≫ i) (g ≫ i)] [category_theory.limits.has_pullback (category_theory.limits.pullback.diagonal i) (category_theory.limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) _ _)] :
category_theory.limits.pullback (category_theory.limits.pullback.diagonal i) (category_theory.limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) _ _) ≅ category_theory.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_is_pullback.

Equations
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_id_iso_hom_fst {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [category_theory.limits.has_pullback i i] [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (f ≫ i) (g ≫ i)] [category_theory.limits.has_pullback (category_theory.limits.pullback.diagonal i) (category_theory.limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) _ _)] :
(category_theory.limits.pullback_diagonal_map_id_iso f g i).hom ≫ category_theory.limits.pullback.fst = category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_id_iso_hom_fst_assoc {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [category_theory.limits.has_pullback i i] [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (f ≫ i) (g ≫ i)] [category_theory.limits.has_pullback (category_theory.limits.pullback.diagonal i) (category_theory.limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) _ _)] {X' : C} (f' : X ⟶ X') :
(category_theory.limits.pullback_diagonal_map_id_iso f g i).hom ≫ category_theory.limits.pullback.fst ≫ f' = category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst ≫ f'
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_id_iso_hom_snd {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [category_theory.limits.has_pullback i i] [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (f ≫ i) (g ≫ i)] [category_theory.limits.has_pullback (category_theory.limits.pullback.diagonal i) (category_theory.limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) _ _)] :
(category_theory.limits.pullback_diagonal_map_id_iso f g i).hom ≫ category_theory.limits.pullback.snd = category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_id_iso_hom_snd_assoc {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [category_theory.limits.has_pullback i i] [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (f ≫ i) (g ≫ i)] [category_theory.limits.has_pullback (category_theory.limits.pullback.diagonal i) (category_theory.limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) _ _)] {X' : C} (f' : Y ⟶ X') :
(category_theory.limits.pullback_diagonal_map_id_iso f g i).hom ≫ category_theory.limits.pullback.snd ≫ f' = category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd ≫ f'
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_id_iso_inv_fst_assoc {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [category_theory.limits.has_pullback i i] [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (f ≫ i) (g ≫ i)] [category_theory.limits.has_pullback (category_theory.limits.pullback.diagonal i) (category_theory.limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) _ _)] {X' : C} (f' : T ⟶ X') :
(category_theory.limits.pullback_diagonal_map_id_iso f g i).inv ≫ category_theory.limits.pullback.fst ≫ f' = category_theory.limits.pullback.fst ≫ f ≫ f'
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_id_iso_inv_fst {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [category_theory.limits.has_pullback i i] [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (f ≫ i) (g ≫ i)] [category_theory.limits.has_pullback (category_theory.limits.pullback.diagonal i) (category_theory.limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) _ _)] :
(category_theory.limits.pullback_diagonal_map_id_iso f g i).inv ≫ category_theory.limits.pullback.fst = category_theory.limits.pullback.fst ≫ f
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_id_iso_inv_snd_fst {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [category_theory.limits.has_pullback i i] [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (f ≫ i) (g ≫ i)] [category_theory.limits.has_pullback (category_theory.limits.pullback.diagonal i) (category_theory.limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) _ _)] :
(category_theory.limits.pullback_diagonal_map_id_iso f g i).inv ≫ category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst = category_theory.limits.pullback.fst
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_id_iso_inv_snd_fst_assoc {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [category_theory.limits.has_pullback i i] [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (f ≫ i) (g ≫ i)] [category_theory.limits.has_pullback (category_theory.limits.pullback.diagonal i) (category_theory.limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) _ _)] {X' : C} (f' : X ⟶ X') :
(category_theory.limits.pullback_diagonal_map_id_iso f g i).inv ≫ category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst ≫ f' = category_theory.limits.pullback.fst ≫ f'
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_id_iso_inv_snd_snd_assoc {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [category_theory.limits.has_pullback i i] [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (f ≫ i) (g ≫ i)] [category_theory.limits.has_pullback (category_theory.limits.pullback.diagonal i) (category_theory.limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) _ _)] {X' : C} (f' : Y ⟶ X') :
(category_theory.limits.pullback_diagonal_map_id_iso f g i).inv ≫ category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd ≫ f' = category_theory.limits.pullback.snd ≫ f'
source
@[simp]
theorem category_theory.limits.pullback_diagonal_map_id_iso_inv_snd_snd {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [category_theory.limits.has_pullback i i] [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (f ≫ i) (g ≫ i)] [category_theory.limits.has_pullback (category_theory.limits.pullback.diagonal i) (category_theory.limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) _ _)] :
(category_theory.limits.pullback_diagonal_map_id_iso f g i).inv ≫ category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd = category_theory.limits.pullback.snd
source
theorem category_theory.limits.pullback.diagonal_comp {C : Type u_1} [category_theory.category C] {X Y Z : C} [category_theory.limits.has_pullbacks C] (f : X ⟶ Y) (g : Y ⟶ Z) [category_theory.limits.has_pullback f f] [category_theory.limits.has_pullback g g] [category_theory.limits.has_pullback (f ≫ g) (f ≫ g)] :
category_theory.limits.pullback.diagonal (f ≫ g) = category_theory.limits.pullback.diagonal f ≫ (category_theory.limits.pullback_diagonal_map_id_iso f f g).inv ≫ category_theory.limits.pullback.snd
source
theorem category_theory.limits.pullback_map_diagonal_is_pullback {C : Type u_1} [category_theory.category C] {X Y : C} [category_theory.limits.has_pullbacks C] {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [category_theory.limits.has_pullback i i] [category_theory.limits.has_pullback f g] [category_theory.limits.has_pullback (f ≫ i) (g ≫ i)] [category_theory.limits.has_pullback (category_theory.limits.pullback.diagonal i) (category_theory.limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) _ _)] :
category_theory.is_pullback (category_theory.limits.pullback.fst ≫ f) (category_theory.limits.pullback.map f g (f ≫ i) (g ≫ i) (𝟙 X) (𝟙 Y) i _ _) (category_theory.limits.pullback.diagonal i) (category_theory.limits.pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 S) _ _)
source
noncomputable def category_theory.limits.diagonal_obj_pullback_fst_iso {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
category_theory.limits.pullback.diagonal_obj category_theory.limits.pullback.fst ≅ category_theory.limits.pullback (category_theory.limits.pullback.snd ≫ g) f

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

Equations
source
@[simp]
theorem category_theory.limits.diagonal_obj_pullback_fst_iso_hom_fst_fst {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
(category_theory.limits.diagonal_obj_pullback_fst_iso f g).hom ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.fst = category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd
source
@[simp]
theorem category_theory.limits.diagonal_obj_pullback_fst_iso_hom_fst_fst_assoc {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {X' : C} (f' : Y ⟶ X') :
(category_theory.limits.diagonal_obj_pullback_fst_iso f g).hom ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.fst ≫ f' = category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd ≫ f'
source
@[simp]
theorem category_theory.limits.diagonal_obj_pullback_fst_iso_hom_fst_snd {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
(category_theory.limits.diagonal_obj_pullback_fst_iso f g).hom ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd = category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd
source
@[simp]
theorem category_theory.limits.diagonal_obj_pullback_fst_iso_hom_fst_snd_assoc {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {X' : C} (f' : Y ⟶ X') :
(category_theory.limits.diagonal_obj_pullback_fst_iso f g).hom ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd ≫ f' = category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd ≫ f'
source
@[simp]
theorem category_theory.limits.diagonal_obj_pullback_fst_iso_hom_snd_assoc {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {X' : C} (f' : X ⟶ X') :
(category_theory.limits.diagonal_obj_pullback_fst_iso f g).hom ≫ category_theory.limits.pullback.snd ≫ f' = category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.fst ≫ f'
source
@[simp]
theorem category_theory.limits.diagonal_obj_pullback_fst_iso_hom_snd {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
(category_theory.limits.diagonal_obj_pullback_fst_iso f g).hom ≫ category_theory.limits.pullback.snd = category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.fst
source
@[simp]
theorem category_theory.limits.diagonal_obj_pullback_fst_iso_inv_fst_fst {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
(category_theory.limits.diagonal_obj_pullback_fst_iso f g).inv ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.fst = category_theory.limits.pullback.snd
source
@[simp]
theorem category_theory.limits.diagonal_obj_pullback_fst_iso_inv_fst_fst_assoc {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {X' : C} (f' : X ⟶ X') :
(category_theory.limits.diagonal_obj_pullback_fst_iso f g).inv ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.fst ≫ f' = category_theory.limits.pullback.snd ≫ f'
source
@[simp]
theorem category_theory.limits.diagonal_obj_pullback_fst_iso_inv_fst_snd {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
(category_theory.limits.diagonal_obj_pullback_fst_iso f g).inv ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd = category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.fst
source
@[simp]
theorem category_theory.limits.diagonal_obj_pullback_fst_iso_inv_fst_snd_assoc {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {X' : C} (f' : Y ⟶ X') :
(category_theory.limits.diagonal_obj_pullback_fst_iso f g).inv ≫ category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd ≫ f' = category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.fst ≫ f'
source
@[simp]
theorem category_theory.limits.diagonal_obj_pullback_fst_iso_inv_snd_fst_assoc {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {X' : C} (f' : X ⟶ X') :
(category_theory.limits.diagonal_obj_pullback_fst_iso f g).inv ≫ category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst ≫ f' = category_theory.limits.pullback.snd ≫ f'
source
@[simp]
theorem category_theory.limits.diagonal_obj_pullback_fst_iso_inv_snd_fst {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
(category_theory.limits.diagonal_obj_pullback_fst_iso f g).inv ≫ category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst = category_theory.limits.pullback.snd
source
@[simp]
theorem category_theory.limits.diagonal_obj_pullback_fst_iso_inv_snd_snd_assoc {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) {X' : C} (f' : Y ⟶ X') :
(category_theory.limits.diagonal_obj_pullback_fst_iso f g).inv ≫ category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd ≫ f' = category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd ≫ f'
source
@[simp]
theorem category_theory.limits.diagonal_obj_pullback_fst_iso_inv_snd_snd {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
(category_theory.limits.diagonal_obj_pullback_fst_iso f g).inv ≫ category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd = category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd
source
theorem category_theory.limits.diagonal_pullback_fst {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
category_theory.limits.pullback.diagonal category_theory.limits.pullback.fst = (category_theory.limits.pullback_symmetry f g).hom ≫ ((category_theory.limits.base_change f).map (category_theory.over.hom_mk (category_theory.limits.pullback.diagonal g) _)).left ≫ (category_theory.limits.diagonal_obj_pullback_fst_iso f g).inv
source
@[simp]
theorem category_theory.limits.pullback_fst_fst_iso_inv {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks 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₁ : f ≫ i₃ = i₁ ≫ f') (e₂ : g ≫ i₃ = i₂ ≫ g') [category_theory.mono i₃] :
(category_theory.limits.pullback_fst_fst_iso f g f' g' i₁ i₂ i₃ e₁ e₂).inv = category_theory.limits.pullback.lift (category_theory.limits.pullback.lift (category_theory.limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) category_theory.limits.pullback.fst _) (category_theory.limits.pullback.lift (category_theory.limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) category_theory.limits.pullback.snd _) _
source
noncomputable def category_theory.limits.pullback_fst_fst_iso {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks 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₁ : f ≫ i₃ = i₁ ≫ f') (e₂ : g ≫ i₃ = i₂ ≫ g') [category_theory.mono i₃] :
category_theory.limits.pullback category_theory.limits.pullback.fst category_theory.limits.pullback.fst ≅ category_theory.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
source
@[simp]
theorem category_theory.limits.pullback_fst_fst_iso_hom {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks 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₁ : f ≫ i₃ = i₁ ≫ f') (e₂ : g ≫ i₃ = i₂ ≫ g') [category_theory.mono i₃] :
(category_theory.limits.pullback_fst_fst_iso f g f' g' i₁ i₂ i₃ e₁ e₂).hom = category_theory.limits.pullback.lift (category_theory.limits.pullback.fst ≫ category_theory.limits.pullback.snd) (category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd) _
source
theorem category_theory.limits.pullback_map_eq_pullback_fst_fst_iso_inv {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks 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₁ : f ≫ i₃ = i₁ ≫ f') (e₂ : g ≫ i₃ = i₂ ≫ g') [category_theory.mono i₃] :
category_theory.limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂ = (category_theory.limits.pullback_fst_fst_iso f g f' g' i₁ i₂ i₃ e₁ e₂).inv ≫ category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst
source
theorem category_theory.limits.pullback_lift_map_is_pullback {C : Type u_1} [category_theory.category C] [category_theory.limits.has_pullbacks 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₁ : f ≫ i₃ = i₁ ≫ f') (e₂ : g ≫ i₃ = i₂ ≫ g') [category_theory.mono i₃] :
category_theory.is_pullback (category_theory.limits.pullback.lift (category_theory.limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) category_theory.limits.pullback.fst _) (category_theory.limits.pullback.lift (category_theory.limits.pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) category_theory.limits.pullback.snd _) category_theory.limits.pullback.fst category_theory.limits.pullback.fst