Subobject

📁 Source: Mathlib/Algebra/Category/ModuleCat/Subobject.lean

Statistics

Metric	Count
Definitions subobjectModule, toKernelSubobject	2
Theorems cokernel_π_imageSubobject_ext, toKernelSubobject_arrow, wellPowered_moduleCat	3
Total	5

ModuleCat

Definitions

Name	Category	Theorems
subobjectModule 📖	CompOp	—
toKernelSubobject 📖	CompOp	1 math math: toKernelSubobject_arrow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cokernel_π_imageSubobject_ext 📖	mathematical	carrier AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid isAddCommGroup DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.Subobject ModuleCat moduleCategory Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.imageSubobject CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier CategoryTheory.Limits.factorThruImageSubobject	CategoryTheory.Limits.cokernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive CategoryTheory.Limits.cokernel.π	—	map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass CategoryTheory.Limits.cokernel.condition_apply add_zero
toKernelSubobject_arrow 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.Subobject ModuleCat moduleCategory Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.kernelSubobject CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive CategoryTheory.Limits.HasKernels.has_limit hasKernels_moduleCat carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier CategoryTheory.Subobject.arrow Submodule SetLike.instMembership Submodule.setLike LinearMap.ker Hom.hom Submodule.addCommMonoid Submodule.module toKernelSubobject	—	CategoryTheory.Limits.HasKernels.has_limit hasKernels_moduleCat CategoryTheory.Category.assoc CategoryTheory.Limits.kernelSubobject_arrow' kernelIsoKer_inv_kernel_ι
wellPowered_moduleCat 📖	mathematical	—	CategoryTheory.WellPowered ModuleCat moduleCategory CategoryTheory.locallySmall_of_univLE UnivLE.self	—	CategoryTheory.locallySmall_of_univLE UnivLE.self

---

← Back to Index