Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-05 19:07 d69501f1

View on Github →

feat(category_theory/limits/shapes/multiequalizer): Multi(co)equalizers (#10169) This PR adds another special shape to the limits library, which directly generalizes shapes for many other special limits (like pullbacks, equalizers, etc.). A multiequalizer can be thought of an an equalizer of two maps between two products. This will be used later on in the context of sheafification. I don't know if there is a standard name for the gadgets this PR introduces. I would be happy to change the names if needed.

Estimated changes

Created src/category_theory/limits/shapes/multiequalizer.lean

added def category_theory.limits.has_multicoequalizer

added def category_theory.limits.has_multiequalizer

added theorem category_theory.limits.multicoequalizer.condition

added def category_theory.limits.multicoequalizer.desc

added theorem category_theory.limits.multicoequalizer.hom_ext

added def category_theory.limits.multicoequalizer.multicofork

added theorem category_theory.limits.multicoequalizer.multicofork_ι_app_right

added theorem category_theory.limits.multicoequalizer.multicofork_π

added def category_theory.limits.multicoequalizer.π

added theorem category_theory.limits.multicoequalizer.π_desc

added def category_theory.limits.multicoequalizer

added theorem category_theory.limits.multicofork.condition

added theorem category_theory.limits.multicofork.fst_app_right

added def category_theory.limits.multicofork.of_π

added theorem category_theory.limits.multicofork.snd_app_right

added def category_theory.limits.multicofork.π

added theorem category_theory.limits.multicofork.π_eq_app_right

added def category_theory.limits.multicofork

added def category_theory.limits.multicospan_index.multicospan

added theorem category_theory.limits.multicospan_index.multicospan_map_fst

added theorem category_theory.limits.multicospan_index.multicospan_map_snd

added theorem category_theory.limits.multicospan_index.multicospan_obj_left

added theorem category_theory.limits.multicospan_index.multicospan_obj_right

added structure category_theory.limits.multicospan_index

added theorem category_theory.limits.multiequalizer.condition

added theorem category_theory.limits.multiequalizer.hom_ext

added def category_theory.limits.multiequalizer.lift

added theorem category_theory.limits.multiequalizer.lift_ι

added def category_theory.limits.multiequalizer.multifork

added theorem category_theory.limits.multiequalizer.multifork_ι

added theorem category_theory.limits.multiequalizer.multifork_π_app_left

added def category_theory.limits.multiequalizer.ι

added def category_theory.limits.multiequalizer

added theorem category_theory.limits.multifork.app_left_fst

added theorem category_theory.limits.multifork.app_left_snd

added theorem category_theory.limits.multifork.condition

added def category_theory.limits.multifork.of_ι

added def category_theory.limits.multifork.ι

added theorem category_theory.limits.multifork.ι_eq_app_left

added def category_theory.limits.multifork

added def category_theory.limits.multispan_index.multispan

added theorem category_theory.limits.multispan_index.multispan_map_fst

added theorem category_theory.limits.multispan_index.multispan_map_snd

added theorem category_theory.limits.multispan_index.multispan_obj_left

added theorem category_theory.limits.multispan_index.multispan_obj_right

added structure category_theory.limits.multispan_index

added def category_theory.limits.walking_multicospan.hom.comp

added inductive category_theory.limits.walking_multicospan.hom

added inductive category_theory.limits.walking_multicospan

added def category_theory.limits.walking_multispan.hom.comp

added inductive category_theory.limits.walking_multispan.hom

added inductive category_theory.limits.walking_multispan