Mathlib Map

Theorems · Definition · category theory

CategoryTheory.Limits.pullback.diagonal

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} →
      (f : X ⟶ Y) → [inst_1 : CategoryTheory.Limits.HasPullback f f] → X ⟶ CategoryTheory.Limits.pullback.diagonalObj f

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

Defined in
Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Cited by
67 results in Mathlib
Foundations
Depth 25 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
CategoryTheory.CategoryCategoryTheory.Limits.HasPullback
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

CategoryTheory.Limits.pullback.diagonal_fst · cited by 21pullback.diagonal_fstCategoryTheory.Limits.pullback.diagonal_snd · cited by 19pullback.diagonal_sndCategoryTheory.Limits.pullbackDiagonalMapIdIso · cited by 16Limits.pullbackDiagonalMa…CategoryTheory.Limits.pullbackDiagonalMapIso · cited by 15Limits.pullbackDiagonalMa…CategoryTheory.MorphismProperty.diagonal · cited by 12MorphismProperty.diagonalCategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_fst · cited by 4Limits.pullbackDiagonalMa…CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_snd_snd · cited by 4Limits.pullbackDiagonalMa…CategoryTheory.Limits.pullback.diagonal_fst_assoc · cited by 3pullback.diagonal_fst_ass…CategoryTheory.Limits.pullbackDiagonalMapIso.hom_fst · cited by 3pullbackDiagonalMapIso.ho…CategoryTheory.Limits.pullbackDiagonalMapIso.hom_snd · cited by 3pullbackDiagonalMapIso.ho…CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_fst · cited by 3pullbackDiagonalMapIso.in…CategoryTheory.Limits.pullbackDiagonalMapIso.inv_snd_snd · cited by 3pullbackDiagonalMapIso.in…CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_fst · cited by 3Limits.pullbackDiagonalMa…AlgebraicGeometry.quasiSeparated_iff · cited by 2AlgebraicGeometry.quasiSe…CategoryTheory.Limits.pullback_map_diagonal_isPullback · cited by 2Limits.pullback_map_diago…CategoryTheory.Category · cited by 32673CategoryTheory.CategoryQuiver.Hom · cited by 32603Quiver.HomCategoryTheory.CategoryStruct.id · cited by 6235CategoryStruct.idCategoryTheory.Limits.HasPullback · cited by 434Limits.HasPullbackCategoryTheory.Limits.pullback.lift · cited by 114pullback.liftCategoryTheory.Limits.pullback.diagonalObj · cited by 80pullback.diagonalObjpullback.diagonalCITED BYCITES

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by81

Results whose statement or proof uses this declaration.