Commit 2022-08-13 07:30 239d882c

View on Github →

refactor(category_theory/epi_mono): is_split_epi and split_epi (#16036) This PR makes a distinction between the class is_split_epi f which is a Prop and split_epi f which contains the datum of a section of f.

Estimated changes

Modified src/category_theory/adjunction/reflective.lean

added theorem category_theory.mem_ess_image_of_unit_is_split_mono

deleted theorem category_theory.mem_ess_image_of_unit_split_mono

Modified src/category_theory/closed/cartesian.lean

Modified src/category_theory/closed/ideal.lean

Modified src/category_theory/epi_mono.lean

added theorem category_theory.is_iso.of_epi_section'

modified theorem category_theory.is_iso.of_epi_section

added theorem category_theory.is_iso.of_mono_retraction'

modified theorem category_theory.is_iso.of_mono_retraction

added theorem category_theory.is_iso_of_epi_of_is_split_mono

deleted theorem category_theory.is_iso_of_epi_of_split_mono

added theorem category_theory.is_iso_of_mono_of_is_split_epi

deleted theorem category_theory.is_iso_of_mono_of_split_epi

added theorem category_theory.is_split_epi.id

added theorem category_theory.is_split_epi.mk'

added theorem category_theory.is_split_epi_of_epi

added theorem category_theory.is_split_mono.id

added theorem category_theory.is_split_mono.mk'

added theorem category_theory.is_split_mono_of_mono

deleted def category_theory.retraction

deleted def category_theory.section_

added theorem category_theory.split_epi.epi

deleted theorem category_theory.split_epi.id

added def category_theory.split_epi.map

added def category_theory.split_epi.split_mono

added structure category_theory.split_epi

deleted def category_theory.split_epi_of_epi

deleted theorem category_theory.split_mono.id

added def category_theory.split_mono.map

added theorem category_theory.split_mono.mono

added def category_theory.split_mono.split_epi

added structure category_theory.split_mono

deleted def category_theory.split_mono_of_mono

Modified src/category_theory/functor/epi_mono.lean

deleted def category_theory.functor.map_split_epi

deleted def category_theory.functor.map_split_mono

Modified src/category_theory/generator.lean

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

Modified src/category_theory/limits/preserves/shapes/biproducts.lean

deleted theorem category_theory.functor.retraction_biprod_comparison'

deleted theorem category_theory.functor.retraction_biproduct_comparison'

deleted theorem category_theory.functor.section_biprod_comparison

deleted theorem category_theory.functor.section_biproduct_comparison

added def category_theory.functor.split_epi_biprod_comparison

added def category_theory.functor.split_epi_biproduct_comparison

added def category_theory.functor.split_mono_biprod_comparison'

added def category_theory.functor.split_mono_biproduct_comparison'

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

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

added def category_theory.limits.binary_bicone_of_is_split_epi_of_kernel

added def category_theory.limits.binary_bicone_of_is_split_mono_of_cokernel

deleted def category_theory.limits.binary_bicone_of_split_epi_of_kernel

deleted def category_theory.limits.binary_bicone_of_split_mono_of_cokernel

added def category_theory.limits.is_bilimit_binary_bicone_of_is_split_epi_of_kernel

added def category_theory.limits.is_bilimit_binary_bicone_of_is_split_mono_of_cokernel

deleted def category_theory.limits.is_bilimit_binary_bicone_of_split_epi_of_kernel

deleted def category_theory.limits.is_bilimit_binary_bicone_of_split_mono_of_cokernel

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

added def category_theory.limits.cocone_of_is_split_epi

added theorem category_theory.limits.cocone_of_is_split_epi_π

deleted def category_theory.limits.cocone_of_split_epi

deleted theorem category_theory.limits.cocone_of_split_epi_π

added def category_theory.limits.cone_of_is_split_mono

added theorem category_theory.limits.cone_of_is_split_mono_ι

deleted def category_theory.limits.cone_of_split_mono

deleted theorem category_theory.limits.cone_of_split_mono_ι

added def category_theory.limits.is_split_epi_coequalizes

added def category_theory.limits.is_split_mono_equalizes

deleted def category_theory.limits.split_epi_coequalizes

deleted def category_theory.limits.split_mono_equalizes

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

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

added theorem category_theory.limits.is_initial.is_split_epi_to

deleted def category_theory.limits.is_initial.split_epi_to

added theorem category_theory.limits.is_terminal.is_split_mono_from

deleted def category_theory.limits.is_terminal.split_mono_from

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

added theorem category_theory.limits.is_zero.iff_is_split_epi_eq_zero

added theorem category_theory.limits.is_zero.iff_is_split_mono_eq_zero

deleted theorem category_theory.limits.is_zero.iff_split_epi_eq_zero

deleted theorem category_theory.limits.is_zero.iff_split_mono_eq_zero

Modified src/category_theory/simple.lean

Modified src/category_theory/sites/sheaf_of_types.lean

Modified src/category_theory/sites/sieves.lean

added def category_theory.sieve.galois_insertion_of_is_split_epi

deleted def category_theory.sieve.galois_insertion_of_split_epi

added theorem category_theory.sieve.generate_of_contains_is_split_epi

deleted theorem category_theory.sieve.generate_of_contains_split_epi

added theorem category_theory.sieve.generate_of_singleton_is_split_epi

deleted theorem category_theory.sieve.generate_of_singleton_split_epi

Modified src/category_theory/types.lean