Theorems · Theorem · category theory
CategoryTheory.MorphismProperty.ext
∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] (W W' : CategoryTheory.MorphismProperty C),
(∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f ↔ W' f) → W = W'- Cited by
- 61 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Quiver.Homstatement and proof · cited by 32,603
- CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
- CategoryTheory.CategoryStructstatement and proof · cited by 343
Cited by61
Results whose statement or proof uses this declaration.
- CategoryTheory.ObjectProperty.isLocal_eq_inverseImage_isomorphismsproof · cited by 3
- CategoryTheory.MorphismProperty.ofHoms_homFamilyproof · cited by 2
- SimplexCategory.Truncated.morphismProperty_eq_topproof · cited by 2
- CategoryTheory.GrothendieckTopology.W_inverseImage_whiskeringLeftproof · cited by 2
- CategoryTheory.Abelian.isoModSerre_kernel_eq_inverseImage_isomorphismsproof · cited by 2
- CategoryTheory.MorphismProperty.op_isomorphismsproof · cited by 2
- HomotopyCategory.inverseImage_quotient_isomorphismsproof · cited by 2
- HomotopyCategory.quasiIso_eq_trW_subcategoryAcyclicproof · cited by 2
- CategoryTheory.MorphismProperty.map_eq_isoClosureproof · cited by 2
- AlgebraicGeometry.geometrically_eq_universallyproof · cited by 2