Homology

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

Statistics

Metric	Count
Definitions CategoryWithHomology, HasHomology, HomologyData, canonical, iso, left, ofEpiOfIsIsoOfMono, ofEpiOfIsIsoOfMono', ofHasCokernel, ofHasKernel, ofIsColimitCokernelCofork, ofIsIsoLeftRightHomologyComparison', ofIsLimitKernelFork, ofIso, ofZeros, op, right, unop, HomologyMapData, comp, compatibilityOfZerosOfIsColimitCokernelCofork, compatibilityOfZerosOfIsLimitKernelFork, homologyMapData, id, instInhabited, instUnique, left, ofEpiOfIsIsoOfMono, ofEpiOfIsIsoOfMono', ofIsColimitCokernelCofork, ofIsLimitKernelFork, ofZeros, op, right, unop, zero, canonical, homologyIso, canonical, homologyIso, asIsoHomologyι, asIsoHomologyπ, descHomology, homology, homologyData, homologyFunctor, homologyFunctorOpNatIso, homologyIsCokernel, homologyIsKernel, homologyIsoCokernelLift, homologyIsoKernelDesc, homologyMap, homologyMap', homologyMapIso, homologyMapIso', homologyOpIso, homologyι, homologyπ, leftHomologyIso, leftRightHomologyComparison, leftRightHomologyComparison', liftHomology, rightHomologyIso	63
Theorems hasHomology, condition, mk', canonical_iso_hom, canonical_iso_inv, canonical_left_H, canonical_left_K, canonical_left_i, canonical_left_π, canonical_right_H, canonical_right_Q, canonical_right_p, canonical_right_ι, comm, comm_assoc, leftRightHomologyComparison'_eq, left_homologyIso_eq_right_homologyIso_trans_iso_symm, ofEpiOfIsIsoOfMono'_iso, ofEpiOfIsIsoOfMono'_left, ofEpiOfIsIsoOfMono'_right, ofEpiOfIsIsoOfMono_iso, ofEpiOfIsIsoOfMono_left, ofEpiOfIsIsoOfMono_right, ofHasCokernel_iso, ofHasCokernel_left, ofHasCokernel_right, ofHasKernel_iso, ofHasKernel_left, ofHasKernel_right, ofIsColimitCokernelCofork_iso, ofIsColimitCokernelCofork_left, ofIsColimitCokernelCofork_right, ofIsIsoLeftRightHomologyComparison'_iso, ofIsIsoLeftRightHomologyComparison'_left, ofIsIsoLeftRightHomologyComparison'_right, ofIsLimitKernelFork_iso, ofIsLimitKernelFork_left, ofIsLimitKernelFork_right, ofIso_iso, ofIso_left_H, ofIso_left_K, ofIso_left_i, ofIso_left_π, ofIso_right_H, ofIso_right_Q, ofIso_right_p, ofIso_right_ι, ofZeros_iso, ofZeros_left, ofZeros_right, op_iso, op_left, op_right, right_homologyIso_eq_left_homologyIso_trans_iso, unop_iso, unop_left, unop_right, comm, comm_assoc, comp_left, comp_right, compatibilityOfZerosOfIsLimitKernelFork_left, compatibilityOfZerosOfIsLimitKernelFork_right, congr_left_φH, cyclesMap'_eq, homologyMap'_eq, id_left, id_right, instSubsingleton, ofIsColimitCokernelCofork_left, ofIsColimitCokernelCofork_right, ofIsLimitKernelFork_left, ofIsLimitKernelFork_right, ofZeros_left, ofZeros_right, op_left, op_right, opcyclesMap'_eq, unop_left, unop_right, zero_left, zero_right, canonical_H, canonical_K, canonical_f', canonical_i, canonical_π, homologyIso_hom_comp_leftHomologyIso_inv, homologyIso_hom_comp_leftHomologyIso_inv_assoc, homologyIso_leftHomologyData, homologyπ_comp_homologyIso_hom, homologyπ_comp_homologyIso_hom_assoc, leftHomologyIso_hom_comp_homologyIso_inv, leftHomologyIso_hom_comp_homologyIso_inv_assoc, leftHomologyIso_hom_naturality, leftHomologyIso_hom_naturality_assoc, leftHomologyIso_inv_naturality, leftHomologyIso_inv_naturality_assoc, π_comp_homologyIso_inv, π_comp_homologyIso_inv_assoc, homologyMap_comm, homologyMap_eq, canonical_H, canonical_Q, canonical_g', canonical_p, canonical_ι, homologyIso_hom_comp_rightHomologyIso_inv, homologyIso_hom_comp_rightHomologyIso_inv_assoc, homologyIso_hom_comp_ι, homologyIso_hom_comp_ι_assoc, homologyIso_inv_comp_homologyι, homologyIso_inv_comp_homologyι_assoc, homologyIso_rightHomologyData, rightHomologyIso_hom_comp_homologyIso_inv, rightHomologyIso_hom_comp_homologyIso_inv_assoc, rightHomologyIso_hom_naturality, rightHomologyIso_hom_naturality_assoc, rightHomologyIso_inv_naturality, rightHomologyIso_inv_naturality_assoc, homologyMap_comm, homologyMap_eq, asIsoHomologyι_hom, asIsoHomologyι_inv_comp_homologyι, asIsoHomologyι_inv_comp_homologyι_assoc, asIsoHomologyπ_hom, asIsoHomologyπ_inv_comp_homologyπ, asIsoHomologyπ_inv_comp_homologyπ_assoc, comp_homologyMap_comp, comp_homologyMap_comp_assoc, epi_homologyMap_of_epi_cyclesMap, epi_homologyMap_of_epi_cyclesMap', hasHomology_of_epi_of_isIso_of_mono, hasHomology_of_epi_of_isIso_of_mono', hasHomology_of_hasCokernel, hasHomology_of_hasKernel, hasHomology_of_isIsoLeftRightHomologyComparison, hasHomology_of_isIso_leftRightHomologyComparison', hasHomology_of_iso, hasHomology_of_zeros, hasLeftHomology_of_hasHomology, hasRightHomology_of_hasHomology, homologyFunctor_map, homologyFunctor_obj, homologyMap'_comp, homologyMap'_id, homologyMap'_op, homologyMap'_zero, homologyMapIso'_hom, homologyMapIso'_inv, homologyMapIso_hom, homologyMapIso_inv, homologyMap_comp, homologyMap_id, homologyMap_op, homologyMap_zero, homologyOpIso_hom_naturality, homologyOpIso_hom_naturality_assoc, homologyOpIso_inv_naturality, homologyOpIso_inv_naturality_assoc, homology_π_ι, homology_π_ι_assoc, homologyι_comp_asIsoHomologyι_inv, homologyι_comp_asIsoHomologyι_inv_assoc, homologyι_comp_fromOpcycles, homologyι_comp_fromOpcycles_assoc, homologyι_descOpcycles_eq_zero_of_boundary, homologyι_descOpcycles_eq_zero_of_boundary_assoc, homologyι_naturality, homologyι_naturality_assoc, homologyπ_comp_asIsoHomologyπ_inv, homologyπ_comp_asIsoHomologyπ_inv_assoc, homologyπ_comp_leftHomologyIso_inv, homologyπ_comp_leftHomologyIso_inv_assoc, homologyπ_naturality, homologyπ_naturality_assoc, instCategoryWithHomologyOpposite, instEpiHomologyπ, instHasHomologyOppositeOp, instHasHomologyUnopOfOpposite, instMonoHomologyι, isIso_homologyFunctor_map_of_epi_of_isIso_of_mono, isIso_homologyMap'_of_epi_of_isIso_of_mono, isIso_homologyMap'_of_isIso, isIso_homologyMap_of_epi_of_isIso_of_mono, isIso_homologyMap_of_epi_of_isIso_of_mono', isIso_homologyMap_of_isIso, isIso_homologyMap_of_isIso_cyclesMap_of_epi, isIso_homologyMap_of_isIso_opcyclesMap_of_mono, isIso_homologyMap_of_iso, isIso_homologyι, isIso_homologyπ, isIso_leftRightHomologyComparison, isIso_leftRightHomologyComparison', isIso_leftRightHomologyComparison'_of_homologyData, isZero_homology_of_isZero_X₂, leftHomologyIso_hom_naturality, leftHomologyIso_hom_naturality_assoc, leftHomologyIso_inv_naturality, leftHomologyIso_inv_naturality_assoc, leftRightHomologyComparison'_compatibility, leftRightHomologyComparison'_eq_descH, leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap', leftRightHomologyComparison'_eq_liftH, leftRightHomologyComparison'_fac, leftRightHomologyComparison'_fac_assoc, leftRightHomologyComparison'_naturality, leftRightHomologyComparison'_naturality_assoc, leftRightHomologyComparison_eq, leftRightHomologyComparison_fac, leftRightHomologyComparison_fac_assoc, liftCycles_homologyπ_eq_zero_of_boundary, liftHomology_ι, liftHomology_ι_assoc, mono_homologyMap_of_mono_opcyclesMap, mono_homologyMap_of_mono_opcyclesMap', rightHomologyIso_hom_comp_homologyι, rightHomologyIso_hom_comp_homologyι_assoc, rightHomologyIso_hom_naturality, rightHomologyIso_hom_naturality_assoc, rightHomologyIso_inv_naturality, rightHomologyIso_inv_naturality_assoc, toCycles_comp_homologyπ, toCycles_comp_homologyπ_assoc, π_descHomology, π_descHomology_assoc, π_homologyMap_ι, π_homologyMap_ι_assoc, π_leftRightHomologyComparison'_ι, π_leftRightHomologyComparison'_ι_assoc, π_leftRightHomologyComparison_ι, π_leftRightHomologyComparison_ι_assoc	232
Total	295

CategoryTheory

Definitions

Name	Category	Theorems
CategoryWithHomology 📖	CompData	3 math math: ShortComplex.instCategoryWithHomologyOpposite, TopModuleCat.instCategoryWithHomology, categoryWithHomology_of_abelian

CategoryTheory.CategoryWithHomology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasHomology 📖	mathematical	—	CategoryTheory.ShortComplex.HasHomology	—	—

CategoryTheory.ShortComplex

Definitions

Name	Category	Theorems
HasHomology 📖	CompData	16 math math: hasHomology_of_zeros, hasHomology_of_preserves', hasHomology_of_preserves, hasHomology_of_hasCokernel, hasHomology_of_epi_of_isIso_of_mono, hasHomology_of_isIsoLeftRightHomologyComparison, HomologicalComplex.truncGE'.hasHomology_sc'_of_not_mem_boundary, instHasHomologyOppositeOp, HasHomology.mk', hasHomology_of_epi_of_isIso_of_mono', CategoryTheory.CategoryWithHomology.hasHomology, instHasHomologyUnopOfOpposite, hasHomology_of_iso, hasHomology_of_isIso_leftRightHomologyComparison', Exact.hasHomology, hasHomology_of_hasKernel
HomologyData 📖	CompData	1 math math: HasHomology.condition
HomologyMapData 📖	CompData	1 math math: HomologyMapData.instSubsingleton
asIsoHomologyι 📖	CompOp	5 math math: homologyι_comp_asIsoHomologyι_inv, asIsoHomologyι_hom, homologyι_comp_asIsoHomologyι_inv_assoc, asIsoHomologyι_inv_comp_homologyι_assoc, asIsoHomologyι_inv_comp_homologyι
asIsoHomologyπ 📖	CompOp	5 math math: asIsoHomologyπ_hom, asIsoHomologyπ_inv_comp_homologyπ, asIsoHomologyπ_inv_comp_homologyπ_assoc, homologyπ_comp_asIsoHomologyπ_inv_assoc, homologyπ_comp_asIsoHomologyπ_inv
descHomology 📖	CompOp	2 math math: π_descHomology, π_descHomology_assoc
homology 📖	CompOp	160 math math: toCycles_comp_homologyπ, toCycles_comp_homologyπ_assoc, HomologyData.canonical_iso_hom, homologyι_naturality, π_moduleCatCyclesIso_hom, homologyMap_smul, HomologicalComplex.π_homologyIsoSc'_hom, homologyOpIso_hom_naturality, homologyMap_add, homology_π_ι_assoc, homologyMap_zero, RightHomologyData.homologyIso_hom_comp_rightHomologyIso_inv, isIso_homologyMap_of_isIso_cyclesMap_of_epi, RightHomologyMapData.homologyMap_eq, RightHomologyData.rightHomologyIso_inv_naturality_assoc, mapHomologyIso_hom_naturality, LeftHomologyData.π_comp_homologyIso_inv, isIso_homologyπ, homologyMapIso_inv, RightHomologyData.homologyIso_inv_comp_homologyι, LeftHomologyData.leftHomologyIso_hom_comp_homologyIso_inv, HomologyData.ofEpiMonoFactorisation.isoHomology_inv_homologyι_assoc, leftRightHomologyComparison_fac, HomologyData.right_homologyIso_eq_left_homologyIso_trans_iso, leftRightHomologyComparison'_fac, isZero_homology_of_isZero_X₂, homologyπ_naturality_assoc, RightHomologyData.homologyIso_hom_comp_ι, homologyOpIso_inv_naturality, RightHomologyData.rightHomologyIso_hom_naturality, HomologyData.ofEpiMonoFactorisation.homologyπ_isoHomology_inv_assoc, HomologyData.canonical_right_H, homologyMapIso_hom, RightHomologyMapData.homologyMap_comm, RightHomologyData.rightHomologyIso_inv_naturality, homology_π_ι, homologyι_naturality_assoc, mapHomologyIso_hom_naturality_assoc, LeftHomologyMapData.homologyMap_comm, CategoryTheory.NatTrans.app_homology, QuasiIso.isIso, HomologyData.canonical_left_H, leftHomologyIso_hom_naturality, homologyι_comp_fromOpcycles_assoc, HomologicalComplex.homologyIsoSc'_hom_ι_assoc, moduleCatCyclesIso_inv_π_assoc_apply, RightHomologyData.homologyIso_hom_comp_rightHomologyIso_inv_assoc, leftHomologyIso_hom_naturality_assoc, exact_iff_isZero_homology, asIsoHomologyπ_hom, HomologyData.ofEpiMonoFactorisation.isoHomology_inv_homologyι, homologyπ_comp_leftHomologyIso_inv, leftHomologyIso_inv_naturality_assoc, homologyι_descOpcycles_eq_zero_of_boundary, QuasiIso.isIso', mapHomologyIso'_hom_naturality, homologyπ_naturality, LeftHomologyMapData.homologyMap_eq, homologyOpIso_hom_naturality_assoc, homologyMap_mapNatTrans, rightHomologyIso_inv_naturality_assoc, rightHomologyIso_hom_comp_homologyι, homologyMap_neg, liftHomology_ι, HomologicalComplex.π_homologyIsoSc'_hom_assoc, isIso_homologyι, RightHomologyData.homologyIso_hom_comp_ι_assoc, liftHomology_ι_assoc, LeftHomologyData.homologyπ_comp_homologyIso_hom_assoc, HomologicalComplex.π_homologyIsoSc'_inv_assoc, RightHomologyData.homologyIso_inv_comp_homologyι_assoc, π_descHomology, π_moduleCatCyclesIso_hom_assoc_apply, LeftHomologyData.leftHomologyIso_hom_naturality_assoc, LeftHomologyData.leftHomologyIso_hom_naturality, comp_homologyMap_comp_assoc, RightHomologyData.rightHomologyIso_hom_comp_homologyIso_inv_assoc, HomologyData.left_homologyIso_eq_right_homologyIso_trans_iso_symm, mono_homologyMap_of_mono_opcyclesMap', LeftHomologyData.leftHomologyIso_inv_naturality_assoc, asIsoHomologyπ_inv_comp_homologyπ, homologyι_comp_asIsoHomologyι_inv, homologyMap_comp, LeftHomologyData.π_comp_homologyIso_inv_assoc, LeftHomologyData.homologyIso_hom_comp_leftHomologyIso_inv_assoc, LeftHomologyData.canonical_H, homologyπ_comp_leftHomologyIso_inv_assoc, homologyOpIso_inv_naturality_assoc, homologyFunctor_obj, homologyMap_sub, LeftHomologyData.homologyIso_leftHomologyData, isIso_homologyMap_of_isIso, rightHomologyIso_hom_naturality_assoc, asIsoHomologyπ_inv_comp_homologyπ_assoc, π_moduleCatCyclesIso_hom_apply, homologyIsoImageICyclesCompPOpcycles_ι, eq_liftCycles_homologyπ_up_to_refinements, quasiIso_iff, π_homologyMap_ι_assoc, HomologicalComplex.homologyIsoSc'_inv_ι, homologyι_comp_fromOpcycles, HomologyData.ofEpiMonoFactorisation.isoHomology_hom_comp_ι_assoc, homologyι_descOpcycles_eq_zero_of_boundary_assoc, moduleCatCyclesIso_inv_π_assoc, HomologyData.canonical_iso_inv, rightHomologyIso_hom_comp_homologyι_assoc, isIso_homologyMap_of_isIso_opcyclesMap_of_mono, RightHomologyData.rightHomologyIso_hom_naturality_assoc, asIsoHomologyι_hom, LeftHomologyData.mapHomologyIso_eq, homologyMap_op, isIso_homologyMap_of_iso, HomologicalComplex.π_homologyIsoSc'_inv, LeftHomologyData.homologyIso_hom_comp_leftHomologyIso_inv, rightHomologyIso_inv_naturality, π_moduleCatCyclesIso_hom_assoc, RightHomologyData.canonical_H, homologyMap_nullHomotopic, homologyπ_comp_asIsoHomologyπ_inv_assoc, leftHomologyIso_inv_naturality, HomologyData.ofEpiMonoFactorisation.homologyπ_isoHomology_inv, homologyMap_id, exact_iff_homology_iso_zero, mapHomologyIso_inv_naturality, mapHomologyIso'_hom_naturality_assoc, moduleCatCyclesIso_inv_π_apply, isIso_homologyMap_of_epi_of_isIso_of_mono', LeftHomologyData.homologyπ_comp_homologyIso_hom, isIso_homologyMap_of_epi_of_isIso_of_mono, epi_homologyMap_of_epi_cyclesMap, LeftHomologyData.leftHomologyIso_inv_naturality, HomologicalComplex.homologyIsoSc'_inv_ι_assoc, liftCycles_homologyπ_eq_zero_of_boundary, rightHomologyIso_hom_naturality, HomologyData.ofEpiMonoFactorisation.π_comp_isoHomology_hom, mapHomologyIso_inv_naturality_assoc, RightHomologyData.rightHomologyIso_hom_comp_homologyIso_inv, comp_homologyMap_comp, LeftHomologyData.leftHomologyIso_hom_comp_homologyIso_inv_assoc, HomologicalComplex.homologyIsoSc'_hom_ι, HomologyData.ofEpiMonoFactorisation.π_comp_isoHomology_hom_assoc, moduleCatCyclesIso_inv_π, leftRightHomologyComparison_fac_assoc, instMonoHomologyι, homologyπ_comp_asIsoHomologyπ_inv, epi_homologyMap_of_epi_cyclesMap', HomologyData.ofEpiMonoFactorisation.isoHomology_hom_comp_ι, homologyι_comp_asIsoHomologyι_inv_assoc, π_descHomology_assoc, mono_homologyMap_of_mono_opcyclesMap, leftRightHomologyComparison'_fac_assoc, homologyIsoImageICyclesCompPOpcycles_ι_assoc, RightHomologyData.mapHomologyIso'_eq, asIsoHomologyι_inv_comp_homologyι_assoc, RightHomologyData.homologyIso_rightHomologyData, instEpiHomologyπ, mapHomologyIso'_inv_naturality_assoc, π_homologyMap_ι, mapHomologyIso'_inv_naturality, asIsoHomologyι_inv_comp_homologyι
homologyData 📖	CompOp	—
homologyFunctor 📖	CompOp	7 math math: isIso_homologyFunctor_map_of_epi_of_isIso_of_mono, homologyFunctor_obj, homologyFunctor_linear, homologyFunctor_map, HomologicalComplex.homologyFunctorIso_hom_app, HomologicalComplex.homologyFunctorIso_inv_app, homologyFunctor_additive
homologyFunctorOpNatIso 📖	CompOp	—
homologyIsCokernel 📖	CompOp	—
homologyIsKernel 📖	CompOp	—
homologyIsoCokernelLift 📖	CompOp	—
homologyIsoKernelDesc 📖	CompOp	—
homologyMap 📖	CompOp	70 math math: homologyι_naturality, homologyMap_smul, homologyOpIso_hom_naturality, homologyMap_add, homologyMap_zero, isIso_homologyMap_of_isIso_cyclesMap_of_epi, RightHomologyMapData.homologyMap_eq, RightHomologyData.rightHomologyIso_inv_naturality_assoc, mapHomologyIso_hom_naturality, homologyMapIso_inv, homologyπ_naturality_assoc, homologyOpIso_inv_naturality, RightHomologyData.rightHomologyIso_hom_naturality, homologyMapIso_hom, RightHomologyMapData.homologyMap_comm, RightHomologyData.rightHomologyIso_inv_naturality, homologyι_naturality_assoc, mapHomologyIso_hom_naturality_assoc, LeftHomologyMapData.homologyMap_comm, CategoryTheory.NatTrans.app_homology, QuasiIso.isIso, leftHomologyIso_hom_naturality, leftHomologyIso_hom_naturality_assoc, leftHomologyIso_inv_naturality_assoc, QuasiIso.isIso', mapHomologyIso'_hom_naturality, homologyπ_naturality, LeftHomologyMapData.homologyMap_eq, homologyOpIso_hom_naturality_assoc, homologyMap_mapNatTrans, rightHomologyIso_inv_naturality_assoc, homologyMap_neg, LeftHomologyData.leftHomologyIso_hom_naturality_assoc, LeftHomologyData.leftHomologyIso_hom_naturality, comp_homologyMap_comp_assoc, mono_homologyMap_of_mono_opcyclesMap', LeftHomologyData.leftHomologyIso_inv_naturality_assoc, homologyMap_comp, homologyOpIso_inv_naturality_assoc, homologyMap_sub, isIso_homologyMap_of_isIso, rightHomologyIso_hom_naturality_assoc, quasiIso_iff, π_homologyMap_ι_assoc, isIso_homologyMap_of_isIso_opcyclesMap_of_mono, RightHomologyData.rightHomologyIso_hom_naturality_assoc, homologyMap_op, isIso_homologyMap_of_iso, rightHomologyIso_inv_naturality, homologyFunctor_map, homologyMap_nullHomotopic, leftHomologyIso_inv_naturality, homologyMap_id, mapHomologyIso_inv_naturality, mapHomologyIso'_hom_naturality_assoc, Homotopy.homologyMap_congr, isIso_homologyMap_of_epi_of_isIso_of_mono', isIso_homologyMap_of_epi_of_isIso_of_mono, epi_homologyMap_of_epi_cyclesMap, LeftHomologyData.leftHomologyIso_inv_naturality, rightHomologyIso_hom_naturality, mapHomologyIso_inv_naturality_assoc, comp_homologyMap_comp, CochainComplex.ShiftSequence.shiftIso_inv_app, epi_homologyMap_of_epi_cyclesMap', mono_homologyMap_of_mono_opcyclesMap, mapHomologyIso'_inv_naturality_assoc, CochainComplex.ShiftSequence.shiftIso_hom_app, π_homologyMap_ι, mapHomologyIso'_inv_naturality
homologyMap' 📖	CompOp	17 math math: homologyMap'_zero, homologyMap'_comp, homologyMap'_nullHomotopic, homologyMap'_sub, HomologyData.map_homologyMap', homologyMap'_add, homologyMap'_op, quasiIso_iff_isIso_homologyMap', homologyMap'_neg, Homotopy.homologyMap'_congr, homologyMap'_id, homologyMapIso'_hom, isIso_homologyMap'_of_epi_of_isIso_of_mono, homologyMap'_smul, HomologyMapData.homologyMap'_eq, isIso_homologyMap'_of_isIso, homologyMapIso'_inv
homologyMapIso 📖	CompOp	2 math math: homologyMapIso_inv, homologyMapIso_hom
homologyMapIso' 📖	CompOp	2 math math: homologyMapIso'_hom, homologyMapIso'_inv
homologyOpIso 📖	CompOp	5 math math: homologyOpIso_hom_naturality, homologyOpIso_inv_naturality, homologyOpIso_hom_naturality_assoc, homologyOpIso_inv_naturality_assoc, homologyMap_op
homologyι 📖	CompOp	37 math math: homologyι_naturality, homology_π_ι_assoc, RightHomologyData.homologyIso_inv_comp_homologyι, HomologyData.ofEpiMonoFactorisation.isoHomology_inv_homologyι_assoc, RightHomologyData.homologyIso_hom_comp_ι, homology_π_ι, homologyι_naturality_assoc, RightHomologyData.canonical_ι, homologyι_comp_fromOpcycles_assoc, HomologicalComplex.homologyIsoSc'_hom_ι_assoc, HomologyData.ofEpiMonoFactorisation.isoHomology_inv_homologyι, homologyι_descOpcycles_eq_zero_of_boundary, rightHomologyIso_hom_comp_homologyι, liftHomology_ι, isIso_homologyι, RightHomologyData.homologyIso_hom_comp_ι_assoc, liftHomology_ι_assoc, RightHomologyData.homologyIso_inv_comp_homologyι_assoc, homologyι_comp_asIsoHomologyι_inv, HomologyData.canonical_right_ι, homologyIsoImageICyclesCompPOpcycles_ι, π_homologyMap_ι_assoc, HomologicalComplex.homologyIsoSc'_inv_ι, homologyι_comp_fromOpcycles, HomologyData.ofEpiMonoFactorisation.isoHomology_hom_comp_ι_assoc, homologyι_descOpcycles_eq_zero_of_boundary_assoc, rightHomologyIso_hom_comp_homologyι_assoc, asIsoHomologyι_hom, HomologicalComplex.homologyIsoSc'_inv_ι_assoc, HomologicalComplex.homologyIsoSc'_hom_ι, instMonoHomologyι, HomologyData.ofEpiMonoFactorisation.isoHomology_hom_comp_ι, homologyι_comp_asIsoHomologyι_inv_assoc, homologyIsoImageICyclesCompPOpcycles_ι_assoc, asIsoHomologyι_inv_comp_homologyι_assoc, π_homologyMap_ι, asIsoHomologyι_inv_comp_homologyι
homologyπ 📖	CompOp	43 math math: toCycles_comp_homologyπ, toCycles_comp_homologyπ_assoc, π_moduleCatCyclesIso_hom, HomologicalComplex.π_homologyIsoSc'_hom, homology_π_ι_assoc, HomologyData.canonical_left_π, LeftHomologyData.π_comp_homologyIso_inv, isIso_homologyπ, homologyπ_naturality_assoc, HomologyData.ofEpiMonoFactorisation.homologyπ_isoHomology_inv_assoc, homology_π_ι, moduleCatCyclesIso_inv_π_assoc_apply, asIsoHomologyπ_hom, homologyπ_comp_leftHomologyIso_inv, homologyπ_naturality, HomologicalComplex.π_homologyIsoSc'_hom_assoc, LeftHomologyData.homologyπ_comp_homologyIso_hom_assoc, HomologicalComplex.π_homologyIsoSc'_inv_assoc, π_descHomology, π_moduleCatCyclesIso_hom_assoc_apply, asIsoHomologyπ_inv_comp_homologyπ, LeftHomologyData.π_comp_homologyIso_inv_assoc, LeftHomologyData.canonical_π, homologyπ_comp_leftHomologyIso_inv_assoc, asIsoHomologyπ_inv_comp_homologyπ_assoc, π_moduleCatCyclesIso_hom_apply, eq_liftCycles_homologyπ_up_to_refinements, π_homologyMap_ι_assoc, moduleCatCyclesIso_inv_π_assoc, HomologicalComplex.π_homologyIsoSc'_inv, π_moduleCatCyclesIso_hom_assoc, homologyπ_comp_asIsoHomologyπ_inv_assoc, HomologyData.ofEpiMonoFactorisation.homologyπ_isoHomology_inv, moduleCatCyclesIso_inv_π_apply, LeftHomologyData.homologyπ_comp_homologyIso_hom, liftCycles_homologyπ_eq_zero_of_boundary, HomologyData.ofEpiMonoFactorisation.π_comp_isoHomology_hom, HomologyData.ofEpiMonoFactorisation.π_comp_isoHomology_hom_assoc, moduleCatCyclesIso_inv_π, homologyπ_comp_asIsoHomologyπ_inv, π_descHomology_assoc, instEpiHomologyπ, π_homologyMap_ι
leftHomologyIso 📖	CompOp	13 math math: LeftHomologyData.leftHomologyIso_hom_comp_homologyIso_inv, leftRightHomologyComparison_fac, leftHomologyIso_hom_naturality, leftHomologyIso_hom_naturality_assoc, homologyπ_comp_leftHomologyIso_inv, leftHomologyIso_inv_naturality_assoc, LeftHomologyData.homologyIso_hom_comp_leftHomologyIso_inv_assoc, homologyπ_comp_leftHomologyIso_inv_assoc, LeftHomologyData.homologyIso_leftHomologyData, LeftHomologyData.homologyIso_hom_comp_leftHomologyIso_inv, leftHomologyIso_inv_naturality, LeftHomologyData.leftHomologyIso_hom_comp_homologyIso_inv_assoc, leftRightHomologyComparison_fac_assoc
leftRightHomologyComparison 📖	CompOp	6 math math: isIso_leftRightHomologyComparison, leftRightHomologyComparison_fac, leftRightHomologyComparison_eq, π_leftRightHomologyComparison_ι_assoc, π_leftRightHomologyComparison_ι, leftRightHomologyComparison_fac_assoc
leftRightHomologyComparison' 📖	CompOp	16 math math: leftRightHomologyComparison'_fac, π_leftRightHomologyComparison'_ι, isIso_leftRightHomologyComparison', leftRightHomologyComparison'_eq_descH, isIso_leftRightHomologyComparison'_of_homologyData, leftRightHomologyComparison_eq, leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap', π_leftRightHomologyComparison'_ι_assoc, leftRightHomologyComparison'_eq_liftH, leftRightHomologyComparison'_naturality_assoc, map_leftRightHomologyComparison', leftRightHomologyComparison'_naturality, HomologyData.ofIsIsoLeftRightHomologyComparison'_iso, leftRightHomologyComparison'_compatibility, HomologyData.leftRightHomologyComparison'_eq, leftRightHomologyComparison'_fac_assoc
liftHomology 📖	CompOp	2 math math: liftHomology_ι, liftHomology_ι_assoc
rightHomologyIso 📖	CompOp	13 math math: RightHomologyData.homologyIso_hom_comp_rightHomologyIso_inv, leftRightHomologyComparison_fac, RightHomologyData.homologyIso_hom_comp_rightHomologyIso_inv_assoc, rightHomologyIso_inv_naturality_assoc, rightHomologyIso_hom_comp_homologyι, RightHomologyData.rightHomologyIso_hom_comp_homologyIso_inv_assoc, rightHomologyIso_hom_naturality_assoc, rightHomologyIso_hom_comp_homologyι_assoc, rightHomologyIso_inv_naturality, rightHomologyIso_hom_naturality, RightHomologyData.rightHomologyIso_hom_comp_homologyIso_inv, leftRightHomologyComparison_fac_assoc, RightHomologyData.homologyIso_rightHomologyData

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
asIsoHomologyι_hom 📖	mathematical	g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Iso.hom homology opcycles hasRightHomology_of_hasHomology asIsoHomologyι homologyι	—	hasRightHomology_of_hasHomology
asIsoHomologyι_inv_comp_homologyι 📖	mathematical	g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp opcycles hasRightHomology_of_hasHomology homology CategoryTheory.Iso.inv asIsoHomologyι homologyι CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.inv_hom_id hasRightHomology_of_hasHomology
asIsoHomologyι_inv_comp_homologyι_assoc 📖	mathematical	g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp opcycles hasRightHomology_of_hasHomology homology CategoryTheory.Iso.inv asIsoHomologyι homologyι	—	hasRightHomology_of_hasHomology CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' asIsoHomologyι_inv_comp_homologyι
asIsoHomologyπ_hom 📖	mathematical	f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Iso.hom cycles hasLeftHomology_of_hasHomology homology asIsoHomologyπ homologyπ	—	hasLeftHomology_of_hasHomology
asIsoHomologyπ_inv_comp_homologyπ 📖	mathematical	f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp homology cycles hasLeftHomology_of_hasHomology CategoryTheory.Iso.inv asIsoHomologyπ homologyπ CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.inv_hom_id hasLeftHomology_of_hasHomology
asIsoHomologyπ_inv_comp_homologyπ_assoc 📖	mathematical	f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp homology cycles hasLeftHomology_of_hasHomology CategoryTheory.Iso.inv asIsoHomologyπ homologyπ	—	hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' asIsoHomologyπ_inv_comp_homologyπ
comp_homologyMap_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct LeftHomologyData.K LeftHomologyData.H RightHomologyData.Q LeftHomologyData.π homology CategoryTheory.Iso.inv LeftHomologyData.homologyIso homologyMap RightHomologyData.H CategoryTheory.Iso.hom RightHomologyData.homologyIso RightHomologyData.ι X₂ LeftHomologyData.i Hom.τ₂ RightHomologyData.p	—	hasLeftHomology_of_hasHomology hasRightHomology_of_hasHomology CategoryTheory.Category.assoc rightHomologyι_naturality' rightHomologyι_naturality'_assoc leftHomologyπ_naturality'_assoc HomologyData.comm_assoc p_opcyclesMap'_assoc p_opcyclesMap' CategoryTheory.Category.id_comp cyclesMap'_i_assoc
comp_homologyMap_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct LeftHomologyData.K LeftHomologyData.H LeftHomologyData.π homology CategoryTheory.Iso.inv LeftHomologyData.homologyIso homologyMap RightHomologyData.H CategoryTheory.Iso.hom RightHomologyData.homologyIso RightHomologyData.Q RightHomologyData.ι X₂ LeftHomologyData.i Hom.τ₂ RightHomologyData.p	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_homologyMap_comp
epi_homologyMap_of_epi_cyclesMap 📖	mathematical	—	CategoryTheory.Epi homology homologyMap	—	hasLeftHomology_of_hasHomology epi_homologyMap_of_epi_cyclesMap'
epi_homologyMap_of_epi_cyclesMap' 📖	mathematical	—	CategoryTheory.Epi homology homologyMap	—	hasLeftHomology_of_hasHomology homologyπ_naturality CategoryTheory.epi_comp instEpiHomologyπ CategoryTheory.epi_of_epi
hasHomology_of_epi_of_isIso_of_mono 📖	mathematical	—	HasHomology	—	HasHomology.mk'
hasHomology_of_epi_of_isIso_of_mono' 📖	mathematical	—	HasHomology	—	HasHomology.mk'
hasHomology_of_hasCokernel 📖	mathematical	—	HasHomology Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.comp_zero	—	HasHomology.mk' CategoryTheory.Limits.comp_zero
hasHomology_of_hasKernel 📖	mathematical	—	HasHomology Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.zero_comp	—	HasHomology.mk' CategoryTheory.Limits.zero_comp
hasHomology_of_isIsoLeftRightHomologyComparison 📖	mathematical	—	HasHomology	—	hasHomology_of_isIso_leftRightHomologyComparison'
hasHomology_of_isIso_leftRightHomologyComparison' 📖	mathematical	—	HasHomology	—	HasHomology.mk'
hasHomology_of_iso 📖	mathematical	—	HasHomology	—	HasHomology.mk'
hasHomology_of_zeros 📖	mathematical	—	HasHomology Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.zero_comp	—	HasHomology.mk' CategoryTheory.Limits.zero_comp
hasLeftHomology_of_hasHomology 📖	mathematical	—	HasLeftHomology	—	HasLeftHomology.mk'
hasRightHomology_of_hasHomology 📖	mathematical	—	HasRightHomology	—	HasRightHomology.mk'
homologyFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.ShortComplex instCategory homologyFunctor homologyMap CategoryTheory.CategoryWithHomology.hasHomology	—	CategoryTheory.CategoryWithHomology.hasHomology
homologyFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.ShortComplex instCategory homologyFunctor homology CategoryTheory.CategoryWithHomology.hasHomology	—	—
homologyMap'_comp 📖	mathematical	—	homologyMap' CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory LeftHomologyData.H HomologyData.left	—	leftHomologyMap'_comp
homologyMap'_id 📖	mathematical	—	homologyMap' CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory LeftHomologyData.H HomologyData.left	—	HomologyMapData.homologyMap'_eq
homologyMap'_op 📖	mathematical	—	Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct LeftHomologyData.H HomologyData.left homologyMap' CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite Opposite.op RightHomologyData.H HomologyData.right CategoryTheory.Iso.inv HomologyData.iso CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite op HomologyData.op opMap CategoryTheory.Iso.hom	—	HomologyMapData.homologyMap'_eq CategoryTheory.Category.assoc HomologyMapData.comm_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
homologyMap'_zero 📖	mathematical	—	homologyMap' Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instZeroHom LeftHomologyData.H HomologyData.left CategoryTheory.Limits.HasZeroMorphisms.zero	—	HomologyMapData.homologyMap'_eq
homologyMapIso'_hom 📖	mathematical	—	CategoryTheory.Iso.hom LeftHomologyData.H HomologyData.left homologyMapIso' homologyMap' CategoryTheory.ShortComplex instCategory	—	—
homologyMapIso'_inv 📖	mathematical	—	CategoryTheory.Iso.inv LeftHomologyData.H HomologyData.left homologyMapIso' homologyMap' CategoryTheory.ShortComplex instCategory	—	—
homologyMapIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom homology homologyMapIso homologyMap CategoryTheory.ShortComplex instCategory	—	—
homologyMapIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv homology homologyMapIso homologyMap CategoryTheory.ShortComplex instCategory	—	—
homologyMap_comp 📖	mathematical	—	homologyMap CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory homology	—	homologyMap'_comp
homologyMap_id 📖	mathematical	—	homologyMap CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory homology	—	homologyMap'_id
homologyMap_op 📖	mathematical	—	Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct homology homologyMap CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite Opposite.op CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasHomologyOppositeOp CategoryTheory.Iso.inv homologyOpIso opMap CategoryTheory.Iso.hom	—	instHasHomologyOppositeOp hasRightHomology_of_hasHomology homologyMap'_op instHasLeftHomologyOppositeOpOfHasRightHomology hasLeftHomology_of_hasHomology rightHomologyMap'_op CategoryTheory.Category.assoc CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
homologyMap_zero 📖	mathematical	—	homologyMap Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instZeroHom homology CategoryTheory.Limits.HasZeroMorphisms.zero	—	homologyMap'_zero
homologyOpIso_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct homology CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasHomologyOppositeOp Opposite.op homologyMap opMap CategoryTheory.Iso.hom homologyOpIso Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	instHasHomologyOppositeOp homologyMap_op CategoryTheory.Iso.hom_inv_id_assoc
homologyOpIso_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite homology CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasHomologyOppositeOp homologyMap opMap Opposite.op CategoryTheory.Iso.hom homologyOpIso Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver	—	instHasHomologyOppositeOp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyOpIso_hom_naturality
homologyOpIso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op homology CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasHomologyOppositeOp Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver homologyMap CategoryTheory.Iso.inv homologyOpIso opMap	—	instHasHomologyOppositeOp homologyMap_op CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
homologyOpIso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite Opposite.op homology Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver homologyMap CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasHomologyOppositeOp CategoryTheory.Iso.inv homologyOpIso opMap	—	instHasHomologyOppositeOp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyOpIso_inv_naturality
homology_π_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles hasLeftHomology_of_hasHomology homology opcycles hasRightHomology_of_hasHomology homologyπ homologyι X₂ iCycles pOpcycles	—	hasLeftHomology_of_hasHomology hasRightHomology_of_hasHomology CategoryTheory.Category.assoc leftRightHomologyComparison_fac π_leftRightHomologyComparison_ι
homology_π_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles hasLeftHomology_of_hasHomology homology homologyπ opcycles hasRightHomology_of_hasHomology homologyι X₂ iCycles pOpcycles	—	hasRightHomology_of_hasHomology hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homology_π_ι
homologyι_comp_asIsoHomologyι_inv 📖	mathematical	g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp homology opcycles hasRightHomology_of_hasHomology homologyι CategoryTheory.Iso.inv asIsoHomologyι CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.hom_inv_id hasRightHomology_of_hasHomology
homologyι_comp_asIsoHomologyι_inv_assoc 📖	mathematical	g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp homology opcycles hasRightHomology_of_hasHomology homologyι CategoryTheory.Iso.inv asIsoHomologyι	—	hasRightHomology_of_hasHomology CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' homologyι_comp_asIsoHomologyι_inv
homologyι_comp_fromOpcycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology opcycles hasRightHomology_of_hasHomology X₃ homologyι fromOpcycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	hasRightHomology_of_hasHomology CategoryTheory.Category.assoc rightHomologyι_comp_fromOpcycles CategoryTheory.Limits.comp_zero
homologyι_comp_fromOpcycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology opcycles hasRightHomology_of_hasHomology homologyι X₃ fromOpcycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	hasRightHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyι_comp_fromOpcycles
homologyι_descOpcycles_eq_zero_of_boundary 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ X₃ g	homology opcycles hasRightHomology_of_hasHomology homologyι descOpcycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	hasRightHomology_of_hasHomology CategoryTheory.Category.assoc rightHomologyι_descOpcycles_π_eq_zero_of_boundary CategoryTheory.Limits.comp_zero
homologyι_descOpcycles_eq_zero_of_boundary_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ X₃ g	homology opcycles hasRightHomology_of_hasHomology homologyι descOpcycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	hasRightHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyι_descOpcycles_eq_zero_of_boundary
homologyι_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology opcycles hasRightHomology_of_hasHomology homologyMap homologyι opcyclesMap	—	hasRightHomology_of_hasHomology CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_hom rightHomologyIso_hom_naturality_assoc rightHomologyIso_hom_comp_homologyι rightHomologyι_naturality CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_assoc
homologyι_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology homologyMap opcycles hasRightHomology_of_hasHomology homologyι opcyclesMap	—	hasRightHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyι_naturality
homologyπ_comp_asIsoHomologyπ_inv 📖	mathematical	f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp cycles hasLeftHomology_of_hasHomology homology homologyπ CategoryTheory.Iso.inv asIsoHomologyπ CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.hom_inv_id hasLeftHomology_of_hasHomology
homologyπ_comp_asIsoHomologyπ_inv_assoc 📖	mathematical	f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp cycles hasLeftHomology_of_hasHomology homology homologyπ CategoryTheory.Iso.inv asIsoHomologyπ	—	hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' homologyπ_comp_asIsoHomologyπ_inv
homologyπ_comp_leftHomologyIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles hasLeftHomology_of_hasHomology homology leftHomology homologyπ CategoryTheory.Iso.inv leftHomologyIso leftHomologyπ	—	hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
homologyπ_comp_leftHomologyIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles hasLeftHomology_of_hasHomology homology homologyπ leftHomology CategoryTheory.Iso.inv leftHomologyIso leftHomologyπ	—	hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyπ_comp_leftHomologyIso_inv
homologyπ_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles hasLeftHomology_of_hasHomology homology homologyπ homologyMap cyclesMap	—	hasLeftHomology_of_hasHomology CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc leftHomologyIso_inv_naturality homologyπ_comp_leftHomologyIso_inv CategoryTheory.Iso.hom_inv_id_assoc leftHomologyπ_naturality
homologyπ_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles hasLeftHomology_of_hasHomology homology homologyπ homologyMap cyclesMap	—	hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyπ_naturality
instCategoryWithHomologyOpposite 📖	mathematical	—	CategoryTheory.CategoryWithHomology Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite	—	HasHomology.mk' CategoryTheory.CategoryWithHomology.hasHomology
instEpiHomologyπ 📖	mathematical	—	CategoryTheory.Epi cycles hasLeftHomology_of_hasHomology homology homologyπ	—	CategoryTheory.Limits.epi_of_isColimit_cofork hasLeftHomology_of_hasHomology toCycles_comp_homologyπ
instHasHomologyOppositeOp 📖	mathematical	—	HasHomology Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite op	—	HasHomology.mk'
instHasHomologyUnopOfOpposite 📖	mathematical	—	HasHomology unop	—	HasHomology.mk'
instMonoHomologyι 📖	mathematical	—	CategoryTheory.Mono homology opcycles hasRightHomology_of_hasHomology homologyι	—	CategoryTheory.Limits.mono_of_isLimit_fork hasRightHomology_of_hasHomology homologyι_comp_fromOpcycles
isIso_homologyFunctor_map_of_epi_of_isIso_of_mono 📖	mathematical	—	CategoryTheory.IsIso CategoryTheory.Functor.obj CategoryTheory.ShortComplex instCategory homologyFunctor CategoryTheory.Functor.map	—	CategoryTheory.CategoryWithHomology.hasHomology isIso_homologyMap_of_epi_of_isIso_of_mono
isIso_homologyMap'_of_epi_of_isIso_of_mono 📖	mathematical	—	CategoryTheory.IsIso LeftHomologyData.H HomologyData.left homologyMap'	—	instIsIsoLeftHomologyMap'OfEpiτ₁Ofτ₂OfMonoτ₃
isIso_homologyMap'_of_isIso 📖	mathematical	—	CategoryTheory.IsIso LeftHomologyData.H HomologyData.left homologyMap'	—	CategoryTheory.Iso.isIso_hom
isIso_homologyMap_of_epi_of_isIso_of_mono 📖	mathematical	—	CategoryTheory.IsIso homology homologyMap	—	isIso_homologyMap_of_epi_of_isIso_of_mono'
isIso_homologyMap_of_epi_of_isIso_of_mono' 📖	mathematical	—	CategoryTheory.IsIso homology homologyMap	—	isIso_homologyMap'_of_epi_of_isIso_of_mono
isIso_homologyMap_of_isIso 📖	mathematical	—	CategoryTheory.IsIso homology homologyMap	—	instIsIsoLeftHomologyMap'OfEpiτ₁Ofτ₂OfMonoτ₃ CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso instIsIsoτ₁ instIsIsoτ₂ CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso instIsIsoτ₃
isIso_homologyMap_of_isIso_cyclesMap_of_epi 📖	mathematical	—	CategoryTheory.IsIso homology homologyMap	—	hasLeftHomology_of_hasHomology CategoryTheory.cancel_epi CategoryTheory.IsIso.hom_inv_id_assoc toCycles_comp_homologyπ CategoryTheory.Limits.comp_zero instEpiHomologyπ homologyπ_naturality_assoc CategoryTheory.Category.comp_id CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyπ_naturality CategoryTheory.IsIso.inv_hom_id_assoc
isIso_homologyMap_of_isIso_opcyclesMap_of_mono 📖	mathematical	—	CategoryTheory.IsIso homology homologyMap	—	hasRightHomology_of_hasHomology CategoryTheory.Category.assoc CategoryTheory.cancel_mono CategoryTheory.IsIso.inv_hom_id_assoc homologyι_comp_fromOpcycles CategoryTheory.Limits.zero_comp instMonoHomologyι CategoryTheory.Category.id_comp homologyι_naturality_assoc CategoryTheory.IsIso.hom_inv_id CategoryTheory.Category.comp_id homologyι_naturality Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.IsIso.inv_hom_id
isIso_homologyMap_of_iso 📖	mathematical	—	CategoryTheory.IsIso homology homologyMap	—	CategoryTheory.Iso.isIso_hom
isIso_homologyι 📖	mathematical	g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.IsIso homology opcycles hasRightHomology_of_hasHomology homologyι	—	hasRightHomology_of_hasHomology isIso_rightHomologyι CategoryTheory.IsIso.comp_isIso CategoryTheory.Iso.isIso_inv
isIso_homologyπ 📖	mathematical	f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.IsIso cycles hasLeftHomology_of_hasHomology homology homologyπ	—	hasLeftHomology_of_hasHomology isIso_leftHomologyπ CategoryTheory.IsIso.comp_isIso CategoryTheory.Iso.isIso_hom
isIso_leftRightHomologyComparison 📖	mathematical	—	CategoryTheory.IsIso leftHomology hasLeftHomology_of_hasHomology rightHomology hasRightHomology_of_hasHomology leftRightHomologyComparison	—	hasLeftHomology_of_hasHomology hasRightHomology_of_hasHomology isIso_leftRightHomologyComparison'
isIso_leftRightHomologyComparison' 📖	mathematical	—	CategoryTheory.IsIso LeftHomologyData.H RightHomologyData.H leftRightHomologyComparison'	—	leftRightHomologyComparison'_compatibility CategoryTheory.IsIso.comp_isIso instIsIsoLeftHomologyMap'OfEpiτ₁Ofτ₂OfMonoτ₃ CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso instIsIsoτ₁ CategoryTheory.IsIso.id instIsIsoτ₂ CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso instIsIsoτ₃ isIso_leftRightHomologyComparison'_of_homologyData instIsIsoRightHomologyMap'OfEpiτ₁Ofτ₂OfMonoτ₃
isIso_leftRightHomologyComparison'_of_homologyData 📖	mathematical	—	CategoryTheory.IsIso LeftHomologyData.H HomologyData.left RightHomologyData.H HomologyData.right leftRightHomologyComparison'	—	HomologyData.leftRightHomologyComparison'_eq CategoryTheory.Iso.isIso_hom
isZero_homology_of_isZero_X₂ 📖	mathematical	CategoryTheory.Limits.IsZero X₂	homology	—	CategoryTheory.Limits.IsZero.of_iso CategoryTheory.Limits.IsZero.eq_of_tgt CategoryTheory.Limits.IsZero.eq_of_src
leftHomologyIso_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct leftHomology hasLeftHomology_of_hasHomology homology CategoryTheory.Iso.hom leftHomologyIso homologyMap leftHomologyMap	—	hasLeftHomology_of_hasHomology LeftHomologyData.homologyIso_leftHomologyData LeftHomologyData.leftHomologyIso_inv_naturality
leftHomologyIso_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct leftHomology hasLeftHomology_of_hasHomology homology CategoryTheory.Iso.hom leftHomologyIso homologyMap leftHomologyMap	—	hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftHomologyIso_hom_naturality
leftHomologyIso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology leftHomology hasLeftHomology_of_hasHomology CategoryTheory.Iso.inv leftHomologyIso leftHomologyMap homologyMap	—	hasLeftHomology_of_hasHomology LeftHomologyData.homologyIso_leftHomologyData LeftHomologyData.leftHomologyIso_hom_naturality
leftHomologyIso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology leftHomology hasLeftHomology_of_hasHomology CategoryTheory.Iso.inv leftHomologyIso leftHomologyMap homologyMap	—	hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftHomologyIso_inv_naturality
leftRightHomologyComparison'_compatibility 📖	mathematical	—	leftRightHomologyComparison' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct LeftHomologyData.H RightHomologyData.H leftHomologyMap' CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex instCategory rightHomologyMap'	—	leftRightHomologyComparison'_naturality_assoc rightHomologyMap'_comp CategoryTheory.Category.comp_id rightHomologyMap'_id
leftRightHomologyComparison'_eq_descH 📖	mathematical	—	leftRightHomologyComparison' LeftHomologyData.descH RightHomologyData.H RightHomologyData.liftH LeftHomologyData.K CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ RightHomologyData.Q LeftHomologyData.i RightHomologyData.p	—	CategoryTheory.cancel_mono RightHomologyData.instMonoι CategoryTheory.cancel_epi LeftHomologyData.instEpiπ π_leftRightHomologyComparison'_ι LeftHomologyData.π_descH_assoc RightHomologyData.liftH_ι
leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap' 📖	mathematical	—	leftRightHomologyComparison' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct LeftHomologyData.H HomologyData.left RightHomologyData.H leftHomologyMap' CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex instCategory HomologyData.right CategoryTheory.Iso.hom HomologyData.iso rightHomologyMap'	—	HomologyData.leftRightHomologyComparison'_eq leftRightHomologyComparison'_compatibility
leftRightHomologyComparison'_eq_liftH 📖	mathematical	—	leftRightHomologyComparison' RightHomologyData.liftH LeftHomologyData.H LeftHomologyData.descH RightHomologyData.Q CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct LeftHomologyData.K X₂ LeftHomologyData.i RightHomologyData.p	—	—
leftRightHomologyComparison'_fac 📖	mathematical	—	leftRightHomologyComparison' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct LeftHomologyData.H homology RightHomologyData.H CategoryTheory.Iso.inv LeftHomologyData.homologyIso CategoryTheory.Iso.hom RightHomologyData.homologyIso	—	leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap' hasLeftHomology_of_hasHomology hasRightHomology_of_hasHomology CategoryTheory.Category.assoc CategoryTheory.Category.id_comp
leftRightHomologyComparison'_fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct LeftHomologyData.H RightHomologyData.H leftRightHomologyComparison' homology CategoryTheory.Iso.inv LeftHomologyData.homologyIso CategoryTheory.Iso.hom RightHomologyData.homologyIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftRightHomologyComparison'_fac
leftRightHomologyComparison'_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct LeftHomologyData.H RightHomologyData.H leftHomologyMap' leftRightHomologyComparison' rightHomologyMap'	—	CategoryTheory.cancel_epi LeftHomologyData.instEpiπ leftHomologyπ_naturality'_assoc CategoryTheory.cancel_mono RightHomologyData.instMonoι CategoryTheory.Category.assoc π_leftRightHomologyComparison'_ι cyclesMap'_i_assoc rightHomologyι_naturality' π_leftRightHomologyComparison'_ι_assoc p_opcyclesMap'
leftRightHomologyComparison'_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct LeftHomologyData.H leftHomologyMap' RightHomologyData.H leftRightHomologyComparison' rightHomologyMap'	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftRightHomologyComparison'_naturality
leftRightHomologyComparison_eq 📖	mathematical	—	leftRightHomologyComparison CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct leftHomology LeftHomologyData.H rightHomology CategoryTheory.Iso.hom LeftHomologyData.leftHomologyIso RightHomologyData.H leftRightHomologyComparison' CategoryTheory.Iso.inv RightHomologyData.rightHomologyIso	—	leftRightHomologyComparison'_compatibility
leftRightHomologyComparison_fac 📖	mathematical	—	leftRightHomologyComparison hasLeftHomology_of_hasHomology hasRightHomology_of_hasHomology CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct leftHomology homology rightHomology CategoryTheory.Iso.hom leftHomologyIso CategoryTheory.Iso.inv rightHomologyIso	—	hasLeftHomology_of_hasHomology hasRightHomology_of_hasHomology LeftHomologyData.homologyIso_leftHomologyData RightHomologyData.homologyIso_rightHomologyData leftRightHomologyComparison'_fac
leftRightHomologyComparison_fac_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct leftHomology hasLeftHomology_of_hasHomology rightHomology hasRightHomology_of_hasHomology leftRightHomologyComparison homology CategoryTheory.Iso.hom leftHomologyIso CategoryTheory.Iso.inv rightHomologyIso	—	hasRightHomology_of_hasHomology hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftRightHomologyComparison_fac
liftCycles_homologyπ_eq_zero_of_boundary 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ X₂ f	cycles hasLeftHomology_of_hasHomology homology liftCycles homologyπ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	hasLeftHomology_of_hasHomology liftCycles_leftHomologyπ_eq_zero_of_boundary_assoc CategoryTheory.Limits.zero_comp
liftHomology_ι 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles hasRightHomology_of_hasHomology X₃ fromOpcycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	homology liftHomology homologyι	—	hasRightHomology_of_hasHomology CategoryTheory.Limits.Fork.IsLimit.lift_ι homologyι_comp_fromOpcycles
liftHomology_ι_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles hasRightHomology_of_hasHomology X₃ fromOpcycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	homology liftHomology homologyι	—	hasRightHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' liftHomology_ι
mono_homologyMap_of_mono_opcyclesMap 📖	mathematical	—	CategoryTheory.Mono homology homologyMap	—	hasRightHomology_of_hasHomology mono_homologyMap_of_mono_opcyclesMap'
mono_homologyMap_of_mono_opcyclesMap' 📖	mathematical	—	CategoryTheory.Mono homology homologyMap	—	hasRightHomology_of_hasHomology homologyι_naturality CategoryTheory.mono_comp instMonoHomologyι CategoryTheory.mono_of_mono
rightHomologyIso_hom_comp_homologyι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct rightHomology hasRightHomology_of_hasHomology homology opcycles CategoryTheory.Iso.hom rightHomologyIso homologyι rightHomologyι	—	hasRightHomology_of_hasHomology CategoryTheory.Iso.hom_inv_id_assoc
rightHomologyIso_hom_comp_homologyι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct rightHomology hasRightHomology_of_hasHomology homology CategoryTheory.Iso.hom rightHomologyIso opcycles homologyι rightHomologyι	—	hasRightHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightHomologyIso_hom_comp_homologyι
rightHomologyIso_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct rightHomology hasRightHomology_of_hasHomology homology CategoryTheory.Iso.hom rightHomologyIso homologyMap rightHomologyMap	—	hasRightHomology_of_hasHomology RightHomologyData.homologyIso_rightHomologyData RightHomologyData.rightHomologyIso_inv_naturality
rightHomologyIso_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct rightHomology hasRightHomology_of_hasHomology homology CategoryTheory.Iso.hom rightHomologyIso homologyMap rightHomologyMap	—	hasRightHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightHomologyIso_hom_naturality
rightHomologyIso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology rightHomology hasRightHomology_of_hasHomology CategoryTheory.Iso.inv rightHomologyIso rightHomologyMap homologyMap	—	hasRightHomology_of_hasHomology RightHomologyData.homologyIso_rightHomologyData RightHomologyData.rightHomologyIso_hom_naturality
rightHomologyIso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct homology rightHomology hasRightHomology_of_hasHomology CategoryTheory.Iso.inv rightHomologyIso rightHomologyMap homologyMap	—	hasRightHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightHomologyIso_inv_naturality
toCycles_comp_homologyπ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ cycles hasLeftHomology_of_hasHomology homology toCycles homologyπ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	hasLeftHomology_of_hasHomology toCycles_comp_leftHomologyπ_assoc CategoryTheory.Limits.zero_comp
toCycles_comp_homologyπ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ cycles hasLeftHomology_of_hasHomology toCycles homology homologyπ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toCycles_comp_homologyπ
π_descHomology 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ cycles hasLeftHomology_of_hasHomology toCycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	homology homologyπ descHomology	—	hasLeftHomology_of_hasHomology CategoryTheory.Limits.Cofork.IsColimit.π_desc toCycles_comp_homologyπ
π_descHomology_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ cycles hasLeftHomology_of_hasHomology toCycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	homology homologyπ descHomology	—	hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_descHomology
π_homologyMap_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles hasLeftHomology_of_hasHomology homology opcycles hasRightHomology_of_hasHomology homologyπ homologyMap homologyι X₂ iCycles Hom.τ₂ pOpcycles	—	hasLeftHomology_of_hasHomology hasRightHomology_of_hasHomology homologyι_naturality homology_π_ι_assoc p_opcyclesMap
π_homologyMap_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles hasLeftHomology_of_hasHomology homology homologyπ homologyMap opcycles hasRightHomology_of_hasHomology homologyι X₂ iCycles Hom.τ₂ pOpcycles	—	hasRightHomology_of_hasHomology hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_homologyMap_ι
π_leftRightHomologyComparison'_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct LeftHomologyData.K LeftHomologyData.H RightHomologyData.Q LeftHomologyData.π RightHomologyData.H leftRightHomologyComparison' RightHomologyData.ι X₂ LeftHomologyData.i RightHomologyData.p	—	RightHomologyData.liftH_ι LeftHomologyData.π_descH
π_leftRightHomologyComparison'_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct LeftHomologyData.K LeftHomologyData.H LeftHomologyData.π RightHomologyData.H leftRightHomologyComparison' RightHomologyData.Q RightHomologyData.ι X₂ LeftHomologyData.i RightHomologyData.p	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_leftRightHomologyComparison'_ι
π_leftRightHomologyComparison_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles leftHomology opcycles leftHomologyπ rightHomology leftRightHomologyComparison rightHomologyι X₂ iCycles pOpcycles	—	π_leftRightHomologyComparison'_ι
π_leftRightHomologyComparison_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles leftHomology leftHomologyπ rightHomology leftRightHomologyComparison opcycles rightHomologyι X₂ iCycles pOpcycles	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_leftRightHomologyComparison_ι

CategoryTheory.ShortComplex.HasHomology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	—	CategoryTheory.ShortComplex.HomologyData	—	—
mk' 📖	mathematical	—	CategoryTheory.ShortComplex.HasHomology	—	—

CategoryTheory.ShortComplex.HomologyData

Definitions

Name	Category	Theorems
canonical 📖	CompOp	10 math math: canonical_iso_hom, canonical_left_i, canonical_left_π, canonical_right_H, canonical_right_Q, canonical_left_K, canonical_left_H, canonical_right_p, canonical_right_ι, canonical_iso_inv
iso 📖	CompOp	27 math math: ofIsColimitCokernelCofork_iso, canonical_iso_hom, ofIso_iso, right_homologyIso_eq_left_homologyIso_trans_iso, CategoryTheory.ShortComplex.homologyMap'_op, comm_assoc, ofEpiOfIsIsoOfMono'_iso, ofHasCokernel_iso, HomologicalComplex.extend.homologyData'_iso, CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap', left_homologyIso_eq_right_homologyIso_trans_iso_symm, CategoryTheory.ShortComplex.HomologyMapData.comm, CategoryTheory.ShortComplex.HomologyMapData.comm_assoc, ofEpiMonoFactorisation_iso, ofIsLimitKernelFork_iso, canonical_iso_inv, ofZeros_iso, unop_iso, op_iso, ofEpiOfIsIsoOfMono_iso, map_iso, HomologicalComplex.extend.homologyData_iso, ofIsIsoLeftRightHomologyComparison'_iso, comm, leftRightHomologyComparison'_eq, ofHasKernel_iso, CategoryTheory.ShortComplex.Splitting.homologyData_iso
left 📖	CompOp	73 math math: ofEpiMonoFactorisation_left, exact_iff, ofZeros_left, canonical_left_i, HomologicalComplex.extend.homologyData_left, canonical_left_π, HomologicalComplex.extend.homologyData'_left_H, ofIsIsoLeftRightHomologyComparison'_left, CategoryTheory.ShortComplex.homologyMap'_zero, ofIsLimitKernelFork_left, CategoryTheory.ShortComplex.homologyMap'_comp, CategoryTheory.ShortComplex.HomologyMapData.add_left, CategoryTheory.ShortComplex.HomologyMapData.unop_right, CategoryTheory.ShortComplex.HomologyMapData.map_left, right_homologyIso_eq_left_homologyIso_trans_iso, CategoryTheory.ShortComplex.HomologyMapData.natTransApp_left, CategoryTheory.ShortComplex.HomologyMapData.neg_left, CategoryTheory.ShortComplex.homologyMap'_nullHomotopic, CategoryTheory.ShortComplex.homologyMap'_sub, CategoryTheory.ShortComplex.HomologyMapData.comp_left, op_right, map_homologyMap', CategoryTheory.ShortComplex.homologyMap'_add, CategoryTheory.ShortComplex.Exact.condition, CategoryTheory.ShortComplex.HomologyMapData.congr_left_φH, CategoryTheory.ShortComplex.homologyMap'_op, ofIso_left_i, canonical_left_K, CategoryTheory.ShortComplex.quasiIso_iff_isIso_homologyMap', canonical_left_H, CategoryTheory.ShortComplex.homologyMap'_neg, comm_assoc, CategoryTheory.ShortComplex.HomologyMapData.zero_left, CategoryTheory.ShortComplex.isIso_leftRightHomologyComparison'_of_homologyData, unop_left, CategoryTheory.ShortComplex.HomologyMapData.op_right, ofEpiOfIsIsoOfMono'_left, CategoryTheory.ShortComplex.homologyMap'_id, CategoryTheory.ShortComplex.Exact.shortExact, map_left, ofHasKernel_left, CategoryTheory.ShortComplex.HomologyMapData.cyclesMap'_eq, CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap', left_homologyIso_eq_right_homologyIso_trans_iso_symm, HomologicalComplex.extend.homologyData'_left_i, CategoryTheory.ShortComplex.homologyMapIso'_hom, op_left, CategoryTheory.ShortComplex.isIso_homologyMap'_of_epi_of_isIso_of_mono, ofHasCokernel_left, exact_iff_i_p_zero, CategoryTheory.ShortComplex.HomologyMapData.comm, CategoryTheory.ShortComplex.HomologyMapData.comm_assoc, CategoryTheory.ShortComplex.homologyMap'_smul, ofIso_left_π, CategoryTheory.ShortComplex.HomologyMapData.homologyMap'_eq, ofIsColimitCokernelCofork_left, unop_iso, op_iso, HomologicalComplex.extend.homologyData'_left_π, map_iso, HomologicalComplex.extend.homologyData'_left_K, ofIso_left_H, CategoryTheory.ShortComplex.isIso_homologyMap'_of_isIso, CategoryTheory.ShortComplex.Splitting.homologyData_left, unop_right, ofIso_left_K, comm, CategoryTheory.ShortComplex.homologyMapIso'_inv, CategoryTheory.ShortComplex.HomologyMapData.smul_left, CategoryTheory.ShortComplex.HomologyMapData.natTransApp_right, leftRightHomologyComparison'_eq, ofEpiOfIsIsoOfMono_left, CategoryTheory.ShortComplex.HomologyMapData.id_left
ofEpiOfIsIsoOfMono 📖	CompOp	3 math math: ofEpiOfIsIsoOfMono_right, ofEpiOfIsIsoOfMono_iso, ofEpiOfIsIsoOfMono_left
ofEpiOfIsIsoOfMono' 📖	CompOp	3 math math: ofEpiOfIsIsoOfMono'_right, ofEpiOfIsIsoOfMono'_iso, ofEpiOfIsIsoOfMono'_left
ofHasCokernel 📖	CompOp	3 math math: ofHasCokernel_right, ofHasCokernel_iso, ofHasCokernel_left
ofHasKernel 📖	CompOp	3 math math: ofHasKernel_left, ofHasKernel_right, ofHasKernel_iso
ofIsColimitCokernelCofork 📖	CompOp	5 math math: ofIsColimitCokernelCofork_iso, CategoryTheory.ShortComplex.HomologyMapData.ofIsColimitCokernelCofork_right, ofIsColimitCokernelCofork_right, ofIsColimitCokernelCofork_left, CategoryTheory.ShortComplex.HomologyMapData.ofIsColimitCokernelCofork_left
ofIsIsoLeftRightHomologyComparison' 📖	CompOp	3 math math: ofIsIsoLeftRightHomologyComparison'_left, ofIsIsoLeftRightHomologyComparison'_right, ofIsIsoLeftRightHomologyComparison'_iso
ofIsLimitKernelFork 📖	CompOp	7 math math: CategoryTheory.ShortComplex.HomologyMapData.ofIsLimitKernelFork_left, ofIsLimitKernelFork_left, CategoryTheory.ShortComplex.HomologyMapData.ofIsLimitKernelFork_right, CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_left, ofIsLimitKernelFork_right, ofIsLimitKernelFork_iso, CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_right
ofIso 📖	CompOp	9 math math: ofIso_right_p, ofIso_right_H, ofIso_iso, ofIso_right_Q, ofIso_left_i, ofIso_right_ι, ofIso_left_π, ofIso_left_H, ofIso_left_K
ofZeros 📖	CompOp	7 math math: ofZeros_left, CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_left, ofZeros_iso, ofZeros_right, CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_right, CategoryTheory.ShortComplex.HomologyMapData.ofZeros_right, CategoryTheory.ShortComplex.HomologyMapData.ofZeros_left
op 📖	CompOp	6 math math: CategoryTheory.ShortComplex.HomologyMapData.op_left, op_right, CategoryTheory.ShortComplex.homologyMap'_op, CategoryTheory.ShortComplex.HomologyMapData.op_right, op_left, op_iso
right 📖	CompOp	59 math math: CategoryTheory.ShortComplex.HomologyMapData.op_left, ofIso_right_p, HomologicalComplex.truncGE.rightHomologyMapData_φQ, ofIso_right_H, CategoryTheory.ShortComplex.Splitting.homologyData_right, right_homologyIso_eq_left_homologyIso_trans_iso, CategoryTheory.ShortComplex.HomologyMapData.natTransApp_left, op_right, CategoryTheory.ShortComplex.HomologyMapData.opcyclesMap'_eq, ofIso_right_Q, canonical_right_H, CategoryTheory.ShortComplex.HomologyMapData.comp_right, ofHasCokernel_right, canonical_right_Q, CategoryTheory.ShortComplex.homologyMap'_op, ofEpiOfIsIsoOfMono'_right, comm_assoc, CategoryTheory.ShortComplex.isIso_leftRightHomologyComparison'_of_homologyData, unop_left, ofIsColimitCokernelCofork_right, CategoryTheory.ShortComplex.Exact.shortExact, HomologicalComplex.truncGE'.homologyData_right_g', canonical_right_p, CategoryTheory.ShortComplex.HomologyMapData.map_right, CategoryTheory.ShortComplex.HomologyMapData.zero_right, CategoryTheory.ShortComplex.HomologyMapData.id_right, HomologicalComplex.extend.homologyData'_right_H, ofIso_right_ι, ofEpiOfIsIsoOfMono_right, ofEpiMonoFactorisation_right, CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap', left_homologyIso_eq_right_homologyIso_trans_iso_symm, HomologicalComplex.extend.homologyData'_right_p, canonical_right_ι, ofIsIsoLeftRightHomologyComparison'_right, CategoryTheory.ShortComplex.HomologyMapData.add_right, op_left, ofHasKernel_right, exact_iff_i_p_zero, ofIsLimitKernelFork_right, CategoryTheory.ShortComplex.HomologyMapData.comm, CategoryTheory.ShortComplex.HomologyMapData.comm_assoc, HomologicalComplex.truncGE.rightHomologyMapData_φH, HomologicalComplex.extend.homologyData'_right_ι, map_right, CategoryTheory.ShortComplex.HomologyMapData.neg_right, CategoryTheory.ShortComplex.HomologyMapData.smul_right, ofZeros_right, HomologicalComplex.extend.homologyData'_right_Q, unop_iso, op_iso, map_iso, unop_right, comm, HomologicalComplex.extend.homologyData_right, exact_iff', CategoryTheory.ShortComplex.HomologyMapData.natTransApp_right, leftRightHomologyComparison'_eq, CategoryTheory.ShortComplex.HomologyMapData.unop_left
unop 📖	CompOp	5 math math: CategoryTheory.ShortComplex.HomologyMapData.unop_right, unop_left, unop_iso, unop_right, CategoryTheory.ShortComplex.HomologyMapData.unop_left

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
canonical_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.ShortComplex.LeftHomologyData.canonical iso canonical CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.homology	—	—
canonical_iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.ShortComplex.LeftHomologyData.canonical iso canonical CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.homology	—	—
canonical_left_H 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.H left canonical CategoryTheory.ShortComplex.homology	—	—
canonical_left_K 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.K left canonical CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology	—	—
canonical_left_i 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.i left canonical CategoryTheory.ShortComplex.iCycles CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology
canonical_left_π 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.π left canonical CategoryTheory.ShortComplex.homologyπ	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology
canonical_right_H 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.H right canonical CategoryTheory.ShortComplex.homology	—	—
canonical_right_Q 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.Q right canonical CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology	—	—
canonical_right_p 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.p right canonical CategoryTheory.ShortComplex.pOpcycles CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology	—	CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology
canonical_right_ι 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.ι right canonical CategoryTheory.ShortComplex.homologyι	—	CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology
comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.LeftHomologyData.K left CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.ShortComplex.RightHomologyData.Q right CategoryTheory.ShortComplex.LeftHomologyData.π CategoryTheory.ShortComplex.RightHomologyData.H CategoryTheory.Iso.hom iso CategoryTheory.ShortComplex.RightHomologyData.ι CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.RightHomologyData.p	—	—
comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.LeftHomologyData.K left CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.ShortComplex.LeftHomologyData.π CategoryTheory.ShortComplex.RightHomologyData.H right CategoryTheory.Iso.hom iso CategoryTheory.ShortComplex.RightHomologyData.Q CategoryTheory.ShortComplex.RightHomologyData.ι CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.RightHomologyData.p	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm
leftRightHomologyComparison'_eq 📖	mathematical	—	CategoryTheory.ShortComplex.leftRightHomologyComparison' left right CategoryTheory.Iso.hom CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.ShortComplex.RightHomologyData.H iso	—	CategoryTheory.cancel_epi CategoryTheory.ShortComplex.LeftHomologyData.instEpiπ CategoryTheory.cancel_mono CategoryTheory.ShortComplex.RightHomologyData.instMonoι CategoryTheory.Category.assoc CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι comm
left_homologyIso_eq_right_homologyIso_trans_iso_symm 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.homologyIso left CategoryTheory.Iso.trans CategoryTheory.ShortComplex.homology CategoryTheory.ShortComplex.RightHomologyData.H right CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.ShortComplex.RightHomologyData.homologyIso CategoryTheory.Iso.symm iso	—	right_homologyIso_eq_left_homologyIso_trans_iso CategoryTheory.Iso.trans_assoc CategoryTheory.Iso.self_symm_id CategoryTheory.Iso.trans_refl
ofEpiOfIsIsoOfMono'_iso 📖	mathematical	—	iso ofEpiOfIsIsoOfMono'	—	—
ofEpiOfIsIsoOfMono'_left 📖	mathematical	—	left ofEpiOfIsIsoOfMono' CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono'	—	—
ofEpiOfIsIsoOfMono'_right 📖	mathematical	—	right ofEpiOfIsIsoOfMono' CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono'	—	—
ofEpiOfIsIsoOfMono_iso 📖	mathematical	—	iso ofEpiOfIsIsoOfMono	—	—
ofEpiOfIsIsoOfMono_left 📖	mathematical	—	left ofEpiOfIsIsoOfMono CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono	—	—
ofEpiOfIsIsoOfMono_right 📖	mathematical	—	right ofEpiOfIsIsoOfMono CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono	—	—
ofHasCokernel_iso 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	iso ofHasCokernel CategoryTheory.Iso.refl CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel	—	—
ofHasCokernel_left 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	left ofHasCokernel CategoryTheory.ShortComplex.LeftHomologyData.ofHasCokernel	—	—
ofHasCokernel_right 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	right ofHasCokernel CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernel	—	—
ofHasKernel_iso 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	iso ofHasKernel CategoryTheory.Iso.refl CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernel	—	—
ofHasKernel_left 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	left ofHasKernel CategoryTheory.ShortComplex.LeftHomologyData.ofHasKernel	—	—
ofHasKernel_right 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	right ofHasKernel CategoryTheory.ShortComplex.RightHomologyData.ofHasKernel	—	—
ofIsColimitCokernelCofork_iso 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	iso ofIsColimitCokernelCofork CategoryTheory.Iso.refl CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork	—	—
ofIsColimitCokernelCofork_left 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	left ofIsColimitCokernelCofork CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork	—	—
ofIsColimitCokernelCofork_right 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	right ofIsColimitCokernelCofork CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork	—	—
ofIsIsoLeftRightHomologyComparison'_iso 📖	mathematical	—	iso ofIsIsoLeftRightHomologyComparison' CategoryTheory.asIso CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.ShortComplex.RightHomologyData.H CategoryTheory.ShortComplex.leftRightHomologyComparison'	—	—
ofIsIsoLeftRightHomologyComparison'_left 📖	mathematical	—	left ofIsIsoLeftRightHomologyComparison'	—	—
ofIsIsoLeftRightHomologyComparison'_right 📖	mathematical	—	right ofIsIsoLeftRightHomologyComparison'	—	—
ofIsLimitKernelFork_iso 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	iso ofIsLimitKernelFork CategoryTheory.Iso.refl CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork	—	—
ofIsLimitKernelFork_left 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	left ofIsLimitKernelFork CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork	—	—
ofIsLimitKernelFork_right 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	right ofIsLimitKernelFork CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork	—	—
ofIso_iso 📖	mathematical	—	iso ofIso	—	—
ofIso_left_H 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.H left ofIso	—	—
ofIso_left_K 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.K left ofIso	—	—
ofIso_left_i 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.i left ofIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.LeftHomologyData.K CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Iso.hom CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory	—	—
ofIso_left_π 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.π left ofIso	—	—
ofIso_right_H 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.H right ofIso	—	—
ofIso_right_Q 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.Q right ofIso	—	—
ofIso_right_p 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.p right ofIso CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.RightHomologyData.Q CategoryTheory.inv CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Iso.hom CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory Quiver.Hom CategoryTheory.CategoryStruct.toQuiver Quiver.Hom.unop Opposite.op Quiver.Hom.op CategoryTheory.IsIso CategoryTheory.isIso_unop Opposite.unop	—	CategoryTheory.isIso_unop CategoryTheory.unop_inv
ofIso_right_ι 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.ι right ofIso	—	—
ofZeros_iso 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.ShortComplex.g CategoryTheory.ShortComplex.X₃	iso ofZeros CategoryTheory.Iso.refl CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.ShortComplex.LeftHomologyData.ofZeros	—	—
ofZeros_left 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.ShortComplex.g CategoryTheory.ShortComplex.X₃	left ofZeros CategoryTheory.ShortComplex.LeftHomologyData.ofZeros	—	—
ofZeros_right 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.ShortComplex.g CategoryTheory.ShortComplex.X₃	right ofZeros CategoryTheory.ShortComplex.RightHomologyData.ofZeros	—	—
op_iso 📖	mathematical	—	iso Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.ShortComplex.op op CategoryTheory.Iso.op CategoryTheory.ShortComplex.LeftHomologyData.H left CategoryTheory.ShortComplex.RightHomologyData.H right	—	—
op_left 📖	mathematical	—	left Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.ShortComplex.op op CategoryTheory.ShortComplex.RightHomologyData.op right	—	—
op_right 📖	mathematical	—	right Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.ShortComplex.op op CategoryTheory.ShortComplex.LeftHomologyData.op left	—	—
right_homologyIso_eq_left_homologyIso_trans_iso 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.homologyIso right CategoryTheory.Iso.trans CategoryTheory.ShortComplex.homology CategoryTheory.ShortComplex.LeftHomologyData.H left CategoryTheory.ShortComplex.RightHomologyData.H CategoryTheory.ShortComplex.LeftHomologyData.homologyIso iso	—	CategoryTheory.Iso.ext CategoryTheory.ShortComplex.leftRightHomologyComparison'_fac leftRightHomologyComparison'_eq CategoryTheory.Iso.self_symm_id_assoc
unop_iso 📖	mathematical	—	iso CategoryTheory.ShortComplex.unop unop CategoryTheory.Iso.unop CategoryTheory.ShortComplex.LeftHomologyData.H Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite left CategoryTheory.ShortComplex.RightHomologyData.H right	—	—
unop_left 📖	mathematical	—	left CategoryTheory.ShortComplex.unop unop CategoryTheory.ShortComplex.RightHomologyData.unop right Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite	—	—
unop_right 📖	mathematical	—	right CategoryTheory.ShortComplex.unop unop CategoryTheory.ShortComplex.LeftHomologyData.unop left Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite	—	—

CategoryTheory.ShortComplex.HomologyMapData

Definitions

Name	Category	Theorems
comp 📖	CompOp	2 math math: comp_left, comp_right
compatibilityOfZerosOfIsColimitCokernelCofork 📖	CompOp	—
compatibilityOfZerosOfIsLimitKernelFork 📖	CompOp	2 math math: compatibilityOfZerosOfIsLimitKernelFork_left, compatibilityOfZerosOfIsLimitKernelFork_right
homologyMapData 📖	CompOp	—
id 📖	CompOp	2 math math: id_right, id_left
instInhabited 📖	CompOp	—
instUnique 📖	CompOp	—
left 📖	CompOp	21 math math: op_left, ofIsLimitKernelFork_left, add_left, unop_right, map_left, natTransApp_left, neg_left, comp_left, congr_left_φH, zero_left, op_right, compatibilityOfZerosOfIsLimitKernelFork_left, cyclesMap'_eq, comm, comm_assoc, homologyMap'_eq, ofZeros_left, smul_left, ofIsColimitCokernelCofork_left, id_left, unop_left
ofEpiOfIsIsoOfMono 📖	CompOp	—
ofEpiOfIsIsoOfMono' 📖	CompOp	—
ofIsColimitCokernelCofork 📖	CompOp	2 math math: ofIsColimitCokernelCofork_right, ofIsColimitCokernelCofork_left
ofIsLimitKernelFork 📖	CompOp	2 math math: ofIsLimitKernelFork_left, ofIsLimitKernelFork_right
ofZeros 📖	CompOp	2 math math: ofZeros_right, ofZeros_left
op 📖	CompOp	2 math math: op_left, op_right
right 📖	CompOp	19 math math: op_left, unop_right, opcyclesMap'_eq, comp_right, ofIsColimitCokernelCofork_right, ofIsLimitKernelFork_right, op_right, map_right, zero_right, id_right, add_right, comm, comm_assoc, neg_right, smul_right, compatibilityOfZerosOfIsLimitKernelFork_right, ofZeros_right, natTransApp_right, unop_left
unop 📖	CompOp	2 math math: unop_right, unop_left
zero 📖	CompOp	2 math math: zero_left, zero_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.ShortComplex.HomologyData.left CategoryTheory.ShortComplex.RightHomologyData.H CategoryTheory.ShortComplex.HomologyData.right CategoryTheory.ShortComplex.LeftHomologyMapData.φH left CategoryTheory.Iso.hom CategoryTheory.ShortComplex.HomologyData.iso CategoryTheory.ShortComplex.RightHomologyMapData.φH right	—	CategoryTheory.cancel_epi CategoryTheory.ShortComplex.LeftHomologyData.instEpiπ CategoryTheory.ShortComplex.LeftHomologyMapData.commπ_assoc CategoryTheory.cancel_mono CategoryTheory.ShortComplex.RightHomologyData.instMonoι CategoryTheory.Category.assoc CategoryTheory.ShortComplex.HomologyData.comm CategoryTheory.ShortComplex.LeftHomologyMapData.commi_assoc CategoryTheory.ShortComplex.RightHomologyMapData.commι CategoryTheory.ShortComplex.HomologyData.comm_assoc CategoryTheory.ShortComplex.RightHomologyMapData.commp
comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.ShortComplex.HomologyData.left CategoryTheory.ShortComplex.LeftHomologyMapData.φH left CategoryTheory.ShortComplex.RightHomologyData.H CategoryTheory.ShortComplex.HomologyData.right CategoryTheory.Iso.hom CategoryTheory.ShortComplex.HomologyData.iso CategoryTheory.ShortComplex.RightHomologyMapData.φH right	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm
comp_left 📖	mathematical	—	left CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory comp CategoryTheory.ShortComplex.LeftHomologyMapData.comp CategoryTheory.ShortComplex.HomologyData.left	—	—
comp_right 📖	mathematical	—	right CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory comp CategoryTheory.ShortComplex.RightHomologyMapData.comp CategoryTheory.ShortComplex.HomologyData.right	—	—
compatibilityOfZerosOfIsLimitKernelFork_left 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.ShortComplex.g CategoryTheory.ShortComplex.X₃	left CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork CategoryTheory.ShortComplex.HomologyData.ofZeros compatibilityOfZerosOfIsLimitKernelFork CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork	—	—
compatibilityOfZerosOfIsLimitKernelFork_right 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.ShortComplex.g CategoryTheory.ShortComplex.X₃	right CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork CategoryTheory.ShortComplex.HomologyData.ofZeros compatibilityOfZerosOfIsLimitKernelFork CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork	—	—
congr_left_φH 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyMapData.φH CategoryTheory.ShortComplex.HomologyData.left left	—	—
cyclesMap'_eq 📖	mathematical	—	CategoryTheory.ShortComplex.cyclesMap' CategoryTheory.ShortComplex.HomologyData.left CategoryTheory.ShortComplex.LeftHomologyMapData.φK left	—	CategoryTheory.ShortComplex.LeftHomologyMapData.congr_φK CategoryTheory.ShortComplex.LeftHomologyMapData.instSubsingleton
homologyMap'_eq 📖	mathematical	—	CategoryTheory.ShortComplex.homologyMap' CategoryTheory.ShortComplex.LeftHomologyMapData.φH CategoryTheory.ShortComplex.HomologyData.left left	—	CategoryTheory.ShortComplex.LeftHomologyMapData.congr_φH CategoryTheory.ShortComplex.LeftHomologyMapData.instSubsingleton
id_left 📖	mathematical	—	left CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory id CategoryTheory.ShortComplex.LeftHomologyMapData.id CategoryTheory.ShortComplex.HomologyData.left	—	—
id_right 📖	mathematical	—	right CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory id CategoryTheory.ShortComplex.RightHomologyMapData.id CategoryTheory.ShortComplex.HomologyData.right	—	—
instSubsingleton 📖	mathematical	—	CategoryTheory.ShortComplex.HomologyMapData	—	CategoryTheory.ShortComplex.LeftHomologyMapData.instSubsingleton CategoryTheory.ShortComplex.RightHomologyMapData.instSubsingleton
ofIsColimitCokernelCofork_left 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Limits.Cofork.π	left CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork ofIsColimitCokernelCofork CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsColimitCokernelCofork	—	—
ofIsColimitCokernelCofork_right 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Limits.Cofork.π	right CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork ofIsColimitCokernelCofork CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork	—	—
ofIsLimitKernelFork_left 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.CategoryStruct.comp 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.ShortComplex.g CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Fork.ι CategoryTheory.ShortComplex.Hom.τ₂	left CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork ofIsLimitKernelFork CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsLimitKernelFork	—	—
ofIsLimitKernelFork_right 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.CategoryStruct.comp 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.ShortComplex.g CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Fork.ι CategoryTheory.ShortComplex.Hom.τ₂	right CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork ofIsLimitKernelFork CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork	—	—
ofZeros_left 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.ShortComplex.g CategoryTheory.ShortComplex.X₃	left CategoryTheory.ShortComplex.HomologyData.ofZeros ofZeros CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros	—	—
ofZeros_right 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.ShortComplex.g CategoryTheory.ShortComplex.X₃	right CategoryTheory.ShortComplex.HomologyData.ofZeros ofZeros CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros	—	—
op_left 📖	mathematical	—	left Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.ShortComplex.op CategoryTheory.ShortComplex.opMap CategoryTheory.ShortComplex.HomologyData.op op CategoryTheory.ShortComplex.RightHomologyMapData.op CategoryTheory.ShortComplex.HomologyData.right right	—	—
op_right 📖	mathematical	—	right Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.ShortComplex.op CategoryTheory.ShortComplex.opMap CategoryTheory.ShortComplex.HomologyData.op op CategoryTheory.ShortComplex.LeftHomologyMapData.op CategoryTheory.ShortComplex.HomologyData.left left	—	—
opcyclesMap'_eq 📖	mathematical	—	CategoryTheory.ShortComplex.opcyclesMap' CategoryTheory.ShortComplex.HomologyData.right CategoryTheory.ShortComplex.RightHomologyMapData.φQ right	—	CategoryTheory.ShortComplex.RightHomologyMapData.congr_φQ CategoryTheory.ShortComplex.RightHomologyMapData.instSubsingleton
unop_left 📖	mathematical	—	left CategoryTheory.ShortComplex.unop CategoryTheory.ShortComplex.unopMap CategoryTheory.ShortComplex.HomologyData.unop unop CategoryTheory.ShortComplex.RightHomologyMapData.unop CategoryTheory.ShortComplex.HomologyData.right Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite right	—	—
unop_right 📖	mathematical	—	right CategoryTheory.ShortComplex.unop CategoryTheory.ShortComplex.unopMap CategoryTheory.ShortComplex.HomologyData.unop unop CategoryTheory.ShortComplex.LeftHomologyMapData.unop CategoryTheory.ShortComplex.HomologyData.left Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite left	—	—
zero_left 📖	mathematical	—	left Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instZeroHom zero CategoryTheory.ShortComplex.LeftHomologyMapData.zero CategoryTheory.ShortComplex.HomologyData.left	—	—
zero_right 📖	mathematical	—	right Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instZeroHom zero CategoryTheory.ShortComplex.RightHomologyMapData.zero CategoryTheory.ShortComplex.HomologyData.right	—	—

CategoryTheory.ShortComplex.LeftHomologyData

Definitions

Name	Category	Theorems
canonical 📖	CompOp	7 math math: CategoryTheory.ShortComplex.HomologyData.canonical_iso_hom, canonical_i, canonical_f', canonical_H, canonical_π, CategoryTheory.ShortComplex.HomologyData.canonical_iso_inv, canonical_K
homologyIso 📖	CompOp	22 math math: π_comp_homologyIso_inv, leftHomologyIso_hom_comp_homologyIso_inv, CategoryTheory.ShortComplex.HomologyData.right_homologyIso_eq_left_homologyIso_trans_iso, CategoryTheory.ShortComplex.leftRightHomologyComparison'_fac, CategoryTheory.ShortComplex.LeftHomologyMapData.homologyMap_comm, CategoryTheory.ShortComplex.LeftHomologyMapData.homologyMap_eq, homologyπ_comp_homologyIso_hom_assoc, leftHomologyIso_hom_naturality_assoc, leftHomologyIso_hom_naturality, CategoryTheory.ShortComplex.comp_homologyMap_comp_assoc, CategoryTheory.ShortComplex.HomologyData.left_homologyIso_eq_right_homologyIso_trans_iso_symm, leftHomologyIso_inv_naturality_assoc, π_comp_homologyIso_inv_assoc, homologyIso_hom_comp_leftHomologyIso_inv_assoc, homologyIso_leftHomologyData, mapHomologyIso_eq, homologyIso_hom_comp_leftHomologyIso_inv, homologyπ_comp_homologyIso_hom, leftHomologyIso_inv_naturality, CategoryTheory.ShortComplex.comp_homologyMap_comp, leftHomologyIso_hom_comp_homologyIso_inv_assoc, CategoryTheory.ShortComplex.leftRightHomologyComparison'_fac_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
canonical_H 📖	mathematical	—	H canonical CategoryTheory.ShortComplex.homology	—	—
canonical_K 📖	mathematical	—	K canonical CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology	—	—
canonical_f' 📖	mathematical	—	f' canonical CategoryTheory.ShortComplex.toCycles CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology	—	—
canonical_i 📖	mathematical	—	i canonical CategoryTheory.ShortComplex.iCycles CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology
canonical_π 📖	mathematical	—	π canonical CategoryTheory.ShortComplex.homologyπ	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology
homologyIso_hom_comp_leftHomologyIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.homology H CategoryTheory.ShortComplex.leftHomology CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.Iso.hom homologyIso CategoryTheory.Iso.inv leftHomologyIso CategoryTheory.ShortComplex.leftHomologyIso	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
homologyIso_hom_comp_leftHomologyIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.homology H CategoryTheory.Iso.hom homologyIso CategoryTheory.ShortComplex.leftHomology CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.Iso.inv leftHomologyIso CategoryTheory.ShortComplex.leftHomologyIso	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyIso_hom_comp_leftHomologyIso_inv
homologyIso_leftHomologyData 📖	mathematical	—	homologyIso CategoryTheory.ShortComplex.leftHomologyData CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.Iso.symm CategoryTheory.ShortComplex.leftHomology CategoryTheory.ShortComplex.homology CategoryTheory.ShortComplex.leftHomologyIso	—	CategoryTheory.Iso.ext CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.ShortComplex.leftHomologyMap'_comp CategoryTheory.Category.comp_id
homologyπ_comp_homologyIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.ShortComplex.homology H CategoryTheory.ShortComplex.homologyπ CategoryTheory.Iso.hom homologyIso K cyclesIso π	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_assoc leftHomologyπ_comp_leftHomologyIso_hom
homologyπ_comp_homologyIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.ShortComplex.homology CategoryTheory.ShortComplex.homologyπ H CategoryTheory.Iso.hom homologyIso K cyclesIso π	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyπ_comp_homologyIso_hom
leftHomologyIso_hom_comp_homologyIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.leftHomology CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology H CategoryTheory.ShortComplex.homology CategoryTheory.Iso.hom leftHomologyIso CategoryTheory.Iso.inv homologyIso CategoryTheory.ShortComplex.leftHomologyIso	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.Iso.hom_inv_id_assoc
leftHomologyIso_hom_comp_homologyIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.leftHomology CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology H CategoryTheory.Iso.hom leftHomologyIso CategoryTheory.ShortComplex.homology CategoryTheory.Iso.inv homologyIso CategoryTheory.ShortComplex.leftHomologyIso	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftHomologyIso_hom_comp_homologyIso_inv
leftHomologyIso_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.homology H CategoryTheory.Iso.hom homologyIso CategoryTheory.ShortComplex.leftHomologyMap' CategoryTheory.ShortComplex.homologyMap	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
leftHomologyIso_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.homology H CategoryTheory.Iso.hom homologyIso CategoryTheory.ShortComplex.leftHomologyMap' CategoryTheory.ShortComplex.homologyMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftHomologyIso_hom_naturality
leftHomologyIso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct H CategoryTheory.ShortComplex.homology CategoryTheory.Iso.inv homologyIso CategoryTheory.ShortComplex.homologyMap CategoryTheory.ShortComplex.leftHomologyMap'	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
leftHomologyIso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct H CategoryTheory.ShortComplex.homology CategoryTheory.Iso.inv homologyIso CategoryTheory.ShortComplex.homologyMap CategoryTheory.ShortComplex.leftHomologyMap'	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftHomologyIso_inv_naturality
π_comp_homologyIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct K H CategoryTheory.ShortComplex.homology π CategoryTheory.Iso.inv homologyIso CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology cyclesIso CategoryTheory.ShortComplex.homologyπ	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology π_comp_leftHomologyIso_inv_assoc
π_comp_homologyIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct K H π CategoryTheory.ShortComplex.homology CategoryTheory.Iso.inv homologyIso CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology cyclesIso CategoryTheory.ShortComplex.homologyπ	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_comp_homologyIso_inv

CategoryTheory.ShortComplex.LeftHomologyMapData

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homologyMap_comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.homology CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.ShortComplex.homologyMap CategoryTheory.Iso.hom CategoryTheory.ShortComplex.LeftHomologyData.homologyIso φH	—	homologyMap_eq CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
homologyMap_eq 📖	mathematical	—	CategoryTheory.ShortComplex.homologyMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.homology CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.Iso.hom CategoryTheory.ShortComplex.LeftHomologyData.homologyIso φH CategoryTheory.Iso.inv	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.Category.comp_id leftHomologyMap'_eq CategoryTheory.Category.id_comp

CategoryTheory.ShortComplex.RightHomologyData

Definitions

Name	Category	Theorems
canonical 📖	CompOp	7 math math: HomologicalComplex.truncGE.rightHomologyMapData_φQ, canonical_Q, canonical_ι, canonical_g', canonical_p, HomologicalComplex.truncGE.rightHomologyMapData_φH, canonical_H
homologyIso 📖	CompOp	22 math math: homologyIso_hom_comp_rightHomologyIso_inv, CategoryTheory.ShortComplex.RightHomologyMapData.homologyMap_eq, rightHomologyIso_inv_naturality_assoc, homologyIso_inv_comp_homologyι, CategoryTheory.ShortComplex.HomologyData.right_homologyIso_eq_left_homologyIso_trans_iso, CategoryTheory.ShortComplex.leftRightHomologyComparison'_fac, homologyIso_hom_comp_ι, rightHomologyIso_hom_naturality, CategoryTheory.ShortComplex.RightHomologyMapData.homologyMap_comm, rightHomologyIso_inv_naturality, homologyIso_hom_comp_rightHomologyIso_inv_assoc, homologyIso_hom_comp_ι_assoc, homologyIso_inv_comp_homologyι_assoc, CategoryTheory.ShortComplex.comp_homologyMap_comp_assoc, rightHomologyIso_hom_comp_homologyIso_inv_assoc, CategoryTheory.ShortComplex.HomologyData.left_homologyIso_eq_right_homologyIso_trans_iso_symm, rightHomologyIso_hom_naturality_assoc, rightHomologyIso_hom_comp_homologyIso_inv, CategoryTheory.ShortComplex.comp_homologyMap_comp, CategoryTheory.ShortComplex.leftRightHomologyComparison'_fac_assoc, mapHomologyIso'_eq, homologyIso_rightHomologyData

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
canonical_H 📖	mathematical	—	H canonical CategoryTheory.ShortComplex.homology	—	—
canonical_Q 📖	mathematical	—	Q canonical CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology	—	—
canonical_g' 📖	mathematical	—	g' canonical CategoryTheory.ShortComplex.fromOpcycles CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology	—	—
canonical_p 📖	mathematical	—	p canonical CategoryTheory.ShortComplex.pOpcycles CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology	—	CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology
canonical_ι 📖	mathematical	—	ι canonical CategoryTheory.ShortComplex.homologyι	—	CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology
homologyIso_hom_comp_rightHomologyIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.homology H CategoryTheory.ShortComplex.rightHomology CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.Iso.hom homologyIso CategoryTheory.Iso.inv rightHomologyIso CategoryTheory.ShortComplex.rightHomologyIso	—	CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
homologyIso_hom_comp_rightHomologyIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.homology H CategoryTheory.Iso.hom homologyIso CategoryTheory.ShortComplex.rightHomology CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.Iso.inv rightHomologyIso CategoryTheory.ShortComplex.rightHomologyIso	—	CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyIso_hom_comp_rightHomologyIso_inv
homologyIso_hom_comp_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.homology H Q CategoryTheory.Iso.hom homologyIso ι CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.homologyι opcyclesIso	—	CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.Category.assoc rightHomologyIso_hom_comp_ι
homologyIso_hom_comp_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.homology H CategoryTheory.Iso.hom homologyIso Q ι CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.homologyι opcyclesIso	—	CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyIso_hom_comp_ι
homologyIso_inv_comp_homologyι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct H CategoryTheory.ShortComplex.homology CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.Iso.inv homologyIso CategoryTheory.ShortComplex.homologyι Q ι opcyclesIso	—	CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_assoc rightHomologyIso_inv_comp_rightHomologyι
homologyIso_inv_comp_homologyι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct H CategoryTheory.ShortComplex.homology CategoryTheory.Iso.inv homologyIso CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.homologyι Q ι opcyclesIso	—	CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homologyIso_inv_comp_homologyι
homologyIso_rightHomologyData 📖	mathematical	—	homologyIso CategoryTheory.ShortComplex.rightHomologyData CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.Iso.symm CategoryTheory.ShortComplex.rightHomology CategoryTheory.ShortComplex.homology CategoryTheory.ShortComplex.rightHomologyIso	—	CategoryTheory.Iso.ext CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.rightHomologyMap'_id CategoryTheory.Category.comp_id
rightHomologyIso_hom_comp_homologyIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.rightHomology CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology H CategoryTheory.ShortComplex.homology CategoryTheory.Iso.hom rightHomologyIso CategoryTheory.Iso.inv homologyIso CategoryTheory.ShortComplex.rightHomologyIso	—	CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.Iso.hom_inv_id_assoc
rightHomologyIso_hom_comp_homologyIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.rightHomology CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology H CategoryTheory.Iso.hom rightHomologyIso CategoryTheory.ShortComplex.homology CategoryTheory.Iso.inv homologyIso CategoryTheory.ShortComplex.rightHomologyIso	—	CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightHomologyIso_hom_comp_homologyIso_inv
rightHomologyIso_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.homology H CategoryTheory.Iso.hom homologyIso CategoryTheory.ShortComplex.rightHomologyMap' CategoryTheory.ShortComplex.homologyMap	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.ShortComplex.isIso_leftRightHomologyComparison' CategoryTheory.ShortComplex.leftRightHomologyComparison'_naturality CategoryTheory.Iso.isIso_hom CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso_hom_naturality_assoc CategoryTheory.ShortComplex.leftRightHomologyComparison'_fac CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id_assoc
rightHomologyIso_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.homology H CategoryTheory.Iso.hom homologyIso CategoryTheory.ShortComplex.rightHomologyMap' CategoryTheory.ShortComplex.homologyMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightHomologyIso_hom_naturality
rightHomologyIso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct H CategoryTheory.ShortComplex.homology CategoryTheory.Iso.inv homologyIso CategoryTheory.ShortComplex.homologyMap CategoryTheory.ShortComplex.rightHomologyMap'	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc rightHomologyIso_hom_naturality CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
rightHomologyIso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct H CategoryTheory.ShortComplex.homology CategoryTheory.Iso.inv homologyIso CategoryTheory.ShortComplex.homologyMap CategoryTheory.ShortComplex.rightHomologyMap'	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightHomologyIso_inv_naturality

CategoryTheory.ShortComplex.RightHomologyMapData

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
homologyMap_comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.homology CategoryTheory.ShortComplex.RightHomologyData.H CategoryTheory.ShortComplex.homologyMap CategoryTheory.Iso.hom CategoryTheory.ShortComplex.RightHomologyData.homologyIso φH	—	homologyMap_eq CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
homologyMap_eq 📖	mathematical	—	CategoryTheory.ShortComplex.homologyMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.homology CategoryTheory.ShortComplex.RightHomologyData.H CategoryTheory.Iso.hom CategoryTheory.ShortComplex.RightHomologyData.homologyIso φH CategoryTheory.Iso.inv	—	CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap'_eq CategoryTheory.Category.assoc rightHomologyMap'_eq CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.ShortComplex.HomologyMapData.comm_assoc CategoryTheory.Iso.hom_inv_id

---

← Back to Index