Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-23 07:23 a5866810

View on Github →

feat(category_theory/limits/shapes): Multiequalizer is the equalizer (#10267)

Estimated changes

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

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

added def category_theory.limits.multicoequalizer.iso_coequalizer

added def category_theory.limits.multicoequalizer.sigma_π

added theorem category_theory.limits.multicoequalizer.ι_sigma_π

added def category_theory.limits.multicofork.of_sigma_cofork

added theorem category_theory.limits.multicofork.of_sigma_cofork_ι_app_left

added theorem category_theory.limits.multicofork.of_sigma_cofork_ι_app_right

added theorem category_theory.limits.multicofork.sigma_condition

added def category_theory.limits.multicofork.to_sigma_cofork

added theorem category_theory.limits.multicofork.to_sigma_cofork_ι_app_one

added theorem category_theory.limits.multicofork.to_sigma_cofork_ι_app_zero

modified def category_theory.limits.multicofork

added def category_theory.limits.multicospan_index.fst_pi_map

added theorem category_theory.limits.multicospan_index.fst_pi_map_π

added def category_theory.limits.multicospan_index.multifork_equiv_pi_fork

added def category_theory.limits.multicospan_index.of_pi_fork_functor

added def category_theory.limits.multicospan_index.parallel_pair_diagram

added def category_theory.limits.multicospan_index.snd_pi_map

added theorem category_theory.limits.multicospan_index.snd_pi_map_π

added def category_theory.limits.multicospan_index.to_pi_fork_functor

added def category_theory.limits.multiequalizer.iso_equalizer

added def category_theory.limits.multiequalizer.ι_pi

added theorem category_theory.limits.multiequalizer.ι_pi_π

added def category_theory.limits.multifork.of_pi_fork

added theorem category_theory.limits.multifork.of_pi_fork_π_app_left

added theorem category_theory.limits.multifork.of_pi_fork_π_app_right

added theorem category_theory.limits.multifork.pi_condition

added def category_theory.limits.multifork.to_pi_fork

added theorem category_theory.limits.multifork.to_pi_fork_π_app_one

added theorem category_theory.limits.multifork.to_pi_fork_π_app_zero

modified def category_theory.limits.multifork

added def category_theory.limits.multispan_index.fst_sigma_map

added def category_theory.limits.multispan_index.multicofork_equiv_sigma_cofork

added def category_theory.limits.multispan_index.of_sigma_cofork_functor

added def category_theory.limits.multispan_index.parallel_pair_diagram

added def category_theory.limits.multispan_index.snd_sigma_map

added def category_theory.limits.multispan_index.to_sigma_cofork_functor

added theorem category_theory.limits.multispan_index.ι_fst_sigma_map

added theorem category_theory.limits.multispan_index.ι_snd_sigma_map