Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-11 09:33 f7baecbb

View on Github →

feat(category_theory/functor): preserving/reflecting monos/epis (#14829)

Estimated changes

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

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

Modified src/algebraic_geometry/open_immersion.lean

Modified src/category_theory/adjunction/evaluation.lean

Modified src/category_theory/concrete_category/basic.lean

Modified src/category_theory/epi_mono.lean

deleted theorem category_theory.faithful_reflects_epi

deleted theorem category_theory.faithful_reflects_mono

deleted theorem category_theory.left_adjoint_preserves_epi

deleted theorem category_theory.right_adjoint_preserves_mono

Created src/category_theory/functor/epi_mono.lean

added theorem category_theory.functor.epi_of_epi_map

added theorem category_theory.functor.mono_of_mono_map

added theorem category_theory.functor.preserves_epimorphisms.iso_iff

added theorem category_theory.functor.preserves_epimorphisms.of_iso

added theorem category_theory.functor.preserves_epimorphsisms_of_adjunction

added theorem category_theory.functor.preserves_monomorphisms.iso_iff

added theorem category_theory.functor.preserves_monomorphisms.of_iso

added theorem category_theory.functor.preserves_monomorphisms_of_adjunction

added theorem category_theory.functor.reflects_epimorphisms.iso_iff

added theorem category_theory.functor.reflects_epimorphisms.of_iso

added theorem category_theory.functor.reflects_monomorphisms.iso_iff

added theorem category_theory.functor.reflects_monomorphisms.of_iso

Modified src/category_theory/glue_data.lean

Modified src/category_theory/limits/constructions/epi_mono.lean

added theorem category_theory.preserves_epi_of_preserves_colimit

added theorem category_theory.preserves_mono_of_preserves_limit

deleted theorem category_theory.reflects_epi

added theorem category_theory.reflects_epi_of_reflects_colimit

deleted theorem category_theory.reflects_mono

added theorem category_theory.reflects_mono_of_reflects_limit

Modified src/category_theory/over.lean

Modified src/topology/category/CompHaus/default.lean

Modified src/topology/category/Profinite/default.lean

Modified src/topology/category/Top/adjunctions.lean

Modified src/topology/category/Top/epi_mono.lean