Commit 2023-10-26 10:03 3716d38c

View on Github →

feat(CategoryTheory/Limits/VanKampen): Properties of van Kampen colimits (#7745) Also moves the definition of van Kampen colimits from CategoryTheory/Extensive.lean into a new file.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Extensive.lean

deleted theorem CategoryTheory.BinaryCofan.isPullback_initial_to_of_isVanKampen

deleted theorem CategoryTheory.BinaryCofan.isVanKampen_iff

deleted theorem CategoryTheory.BinaryCofan.isVanKampen_mk

deleted theorem CategoryTheory.BinaryCofan.mono_inr_of_isVanKampen

deleted theorem CategoryTheory.IsInitial.isVanKampenColimit

deleted def CategoryTheory.IsUniversalColimit

deleted theorem CategoryTheory.IsVanKampenColimit.isUniversal

deleted theorem CategoryTheory.IsVanKampenColimit.of_iso

deleted theorem CategoryTheory.IsVanKampenColimit.of_map

deleted def CategoryTheory.IsVanKampenColimit

deleted theorem CategoryTheory.NatTrans.Equifibered.comp

deleted theorem CategoryTheory.NatTrans.Equifibered.whiskerRight

deleted def CategoryTheory.NatTrans.Equifibered

deleted theorem CategoryTheory.NatTrans.equifibered_of_isIso

deleted theorem CategoryTheory.hasStrictInitial_of_isUniversal

deleted theorem CategoryTheory.isVanKampenColimit_of_evaluation

deleted theorem CategoryTheory.mapPair_equifibered

Created Mathlib/CategoryTheory/Limits/VanKampen.lean

added theorem CategoryTheory.BinaryCofan.isPullback_initial_to_of_isVanKampen

added theorem CategoryTheory.BinaryCofan.isVanKampen_iff

added theorem CategoryTheory.BinaryCofan.isVanKampen_mk

added theorem CategoryTheory.BinaryCofan.mono_inr_of_isVanKampen

added theorem CategoryTheory.IsInitial.isVanKampenColimit

added def CategoryTheory.IsUniversalColimit

added theorem CategoryTheory.IsVanKampenColimit.isUniversal

added theorem CategoryTheory.IsVanKampenColimit.mapCocone_iff

added theorem CategoryTheory.IsVanKampenColimit.of_iso

added theorem CategoryTheory.IsVanKampenColimit.of_mapCocone

added theorem CategoryTheory.IsVanKampenColimit.precompose_isIso

added theorem CategoryTheory.IsVanKampenColimit.precompose_isIso_iff

added theorem CategoryTheory.IsVanKampenColimit.whiskerEquivalence

added theorem CategoryTheory.IsVanKampenColimit.whiskerEquivalence_iff

added def CategoryTheory.IsVanKampenColimit

added theorem CategoryTheory.NatTrans.Equifibered.comp

added theorem CategoryTheory.NatTrans.Equifibered.whiskerLeft

added theorem CategoryTheory.NatTrans.Equifibered.whiskerRight

added def CategoryTheory.NatTrans.Equifibered

added theorem CategoryTheory.NatTrans.equifibered_of_discrete

added theorem CategoryTheory.NatTrans.equifibered_of_isIso

added theorem CategoryTheory.hasStrictInitial_of_isUniversal

added theorem CategoryTheory.isUniversalColimit_extendCofan

added theorem CategoryTheory.isVanKampenColimit_extendCofan

added theorem CategoryTheory.isVanKampenColimit_of_evaluation

added theorem CategoryTheory.isVanKampenColimit_of_isEmpty

added theorem CategoryTheory.mapPair_equifibered

Modified Mathlib/CategoryTheory/PEmpty.lean

deleted def CategoryTheory.Functor.emptyEquivalence

added def CategoryTheory.Functor.isEmptyExt

added def CategoryTheory.emptyEquivalence

added def CategoryTheory.equivalenceOfIsEmpty

added def CategoryTheory.functorOfIsEmpty