Kernels

📁 Source: Mathlib/CategoryTheory/ObjectProperty/Kernels.lean

Statistics

Metric	Count
Definitions cokernels, kernels, IsClosedUnderCokernels, IsClosedUnderKernels, createsCokernels, createsKernels	6
Theorems instIsClosedUnderIsomorphismsCokernels, instIsClosedUnderIsomorphismsKernels, cokernels_le, kernels_le, hasColimit_parallelPair_comp_ι, hasLimit_parallelPair_comp_ι, instHasCokernelsFullSubcategoryOfIsClosedUnderCokernels, instHasKernelsFullSubcategoryOfIsClosedUnderKernels, instIsClosedUnderCokernelsOfIsClosedUnderQuotients, instIsClosedUnderKernelsOfIsClosedUnderSubobjects, isClosedUnderCokernels_iff, isClosedUnderKernels_iff, preservesCokernels_ι, preservesKernels_ι, prop_cokernel, prop_kernel, prop_of_isColimit_cokernelCofork, prop_of_isLimit_kernelFork	18
Total	24

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
cokernels 📖	CompData	3 math math: CategoryTheory.ObjectProperty.IsClosedUnderCokernels.cokernels_le, CategoryTheory.ObjectProperty.isClosedUnderCokernels_iff, instIsClosedUnderIsomorphismsCokernels
kernels 📖	CompData	3 math math: CategoryTheory.ObjectProperty.IsClosedUnderKernels.kernels_le, instIsClosedUnderIsomorphismsKernels, CategoryTheory.ObjectProperty.isClosedUnderKernels_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsClosedUnderIsomorphismsCokernels 📖	mathematical	—	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms cokernels	—	CategoryTheory.Limits.CokernelCofork.condition_assoc CategoryTheory.Limits.zero_comp
instIsClosedUnderIsomorphismsKernels 📖	mathematical	—	CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms kernels	—	CategoryTheory.Category.assoc CategoryTheory.Limits.KernelFork.condition CategoryTheory.Limits.comp_zero CategoryTheory.Iso.hom_inv_id_assoc

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
IsClosedUnderCokernels 📖	CompData	2 math math: isClosedUnderCokernels_iff, instIsClosedUnderCokernelsOfIsClosedUnderQuotients
IsClosedUnderKernels 📖	CompData	2 math math: instIsClosedUnderKernelsOfIsClosedUnderSubobjects, isClosedUnderKernels_iff
createsCokernels 📖	CompOp	—
createsKernels 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasColimit_parallelPair_comp_ι 📖	mathematical	—	CategoryTheory.Limits.HasColimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor.comp FullSubcategory FullSubcategory.category CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero instHasZeroMorphismsFullSubcategory ι	—	CategoryTheory.Limits.hasColimit_of_iso
hasLimit_parallelPair_comp_ι 📖	mathematical	—	CategoryTheory.Limits.HasLimit CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor.comp FullSubcategory FullSubcategory.category CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero instHasZeroMorphismsFullSubcategory ι	—	CategoryTheory.Limits.hasLimit_of_iso
instHasCokernelsFullSubcategoryOfIsClosedUnderCokernels 📖	mathematical	—	CategoryTheory.Limits.HasCokernels FullSubcategory FullSubcategory.category instHasZeroMorphismsFullSubcategory	—	CategoryTheory.hasColimit_of_created hasColimit_parallelPair_comp_ι CategoryTheory.Limits.HasCokernels.has_colimit
instHasKernelsFullSubcategoryOfIsClosedUnderKernels 📖	mathematical	—	CategoryTheory.Limits.HasKernels FullSubcategory FullSubcategory.category instHasZeroMorphismsFullSubcategory	—	CategoryTheory.hasLimit_of_created hasLimit_parallelPair_comp_ι CategoryTheory.Limits.HasKernels.has_limit
instIsClosedUnderCokernelsOfIsClosedUnderQuotients 📖	mathematical	—	IsClosedUnderCokernels	—	prop_of_epi CategoryTheory.Limits.Cofork.IsColimit.epi
instIsClosedUnderKernelsOfIsClosedUnderSubobjects 📖	mathematical	—	IsClosedUnderKernels	—	prop_of_mono CategoryTheory.Limits.Fork.IsLimit.mono
isClosedUnderCokernels_iff 📖	mathematical	—	IsClosedUnderCokernels CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le CategoryTheory.MorphismProperty.cokernels CategoryTheory.MorphismProperty.ofObjectProperty	—	—
isClosedUnderKernels_iff 📖	mathematical	—	IsClosedUnderKernels CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le CategoryTheory.MorphismProperty.kernels CategoryTheory.MorphismProperty.ofObjectProperty	—	—
preservesCokernels_ι 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit FullSubcategory FullSubcategory.category CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero instHasZeroMorphismsFullSubcategory ι	—	CategoryTheory.Limits.HasCokernels.has_colimit hasColimit_parallelPair_comp_ι CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit
preservesKernels_ι 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit FullSubcategory FullSubcategory.category CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero instHasZeroMorphismsFullSubcategory ι	—	CategoryTheory.Limits.HasKernels.has_limit hasLimit_parallelPair_comp_ι CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit
prop_cokernel 📖	mathematical	—	CategoryTheory.Limits.cokernel	—	prop_of_isColimit_cokernelCofork CategoryTheory.Limits.cokernel.condition CategoryTheory.Limits.zero_comp
prop_kernel 📖	mathematical	—	CategoryTheory.Limits.kernel	—	prop_of_isLimit_kernelFork CategoryTheory.Limits.kernel.condition CategoryTheory.Limits.comp_zero
prop_of_isColimit_cokernelCofork 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	—	IsClosedUnderCokernels.cokernels_le
prop_of_isLimit_kernelFork 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero	—	IsClosedUnderKernels.kernels_le

CategoryTheory.ObjectProperty.IsClosedUnderCokernels

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cokernels_le 📖	mathematical	—	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le CategoryTheory.MorphismProperty.cokernels CategoryTheory.MorphismProperty.ofObjectProperty	—	—

CategoryTheory.ObjectProperty.IsClosedUnderKernels

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
kernels_le 📖	mathematical	—	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le CategoryTheory.MorphismProperty.kernels CategoryTheory.MorphismProperty.ofObjectProperty	—	—

---

← Back to Index