Documentation

Mathlib.CategoryTheory.Adhesive.Subobject

Subobjects in adhesive categories #

Main Results #

source
🔸 coverage
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.

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