Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-01 11:17 563aed34

View on Github →

feat(algebraic_topology/simplex_category): strong epi mono factorisations (#16276) In this PR, it is shown that there exists (unique) strong epi mono factorisations in simplex_category.

Estimated changes

Modified src/algebraic_topology/simplex_category.lean

modified theorem simplex_category.eq_id_of_is_iso

added theorem simplex_category.factor_thru_image_eq

added theorem simplex_category.image_eq

added theorem simplex_category.image_ι_eq

added theorem simplex_category.skeletal_functor.coe_map

Modified src/category_theory/functor/epi_mono.lean

added def category_theory.functor.split_epi_category_imp_of_is_equivalence

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

added theorem category_theory.functor.has_strong_epi_mono_factorisations_imp_of_is_equivalence

Modified src/order/category/NonemptyFinLinOrd.lean

added theorem NonemptyFinLinOrd.epi_iff_surjective

added theorem NonemptyFinLinOrd.mono_iff_injective