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
.
The diagonal object of a morphism f : X ⟶ Y
is Δ_{X/Y} := pullback f f
.
The diagonal morphism X ⟶ Δ_{X/Y}
for a morphism f : X ⟶ Y
.
Equations
Instances for category_theory.limits.pullback.diagonal
The two projections Δ_{X/Y} ⟶ X
form a kernel pair for f : X ⟶ Y
.
Equations
- category_theory.limits.pullback.diagonal_is_kernel_pair f = {comm := _, is_limit := category_theory.limits.pullback_is_pullback f f _inst_2}
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
- category_theory.limits.pullback_diagonal_map_iso f i i₁ i₂ = {hom := category_theory.limits.pullback.lift (category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.fst) (category_theory.limits.pullback.snd ≫ category_theory.limits.pullback.snd) _, inv := category_theory.limits.pullback.lift (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 _ _) _, hom_inv_id' := _, inv_hom_id' := _}
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
- category_theory.limits.pullback_diagonal_map_id_iso f g i = category_theory.as_iso (category_theory.limits.pullback.map (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 i) (category_theory.limits.pullback.map ((f ≫ category_theory.inv category_theory.limits.pullback.fst) ≫ category_theory.limits.pullback.snd) ((g ≫ category_theory.inv category_theory.limits.pullback.fst) ≫ category_theory.limits.pullback.snd) i i ((f ≫ category_theory.inv category_theory.limits.pullback.fst) ≫ category_theory.limits.pullback.fst) ((g ≫ category_theory.inv category_theory.limits.pullback.fst) ≫ category_theory.limits.pullback.fst) (𝟙 S) _ _) (𝟙 T) (category_theory.limits.pullback.congr_hom _ _).hom (𝟙 (category_theory.limits.pullback.diagonal_obj i)) _ _) ≪≫ category_theory.limits.pullback_diagonal_map_iso i (𝟙 S) (f ≫ category_theory.inv category_theory.limits.pullback.fst) (g ≫ category_theory.inv category_theory.limits.pullback.fst) ≪≫ category_theory.as_iso (category_theory.limits.pullback.map (f ≫ category_theory.inv category_theory.limits.pullback.fst) (g ≫ category_theory.inv category_theory.limits.pullback.fst) f g (𝟙 X) (𝟙 Y) category_theory.limits.pullback.fst _ _)
The diagonal object of X ×[Z] Y ⟶ X
is isomorphic to Δ_{Y/Z} ×[Z] X
.
Equations
- category_theory.limits.diagonal_obj_pullback_fst_iso f g = category_theory.limits.pullback_right_pullback_fst_iso f g category_theory.limits.pullback.fst ≪≫ category_theory.limits.pullback.congr_hom _ _ ≪≫ category_theory.limits.pullback_assoc f g g g ≪≫ category_theory.limits.pullback_symmetry f (category_theory.limits.pullback.fst ≫ g) ≪≫ category_theory.limits.pullback.congr_hom _ _
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
- 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) _, 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 _) _, hom_inv_id' := _, inv_hom_id' := _}