Commit 2025-06-22 09:40 872fd693

View on Github →

feat(CategoryTheory/Extensive): pullbacks distribute over finite coproducts (#26186) More generally, we show that this holds whenever the coproduct is a universal colimit.

Estimated changes

Modified Mathlib/CategoryTheory/EffectiveEpi/Extensive.lean

Modified Mathlib/CategoryTheory/Extensive.lean

added theorem CategoryTheory.FinitaryPreExtensive.isIso_sigmaDesc_fst

added theorem CategoryTheory.FinitaryPreExtensive.isPullback_sigmaDesc

deleted theorem CategoryTheory.FinitaryPreExtensive.sigma_desc_iso

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

added def CategoryTheory.Limits.Cofan.IsColimit.prod

added def CategoryTheory.Limits.Fan.IsLimit.prod

Modified Mathlib/CategoryTheory/Limits/VanKampen.lean

added theorem CategoryTheory.IsUniversalColimit.isPullback_of_isColimit_left

added theorem CategoryTheory.IsUniversalColimit.isPullback_of_isColimit_right

added theorem CategoryTheory.IsUniversalColimit.isPullback_prod_of_isColimit

added theorem CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_isPullback_left

added theorem CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_isPullback_right

added theorem CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_left

added theorem CategoryTheory.IsUniversalColimit.nonempty_isColimit_of_pullbackCone_right

added theorem CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_isPullback

added theorem CategoryTheory.IsUniversalColimit.nonempty_isColimit_prod_of_pullbackCone

Modified Mathlib/CategoryTheory/Sites/Coherent/Basic.lean

Modified Mathlib/CategoryTheory/Sites/Coherent/Comparison.lean