Images

📁 Source: Mathlib/CategoryTheory/Abelian/Images.lean

Statistics

Metric	Count
Definitions coimage, π, coimageImageComparison, coimageImageComparison', coimageImageComparisonFunctor, factorThruCoimage, factorThruImage, image, ι	9
Theorems fac, coimageImageComparisonFunctor_map, coimageImageComparisonFunctor_obj, coimageImageComparison_eq_coimageImageComparison', coimage_image_factorisation, coimage_image_factorisation_assoc, epi_factorThruCoimage, fac, mono_factorThruImage	9
Total	18

CategoryTheory.Abelian

Definitions

Name	Category	Theorems
coimage 📖	CompOp	45 math math: FunctorCategory.coimageImageComparison_app', CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage_assoc, PreservesCoimage.iso_hom_π_assoc, PreservesCoimageImageComparison.iso_inv_left, CategoryTheory.ShortComplex.LeftHomologyData.ofAbelian_H, coimage_image_factorisation, coim_map, CategoryTheory.NonPreadditiveAbelian.isIso_factorThruCoimage, FunctorCategory.coimageImageComparison_app, PreservesCoimageImageComparison.iso_hom_left, epi_factorThruCoimage, CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage, PreservesCoimageImageComparison.iso_hom_right, instMonoFactorThruCoimage, coimageStrongEpiMonoFactorisation_I, PreservesCoimage.factorThruCoimage_iso_inv, CategoryTheory.instIsIsoIndCoimageImageComparison, PreservesCoimage.factorThruCoimage_iso_hom_assoc, PreservesCoimage.factorThruCoimage_iso_inv_assoc, factorThruImage_comp_coimageIsoImage'_inv, coim_obj, CategoryTheory.ShortComplex.kernel_ι_comp_cokernel_π_comp_cokernelToAbelianCoimage, coimageImageComparisonFunctor_obj, PreservesCoimage.iso_inv_π, coimage.fac, coimage_image_factorisation_assoc, PreservesCoimage.factorThruCoimage_iso_hom, PreservesCoimageImageComparison.iso_inv_right, CategoryTheory.ShortComplex.instEpiCokernelToAbelianCoimage, coimageImageComparisonFunctor_map, coimage.comp_π_eq_zero, coimageIsoImage'_hom, FunctorCategory.coimageObjIso_inv, PreservesCoimage.hom_coimageImageComparison, CategoryTheory.NonPreadditiveAbelian.instMonoFactorThruCoimage, CategoryTheory.ShortComplex.exact_iff_exact_coimage_π, FunctorCategory.functor_category_isIso_coimageImageComparison, PreservesCoimage.iso_inv_π_assoc, instIsIsoCoimageImageComparison, FunctorCategory.coimageObjIso_hom, isIso_factorThruCoimage, comp_coimage_π_eq_zero, coimIsoIm_inv_app, PreservesCoimage.iso_hom_π, FGModuleCat.instIsIsoCoimageImageComparison
coimageImageComparison 📖	CompOp	19 math math: FunctorCategory.coimageImageComparison_app', PreservesCoimageImageComparison.iso_inv_left, coimage_image_factorisation, FunctorCategory.coimageImageComparison_app, PreservesCoimageImageComparison.iso_hom_left, coimageImageComparison_eq_coimageImageComparison', PreservesCoimageImageComparison.iso_hom_right, CategoryTheory.instIsIsoIndCoimageImageComparison, coimageImageComparisonFunctor_obj, OfCoimageImageComparisonIsIso.imageMonoFactorisation_e', coimage_image_factorisation_assoc, PreservesCoimageImageComparison.iso_inv_right, coimageImageComparisonFunctor_map, PreservesCoimage.hom_coimageImageComparison, FunctorCategory.functor_category_isIso_coimageImageComparison, instIsIsoCoimageImageComparison, coimIsoIm_hom_app, coimIsoIm_inv_app, FGModuleCat.instIsIsoCoimageImageComparison
coimageImageComparison' 📖	CompOp	1 math math: coimageImageComparison_eq_coimageImageComparison'
coimageImageComparisonFunctor 📖	CompOp	2 math math: coimageImageComparisonFunctor_obj, coimageImageComparisonFunctor_map
factorThruCoimage 📖	CompOp	11 math math: CategoryTheory.NonPreadditiveAbelian.isIso_factorThruCoimage, epi_factorThruCoimage, instMonoFactorThruCoimage, PreservesCoimage.factorThruCoimage_iso_inv, PreservesCoimage.factorThruCoimage_iso_hom_assoc, PreservesCoimage.factorThruCoimage_iso_inv_assoc, coimage.fac, PreservesCoimage.factorThruCoimage_iso_hom, CategoryTheory.NonPreadditiveAbelian.instMonoFactorThruCoimage, isIso_factorThruCoimage, coimageStrongEpiMonoFactorisation_m
factorThruImage 📖	CompOp	11 math math: imageStrongEpiMonoFactorisation_e, image.fac, PreservesImage.factorThruImage_iso_hom, instEpiFactorThruImage, CategoryTheory.NonPreadditiveAbelian.instEpiFactorThruImage, PreservesImage.factorThruImage_iso_hom_assoc, mono_factorThruImage, PreservesImage.factorThruImage_iso_inv, PreservesImage.factorThruImage_iso_inv_assoc, isIso_factorThruImage, CategoryTheory.NonPreadditiveAbelian.isIso_factorThruImage
image 📖	CompOp	48 math math: FunctorCategory.coimageImageComparison_app', CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π_assoc, CategoryTheory.ShortComplex.RightHomologyData.ofAbelian_H, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι, PreservesCoimageImageComparison.iso_inv_left, image.fac, OfCoimageImageComparisonIsIso.imageMonoFactorisation_I, coimage_image_factorisation, PreservesImage.factorThruImage_iso_hom, instEpiFactorThruImage, FunctorCategory.coimageImageComparison_app, PreservesCoimageImageComparison.iso_hom_left, im_map, CategoryTheory.ShortComplex.exact_iff_exact_image_ι, image_ι_comp_eq_zero, PreservesCoimageImageComparison.iso_hom_right, CategoryTheory.NonPreadditiveAbelian.instEpiFactorThruImage, CategoryTheory.ShortComplex.instMonoAbelianImageToKernel, PreservesImage.iso_hom_ι, PreservesImage.factorThruImage_iso_hom_assoc, imageIsoImage_inv, CategoryTheory.instIsIsoIndCoimageImageComparison, PreservesImage.iso_inv_ι_assoc, coimageImageComparisonFunctor_obj, OfCoimageImageComparisonIsIso.imageMonoFactorisation_e', PreservesImage.iso_hom_ι_assoc, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_assoc, coimage_image_factorisation_assoc, mono_factorThruImage, PreservesCoimageImageComparison.iso_inv_right, im_obj, PreservesImage.iso_inv_ι, coimageImageComparisonFunctor_map, imageIsoImage_hom_comp_image_ι, PreservesCoimage.hom_coimageImageComparison, PreservesImage.factorThruImage_iso_inv, image.ι_comp_eq_zero, PreservesImage.factorThruImage_iso_inv_assoc, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_comp_cokernel_π, imageStrongEpiMonoFactorisation_I, FunctorCategory.imageObjIso_hom, FunctorCategory.functor_category_isIso_coimageImageComparison, isIso_factorThruImage, CategoryTheory.NonPreadditiveAbelian.isIso_factorThruImage, instIsIsoCoimageImageComparison, FunctorCategory.imageObjIso_inv, coimIsoIm_inv_app, FGModuleCat.instIsIsoCoimageImageComparison

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coimageImageComparisonFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Arrow CategoryTheory.instCategoryArrow coimageImageComparisonFunctor CategoryTheory.Arrow.homMk coimage CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom image coimageImageComparison CategoryTheory.Limits.cokernel.map CategoryTheory.Limits.kernel CategoryTheory.Limits.kernel.ι CategoryTheory.Limits.kernel.map CategoryTheory.CommaMorphism.left CategoryTheory.CommaMorphism.right CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π	—	—
coimageImageComparisonFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Arrow CategoryTheory.instCategoryArrow coimageImageComparisonFunctor coimage CategoryTheory.Comma.left CategoryTheory.Functor.id CategoryTheory.Comma.right CategoryTheory.Comma.hom image coimageImageComparison	—	—
coimageImageComparison_eq_coimageImageComparison' 📖	mathematical	—	coimageImageComparison coimageImageComparison'	—	CategoryTheory.Limits.coequalizer.hom_ext CategoryTheory.Limits.equalizer.hom_ext CategoryTheory.Limits.cokernel.π_desc CategoryTheory.Limits.kernel.lift_ι CategoryTheory.Category.assoc
coimage_image_factorisation 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct coimage coimage.π image coimageImageComparison image.ι	—	CategoryTheory.Limits.cokernel.π_desc_assoc CategoryTheory.Limits.kernel.lift_ι
coimage_image_factorisation_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct coimage coimage.π image coimageImageComparison image.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coimage_image_factorisation
epi_factorThruCoimage 📖	mathematical	—	CategoryTheory.Epi coimage factorThruCoimage	—	CategoryTheory.epi_of_epi_fac coimage.fac
mono_factorThruImage 📖	mathematical	—	CategoryTheory.Mono image factorThruImage	—	CategoryTheory.mono_of_mono_fac image.fac

CategoryTheory.Abelian.coimage

Definitions

Name	Category	Theorems
π 📖	CompOp	14 math math: CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage_assoc, CategoryTheory.Abelian.PreservesCoimage.iso_hom_π_assoc, CategoryTheory.Abelian.coimage_image_factorisation, CategoryTheory.Abelian.coim_map, CategoryTheory.Abelian.coimageStrongEpiMonoFactorisation_e, CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage, CategoryTheory.Abelian.PreservesCoimage.iso_inv_π, fac, CategoryTheory.Abelian.coimage_image_factorisation_assoc, comp_π_eq_zero, CategoryTheory.ShortComplex.exact_iff_exact_coimage_π, CategoryTheory.Abelian.PreservesCoimage.iso_inv_π_assoc, CategoryTheory.Abelian.comp_coimage_π_eq_zero, CategoryTheory.Abelian.PreservesCoimage.iso_hom_π

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Abelian.coimage π CategoryTheory.Abelian.factorThruCoimage	—	CategoryTheory.Limits.cokernel.π_desc CategoryTheory.Limits.kernel.condition

CategoryTheory.Abelian.image

Definitions

Name	Category	Theorems
ι 📖	CompOp	14 math math: CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι, fac, CategoryTheory.Abelian.coimage_image_factorisation, CategoryTheory.Abelian.im_map, CategoryTheory.ShortComplex.exact_iff_exact_image_ι, CategoryTheory.Abelian.image_ι_comp_eq_zero, CategoryTheory.Abelian.PreservesImage.iso_hom_ι, CategoryTheory.Abelian.imageStrongEpiMonoFactorisation_m, CategoryTheory.Abelian.PreservesImage.iso_inv_ι_assoc, CategoryTheory.Abelian.PreservesImage.iso_hom_ι_assoc, CategoryTheory.ShortComplex.abelianImageToKernel_comp_kernel_ι_assoc, CategoryTheory.Abelian.coimage_image_factorisation_assoc, CategoryTheory.Abelian.PreservesImage.iso_inv_ι, ι_comp_eq_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fac 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Abelian.image CategoryTheory.Abelian.factorThruImage ι	—	CategoryTheory.Limits.kernel.lift_ι CategoryTheory.Limits.cokernel.condition

---

← Back to Index