Subobjects in adhesive categories

Main Results

• Subobjects in adhesive categories have binary coproducts

noncomputable def CategoryTheory.Adhesive.isColimitBinaryCofan {C : Type u} [Category.{v, u} C] [Adhesive C] {X : C} (a b : Subobject X) : Limits.IsColimit (Limits.BinaryCofan.mk ⋯.hom ⋯.hom)

Given an object X of an adhesive category C, the coproduct of two subobjects of X is their pushout in C over their pullback.

Equations

• CategoryTheory.Adhesive.isColimitBinaryCofan a b = CategoryTheory.Limits.BinaryCofan.isColimitMk (fun (s : CategoryTheory.Limits.BinaryCofan a b) => ⋯.hom) ⋯ ⋯ ⋯

instance CategoryTheory.Adhesive.instHasBinaryCoproductsSubobject {C : Type u} [Category.{v, u} C] [Adhesive C] {X : C} : Limits.HasBinaryCoproducts (Subobject X)