Commit 2023-03-23 16:06 b8ffec92

View on Github →

feat: Port CategoryTheory.Limits.Shapes.Multiequalizer (#2786)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean

added theorem CategoryTheory.Limits.Multicoequalizer.condition

added theorem CategoryTheory.Limits.Multicoequalizer.hom_ext

added def CategoryTheory.Limits.Multicoequalizer.isoCoequalizer

added theorem CategoryTheory.Limits.Multicoequalizer.multicofork_ι_app_right'

added theorem CategoryTheory.Limits.Multicoequalizer.multicofork_ι_app_right

added theorem CategoryTheory.Limits.Multicoequalizer.multicofork_π

added def CategoryTheory.Limits.Multicoequalizer.sigmaπ

added theorem CategoryTheory.Limits.Multicoequalizer.ι_sigmaπ

added theorem CategoryTheory.Limits.Multicoequalizer.π_desc

added def CategoryTheory.Limits.Multicofork.IsColimit.mk

added theorem CategoryTheory.Limits.Multicofork.condition

added theorem CategoryTheory.Limits.Multicofork.fst_app_right

added theorem CategoryTheory.Limits.Multicofork.ofSigmaCofork_ι_app_left

added theorem CategoryTheory.Limits.Multicofork.ofSigmaCofork_ι_app_right'

added theorem CategoryTheory.Limits.Multicofork.ofSigmaCofork_ι_app_right

added def CategoryTheory.Limits.Multicofork.ofπ

added theorem CategoryTheory.Limits.Multicofork.sigma_condition

added theorem CategoryTheory.Limits.Multicofork.snd_app_right

added theorem CategoryTheory.Limits.Multicofork.toSigmaCofork_π

added def CategoryTheory.Limits.Multicofork.π

added theorem CategoryTheory.Limits.Multicofork.π_comp_hom

added theorem CategoryTheory.Limits.Multicofork.π_eq_app_right

added theorem CategoryTheory.Limits.MulticospanIndex.fstPiMap_π

added def CategoryTheory.Limits.MulticospanIndex.multicospan

added theorem CategoryTheory.Limits.MulticospanIndex.multicospan_map_fst

added theorem CategoryTheory.Limits.MulticospanIndex.multicospan_map_snd

added theorem CategoryTheory.Limits.MulticospanIndex.multicospan_obj_left

added theorem CategoryTheory.Limits.MulticospanIndex.multicospan_obj_right

added theorem CategoryTheory.Limits.MulticospanIndex.sndPiMap_π

added structure CategoryTheory.Limits.MulticospanIndex

added theorem CategoryTheory.Limits.Multiequalizer.condition

added theorem CategoryTheory.Limits.Multiequalizer.hom_ext

added def CategoryTheory.Limits.Multiequalizer.isoEqualizer

added theorem CategoryTheory.Limits.Multiequalizer.lift_ι

added theorem CategoryTheory.Limits.Multiequalizer.multifork_ι

added theorem CategoryTheory.Limits.Multiequalizer.multifork_π_app_left

added def CategoryTheory.Limits.Multiequalizer.ιPi

added theorem CategoryTheory.Limits.Multiequalizer.ιPi_π

added def CategoryTheory.Limits.Multifork.IsLimit.mk

added theorem CategoryTheory.Limits.Multifork.app_left_eq_ι

added theorem CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_fst

added theorem CategoryTheory.Limits.Multifork.app_right_eq_ι_comp_snd

added theorem CategoryTheory.Limits.Multifork.condition

added theorem CategoryTheory.Limits.Multifork.hom_comp_ι

added theorem CategoryTheory.Limits.Multifork.ofPiFork_π_app_left

added theorem CategoryTheory.Limits.Multifork.ofPiFork_π_app_right

added def CategoryTheory.Limits.Multifork.ofι

added theorem CategoryTheory.Limits.Multifork.pi_condition

added theorem CategoryTheory.Limits.Multifork.toPiFork_π_app_one

added theorem CategoryTheory.Limits.Multifork.toPiFork_π_app_zero

added def CategoryTheory.Limits.Multifork.ι

added def CategoryTheory.Limits.MultispanIndex.multispan

added theorem CategoryTheory.Limits.MultispanIndex.multispan_map_fst

added theorem CategoryTheory.Limits.MultispanIndex.multispan_map_snd

added theorem CategoryTheory.Limits.MultispanIndex.multispan_obj_left

added theorem CategoryTheory.Limits.MultispanIndex.multispan_obj_right

added theorem CategoryTheory.Limits.MultispanIndex.ι_fstSigmaMap

added theorem CategoryTheory.Limits.MultispanIndex.ι_sndSigmaMap

added structure CategoryTheory.Limits.MultispanIndex

added def CategoryTheory.Limits.WalkingMulticospan.Hom.comp

added theorem CategoryTheory.Limits.WalkingMulticospan.Hom.comp_eq_comp

added theorem CategoryTheory.Limits.WalkingMulticospan.Hom.id_eq_id

added inductive CategoryTheory.Limits.WalkingMulticospan.Hom

added inductive CategoryTheory.Limits.WalkingMulticospan

added def CategoryTheory.Limits.WalkingMultispan.Hom.comp

added theorem CategoryTheory.Limits.WalkingMultispan.Hom.comp_eq_comp

added theorem CategoryTheory.Limits.WalkingMultispan.Hom.id_eq_id

added inductive CategoryTheory.Limits.WalkingMultispan.Hom

added inductive CategoryTheory.Limits.WalkingMultispan