Commit 2024-02-12 10:30 88b30bb7

View on Github →

feat(CategoryTheory/Limits/MonoCoprod): inclusions of subcoproducts are mono (#10400) In this PR, it is shown that when suitable coproducts exists in a category satisfying [MonoCoprod C], then if X : I → C and ι : J → I is an injective map, the canonical morphism ∐ (X ∘ ι) ⟶ ∐ X is a monomorphism.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/MonoCoprod.lean

added def CategoryTheory.Limits.MonoCoprod.binaryCofanSum

added def CategoryTheory.Limits.MonoCoprod.isColimitBinaryCofanSum

added theorem CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inl'

added theorem CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inl

added theorem CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inr'

added theorem CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inr

added theorem CategoryTheory.Limits.MonoCoprod.mono_inj

added theorem CategoryTheory.Limits.MonoCoprod.mono_map'_of_injective

added theorem CategoryTheory.Limits.MonoCoprod.mono_of_injective'

added theorem CategoryTheory.Limits.MonoCoprod.mono_of_injective

added theorem CategoryTheory.Limits.MonoCoprod.mono_of_injective_aux