Subobject

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

Statistics

Metric	Count
Definitions subobjectIsoSubobjectOp	1
Theorems subobjectIsoSubobjectOp_apply, subobjectIsoSubobjectOp_symm_apply, wellPowered_opposite	3
Total	4

CategoryTheory.Abelian

Definitions

Name	Category	Theorems
subobjectIsoSubobjectOp 📖	CompOp	2 math math: subobjectIsoSubobjectOp_apply, subobjectIsoSubobjectOp_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
subobjectIsoSubobjectOp_apply 📖	mathematical	—	DFunLike.coe RelIso CategoryTheory.Subobject OrderDual Opposite CategoryTheory.Category.opposite Opposite.op Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject OrderDual.instLE RelIso.instFunLike subobjectIsoSubobjectOp CategoryTheory.Subobject.lift CategoryTheory.Limits.cokernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive CategoryTheory.Limits.HasCokernels.has_colimit has_cokernels Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.cokernel.π	—	—
subobjectIsoSubobjectOp_symm_apply 📖	mathematical	—	DFunLike.coe RelIso OrderDual CategoryTheory.Subobject Opposite CategoryTheory.Category.opposite Opposite.op OrderDual.instLE Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject RelIso.instFunLike RelIso.symm subobjectIsoSubobjectOp CategoryTheory.Subobject.lift CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms toPreadditive Opposite.unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct has_kernels CategoryTheory.Limits.kernel.ι	—	—
wellPowered_opposite 📖	mathematical	—	CategoryTheory.WellPowered Opposite CategoryTheory.Category.opposite CategoryTheory.instLocallySmallOpposite	—	CategoryTheory.instLocallySmallOpposite small_congr CategoryTheory.small_subobject

---

← Back to Index