Kernels

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

Statistics

Metric	Count
Definitions cokernelCocone, cokernelIsColimit, cokernelIsoRangeQuotient, isColimitCokernelCofork, isLimitKernelFork, kernelCone, kernelIsLimit, kernelIsoKer	8
Theorems cokernel_π_cokernelIsoRangeQuotient_hom, cokernel_π_cokernelIsoRangeQuotient_hom_apply, cokernel_π_ext, hasCokernels_moduleCat, hasKernels_moduleCat, kernelIsoKer_hom_ker_subtype, kernelIsoKer_hom_ker_subtype_apply, kernelIsoKer_inv_kernel_ι, kernelIsoKer_inv_kernel_ι_apply, range_mkQ_cokernelIsoRangeQuotient_inv, range_mkQ_cokernelIsoRangeQuotient_inv_apply	11
Total	19

ModuleCat

Definitions

Name	Category	Theorems
cokernelCocone 📖	CompOp	—
cokernelIsColimit 📖	CompOp	—
cokernelIsoRangeQuotient 📖	CompOp	4 math math: cokernel_π_cokernelIsoRangeQuotient_hom_apply, cokernel_π_cokernelIsoRangeQuotient_hom, range_mkQ_cokernelIsoRangeQuotient_inv, range_mkQ_cokernelIsoRangeQuotient_inv_apply
isColimitCokernelCofork 📖	CompOp	—
isLimitKernelFork 📖	CompOp	—
kernelCone 📖	CompOp	—
kernelIsLimit 📖	CompOp	—
kernelIsoKer 📖	CompOp	4 math math: kernelIsoKer_inv_kernel_ι_apply, kernelIsoKer_hom_ker_subtype, kernelIsoKer_hom_ker_subtype_apply, kernelIsoKer_inv_kernel_ι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cokernel_π_cokernelIsoRangeQuotient_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct moduleCategory CategoryTheory.Limits.cokernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive CategoryTheory.Limits.HasCokernels.has_colimit hasCokernels_moduleCat of HasQuotient.Quotient carrier Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid isAddCommGroup isModule Submodule.hasQuotient LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Hom.hom Submodule.Quotient.addCommGroup Submodule.Quotient.module CategoryTheory.Limits.cokernel.π CategoryTheory.Iso.hom cokernelIsoRangeQuotient ofHom Submodule.mkQ	—	CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom CategoryTheory.Limits.HasCokernels.has_colimit hasCokernels_moduleCat
cokernel_π_cokernelIsoRangeQuotient_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier CategoryTheory.Limits.cokernel ModuleCat moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive CategoryTheory.Limits.HasCokernels.has_colimit hasCokernels_moduleCat HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid isAddCommGroup isModule Submodule.hasQuotient LinearMap.range RingHomSurjective.ids Hom.hom Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom instConcreteCategoryLinearMapIdCarrier of CategoryTheory.Iso.hom cokernelIsoRangeQuotient CategoryTheory.Limits.cokernel.π	—	RingHomSurjective.ids CategoryTheory.Limits.HasCokernels.has_colimit hasCokernels_moduleCat CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise cokernel_π_cokernelIsoRangeQuotient_hom
cokernel_π_ext 📖	mathematical	carrier AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid isAddCommGroup DFunLike.coe CategoryTheory.ConcreteCategory.hom ModuleCat moduleCategory LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring isModule LinearMap.instFunLike instConcreteCategoryLinearMapIdCarrier	CategoryTheory.Limits.cokernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive CategoryTheory.Limits.HasCokernels.has_colimit hasCokernels_moduleCat CategoryTheory.Limits.cokernel.π	—	CategoryTheory.Limits.HasCokernels.has_colimit hasCokernels_moduleCat map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass AddLeftCancelSemigroup.toIsLeftCancelAdd CategoryTheory.Limits.cokernel.condition_apply
hasCokernels_moduleCat 📖	mathematical	—	CategoryTheory.Limits.HasCokernels ModuleCat moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive	—	—
hasKernels_moduleCat 📖	mathematical	—	CategoryTheory.Limits.HasKernels ModuleCat moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive	—	—
kernelIsoKer_hom_ker_subtype 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct moduleCategory CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive CategoryTheory.Limits.HasKernels.has_limit hasKernels_moduleCat of carrier Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid isAddCommGroup isModule SetLike.instMembership Submodule.setLike LinearMap.ker RingHom.id Semiring.toNonAssocSemiring Hom.hom Submodule.addCommGroup Submodule.module CategoryTheory.Iso.hom kernelIsoKer ofHom Submodule.subtype CategoryTheory.Limits.kernel.ι	—	CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp
kernelIsoKer_hom_ker_subtype_apply 📖	mathematical	—	carrier Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid isAddCommGroup isModule SetLike.instMembership Submodule.setLike LinearMap.ker RingHom.id Semiring.toNonAssocSemiring Hom.hom DFunLike.coe LinearMap CategoryTheory.Limits.kernel ModuleCat moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive CategoryTheory.Limits.HasKernels.has_limit hasKernels_moduleCat Submodule.addCommGroup Submodule.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom instConcreteCategoryLinearMapIdCarrier of CategoryTheory.Iso.hom kernelIsoKer CategoryTheory.Limits.kernel.ι	—	CategoryTheory.Limits.HasKernels.has_limit hasKernels_moduleCat CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise kernelIsoKer_hom_ker_subtype
kernelIsoKer_inv_kernel_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct moduleCategory of carrier Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid isAddCommGroup isModule SetLike.instMembership Submodule.setLike LinearMap.ker RingHom.id Semiring.toNonAssocSemiring Hom.hom Submodule.addCommGroup Submodule.module CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive CategoryTheory.Limits.HasKernels.has_limit hasKernels_moduleCat CategoryTheory.Iso.inv kernelIsoKer CategoryTheory.Limits.kernel.ι ofHom Submodule.subtype	—	CategoryTheory.Limits.limit.isoLimitCone_inv_π
kernelIsoKer_inv_kernel_ι_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring carrier CategoryTheory.Limits.kernel ModuleCat moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive CategoryTheory.Limits.HasKernels.has_limit hasKernels_moduleCat AddCommGroup.toAddCommMonoid isAddCommGroup isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom instConcreteCategoryLinearMapIdCarrier CategoryTheory.Limits.kernel.ι Submodule SetLike.instMembership Submodule.setLike LinearMap.ker Hom.hom Submodule.addCommGroup Submodule.module of CategoryTheory.Iso.inv kernelIsoKer	—	CategoryTheory.Limits.HasKernels.has_limit hasKernels_moduleCat CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise kernelIsoKer_inv_kernel_ι
range_mkQ_cokernelIsoRangeQuotient_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CategoryTheory.Category.toCategoryStruct moduleCategory of carrier isAddCommGroup isModule HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient LinearMap.range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids Hom.hom Submodule.Quotient.addCommGroup Submodule.Quotient.module CategoryTheory.Limits.cokernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive CategoryTheory.Limits.HasCokernels.has_colimit hasCokernels_moduleCat ofHom Submodule.mkQ CategoryTheory.Iso.inv cokernelIsoRangeQuotient CategoryTheory.Limits.cokernel.π	—	CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv CategoryTheory.Limits.HasCokernels.has_colimit hasCokernels_moduleCat
range_mkQ_cokernelIsoRangeQuotient_inv_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring HasQuotient.Quotient carrier Submodule AddCommGroup.toAddCommMonoid isAddCommGroup isModule Submodule.hasQuotient LinearMap.range RingHomSurjective.ids Hom.hom CategoryTheory.Limits.cokernel ModuleCat moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive CategoryTheory.Limits.HasCokernels.has_colimit hasCokernels_moduleCat Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom instConcreteCategoryLinearMapIdCarrier of CategoryTheory.Iso.inv cokernelIsoRangeQuotient CategoryTheory.Limits.cokernel.π	—	CategoryTheory.Limits.HasCokernels.has_colimit hasCokernels_moduleCat RingHomSurjective.ids CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise range_mkQ_cokernelIsoRangeQuotient_inv

---

← Back to Index