Subobject

📁 Source: Mathlib/CategoryTheory/Adhesive/Subobject.lean

Statistics

Metric	Count
Definitions isColimitBinaryCofan	1
Theorems instHasBinaryCoproductsSubobject	1
Total	2

CategoryTheory.Adhesive

Definitions

Name	Category	Theorems
isColimitBinaryCofan 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasBinaryCoproductsSubobject 📖	mathematical	—	CategoryTheory.Limits.HasBinaryCoproducts CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject	—	hasPullback_of_mono_left CategoryTheory.Subobject.arrow_mono hasPushout_of_mono_left CategoryTheory.Limits.pullback.fst_of_mono CategoryTheory.Limits.pullback.condition desc_mono_of_mono CategoryTheory.Subobject.le_mk_of_comm CategoryTheory.Limits.pushout.inl_desc CategoryTheory.Limits.pushout.inr_desc CategoryTheory.Limits.hasColimit_of_iso

---

← Back to Index