Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-22 12:11 7e350c24

View on Github →

feat(category_theory/*): Fully faithful functors induces equivalence (#9322) Needed for AffineSchemes ≌ CommRingᵒᵖ.

Estimated changes

Modified src/category_theory/equivalence.lean

Modified src/category_theory/essential_image.lean

modified def category_theory.functor.to_ess_image_comp_essential_image_inclusion

Modified src/category_theory/fully_faithful.lean

added def category_theory.full.of_comp_faithful