Mathlib Map

Theorems · Theorem · category theory

CategoryTheory.Limits.pullback.diagonal_fst

∀ {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],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.diagonal f)
      (CategoryTheory.Limits.pullback.fst f f) =
    CategoryTheory.CategoryStruct.id X
Defined in
Mathlib.CategoryTheory.Limits.Shapes.Diagonal
Cited by
21 results in Mathlib
Foundations
Depth 26 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_assoc · cited by 3pullback.diagonal_fst_ass…CategoryTheory.Limits.pullbackDiagonalMapIdIso_inv_fst · cited by 3Limits.pullbackDiagonalMa…CategoryTheory.Limits.pullback_map_diagonal_isPullback · cited by 2Limits.pullback_map_diago…AlgebraicGeometry.universallyInjective_eq_diagonal · cited by 2AlgebraicGeometry.univers…CategoryTheory.Limits.pullback_diagonal_map_snd_fst_fst · cited by 1Limits.pullback_diagonal_…CategoryTheory.Limits.pullback.comp_diagonal · cited by 1pullback.comp_diagonalCategoryTheory.Limits.pushout.op_codiagonal · cited by 1pushout.op_codiagonalCategoryTheory.Limits.pullback_fst_map_snd_isPullback · cited by 1Limits.pullback_fst_map_s…AlgebraicGeometry.Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange · cited by 1Pullback.range_diagonal_s…CategoryTheory.Limits.pullback_lift_diagonal_isPullback · cited by 1Limits.pullback_lift_diag…CategoryTheory.Limits.pullback.isIso_diagonal_iff · cited by 1pullback.isIso_diagonal_i…AlgebraicGeometry.IsSeparated.of_valuativeCriterion · cited by 1IsSeparated.of_valuativeC…AlgebraicGeometry.ExistsHomHomCompEqCompAux.exists_index · cited by 1ExistsHomHomCompEqCompAux…AlgebraicGeometry.IsSeparated.valuativeCriterion · cited by 1IsSeparated.valuativeCrit…AlgebraicGeometry.Scheme.isSeparated_iff_isClosedImmersion_prod_lift · cited by 0Scheme.isSeparated_iff_is…CategoryTheory.Category · cited by 32673CategoryTheory.CategoryQuiver.Hom · cited by 32603Quiver.HomCategoryTheory.CategoryStruct.comp · cited by 17999CategoryStruct.compCategoryTheory.CategoryStruct.id · cited by 6235CategoryStruct.idCategoryTheory.Limits.pullback.fst · cited by 639pullback.fstCategoryTheory.Limits.HasPullback · cited by 434Limits.HasPullbackCategoryTheory.Limits.pullback.diagonalObj · cited by 80pullback.diagonalObjCategoryTheory.Limits.pullback.diagonal · cited by 67pullback.diagonalCategoryTheory.Limits.pullback.lift_fst · cited by 40pullback.lift_fstpullback.diagonal_fstCITED BYCITES

Cites9

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

Cited by21

Results whose statement or proof uses this declaration.