Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-02 06:44 6394e4d4

View on Github →

feat(algebra/category/*): forget reflects isos (#3600)

Estimated changes

Modified src/algebra/category/Algebra/basic.lean

Modified src/algebra/category/CommRing/basic.lean

Modified src/algebra/category/Group/adjunctions.lean

Modified src/algebra/category/Group/basic.lean

Modified src/algebra/category/Group/images.lean

Modified src/algebra/category/Mon/basic.lean

Created src/category_theory/concrete_category/reflects_isomorphisms.lean

Modified src/category_theory/limits/cones.lean

added def category_theory.limits.cocones.cocone_iso_of_hom_iso

added def category_theory.limits.cones.cone_iso_of_hom_iso

Modified src/category_theory/limits/limits.lean

Modified src/category_theory/monad/algebra.lean

Modified src/category_theory/over.lean

Deleted src/category_theory/reflect_isomorphisms.lean

deleted def category_theory.cocone_iso_of_hom_iso

deleted def category_theory.cone_iso_of_hom_iso

deleted def category_theory.is_iso_of_reflects_iso

Created src/category_theory/reflects_isomorphisms.lean

added def category_theory.is_iso_of_reflects_iso

Modified src/topology/category/TopCommRing.lean

Modified src/topology/sheaves/presheaf_of_functions.lean