Structures · Category theory
CategoryTheory.Limits.HasKernels
HasKernels represents the existence of kernels for every morphism.
- Shape
- One type argument · adds has_limit
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- CategoryTheory.ObjectProperty.FullSubcategory
- FDRep
How is a type an instance?
Loading the hierarchy index…
Assumed by105
- CategoryTheory.ShortComplex.leftHomologyFunctor
- CategoryTheory.ShortComplex.rightHomologyFunctor
- imageToKernel'
- CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation
- CategoryTheory.Limits.ker
- CategoryTheory.ShortComplex.opcyclesFunctor
- CategoryTheory.ShortComplex.cyclesFunctor
- CategoryTheory.Functor.preservesFiniteLimits_of_preservesHomology
- CategoryTheory.isIso_iff_nonzero
- CategoryTheory.Limits.ker.ι
- CategoryTheory.ShortComplex.leftHomologyFunctorOpNatIso
- CategoryTheory.Abelian.coimageImageComparisonFunctor
- CategoryTheory.finrank_hom_simple_simple_le_one
- CategoryTheory.NormalMonoCategory.epi_of_zero_cokernel
- CategoryTheory.finrank_hom_simple_simple_eq_one_iff
- CategoryTheory.ShortComplex.rightHomologyFunctorOpNatIso
- CategoryTheory.finrank_endomorphism_simple_eq_one
- CategoryTheory.Preadditive.hasEqualizers_of_hasKernels
- CategoryTheory.isIso_of_hom_simple
- CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e'
- CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageFactorisation
- CategoryTheory.ShortComplex.rightHomologyιNatTrans
- CategoryTheory.finrank_hom_simple_simple_eq_zero_iff
- CategoryTheory.endomorphism_simple_eq_smul_id
- CategoryTheory.ObjectProperty.preservesKernels_ι
- CategoryTheory.ShortComplex.toCyclesNatTrans
- imageToKernel'_kernelSubobjectIso
- CategoryTheory.ShortComplex.leftHomologyπNatTrans
- CategoryTheory.finrank_hom_simple_simple
- CategoryTheory.ShortComplex.pOpcyclesNatTrans
- CategoryTheory.NormalMonoCategory.preservesEpimorphisms_of_preservesCokernels
- CategoryTheory.Limits.ker.condition
- CategoryTheory.ShortComplex.fromOpcyclesNatTrans
- CategoryTheory.Limits.kernelOrderHom
- CategoryTheory.ShortComplex.iCyclesNatTrans
- CategoryTheory.Limits.kernelOrderHom_coe
- CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_m
- CategoryTheory.ShortComplex.rightHomologyFunctor_obj
- CategoryTheory.ShortComplex.iCyclesNatTrans_app
- CategoryTheory.NormalMonoCategory.pullback_of_mono
- CategoryTheory.Limits.ker.ι_app
- CategoryTheory.Abelian.coimageImageComparisonFunctor_obj
- imageSubobjectIso_imageToKernel'
- HomologicalComplex.kernel_from_eq_kernel
- CategoryTheory.ShortComplex.cyclesFunctor_map
- imageToKernel_epi_comp
- imageToKernel_epi_of_zero_of_mono
- CategoryTheory.mono_of_nonzero_from_simple
- CategoryTheory.ShortComplex.cyclesFunctor_additive
- CategoryTheory.ShortComplex.opcyclesFunctor_linear
Ancestors0
No ancestors.