AbelianImages

📁 Source: Mathlib/CategoryTheory/Limits/Preserves/Shapes/AbelianImages.lean

Statistics

Metric	Count
Definitions iso, iso, iso	3
Theorems factorThruCoimage_iso_hom, factorThruCoimage_iso_hom_assoc, factorThruCoimage_iso_inv, factorThruCoimage_iso_inv_assoc, hom_coimageImageComparison, iso_hom_π, iso_hom_π_assoc, iso_inv_π, iso_inv_π_assoc, iso_hom_left, iso_hom_right, iso_inv_left, iso_inv_right, factorThruImage_iso_hom, factorThruImage_iso_hom_assoc, factorThruImage_iso_inv, factorThruImage_iso_inv_assoc, iso_hom_ι, iso_hom_ι_assoc, iso_inv_ι, iso_inv_ι_assoc	21
Total	24

CategoryTheory.Abelian.PreservesCoimage

Definitions

Name	Category	Theorems
iso 📖	CompOp	11 math math: iso_hom_π_assoc, CategoryTheory.Abelian.PreservesCoimageImageComparison.iso_inv_left, CategoryTheory.Abelian.PreservesCoimageImageComparison.iso_hom_left, factorThruCoimage_iso_inv, factorThruCoimage_iso_hom_assoc, factorThruCoimage_iso_inv_assoc, iso_inv_π, factorThruCoimage_iso_hom, hom_coimageImageComparison, iso_inv_π_assoc, iso_hom_π

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
factorThruCoimage_iso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Abelian.coimage CategoryTheory.Functor.map CategoryTheory.Iso.hom iso CategoryTheory.Abelian.factorThruCoimage	—	factorThruCoimage_iso_inv
factorThruCoimage_iso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Abelian.coimage CategoryTheory.Functor.map CategoryTheory.Iso.hom iso CategoryTheory.Abelian.factorThruCoimage	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' factorThruCoimage_iso_hom
factorThruCoimage_iso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Abelian.coimage CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Iso.inv iso CategoryTheory.Abelian.factorThruCoimage	—	CategoryTheory.Limits.coequalizer.hom_ext CategoryTheory.Limits.kernel.condition CategoryTheory.Limits.PreservesCokernel.iso_inv CategoryTheory.Category.assoc CategoryTheory.Limits.cokernelComparison_map_desc CategoryTheory.Limits.cokernel.π_desc_assoc CategoryTheory.Category.id_comp CategoryTheory.Limits.cokernel.π_desc
factorThruCoimage_iso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Abelian.coimage CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Iso.inv iso CategoryTheory.Abelian.factorThruCoimage	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' factorThruCoimage_iso_inv
hom_coimageImageComparison 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Abelian.coimage CategoryTheory.Functor.map CategoryTheory.Limits.instHasKernelMapOfPreservesLimitWalkingParallelPairParallelPairOfNatHom CategoryTheory.Abelian.image CategoryTheory.Limits.instHasCokernelMapOfPreservesColimitWalkingParallelPairParallelPairOfNatHom CategoryTheory.Iso.hom iso CategoryTheory.Abelian.coimageImageComparison CategoryTheory.Abelian.PreservesImage.iso	—	CategoryTheory.Limits.instHasCokernelMapOfPreservesColimitWalkingParallelPairParallelPairOfNatHom CategoryTheory.Limits.instHasKernelMapOfPreservesLimitWalkingParallelPairParallelPairOfNatHom CategoryTheory.cancel_mono CategoryTheory.Limits.equalizer.ι_mono CategoryTheory.Category.assoc CategoryTheory.Abelian.PreservesImage.iso_hom_ι CategoryTheory.cancel_epi CategoryTheory.Limits.coequalizer.π_epi CategoryTheory.Abelian.coimage_image_factorisation iso_inv_π_assoc
iso_hom_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Abelian.coimage CategoryTheory.Functor.map CategoryTheory.Abelian.coimage.π CategoryTheory.Iso.hom iso	—	CategoryTheory.Limits.PreservesKernel.iso_hom CategoryTheory.Limits.cokernel.map.congr_simp CategoryTheory.Limits.PreservesCokernel.π_iso_hom_assoc CategoryTheory.Limits.cokernel.π_desc CategoryTheory.Category.id_comp
iso_hom_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Abelian.coimage CategoryTheory.Functor.map CategoryTheory.Abelian.coimage.π CategoryTheory.Iso.hom iso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' iso_hom_π
iso_inv_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Abelian.coimage CategoryTheory.Functor.map CategoryTheory.Abelian.coimage.π CategoryTheory.Iso.inv iso	—	iso_hom_π
iso_inv_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Abelian.coimage CategoryTheory.Functor.map CategoryTheory.Abelian.coimage.π CategoryTheory.Iso.inv iso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' iso_inv_π

CategoryTheory.Abelian.PreservesCoimageImageComparison

Definitions

Name	Category	Theorems
iso 📖	CompOp	4 math math: iso_inv_left, iso_hom_left, iso_hom_right, iso_inv_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iso_hom_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Abelian.coimage CategoryTheory.Abelian.image CategoryTheory.Functor.map CategoryTheory.Abelian.coimageImageComparison CategoryTheory.Limits.instHasKernelMapOfPreservesLimitWalkingParallelPairParallelPairOfNatHom CategoryTheory.Limits.instHasCokernelMapOfPreservesColimitWalkingParallelPairParallelPairOfNatHom CategoryTheory.Iso.hom CategoryTheory.Arrow CategoryTheory.instCategoryArrow iso CategoryTheory.Abelian.PreservesCoimage.iso	—	CategoryTheory.Limits.instHasCokernelMapOfPreservesColimitWalkingParallelPairParallelPairOfNatHom CategoryTheory.Limits.instHasKernelMapOfPreservesLimitWalkingParallelPairParallelPairOfNatHom
iso_hom_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Functor.obj CategoryTheory.Abelian.coimage CategoryTheory.Abelian.image CategoryTheory.Functor.map CategoryTheory.Abelian.coimageImageComparison CategoryTheory.Limits.instHasKernelMapOfPreservesLimitWalkingParallelPairParallelPairOfNatHom CategoryTheory.Limits.instHasCokernelMapOfPreservesColimitWalkingParallelPairParallelPairOfNatHom CategoryTheory.Iso.hom CategoryTheory.Arrow CategoryTheory.instCategoryArrow iso CategoryTheory.Abelian.PreservesImage.iso	—	CategoryTheory.Limits.instHasCokernelMapOfPreservesColimitWalkingParallelPairParallelPairOfNatHom CategoryTheory.Limits.instHasKernelMapOfPreservesLimitWalkingParallelPairParallelPairOfNatHom
iso_inv_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id CategoryTheory.Abelian.coimage CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Limits.instHasKernelMapOfPreservesLimitWalkingParallelPairParallelPairOfNatHom CategoryTheory.Abelian.image CategoryTheory.Limits.instHasCokernelMapOfPreservesColimitWalkingParallelPairParallelPairOfNatHom CategoryTheory.Abelian.coimageImageComparison CategoryTheory.Iso.inv CategoryTheory.Arrow CategoryTheory.instCategoryArrow iso CategoryTheory.Abelian.PreservesCoimage.iso	—	CategoryTheory.Limits.instHasCokernelMapOfPreservesColimitWalkingParallelPairParallelPairOfNatHom CategoryTheory.Limits.instHasKernelMapOfPreservesLimitWalkingParallelPairParallelPairOfNatHom
iso_inv_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id CategoryTheory.Abelian.coimage CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Limits.instHasKernelMapOfPreservesLimitWalkingParallelPairParallelPairOfNatHom CategoryTheory.Abelian.image CategoryTheory.Limits.instHasCokernelMapOfPreservesColimitWalkingParallelPairParallelPairOfNatHom CategoryTheory.Abelian.coimageImageComparison CategoryTheory.Iso.inv CategoryTheory.Arrow CategoryTheory.instCategoryArrow iso CategoryTheory.Abelian.PreservesImage.iso	—	CategoryTheory.Limits.instHasCokernelMapOfPreservesColimitWalkingParallelPairParallelPairOfNatHom CategoryTheory.Limits.instHasKernelMapOfPreservesLimitWalkingParallelPairParallelPairOfNatHom

CategoryTheory.Abelian.PreservesImage

Definitions

Name	Category	Theorems
iso 📖	CompOp	11 math math: factorThruImage_iso_hom, CategoryTheory.Abelian.PreservesCoimageImageComparison.iso_hom_right, iso_hom_ι, factorThruImage_iso_hom_assoc, iso_inv_ι_assoc, iso_hom_ι_assoc, CategoryTheory.Abelian.PreservesCoimageImageComparison.iso_inv_right, iso_inv_ι, CategoryTheory.Abelian.PreservesCoimage.hom_coimageImageComparison, factorThruImage_iso_inv, factorThruImage_iso_inv_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
factorThruImage_iso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Abelian.image CategoryTheory.Functor.map CategoryTheory.Abelian.factorThruImage CategoryTheory.Iso.hom iso	—	CategoryTheory.Limits.equalizer.hom_ext CategoryTheory.Limits.cokernel.condition CategoryTheory.Limits.PreservesKernel.iso_hom CategoryTheory.Limits.map_lift_kernelComparison_assoc CategoryTheory.Category.assoc CategoryTheory.Limits.kernel.lift_ι CategoryTheory.Category.comp_id
factorThruImage_iso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Abelian.image CategoryTheory.Functor.map CategoryTheory.Abelian.factorThruImage CategoryTheory.Iso.hom iso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' factorThruImage_iso_hom
factorThruImage_iso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Abelian.image CategoryTheory.Functor.map CategoryTheory.Abelian.factorThruImage CategoryTheory.Iso.inv iso	—	factorThruImage_iso_hom
factorThruImage_iso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Abelian.image CategoryTheory.Functor.map CategoryTheory.Abelian.factorThruImage CategoryTheory.Iso.inv iso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' factorThruImage_iso_inv
iso_hom_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Abelian.image CategoryTheory.Functor.map CategoryTheory.Iso.hom iso CategoryTheory.Abelian.image.ι	—	CategoryTheory.Limits.PreservesKernel.iso_hom CategoryTheory.Category.assoc CategoryTheory.Limits.kernel.lift_ι CategoryTheory.Category.comp_id CategoryTheory.Limits.kernelComparison_comp_ι
iso_hom_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Abelian.image CategoryTheory.Functor.map CategoryTheory.Iso.hom iso CategoryTheory.Abelian.image.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' iso_hom_ι
iso_inv_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Abelian.image CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Iso.inv iso CategoryTheory.Abelian.image.ι	—	CategoryTheory.Limits.PreservesCokernel.iso_inv CategoryTheory.Limits.kernel.map.congr_simp CategoryTheory.Category.assoc CategoryTheory.Limits.PreservesKernel.iso_inv_ι CategoryTheory.Limits.kernel.lift_ι CategoryTheory.Category.comp_id
iso_inv_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Abelian.image CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Iso.inv iso CategoryTheory.Abelian.image.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' iso_inv_ι

---

← Back to Index