Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-22 10:34 4591eb5c

View on Github →

chore(category_theory): replace has_hom with quiver (#7151)

Estimated changes

Modified src/algebraic_geometry/locally_ringed_space.lean

Modified src/algebraic_geometry/presheafed_space/has_colimits.lean

Modified src/category_theory/category/default.lean

Modified src/category_theory/epi_mono.lean

Modified src/category_theory/limits/cofinal.lean

Modified src/category_theory/limits/cones.lean

Modified src/category_theory/limits/has_limits.lean

Modified src/category_theory/limits/opposites.lean

Modified src/category_theory/limits/presheaf.lean

Modified src/category_theory/limits/shapes/terminal.lean

Modified src/category_theory/limits/yoneda.lean

Modified src/category_theory/opposites.lean

deleted def category_theory.has_hom.hom.op

deleted theorem category_theory.has_hom.hom.op_inj

deleted theorem category_theory.has_hom.hom.op_unop

deleted def category_theory.has_hom.hom.unop

deleted theorem category_theory.has_hom.hom.unop_inj

deleted theorem category_theory.has_hom.hom.unop_op

added theorem quiver.hom.op_inj

added theorem quiver.hom.op_unop

added theorem quiver.hom.unop_inj

added theorem quiver.hom.unop_op

Modified src/category_theory/yoneda.lean

Modified src/combinatorics/quiver.lean

added def quiver.hom.op

added def quiver.hom.unop

Modified src/tactic/elementwise.lean

Modified src/tactic/reassoc_axiom.lean

Modified src/topology/sheaves/presheaf.lean

Modified src/topology/sheaves/sheaf_condition/equalizer_products.lean

Modified src/topology/sheaves/sheaf_condition/pairwise_intersections.lean