Commit 2025-12-09 16:30 ba422618

View on Github →

chore(CategoryTheory/Limits): upgrade MulticospanIndex.multiforkEquivPiFork from HasLimit to IsLimit (#32576) We also adapt the dual version.

Estimated changes

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

modified theorem CategoryTheory.Limits.Multicofork.ofSigmaCofork_ι_app_left

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

deleted theorem CategoryTheory.Limits.Multicofork.ofSigmaCofork_ι_app_right

added theorem CategoryTheory.Limits.Multicofork.ofSigmaCofork_π

modified theorem CategoryTheory.Limits.Multicofork.sigma_condition

modified theorem CategoryTheory.Limits.Multicofork.toSigmaCofork_π

added def CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimit

added theorem CategoryTheory.Limits.MulticospanIndex.fstPiMapOfIsLimit_proj

modified theorem CategoryTheory.Limits.MulticospanIndex.fstPiMap_π

added def CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit

added def CategoryTheory.Limits.MulticospanIndex.ofPiForkFunctor

added def CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit

added theorem CategoryTheory.Limits.MulticospanIndex.sndPiMapOfIsLimit_proj

modified theorem CategoryTheory.Limits.MulticospanIndex.sndPiMap_π

added def CategoryTheory.Limits.MulticospanIndex.toPiForkFunctor

added def CategoryTheory.Limits.Multifork.ofPiFork

added theorem CategoryTheory.Limits.Multifork.ofPiFork_ι

deleted theorem CategoryTheory.Limits.Multifork.ofPiFork_π_app_left

modified theorem CategoryTheory.Limits.Multifork.ofPiFork_π_app_right

modified theorem CategoryTheory.Limits.Multifork.pi_condition

added def CategoryTheory.Limits.Multifork.toPiFork

modified theorem CategoryTheory.Limits.Multifork.toPiFork_π_app_one

modified theorem CategoryTheory.Limits.Multifork.toPiFork_π_app_zero

added def CategoryTheory.Limits.MultispanIndex.fstSigmaMapOfIsColimit

added theorem CategoryTheory.Limits.MultispanIndex.inj_fstSigmaMapOfIsColimit

added theorem CategoryTheory.Limits.MultispanIndex.inj_sndSigmaMapOfIsColimit

added def CategoryTheory.Limits.MultispanIndex.sndSigmaMapOfIsColimit

modified theorem CategoryTheory.Limits.MultispanIndex.ι_fstSigmaMap

modified theorem CategoryTheory.Limits.MultispanIndex.ι_sndSigmaMap