Commit 2023-06-02 11:07 7a20abe4

View on Github →

feat: port CategoryTheory.Extensive (#4022)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Extensive.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.FinitaryExtensive.isPullback_initial_to_binaryCofan

added theorem CategoryTheory.FinitaryExtensive.mono_inl_of_isColimit

added theorem CategoryTheory.FinitaryExtensive.mono_inr_of_isColimit

added theorem CategoryTheory.FinitaryExtensive.vanKampen

added theorem CategoryTheory.IsInitial.isVanKampenColimit

added def CategoryTheory.IsUniversalColimit

added theorem CategoryTheory.IsVanKampenColimit.isUniversal

added theorem CategoryTheory.IsVanKampenColimit.of_iso

added theorem CategoryTheory.IsVanKampenColimit.of_map

added def CategoryTheory.IsVanKampenColimit

added theorem CategoryTheory.NatTrans.Equifibered.comp

added theorem CategoryTheory.NatTrans.Equifibered.whiskerRight

added def CategoryTheory.NatTrans.Equifibered

added theorem CategoryTheory.NatTrans.equifibered_of_isIso

added theorem CategoryTheory.finitaryExtensive_iff_of_isTerminal

added theorem CategoryTheory.finitaryExtensive_of_preserves_and_reflects

added theorem CategoryTheory.finitaryExtensive_of_preserves_and_reflects_isomorphism

added theorem CategoryTheory.hasStrictInitial_of_isUniversal

added theorem CategoryTheory.isVanKampenColimit_of_evaluation

added theorem CategoryTheory.mapPair_equifibered