Commit 2025-12-11 00:39 f9a33234

View on Github →

feat(CategoryTheory): monomorphisms in Type are stable under coproducts (#32515) We develop the API regarding colimit cofans in the category of types, and we apply it in order to show that monomorphisms are stable under coproducts in the category of types. From https://github.com/joelriou/topcat-model-category

Estimated changes

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

added theorem CategoryTheory.Limits.Pi.map_π

added theorem CategoryTheory.Limits.Sigma.ι_map

Modified Mathlib/CategoryTheory/Limits/Types/ColimitType.lean

added theorem CategoryTheory.Functor.CoconeTypes.IsColimit.iff_bijective

Modified Mathlib/CategoryTheory/Limits/Types/Coproducts.lean

added def CategoryTheory.Limits.Cofan.cofanTypes

added theorem CategoryTheory.Limits.Cofan.eq_of_inj_apply_eq_of_isColimit

added theorem CategoryTheory.Limits.Cofan.inj_injective_of_isColimit

added theorem CategoryTheory.Limits.Cofan.inj_jointly_surjective_of_isColimit

added theorem CategoryTheory.Limits.Cofan.isColimit_cofanTypes_iff

added theorem CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_bijective_fromSigma

added theorem CategoryTheory.Limits.CofanTypes.bijective_fromSigma_of_isColimit

added theorem CategoryTheory.Limits.CofanTypes.eq_of_inj_apply_eq_of_isColimit

added theorem CategoryTheory.Limits.CofanTypes.equivOfIsColimit_apply

added theorem CategoryTheory.Limits.CofanTypes.equivOfIsColimit_symm_apply

added def CategoryTheory.Limits.CofanTypes.fromSigma

added theorem CategoryTheory.Limits.CofanTypes.inj_injective_of_isColimit

added theorem CategoryTheory.Limits.CofanTypes.inj_jointly_surjective_of_isColimit

added theorem CategoryTheory.Limits.CofanTypes.isColimit_iff_bijective_fromSigma

added theorem CategoryTheory.Limits.CofanTypes.isColimit_mk

added theorem CategoryTheory.Limits.CofanTypes.isColimit_sigma

added def CategoryTheory.Limits.CofanTypes.sigma

added theorem CategoryTheory.Limits.CofanTypes.sigma_inj

Modified Mathlib/CategoryTheory/Types/Monomorphisms.lean