Structures · Category theory
CategoryTheory.Limits.HasCokernels
HasCokernels represents the existence of cokernels for every morphism.
- Shape
- One type argument · adds has_colimit
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances4
- CategoryTheory.ObjectProperty.FullSubcategory
- CategoryTheory.Preadditive.RightFreyd
- SemiNormedGrp
- SemiNormedGrp₁
How is a type an instance?
Loading the hierarchy index…
Assumed by80
- CategoryTheory.ShortComplex.leftHomologyFunctor
- CategoryTheory.ShortComplex.rightHomologyFunctor
- CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation
- CategoryTheory.ShortComplex.opcyclesFunctor
- CategoryTheory.ShortComplex.cyclesFunctor
- CategoryTheory.Limits.coker
- CategoryTheory.Limits.coker.π
- CategoryTheory.ShortComplex.leftHomologyFunctorOpNatIso
- CategoryTheory.Abelian.coimageImageComparisonFunctor
- CategoryTheory.Functor.preservesFiniteColimits_of_preservesHomology
- CategoryTheory.NormalEpiCategory.mono_of_zero_kernel
- CategoryTheory.ShortComplex.rightHomologyFunctorOpNatIso
- CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e'
- CategoryTheory.Preadditive.hasCoequalizers_of_hasCokernels
- CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageFactorisation
- CategoryTheory.Limits.cokernelOrderHom
- CategoryTheory.ObjectProperty.preservesCokernels_ι
- CategoryTheory.ShortComplex.rightHomologyιNatTrans
- CategoryTheory.ShortComplex.toCyclesNatTrans
- CategoryTheory.ShortComplex.leftHomologyπNatTrans
- CategoryTheory.ShortComplex.pOpcyclesNatTrans
- CategoryTheory.Limits.coker.condition
- CategoryTheory.ShortComplex.fromOpcyclesNatTrans
- CategoryTheory.ShortComplex.iCyclesNatTrans
- CategoryTheory.NormalEpiCategory.preservesMonomorphisms_of_preservesKernels
- CategoryTheory.Limits.coker.π_app
- CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_m
- CategoryTheory.Limits.cokernelOrderHom_coe
- CategoryTheory.ShortComplex.rightHomologyFunctor_obj
- CategoryTheory.ShortComplex.iCyclesNatTrans_app
- CategoryTheory.Limits.cokerIsCokernel
- CategoryTheory.Abelian.coimageImageComparisonFunctor_obj
- CategoryTheory.NormalEpiCategory.hasColimit_parallelPair
- CategoryTheory.ShortComplex.cyclesFunctor_map
- CategoryTheory.Limits.coker_map
- CategoryTheory.NormalEpiCategory.mono_of_cancel_zero
- CategoryTheory.ShortComplex.cyclesFunctor_additive
- CategoryTheory.ShortComplex.opcyclesFunctor_linear
- CategoryTheory.ShortComplex.opcyclesFunctor_map
- CategoryTheory.ShortComplex.leftHomologyFunctorOpNatIso_inv_app
- CategoryTheory.ShortComplex.leftHomologyFunctor_linear
- CategoryTheory.ShortComplex.rightHomologyFunctorOpNatIso_hom_app
- CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.hasImages
- CategoryTheory.ShortComplex.opcyclesFunctor_additive
- CategoryTheory.ShortComplex.fromOpcyclesNatTrans_app
- CategoryTheory.Limits.coker.condition_assoc
- CategoryTheory.ShortComplex.leftHomologyFunctor_obj
- CategoryTheory.ShortComplex.rightHomologyιNatTrans_app
- CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.isNormalEpiCategory
- CategoryTheory.ShortComplex.cyclesFunctorIso
Ancestors0
No ancestors.