Theorems · Theorem · category theory
CategoryTheory.MorphismProperty.ofHoms_iff
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_3} {X Y : ι → C} (f : (i : ι) → X i ⟶ Y i)
{A B : C} (g : A ⟶ B),
CategoryTheory.MorphismProperty.ofHoms f g ↔ ∃ i, CategoryTheory.Arrow.mk g = CategoryTheory.Arrow.mk (f i)- Cited by
- 8 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites8
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.Arrowstatement and proof · cited by 713
- CategoryTheory.Arrow.mkstatement and proof · cited by 421
- CategoryTheory.MorphismProperty.ofHomsstatement and proof · cited by 30
- CategoryTheory.MorphismProperty.ofHoms.casesOnproof · cited by 26
- CategoryTheory.MorphismProperty.toSetproof · cited by 26
- CategoryTheory.MorphismProperty.arrow_mk_mem_toSet_iffproof · cited by 4
Cited by8
Results whose statement or proof uses this declaration.
- CategoryTheory.MorphismProperty.ofHoms_homFamilyproof · cited by 2
- CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.eq_id_of_D₂_Wproof · cited by 1
- CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.final_functorproof · cited by 1
- CategoryTheory.Cat.FreeRefl.morphismPropertyHomMk_homMkproof · cited by 1
- SSet.Truncated.HomotopyCategory.morphismPropertyHomMk_of_edgeproof · cited by 1
- CategoryTheory.MorphismProperty.isSmall_iff_eq_ofHomsproof · cited by 0
- CategoryTheory.MorphismProperty.hasCardinalLT_ofHomsproof · cited by 0
- HomotopicalAlgebra.nonempty_attachCells_iffproof · cited by 0