Commit 2023-10-28 11:22 d70b0296

View on Github →

feat: Remove Extensive in favour of FinitaryExtensive. (#7731)

Estimated changes

Modified Mathlib/CategoryTheory/Extensive.lean

added theorem CategoryTheory.FinitaryExtensive.isPullback_initial_to

added theorem CategoryTheory.FinitaryExtensive.isPullback_initial_to_sigma_ι

added theorem CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproducts

added theorem CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproducts_Fin

added theorem CategoryTheory.FinitaryExtensive.mono_ι

added theorem CategoryTheory.FinitaryPreExtensive.hasPullbacks_of_is_coproduct

added theorem CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts

added theorem CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts_Fin

added theorem CategoryTheory.FinitaryPreExtensive.sigma_desc_iso

Modified Mathlib/CategoryTheory/Limits/VanKampen.lean

added theorem CategoryTheory.IsUniversalColimit.of_iso

added theorem CategoryTheory.IsUniversalColimit.precompose_isIso

added theorem CategoryTheory.IsUniversalColimit.whiskerEquivalence

added theorem CategoryTheory.IsUniversalColimit.whiskerEquivalence_iff

added theorem CategoryTheory.isPullback_initial_to_of_cofan_isVanKampen

added theorem CategoryTheory.isPullback_of_cofan_isVanKampen

added theorem CategoryTheory.mono_of_cofan_isVanKampen

Modified Mathlib/CategoryTheory/Sites/RegularExtensive.lean

modified def CategoryTheory.extensiveCoverage

modified theorem CategoryTheory.extensive_regular_generate_coherent