Abelian

📁 Source: Mathlib/Algebra/Homology/ShortComplex/Abelian.lean

Statistics

Metric	Count
Definitions ofAbelian, ofEpiMonoFactorisation, isoHomology, isoImage, leftHomologyData, rightHomologyData, ofAbelian, ofAbelian, abelianImageToKernel, abelianImageToKernelIsKernel, cokernelToAbelianCoimage, cokernelToAbelianCoimageIsCokernel, homologyIsoImageICyclesCompPOpcycles, instAbelian	14
Theorems f'_eq, g'_eq, homologyπ_isoHomology_inv, homologyπ_isoHomology_inv_assoc, isoHomology_hom_comp_ι, isoHomology_hom_comp_ι_assoc, isoHomology_inv_homologyι, isoHomology_inv_homologyι_assoc, isoImage_ι, isoImage_ι_assoc, leftHomologyData_H, leftHomologyData_K, leftHomologyData_i, leftHomologyData_π, rightHomologyData_H, rightHomologyData_Q, rightHomologyData_p, rightHomologyData_ι, π_comp_isoHomology_hom, π_comp_isoHomology_hom_assoc, ofEpiMonoFactorisation_iso, ofEpiMonoFactorisation_left, ofEpiMonoFactorisation_right, ofAbelian_H, ofAbelian_K, ofAbelian_i, ofAbelian_π, ofAbelian_H, ofAbelian_Q, ofAbelian_p, ofAbelian_ι, abelianImageToKernel_comp_kernel_ι, abelianImageToKernel_comp_kernel_ι_assoc, abelianImageToKernel_comp_kernel_ι_comp_cokernel_π, abelianImageToKernel_comp_kernel_ι_comp_cokernel_π_assoc, cokernel_π_comp_cokernelToAbelianCoimage, cokernel_π_comp_cokernelToAbelianCoimage_assoc, homologyIsoImageICyclesCompPOpcycles_ι, homologyIsoImageICyclesCompPOpcycles_ι_assoc, instEpiCokernelToAbelianCoimage, instIsNormalEpiCategory, instIsNormalMonoCategory, instMonoAbelianImageToKernel, kernel_ι_comp_cokernel_π_comp_cokernelToAbelianCoimage, categoryWithHomology_of_abelian	45
Total	59

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
categoryWithHomology_of_abelian 📖	mathematical	—	CategoryWithHomology Preadditive.preadditiveHasZeroMorphisms Abelian.toPreadditive	—	ShortComplex.HasHomology.mk'

CategoryTheory.ShortComplex

Definitions

Name	Category	Theorems
abelianImageToKernel 📖	CompOp	5 math math: abelianImageToKernel_comp_kernel_ι_comp_cokernel_π_assoc, abelianImageToKernel_comp_kernel_ι, instMonoAbelianImageToKernel, abelianImageToKernel_comp_kernel_ι_assoc, abelianImageToKernel_comp_kernel_ι_comp_cokernel_π
abelianImageToKernelIsKernel 📖	CompOp	—
cokernelToAbelianCoimage 📖	CompOp	4 math math: cokernel_π_comp_cokernelToAbelianCoimage_assoc, cokernel_π_comp_cokernelToAbelianCoimage, kernel_ι_comp_cokernel_π_comp_cokernelToAbelianCoimage, instEpiCokernelToAbelianCoimage
cokernelToAbelianCoimageIsCokernel 📖	CompOp	—
homologyIsoImageICyclesCompPOpcycles 📖	CompOp	2 math math: homologyIsoImageICyclesCompPOpcycles_ι, homologyIsoImageICyclesCompPOpcycles_ι_assoc
instAbelian 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abelianImageToKernel_comp_kernel_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Abelian.image CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive X₁ X₂ f CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π CategoryTheory.Limits.kernel X₃ g abelianImageToKernel CategoryTheory.Limits.kernel.ι CategoryTheory.Abelian.image.ι	—	CategoryTheory.Limits.kernel.lift_ι CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels
abelianImageToKernel_comp_kernel_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Abelian.image CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive X₁ X₂ f CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π CategoryTheory.Limits.kernel X₃ g abelianImageToKernel CategoryTheory.Limits.kernel.ι CategoryTheory.Abelian.image.ι	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' abelianImageToKernel_comp_kernel_ι
abelianImageToKernel_comp_kernel_ι_comp_cokernel_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Abelian.image CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive X₁ X₂ f CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π CategoryTheory.Limits.kernel X₃ g abelianImageToKernel CategoryTheory.Limits.kernel.ι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels abelianImageToKernel_comp_kernel_ι_assoc CategoryTheory.Limits.kernel.condition
abelianImageToKernel_comp_kernel_ι_comp_cokernel_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Abelian.image CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive X₁ X₂ f CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π CategoryTheory.Limits.kernel X₃ g abelianImageToKernel CategoryTheory.Limits.kernel.ι Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' abelianImageToKernel_comp_kernel_ι_comp_cokernel_π
cokernel_π_comp_cokernelToAbelianCoimage 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.cokernel X₁ f CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Abelian.coimage X₃ g CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.kernel CategoryTheory.Limits.kernel.ι CategoryTheory.Limits.cokernel.π cokernelToAbelianCoimage CategoryTheory.Abelian.coimage.π	—	CategoryTheory.Limits.cokernel.π_desc CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels
cokernel_π_comp_cokernelToAbelianCoimage_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Limits.cokernel X₁ f CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.cokernel.π CategoryTheory.Abelian.coimage X₃ g CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.kernel CategoryTheory.Limits.kernel.ι cokernelToAbelianCoimage CategoryTheory.Abelian.coimage.π	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cokernel_π_comp_cokernelToAbelianCoimage
homologyIsoImageICyclesCompPOpcycles_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Limits.image cycles hasLeftHomology_of_hasHomology opcycles hasRightHomology_of_hasHomology X₂ iCycles pOpcycles CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Iso.hom homologyIsoImageICyclesCompPOpcycles CategoryTheory.Limits.image.ι homologyι	—	CategoryTheory.Limits.image.isoStrongEpiMono_hom_comp_ι CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian
homologyIsoImageICyclesCompPOpcycles_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Limits.image cycles hasLeftHomology_of_hasHomology opcycles hasRightHomology_of_hasHomology X₂ iCycles pOpcycles CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Iso.hom homologyIsoImageICyclesCompPOpcycles CategoryTheory.Limits.image.ι homologyι	—	hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian hasLeftHomology_of_hasHomology CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyIsoImageICyclesCompPOpcycles_ι
instEpiCokernelToAbelianCoimage 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Limits.cokernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive X₁ X₂ f CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Abelian.coimage X₃ g CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.kernel CategoryTheory.Limits.kernel.ι cokernelToAbelianCoimage	—	CategoryTheory.epi_of_epi_fac CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.coequalizer.π_epi cokernel_π_comp_cokernelToAbelianCoimage
instIsNormalEpiCategory 📖	mathematical	—	CategoryTheory.IsNormalEpiCategory CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive instCategory instHasZeroMorphisms	—	hasLimit_of_hasLimitπ CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Abelian.hasEqualizers CategoryTheory.Limits.kernel.condition preservesZeroMorphisms_π₁ CategoryTheory.Functor.map_epi preservesEpimorphisms_π₁ CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits CategoryTheory.Abelian.hasFiniteColimits instPreservesLimitπ₁ CategoryTheory.Limits.instHasLimitCompOfPreservesLimit CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Limits.hasKernels_of_hasEqualizers hasLimitsOfShape CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit instPreservesLimitsOfShapeπ₂ instPreservesLimitsOfShapeπ₃ preservesZeroMorphisms_π₂ preservesEpimorphisms_π₂ instPreservesLimitπ₂ instPreservesLimitsOfShapeπ₁ preservesZeroMorphisms_π₃ preservesEpimorphisms_π₃ instPreservesLimitπ₃
instIsNormalMonoCategory 📖	mathematical	—	CategoryTheory.IsNormalMonoCategory CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive instCategory instHasZeroMorphisms	—	hasColimit_of_hasColimitπ CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Abelian.hasCoequalizers CategoryTheory.Limits.cokernel.condition preservesZeroMorphisms_π₁ CategoryTheory.Functor.map_mono preservesMonomorphisms_π₁ CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits instPreservesColimitπ₁ CategoryTheory.Limits.instHasColimitCompOfPreservesColimit CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Limits.hasCokernels_of_hasCoequalizers hasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit instPreservesColimitsOfShapeπ₂ instPreservesColimitsOfShapeπ₃ preservesZeroMorphisms_π₂ preservesMonomorphisms_π₂ instPreservesColimitπ₂ instPreservesColimitsOfShapeπ₁ preservesZeroMorphisms_π₃ preservesMonomorphisms_π₃ instPreservesColimitπ₃
instMonoAbelianImageToKernel 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Abelian.image CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive X₁ X₂ f CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.cokernel CategoryTheory.Limits.cokernel.π CategoryTheory.Limits.kernel X₃ g abelianImageToKernel	—	CategoryTheory.mono_of_mono_fac CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Limits.equalizer.ι_mono abelianImageToKernel_comp_kernel_ι
kernel_ι_comp_cokernel_π_comp_cokernelToAbelianCoimage 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive X₂ X₃ g CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.cokernel X₁ f CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Abelian.coimage CategoryTheory.Limits.kernel.ι CategoryTheory.Limits.cokernel.π cokernelToAbelianCoimage Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels CategoryTheory.Limits.HasCokernels.has_colimit CategoryTheory.Abelian.has_cokernels CategoryTheory.Category.assoc cokernel_π_comp_cokernelToAbelianCoimage CategoryTheory.Limits.cokernel.condition

CategoryTheory.ShortComplex.HomologyData

Definitions

Name	Category	Theorems
ofAbelian 📖	CompOp	—
ofEpiMonoFactorisation 📖	CompOp	3 math math: ofEpiMonoFactorisation_left, ofEpiMonoFactorisation_right, ofEpiMonoFactorisation_iso

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofEpiMonoFactorisation_iso 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Cofork.π	iso ofEpiMonoFactorisation CategoryTheory.Iso.refl CategoryTheory.ShortComplex.LeftHomologyData.H ofEpiMonoFactorisation.leftHomologyData	—	—
ofEpiMonoFactorisation_left 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Cofork.π	left ofEpiMonoFactorisation ofEpiMonoFactorisation.leftHomologyData	—	—
ofEpiMonoFactorisation_right 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Cofork.π	right ofEpiMonoFactorisation ofEpiMonoFactorisation.rightHomologyData	—	—

CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation

Definitions

Name	Category	Theorems
isoHomology 📖	CompOp	8 math math: isoHomology_inv_homologyι_assoc, homologyπ_isoHomology_inv_assoc, isoHomology_inv_homologyι, isoHomology_hom_comp_ι_assoc, homologyπ_isoHomology_inv, π_comp_isoHomology_hom, π_comp_isoHomology_hom_assoc, isoHomology_hom_comp_ι
isoImage 📖	CompOp	2 math math: isoImage_ι, isoImage_ι_assoc
leftHomologyData 📖	CompOp	6 math math: CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation_left, leftHomologyData_i, leftHomologyData_K, leftHomologyData_π, leftHomologyData_H, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation_iso
rightHomologyData 📖	CompOp	5 math math: rightHomologyData_Q, rightHomologyData_H, rightHomologyData_p, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation_right, rightHomologyData_ι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
f'_eq 📖	mathematical	—	CategoryTheory.Limits.IsLimit.lift CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.KernelFork.ofι CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.zero CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Limits.Cone.pt CategoryTheory.ShortComplex.toCycles CategoryTheory.Iso.inv CategoryTheory.ShortComplex.isoCyclesOfIsLimit	—	CategoryTheory.Limits.Fork.IsLimit.mono CategoryTheory.ShortComplex.zero CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.cancel_mono CategoryTheory.Limits.Fork.IsLimit.lift_ι CategoryTheory.Category.assoc CategoryTheory.ShortComplex.isoCyclesOfIsLimit_inv_ι CategoryTheory.ShortComplex.toCycles_i
g'_eq 📖	mathematical	—	CategoryTheory.Limits.IsColimit.desc CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.CokernelCofork.ofπ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g CategoryTheory.ShortComplex.zero CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Iso.hom CategoryTheory.ShortComplex.isoOpcyclesOfIsColimit CategoryTheory.ShortComplex.fromOpcycles	—	CategoryTheory.Limits.Cofork.IsColimit.epi CategoryTheory.ShortComplex.zero CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.cancel_epi CategoryTheory.Limits.Cofork.IsColimit.π_desc CategoryTheory.ShortComplex.π_isoOpcyclesOfIsColimit_hom_assoc CategoryTheory.ShortComplex.p_fromOpcycles
homologyπ_isoHomology_inv 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Cofork.π	CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.homology CategoryTheory.ShortComplex.homologyπ CategoryTheory.Iso.inv isoHomology CategoryTheory.ShortComplex.isoCyclesOfIsLimit	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id π_comp_isoHomology_hom CategoryTheory.Iso.inv_hom_id_assoc
homologyπ_isoHomology_inv_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Cofork.π	CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.homology CategoryTheory.ShortComplex.homologyπ CategoryTheory.Iso.inv isoHomology CategoryTheory.ShortComplex.isoCyclesOfIsLimit	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyπ_isoHomology_inv
isoHomology_hom_comp_ι 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Cofork.π	CategoryTheory.ShortComplex.homology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Iso.inv isoHomology CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.homologyι CategoryTheory.ShortComplex.isoOpcyclesOfIsColimit	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.cancel_epi CategoryTheory.ShortComplex.instEpiHomologyπ CategoryTheory.ShortComplex.homology_π_ι_assoc CategoryTheory.ShortComplex.pOpcycles_π_isoOpcyclesOfIsColimit_inv CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_hom π_comp_isoHomology_hom_assoc CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.ShortComplex.isoCyclesOfIsLimit_hom_iCycles_assoc
isoHomology_hom_comp_ι_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Cofork.π	CategoryTheory.ShortComplex.homology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Iso.inv isoHomology CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.homologyι CategoryTheory.ShortComplex.isoOpcyclesOfIsColimit	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoHomology_hom_comp_ι
isoHomology_inv_homologyι 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Cofork.π	CategoryTheory.ShortComplex.homology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.Iso.hom isoHomology CategoryTheory.ShortComplex.homologyι CategoryTheory.ShortComplex.isoOpcyclesOfIsColimit	—	CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id isoHomology_hom_comp_ι CategoryTheory.Iso.hom_inv_id_assoc
isoHomology_inv_homologyι_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Cofork.π	CategoryTheory.ShortComplex.homology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Iso.hom isoHomology CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.homologyι CategoryTheory.ShortComplex.isoOpcyclesOfIsColimit	—	CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoHomology_inv_homologyι
isoImage_ι 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Cofork.π	CategoryTheory.Limits.image CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.iCycles CategoryTheory.ShortComplex.pOpcycles CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Iso.hom isoImage CategoryTheory.Limits.image.ι CategoryTheory.ShortComplex.isoOpcyclesOfIsColimit	—	CategoryTheory.Limits.image.isoStrongEpiMono_hom_comp_ι CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.ShortComplex.π_isoOpcyclesOfIsColimit_hom CategoryTheory.ShortComplex.isoCyclesOfIsLimit_inv_ι_assoc
isoImage_ι_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Cofork.π	CategoryTheory.Limits.image CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.iCycles CategoryTheory.ShortComplex.pOpcycles CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Iso.hom isoImage CategoryTheory.Limits.image.ι CategoryTheory.ShortComplex.isoOpcyclesOfIsColimit	—	CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoImage_ι
leftHomologyData_H 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Cofork.π	CategoryTheory.ShortComplex.LeftHomologyData.H leftHomologyData	—	—
leftHomologyData_K 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Cofork.π	CategoryTheory.ShortComplex.LeftHomologyData.K leftHomologyData	—	—
leftHomologyData_i 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Cofork.π	CategoryTheory.ShortComplex.LeftHomologyData.i leftHomologyData	—	—
leftHomologyData_π 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Cofork.π	CategoryTheory.ShortComplex.LeftHomologyData.π leftHomologyData	—	—
rightHomologyData_H 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Cofork.π	CategoryTheory.ShortComplex.RightHomologyData.H rightHomologyData	—	—
rightHomologyData_Q 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Cofork.π	CategoryTheory.ShortComplex.RightHomologyData.Q rightHomologyData	—	—
rightHomologyData_p 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Cofork.π	CategoryTheory.ShortComplex.RightHomologyData.p rightHomologyData	—	—
rightHomologyData_ι 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Cofork.π	CategoryTheory.ShortComplex.RightHomologyData.ι rightHomologyData	—	—
π_comp_isoHomology_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Cofork.π	CategoryTheory.ShortComplex.homology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Iso.hom isoHomology CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.ShortComplex.isoCyclesOfIsLimit CategoryTheory.ShortComplex.homologyπ	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.Limits.HasImages.has_image CategoryTheory.Limits.hasImages_of_hasStrongEpiMonoFactorisations CategoryTheory.Abelian.instHasStrongEpiMonoFactorisations CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id CategoryTheory.Limits.instMonoι isoImage_ι Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.ShortComplex.π_isoOpcyclesOfIsColimit_hom CategoryTheory.ShortComplex.homologyIsoImageICyclesCompPOpcycles_ι CategoryTheory.ShortComplex.homology_π_ι CategoryTheory.ShortComplex.isoCyclesOfIsLimit_hom_iCycles_assoc
π_comp_isoHomology_hom_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Cocone.pt CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Limits.Fork.ι CategoryTheory.Limits.Cofork.π	CategoryTheory.ShortComplex.homology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Iso.hom isoHomology CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.ShortComplex.isoCyclesOfIsLimit CategoryTheory.ShortComplex.homologyπ	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_comp_isoHomology_hom

CategoryTheory.ShortComplex.LeftHomologyData

Definitions

Name	Category	Theorems
ofAbelian 📖	CompOp	4 math math: ofAbelian_K, ofAbelian_H, ofAbelian_i, ofAbelian_π

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofAbelian_H 📖	mathematical	—	H CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ofAbelian CategoryTheory.Abelian.coimage CategoryTheory.Limits.kernel CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g CategoryTheory.Limits.cokernel CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel.ι CategoryTheory.Limits.cokernel.π	—	—
ofAbelian_K 📖	mathematical	—	K CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ofAbelian CategoryTheory.Limits.kernel CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	—
ofAbelian_i 📖	mathematical	—	i CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ofAbelian CategoryTheory.Limits.kernel.ι CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	—
ofAbelian_π 📖	mathematical	—	π CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ofAbelian CategoryTheory.Limits.cokernel.π CategoryTheory.Limits.kernel CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g CategoryTheory.Limits.cokernel CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel.ι	—	—

CategoryTheory.ShortComplex.RightHomologyData

Definitions

Name	Category	Theorems
ofAbelian 📖	CompOp	4 math math: ofAbelian_H, ofAbelian_Q, ofAbelian_p, ofAbelian_ι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ofAbelian_H 📖	mathematical	—	H CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ofAbelian CategoryTheory.Abelian.image CategoryTheory.Limits.kernel CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g CategoryTheory.Limits.cokernel CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.kernel.ι CategoryTheory.Limits.cokernel.π	—	—
ofAbelian_Q 📖	mathematical	—	Q CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ofAbelian CategoryTheory.Limits.cokernel CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	—	—
ofAbelian_p 📖	mathematical	—	p CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ofAbelian CategoryTheory.Limits.cokernel.π CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	—	—
ofAbelian_ι 📖	mathematical	—	ι CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ofAbelian CategoryTheory.Limits.kernel.ι CategoryTheory.Limits.cokernel CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f CategoryTheory.Limits.kernel CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.cokernel.π	—	—

---

← Back to Index