CategoryTheory.Limits.MonoCoprod.binaryCofan_inl
theorem CategoryTheory.Limits.MonoCoprod.binaryCofan_inl :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [self : CategoryTheory.Limits.MonoCoprod C] ⦃A B : C⦄
(c : CategoryTheory.Limits.BinaryCofan A B), CategoryTheory.Limits.IsColimit c → CategoryTheory.Mono c.inl
The theorem `CategoryTheory.Limits.MonoCoprod.binaryCofan_inl` states that, for any category `C` with monoidal coproducts and any two objects `A` and `B` in `C`, if a binary cofan (a cocone on a diagram indexing a coproduct) `c` is a colimit, then the left inclusion morphism `c.inl` of the binary cofan is a monomorphism (an injective morphism in the category theory). A monomorphism is a morphism which is left-cancellative, i.e., if two morphisms composed with it result in the same morphism, then the two original morphisms were equal.
More concisely: If `C` is a category with monoidal coproducts and `c` is a binary cofactorization of objects `A` and `B` in `C` that is a colimit, then `c.inl` is a monomorphism.
|
CategoryTheory.Limits.MonoCoprod.binaryCofan_inr
theorem CategoryTheory.Limits.MonoCoprod.binaryCofan_inr :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {A B : C}
[inst_1 : CategoryTheory.Limits.MonoCoprod C] (c : CategoryTheory.Limits.BinaryCofan A B),
CategoryTheory.Limits.IsColimit c → CategoryTheory.Mono c.inr
The theorem `CategoryTheory.Limits.MonoCoprod.binaryCofan_inr` states that for any category `C` with a `MonoCoprod`, given any binary cofan `c` of objects `A` and `B` in `C`, if `c` is a colimit, then the second inclusion of the binary cofan, denoted by `CategoryTheory.Limits.BinaryCofan.inr c`, is a monomorphism. In category theory, a monomorphism is an injective morphism, and a colimit of a diagram is a universal cone over that diagram. The theorem connects the concepts of colimits and monomorphisms in the context of binary cofans.
More concisely: In any category with a Monocoprod, the second inclusion of a binary colimit is a monomorphism.
|