ImageToKernel

📁 Source: Mathlib/Algebra/Homology/ImageToKernel.lean

Statistics

Metric	Count
Definitions imageToKernel, imageToKernel'	2
Theorems factorThruImageSubobject_comp_imageToKernel, imageSubobjectIso_imageToKernel', imageToKernel'_kernelSubobjectIso, imageToKernel_arrow, imageToKernel_arrow_apply, imageToKernel_arrow_assoc, imageToKernel_comp_hom_inv_comp, imageToKernel_comp_left, imageToKernel_comp_mono, imageToKernel_comp_right, imageToKernel_epi_comp, imageToKernel_epi_of_epi_of_zero, imageToKernel_epi_of_zero_of_mono, imageToKernel_zero_left, imageToKernel_zero_right, image_le_kernel, instMonoImageToKernel, subobject_ofLE_as_imageToKernel	18
Total	20

(root)

Definitions

Name	Category	Theorems
imageToKernel 📖	CompOp	22 math math: imageToKernel_unop, imageToKernel'_kernelSubobjectIso, imageToKernel_op, factorThruImageSubobject_comp_imageToKernel, imageToKernel_comp_right, imageToKernel_comp_hom_inv_comp, CategoryTheory.ShortComplex.Exact.isIso_imageToKernel, imageToKernel_arrow_assoc, CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel, imageToKernel_epi_comp, subobject_ofLE_as_imageToKernel, imageToKernel_arrow, imageToKernel_epi_of_zero_of_mono, imageToKernel_comp_left, imageSubobjectIso_imageToKernel', instMonoImageToKernel, imageToKernel_arrow_apply, CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel, imageToKernel_zero_right, imageToKernel_zero_left, imageToKernel_epi_of_epi_of_zero, imageToKernel_comp_mono
imageToKernel' 📖	CompOp	5 math math: imageToKernel'_kernelSubobjectIso, CategoryTheory.ShortComplex.exact_iff_isIso_imageToKernel', imageSubobjectIso_imageToKernel', CategoryTheory.ShortComplex.Exact.isIso_imageToKernel', CategoryTheory.ShortComplex.exact_iff_epi_imageToKernel'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
factorThruImageSubobject_comp_imageToKernel 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.imageSubobject CategoryTheory.Limits.kernelSubobject CategoryTheory.Limits.factorThruImageSubobject imageToKernel CategoryTheory.Limits.factorThruKernelSubobject	—	CategoryTheory.Subobject.eq_of_comp_arrow_eq CategoryTheory.Category.assoc imageToKernel_arrow CategoryTheory.Limits.imageSubobject_arrow_comp CategoryTheory.Limits.factorThruKernelSubobject_comp_arrow
imageSubobjectIso_imageToKernel' 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.imageSubobject CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.image CategoryTheory.Limits.kernel CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Iso.hom CategoryTheory.Limits.imageSubobjectIso imageToKernel' CategoryTheory.Limits.kernelSubobject imageToKernel CategoryTheory.Limits.kernelSubobjectIso	—	CategoryTheory.Limits.equalizer.hom_ext CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Limits.HasImages.has_image CategoryTheory.Category.assoc CategoryTheory.Limits.kernel.lift_ι CategoryTheory.Limits.imageSubobject_arrow CategoryTheory.Limits.kernelSubobject_arrow imageToKernel_arrow
imageToKernel'_kernelSubobjectIso 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Limits.image CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.kernel CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.kernelSubobject imageToKernel' CategoryTheory.Iso.inv CategoryTheory.Limits.kernelSubobjectIso CategoryTheory.Limits.imageSubobject CategoryTheory.Limits.imageSubobjectIso imageToKernel	—	CategoryTheory.Subobject.eq_of_comp_arrow_eq CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Category.assoc CategoryTheory.Limits.kernelSubobject_arrow' CategoryTheory.Limits.kernel.lift_ι imageToKernel_arrow CategoryTheory.Limits.imageSubobject_arrow'
imageToKernel_arrow 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.imageSubobject CategoryTheory.Limits.kernelSubobject imageToKernel CategoryTheory.Subobject.arrow	—	CategoryTheory.Subobject.ofLE_arrow image_le_kernel
imageToKernel_arrow_apply 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	DFunLike.coe CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.kernelSubobject CategoryTheory.ConcreteCategory.hom CategoryTheory.Subobject.arrow CategoryTheory.Limits.imageSubobject imageToKernel	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise imageToKernel_arrow
imageToKernel_arrow_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.imageSubobject CategoryTheory.Limits.kernelSubobject imageToKernel CategoryTheory.Subobject.arrow	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' imageToKernel_arrow
imageToKernel_comp_hom_inv_comp 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.Iso.inv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	imageToKernel CategoryTheory.Limits.hasImage_comp_iso CategoryTheory.Limits.HasImages.has_image CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.hasKernel_iso_comp CategoryTheory.Iso.isIso_inv CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Limits.hasKernels_of_hasEqualizers CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.imageSubobject CategoryTheory.Limits.kernelSubobject CategoryTheory.Limits.imageSubobjectCompIso CategoryTheory.Limits.kernelSubobjectIsoComp	—	CategoryTheory.Subobject.eq_of_comp_arrow_eq CategoryTheory.Limits.hasImage_comp_iso CategoryTheory.Limits.HasImages.has_image CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.hasKernel_iso_comp CategoryTheory.Iso.isIso_inv CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Limits.hasKernels_of_hasEqualizers imageToKernel_arrow CategoryTheory.Category.assoc CategoryTheory.Limits.kernelSubobjectIsoComp_inv_arrow CategoryTheory.IsIso.Iso.inv_inv imageToKernel_arrow_assoc CategoryTheory.Limits.imageSubobjectCompIso_hom_arrow_assoc CategoryTheory.IsIso.Iso.inv_hom CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
imageToKernel_comp_left 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	imageToKernel CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.imageSubobject CategoryTheory.Limits.kernelSubobject CategoryTheory.Subobject.ofLE CategoryTheory.Limits.imageSubobject_comp_le	—	CategoryTheory.Subobject.eq_of_comp_arrow_eq CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Limits.imageSubobject_comp_le imageToKernel_arrow CategoryTheory.Category.assoc CategoryTheory.Subobject.ofLE_arrow
imageToKernel_comp_mono 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	imageToKernel CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasKernel_comp_mono CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.imageSubobject CategoryTheory.Limits.kernelSubobject CategoryTheory.cancel_mono CategoryTheory.Iso.inv CategoryTheory.Subobject.isoOfEq CategoryTheory.Limits.kernelSubobject_comp_mono	—	CategoryTheory.Subobject.eq_of_comp_arrow_eq CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasKernel_comp_mono CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.cancel_mono CategoryTheory.Limits.kernelSubobject_comp_mono imageToKernel_arrow CategoryTheory.Category.assoc CategoryTheory.Subobject.ofLE_arrow
imageToKernel_comp_right 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	imageToKernel CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.imageSubobject CategoryTheory.Limits.kernelSubobject CategoryTheory.Subobject.ofLE CategoryTheory.Limits.kernelSubobject_comp_le	—	CategoryTheory.Subobject.eq_of_comp_arrow_eq CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Limits.kernelSubobject_comp_le imageToKernel_arrow CategoryTheory.Category.assoc CategoryTheory.Subobject.ofLE_arrow
imageToKernel_epi_comp 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	imageToKernel CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.imageSubobject CategoryTheory.Limits.kernelSubobject CategoryTheory.Subobject.ofLE CategoryTheory.Limits.imageSubobject_comp_le CategoryTheory.cancel_epi	—	CategoryTheory.Subobject.eq_of_comp_arrow_eq CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Limits.imageSubobject_comp_le CategoryTheory.cancel_epi imageToKernel_arrow CategoryTheory.Category.assoc CategoryTheory.Subobject.ofLE_arrow
imageToKernel_epi_of_epi_of_zero 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.imageSubobject CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.kernelSubobject Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.hasEqualizer_of_self imageToKernel	—	CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasEqualizer_of_self CategoryTheory.Limits.isIso_kernelSubobject_zero_arrow imageToKernel_zero_right CategoryTheory.Limits.imageSubobject_arrow CategoryTheory.epi_comp CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.Limits.epi_image_of_epi CategoryTheory.IsIso.inv_isIso
imageToKernel_epi_of_zero_of_mono 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.imageSubobject Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.hasImage_zero CategoryTheory.Limits.kernelSubobject CategoryTheory.Limits.HasKernels.has_limit imageToKernel	—	CategoryTheory.Limits.epi_of_target_iso_zero CategoryTheory.Limits.hasImage_zero CategoryTheory.Limits.HasKernels.has_limit
imageToKernel_zero_left 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	imageToKernel CategoryTheory.Limits.hasImage_zero CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.imageSubobject CategoryTheory.Limits.kernelSubobject	—	CategoryTheory.Subobject.eq_of_comp_arrow_eq CategoryTheory.Limits.hasImage_zero CategoryTheory.Limits.HasKernels.has_limit imageToKernel_arrow CategoryTheory.Limits.imageSubobject_zero_arrow CategoryTheory.Limits.zero_comp
imageToKernel_zero_right 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	imageToKernel CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasEqualizer_of_self CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.imageSubobject CategoryTheory.Limits.kernelSubobject CategoryTheory.Subobject.arrow CategoryTheory.inv CategoryTheory.Limits.isIso_kernelSubobject_zero_arrow	—	CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasEqualizer_of_self CategoryTheory.Limits.isIso_kernelSubobject_zero_arrow imageToKernel_arrow
image_le_kernel 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Subobject Preorder.toLE PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Limits.imageSubobject CategoryTheory.Limits.kernelSubobject	—	CategoryTheory.Limits.kernel.lift_ι
instMonoImageToKernel 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Mono CategoryTheory.Functor.obj CategoryTheory.Subobject Preorder.smallCategory PartialOrder.toPreorder CategoryTheory.instPartialOrderSubobject CategoryTheory.Subobject.underlying CategoryTheory.Limits.imageSubobject CategoryTheory.Limits.kernelSubobject imageToKernel	—	image_le_kernel CategoryTheory.Subobject.instMonoOfLE
subobject_ofLE_as_imageToKernel 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Subobject.ofLE CategoryTheory.Limits.imageSubobject CategoryTheory.Limits.kernelSubobject imageToKernel	—	—

---

← Back to Index