LeftHomology

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

Statistics

Metric	Count
Definitions HasLeftHomology, LeftHomologyData, H, K, copy, cyclesIso, descH, f', hi, hπ, hπ', i, leftHomologyIso, liftH, liftK, ofEpiOfIsIsoOfMono, ofEpiOfIsIsoOfMono', ofHasCokernel, ofHasKernel, ofHasKernelOfHasCokernel, ofIsColimitCokernelCofork, ofIsLimitKernelFork, ofIso, ofZeros, π, LeftHomologyMapData, comp, compatibilityOfZerosOfIsColimitCokernelCofork, compatibilityOfZerosOfIsLimitKernelFork, id, instInhabited, instUnique, ofEpiOfIsIsoOfMono, ofEpiOfIsIsoOfMono', ofIsColimitCokernelCofork, ofIsLimitKernelFork, ofZeros, zero, φH, φK, cycles, cyclesFunctor, cyclesIsKernel, cyclesIsoKernel, cyclesIsoLeftHomology, cyclesIsoX₂, cyclesMap, cyclesMap', cyclesMapIso, cyclesMapIso', iCycles, iCyclesNatTrans, isoCyclesOfIsLimit, leftHomology, leftHomologyData, leftHomologyFunctor, leftHomologyIsCokernel, leftHomologyIsoCokernelLift, leftHomologyMap, leftHomologyMap', leftHomologyMapData, leftHomologyMapIso, leftHomologyMapIso', leftHomologyπ, leftHomologyπNatTrans, liftCycles, liftLeftHomology, toCycles, toCyclesNatTrans	69
Theorems condition, hasCokernel, hasKernel, mk', of_hasCokernel, of_hasKernel, of_hasKernel_of_hasCokernel, of_zeros, copy_H, copy_K, copy_i, copy_π, cyclesIso_hom_comp_i, cyclesIso_hom_comp_i_assoc, cyclesIso_inv_comp_iCycles, cyclesIso_inv_comp_iCycles_assoc, f'_i, f'_i_assoc, f'_π, f'_π_assoc, instEpiπ, instMonoI, isIso_i, isIso_π, leftHomologyπ_comp_leftHomologyIso_hom, leftHomologyπ_comp_leftHomologyIso_hom_assoc, liftCycles_comp_cyclesIso_hom, liftCycles_comp_cyclesIso_hom_assoc, liftK_i, liftK_i_assoc, liftK_π_eq_zero_of_boundary, liftK_π_eq_zero_of_boundary_assoc, lift_K_comp_cyclesIso_inv, lift_K_comp_cyclesIso_inv_assoc, ofEpiOfIsIsoOfMono'_H, ofEpiOfIsIsoOfMono'_K, ofEpiOfIsIsoOfMono'_f', ofEpiOfIsIsoOfMono'_i, ofEpiOfIsIsoOfMono'_π, ofEpiOfIsIsoOfMono_H, ofEpiOfIsIsoOfMono_K, ofEpiOfIsIsoOfMono_i, ofEpiOfIsIsoOfMono_π, ofHasCokernel_H, ofHasCokernel_K, ofHasCokernel_i, ofHasCokernel_π, ofHasKernelOfHasCokernel_H, ofHasKernelOfHasCokernel_K, ofHasKernelOfHasCokernel_i, ofHasKernelOfHasCokernel_π, ofIsColimitCokernelCofork_H, ofIsColimitCokernelCofork_K, ofIsColimitCokernelCofork_f', ofIsColimitCokernelCofork_i, ofIsColimitCokernelCofork_π, ofIsLimitKernelFork_H, ofIsLimitKernelFork_K, ofIsLimitKernelFork_f', ofIsLimitKernelFork_i, ofIsLimitKernelFork_π, ofZeros_H, ofZeros_K, ofZeros_f', ofZeros_i, ofZeros_π, wi, wi_assoc, wπ, wπ_assoc, π_comp_leftHomologyIso_inv, π_comp_leftHomologyIso_inv_assoc, π_descH, π_descH_assoc, τ₁_ofEpiOfIsIsoOfMono_f', commf', commf'_assoc, commi, commi_assoc, commπ, commπ_assoc, comp_φH, comp_φK, compatibilityOfZerosOfIsColimitCokernelCofork_φH, compatibilityOfZerosOfIsColimitCokernelCofork_φK, compatibilityOfZerosOfIsLimitKernelFork_φH, compatibilityOfZerosOfIsLimitKernelFork_φK, congr_φH, congr_φK, cyclesMap'_eq, cyclesMap_comm, cyclesMap_eq, id_φH, id_φK, instSubsingleton, leftHomologyMap'_eq, leftHomologyMap_comm, leftHomologyMap_eq, ofEpiOfIsIsoOfMono'_φH, ofEpiOfIsIsoOfMono'_φK, ofEpiOfIsIsoOfMono_φH, ofEpiOfIsIsoOfMono_φK, ofIsColimitCokernelCofork_φH, ofIsColimitCokernelCofork_φK, ofIsLimitKernelFork_φH, ofIsLimitKernelFork_φK, ofZeros_φH, ofZeros_φK, zero_φH, zero_φK, comp_liftCycles, comp_liftCycles_assoc, cyclesFunctor_map, cyclesFunctor_obj, cyclesIsoKernel_hom, cyclesIsoKernel_inv, cyclesIsoLeftHomology_hom, cyclesIsoLeftHomology_hom_inv_id, cyclesIsoLeftHomology_hom_inv_id_assoc, cyclesIsoLeftHomology_inv_hom_id, cyclesIsoLeftHomology_inv_hom_id_assoc, cyclesIsoX₂_hom, cyclesIsoX₂_hom_inv_id, cyclesIsoX₂_hom_inv_id_assoc, cyclesIsoX₂_inv_hom_id, cyclesIsoX₂_inv_hom_id_assoc, cyclesMap'_comp, cyclesMap'_comp_assoc, cyclesMap'_i, cyclesMap'_i_assoc, cyclesMap'_id, cyclesMap'_zero, cyclesMapIso'_hom, cyclesMapIso'_inv, cyclesMapIso_hom, cyclesMapIso_inv, cyclesMap_comp, cyclesMap_comp_assoc, cyclesMap_i, cyclesMap_i_assoc, cyclesMap_id, cyclesMap_zero, cycles_ext, cycles_ext_iff, f'_cyclesMap', f'_cyclesMap'_assoc, hasLeftHomology_of_epi_of_isIso_of_mono, hasLeftHomology_of_epi_of_isIso_of_mono', hasLeftHomology_of_iso, iCyclesNatTrans_app, iCycles_g, iCycles_g_assoc, instEpiLeftHomologyπ, instIsIsoLeftHomologyMap'OfEpiτ₁Ofτ₂OfMonoτ₃, instIsIsoLeftHomologyMapOfEpiτ₁Ofτ₂OfMonoτ₃, instMonoICycles, isIso_cyclesMap'_of_isIso, isIso_cyclesMap'_of_isIso_of_mono, isIso_cyclesMap_of_isIso_of_mono, isIso_cyclesMap_of_isIso_of_mono', isIso_cyclesMap_of_iso, isIso_iCycles, isIso_leftHomologyMap'_of_isIso, isIso_leftHomologyMap_of_iso, isIso_leftHomologyπ, isoCyclesOfIsLimit_hom_iCycles, isoCyclesOfIsLimit_hom_iCycles_assoc, isoCyclesOfIsLimit_inv_ι, isoCyclesOfIsLimit_inv_ι_assoc, leftHomologyData_H, leftHomologyFunctor_map, leftHomologyFunctor_obj, leftHomologyMap'_comp, leftHomologyMap'_comp_assoc, leftHomologyMap'_id, leftHomologyMap'_zero, leftHomologyMapIso'_hom, leftHomologyMapIso'_inv, leftHomologyMapIso_hom, leftHomologyMapIso_inv, leftHomologyMap_comp, leftHomologyMap_comp_assoc, leftHomologyMap_id, leftHomologyMap_zero, leftHomology_ext, leftHomology_ext_iff, leftHomologyπNatTrans_app, leftHomologyπ_naturality, leftHomologyπ_naturality', leftHomologyπ_naturality'_assoc, leftHomologyπ_naturality_assoc, liftCycles_comp_cyclesMap, liftCycles_comp_cyclesMap_assoc, liftCycles_i, liftCycles_i_assoc, liftCycles_leftHomologyπ_eq_zero_of_boundary, liftCycles_leftHomologyπ_eq_zero_of_boundary_assoc, toCyclesNatTrans_app, toCycles_comp_leftHomologyπ, toCycles_comp_leftHomologyπ_assoc, toCycles_i, toCycles_i_assoc, toCycles_naturality, toCycles_naturality_assoc	204
Total	273

CategoryTheory.ShortComplex

Definitions

Name	Category	Theorems
HasLeftHomology 📖	CompData	16 math math: hasRightHomology_iff_op, HasLeftHomology.of_zeros, hasLeftHomology_iff_op, hasLeftHomology_iff_unop, hasLeftHomology_of_iso, hasLeftHomology_of_epi_of_isIso_of_mono', HasLeftHomology.of_hasCokernel, HasLeftHomology.of_hasKernel_of_hasCokernel, instHasLeftHomologyOppositeOpOfHasRightHomology, hasLeftHomology_of_preserves, hasRightHomology_iff_unop, hasLeftHomology_of_preserves', HasLeftHomology.of_hasKernel, hasLeftHomology_of_epi_of_isIso_of_mono, hasLeftHomology_of_hasHomology, HasLeftHomology.mk'
LeftHomologyData 📖	CompData	1 math math: HasLeftHomology.condition
LeftHomologyMapData 📖	CompData	1 math math: LeftHomologyMapData.instSubsingleton
cycles 📖	CompOp	170 math math: LeftHomologyData.leftHomologyπ_comp_leftHomologyIso_hom, toCycles_comp_homologyπ, toCycles_comp_homologyπ_assoc, π_moduleCatCyclesIso_hom, HomologicalComplex.π_homologyIsoSc'_hom, cyclesOpIso_inv_op_iCycles_assoc, isIso_leftHomologyπ, homology_π_ι_assoc, LeftHomologyData.cyclesIso_inv_comp_iCycles_assoc, moduleCatCyclesIso_hom_i_apply, cyclesIsoX₂_hom_inv_id, liftCycles_comp_cyclesMap_assoc, exact_iff_iCycles_pOpcycles_zero, cyclesIsoX₂_hom_inv_id_assoc, cyclesIsoLeftHomology_hom_inv_id_assoc, isIso_iCycles, cyclesMap_neg, toCycles_comp_leftHomologyπ_assoc, mapCyclesIso_hom_iCycles_assoc, isoCyclesOfIsLimit_hom_iCycles_assoc, LeftHomologyData.π_comp_homologyIso_inv, isIso_homologyπ, cyclesMap_sub, isIso_cyclesMap_of_isIso_of_mono, comp_liftCycles_assoc, liftCycles_comp_cyclesMap, op_pOpcycles_opcyclesOpIso_hom, HomologyData.ofEpiMonoFactorisation.isoImage_ι, CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles_fac_assoc, comp_liftCycles, homologyπ_naturality_assoc, cyclesIsoX₂_inv_hom_id_assoc, iCycles_g, cyclesOpIso_hom_naturality, HomologyData.ofEpiMonoFactorisation.homologyπ_isoHomology_inv_assoc, homology_π_ι, opcyclesOpIso_hom_naturality_assoc, moduleCatCyclesIso_hom_i_assoc, HomologicalComplex.cyclesIsoSc'_inv_iCycles_assoc, HomologyData.canonical_left_K, cyclesMap_smul, op_pOpcycles_opcyclesOpIso_hom_assoc, moduleCatCyclesIso_inv_π_assoc_apply, moduleCatCyclesIso_hom_i, LeftHomologyData.π_comp_leftHomologyIso_inv_assoc, HomologicalComplex.cyclesIsoSc'_hom_iCycles_assoc, asIsoHomologyπ_hom, LeftHomologyData.leftHomologyπ_comp_leftHomologyIso_hom_assoc, i_cyclesMk, CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles_hom_fac_assoc, Exact.epi_toCycles, cyclesIsoKernel_hom, homologyπ_comp_leftHomologyIso_inv, CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles_hom_fac, HomologicalComplex.cyclesIsoSc'_inv_iCycles, fromOpcycles_op_cyclesOpIso_inv_assoc, leftHomologyπ_naturality_assoc, toCycles_i_assoc, isIso_cyclesMap_of_isIso_of_mono', CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles_fac, opcyclesOpIso_hom_toCycles_op_assoc, opcyclesOpIso_hom_naturality, homologyπ_naturality, liftCycles_leftHomologyπ_eq_zero_of_boundary_assoc, cyclesMap_comp, cyclesFunctor_obj, LeftHomologyData.cyclesIso_hom_comp_i_assoc, exact_iff_epi_toCycles, cyclesOpIso_inv_naturality, HomologicalComplex.π_homologyIsoSc'_hom_assoc, toCycles_moduleCatCyclesIso_hom, iCycles_g_assoc, LeftHomologyData.homologyπ_comp_homologyIso_hom_assoc, π_leftRightHomologyComparison_ι_assoc, HomologicalComplex.π_homologyIsoSc'_inv_assoc, π_moduleCatCyclesIso_hom_assoc_apply, leftHomologyπ_naturality, cyclesMap_zero, LeftHomologyMapData.cyclesMap_comm, cyclesIsoLeftHomology_hom_inv_id, asIsoHomologyπ_inv_comp_homologyπ, toCycles_comp_leftHomologyπ, opcyclesOpIso_inv_naturality, liftCycles_i, LeftHomologyData.π_comp_homologyIso_inv_assoc, moduleCatCyclesIso_hom_i_assoc_apply, homologyπ_comp_leftHomologyIso_inv_assoc, mapCyclesIso_hom_naturality_assoc, toCycles_naturality_assoc, LeftHomologyData.lift_K_comp_cyclesIso_inv_assoc, HomologicalComplex.toCycles_cyclesIsoSc'_hom_assoc, mapCyclesIso_inv_naturality_assoc, isoCyclesOfIsLimit_inv_ι_assoc, asIsoHomologyπ_inv_comp_homologyπ_assoc, π_moduleCatCyclesIso_hom_apply, LeftHomologyData.mapCyclesIso_eq, cyclesIsoLeftHomology_inv_hom_id, leftHomology_ext_iff, homologyIsoImageICyclesCompPOpcycles_ι, eq_liftCycles_homologyπ_up_to_refinements, π_homologyMap_ι_assoc, moduleCatCyclesIso_inv_iCycles, toCycles_i, LeftHomologyData.cyclesIso_hom_comp_i, moduleCatCyclesIso_inv_π_assoc, mapCyclesIso_hom_iCycles, mapCyclesIso_inv_naturality, isoCyclesOfIsLimit_hom_iCycles, cyclesMap_id, π_leftRightHomologyComparison_ι, HomologicalComplex.π_homologyIsoSc'_inv, HomologicalComplex.cyclesIsoSc'_hom_iCycles, cyclesMap_i_assoc, π_moduleCatCyclesIso_hom_assoc, homologyπ_comp_asIsoHomologyπ_inv_assoc, instEpiLeftHomologyπ, HomologyData.ofEpiMonoFactorisation.homologyπ_isoHomology_inv, toCycles_moduleCatCyclesIso_hom_apply, cyclesIsoLeftHomology_hom, cyclesIsoX₂_inv_hom_id, cycles_ext_iff, liftCycles_i_assoc, HomologicalComplex.toCycles_cyclesIsoSc'_hom, moduleCatCyclesIso_inv_iCycles_assoc_apply, moduleCatCyclesIso_inv_π_apply, LeftHomologyData.lift_K_comp_cyclesIso_inv, LeftHomologyData.homologyπ_comp_homologyIso_hom, HomologyData.ofEpiMonoFactorisation.f'_eq, liftCycles_homologyπ_eq_zero_of_boundary, toCycles_moduleCatCyclesIso_hom_assoc_apply, opcyclesOpIso_hom_toCycles_op, HomologyData.ofEpiMonoFactorisation.π_comp_isoHomology_hom, cyclesMap_i, isIso_cyclesMap_of_iso, LeftHomologyData.π_comp_leftHomologyIso_inv, cyclesIsoX₂_hom, cyclesOpIso_inv_op_iCycles, LeftHomologyMapData.cyclesMap_eq, LeftHomologyData.liftCycles_comp_cyclesIso_hom_assoc, cyclesOpIso_inv_naturality_assoc, toCycles_moduleCatCyclesIso_hom_assoc, Exact.isIso_toCycles, fromOpcycles_op_cyclesOpIso_inv, liftCycles_leftHomologyπ_eq_zero_of_boundary, HomologyData.ofEpiMonoFactorisation.π_comp_isoHomology_hom_assoc, moduleCatCyclesIso_inv_π, cyclesIsoKernel_inv, homologyπ_comp_asIsoHomologyπ_inv, toCycles_naturality, opcyclesOpIso_inv_naturality_assoc, moduleCatCyclesIso_inv_iCycles_assoc, HomologyData.ofEpiMonoFactorisation.isoImage_ι_assoc, homologyIsoImageICyclesCompPOpcycles_ι_assoc, moduleCatCyclesIso_inv_iCycles_apply, LeftHomologyData.liftCycles_comp_cyclesIso_hom, cyclesMap_comp_assoc, cyclesMapIso_inv, cyclesMap_add, LeftHomologyData.canonical_K, instEpiHomologyπ, cyclesMapIso_hom, isoCyclesOfIsLimit_inv_ι, LeftHomologyData.cyclesIso_inv_comp_iCycles, abCyclesIso_inv_apply_iCycles, quasiIso_iff_isIso_liftCycles, cyclesIsoLeftHomology_inv_hom_id_assoc, π_homologyMap_ι, instMonoICycles, mapCyclesIso_hom_naturality, cyclesOpIso_hom_naturality_assoc
cyclesFunctor 📖	CompOp	7 math math: cyclesFunctor_linear, toCyclesNatTrans_app, leftHomologyπNatTrans_app, cyclesFunctor_obj, cyclesFunctor_map, cyclesFunctor_additive, iCyclesNatTrans_app
cyclesIsKernel 📖	CompOp	—
cyclesIsoKernel 📖	CompOp	2 math math: cyclesIsoKernel_hom, cyclesIsoKernel_inv
cyclesIsoLeftHomology 📖	CompOp	5 math math: cyclesIsoLeftHomology_hom_inv_id_assoc, cyclesIsoLeftHomology_hom_inv_id, cyclesIsoLeftHomology_inv_hom_id, cyclesIsoLeftHomology_hom, cyclesIsoLeftHomology_inv_hom_id_assoc
cyclesIsoX₂ 📖	CompOp	5 math math: cyclesIsoX₂_hom_inv_id, cyclesIsoX₂_hom_inv_id_assoc, cyclesIsoX₂_inv_hom_id_assoc, cyclesIsoX₂_inv_hom_id, cyclesIsoX₂_hom
cyclesMap 📖	CompOp	38 math math: liftCycles_comp_cyclesMap_assoc, cyclesMap_neg, cyclesMap_sub, isIso_cyclesMap_of_isIso_of_mono, liftCycles_comp_cyclesMap, homologyπ_naturality_assoc, cyclesOpIso_hom_naturality, opcyclesOpIso_hom_naturality_assoc, cyclesMap_smul, leftHomologyπ_naturality_assoc, isIso_cyclesMap_of_isIso_of_mono', opcyclesOpIso_hom_naturality, homologyπ_naturality, cyclesMap_comp, cyclesOpIso_inv_naturality, cyclesFunctor_map, leftHomologyπ_naturality, cyclesMap_zero, LeftHomologyMapData.cyclesMap_comm, opcyclesOpIso_inv_naturality, mapCyclesIso_hom_naturality_assoc, toCycles_naturality_assoc, mapCyclesIso_inv_naturality_assoc, mapCyclesIso_inv_naturality, cyclesMap_id, cyclesMap_i_assoc, cyclesMap_i, isIso_cyclesMap_of_iso, LeftHomologyMapData.cyclesMap_eq, cyclesOpIso_inv_naturality_assoc, toCycles_naturality, opcyclesOpIso_inv_naturality_assoc, cyclesMap_comp_assoc, cyclesMapIso_inv, cyclesMap_add, cyclesMapIso_hom, mapCyclesIso_hom_naturality, cyclesOpIso_hom_naturality_assoc
cyclesMap' 📖	CompOp	21 math math: isIso_cyclesMap'_of_isIso_of_mono, cyclesMap'_comp_assoc, cyclesMap'_sub, cyclesMap'_comp, LeftHomologyData.map_cyclesMap', cyclesMapIso'_inv, leftHomologyπ_naturality', leftHomologyπ_naturality'_assoc, cyclesMap'_zero, HomologyMapData.cyclesMap'_eq, cyclesMap'_smul, f'_cyclesMap', cyclesMap'_i_assoc, cyclesMapIso'_hom, cyclesMap'_id, cyclesMap'_add, isIso_cyclesMap'_of_isIso, cyclesMap'_neg, cyclesMap'_i, f'_cyclesMap'_assoc, LeftHomologyMapData.cyclesMap'_eq
cyclesMapIso 📖	CompOp	2 math math: cyclesMapIso_inv, cyclesMapIso_hom
cyclesMapIso' 📖	CompOp	2 math math: cyclesMapIso'_inv, cyclesMapIso'_hom
iCycles 📖	CompOp	63 math math: cyclesOpIso_inv_op_iCycles_assoc, homology_π_ι_assoc, LeftHomologyData.cyclesIso_inv_comp_iCycles_assoc, moduleCatCyclesIso_hom_i_apply, HomologyData.canonical_left_i, cyclesIsoX₂_hom_inv_id, LeftHomologyData.canonical_i, exact_iff_iCycles_pOpcycles_zero, cyclesIsoX₂_hom_inv_id_assoc, isIso_iCycles, mapCyclesIso_hom_iCycles_assoc, isoCyclesOfIsLimit_hom_iCycles_assoc, op_pOpcycles_opcyclesOpIso_hom, HomologyData.ofEpiMonoFactorisation.isoImage_ι, CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles_fac_assoc, cyclesIsoX₂_inv_hom_id_assoc, iCycles_g, homology_π_ι, moduleCatCyclesIso_hom_i_assoc, HomologicalComplex.cyclesIsoSc'_inv_iCycles_assoc, op_pOpcycles_opcyclesOpIso_hom_assoc, moduleCatCyclesIso_hom_i, HomologicalComplex.cyclesIsoSc'_hom_iCycles_assoc, i_cyclesMk, CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles_hom_fac_assoc, cyclesIsoKernel_hom, CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles_hom_fac, HomologicalComplex.cyclesIsoSc'_inv_iCycles, toCycles_i_assoc, CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles_fac, LeftHomologyData.cyclesIso_hom_comp_i_assoc, iCycles_g_assoc, π_leftRightHomologyComparison_ι_assoc, liftCycles_i, moduleCatCyclesIso_hom_i_assoc_apply, isoCyclesOfIsLimit_inv_ι_assoc, homologyIsoImageICyclesCompPOpcycles_ι, π_homologyMap_ι_assoc, moduleCatCyclesIso_inv_iCycles, toCycles_i, LeftHomologyData.cyclesIso_hom_comp_i, mapCyclesIso_hom_iCycles, isoCyclesOfIsLimit_hom_iCycles, π_leftRightHomologyComparison_ι, HomologicalComplex.cyclesIsoSc'_hom_iCycles, cyclesMap_i_assoc, iCyclesNatTrans_app, cyclesIsoX₂_inv_hom_id, cycles_ext_iff, liftCycles_i_assoc, moduleCatCyclesIso_inv_iCycles_assoc_apply, cyclesMap_i, cyclesIsoX₂_hom, cyclesOpIso_inv_op_iCycles, moduleCatCyclesIso_inv_iCycles_assoc, HomologyData.ofEpiMonoFactorisation.isoImage_ι_assoc, homologyIsoImageICyclesCompPOpcycles_ι_assoc, moduleCatCyclesIso_inv_iCycles_apply, isoCyclesOfIsLimit_inv_ι, LeftHomologyData.cyclesIso_inv_comp_iCycles, abCyclesIso_inv_apply_iCycles, π_homologyMap_ι, instMonoICycles
iCyclesNatTrans 📖	CompOp	1 math math: iCyclesNatTrans_app
isoCyclesOfIsLimit 📖	CompOp	9 math math: isoCyclesOfIsLimit_hom_iCycles_assoc, HomologyData.ofEpiMonoFactorisation.homologyπ_isoHomology_inv_assoc, isoCyclesOfIsLimit_inv_ι_assoc, isoCyclesOfIsLimit_hom_iCycles, HomologyData.ofEpiMonoFactorisation.homologyπ_isoHomology_inv, HomologyData.ofEpiMonoFactorisation.f'_eq, HomologyData.ofEpiMonoFactorisation.π_comp_isoHomology_hom, HomologyData.ofEpiMonoFactorisation.π_comp_isoHomology_hom_assoc, isoCyclesOfIsLimit_inv_ι
leftHomology 📖	CompOp	64 math math: LeftHomologyData.leftHomologyπ_comp_leftHomologyIso_hom, leftHomologyMap_comp, isIso_leftHomologyπ, leftHomologyMap_sub, cyclesIsoLeftHomology_hom_inv_id_assoc, toCycles_comp_leftHomologyπ_assoc, LeftHomologyData.leftHomologyIso_hom_comp_homologyIso_inv, isIso_leftRightHomologyComparison, leftRightHomologyComparison_fac, leftHomologyMap_op, mapLeftHomologyIso_hom_naturality, leftHomologyMapIso_inv, leftHomologyMap_add, leftHomologyIso_hom_naturality, LeftHomologyData.π_comp_leftHomologyIso_inv_assoc, leftHomologyIso_hom_naturality_assoc, LeftHomologyData.leftHomologyπ_comp_leftHomologyIso_hom_assoc, homologyπ_comp_leftHomologyIso_inv, leftHomologyIso_inv_naturality_assoc, leftHomologyπ_naturality_assoc, leftHomologyMap_nullHomotopic, liftCycles_leftHomologyπ_eq_zero_of_boundary_assoc, instIsIsoLeftHomologyMapOfEpiτ₁Ofτ₂OfMonoτ₃, LeftHomologyMapData.leftHomologyMap_comm, LeftHomologyMapData.leftHomologyMap_eq, leftRightHomologyComparison_eq, π_leftRightHomologyComparison_ι_assoc, leftHomologyπ_naturality, LeftHomologyData.mapLeftHomologyIso_eq, cyclesIsoLeftHomology_hom_inv_id, toCycles_comp_leftHomologyπ, LeftHomologyData.homologyIso_hom_comp_leftHomologyIso_inv_assoc, homologyπ_comp_leftHomologyIso_inv_assoc, rightHomologyMap_op, exact_iff_isZero_leftHomology, rightHomologyFunctorOpNatIso_hom_app, LeftHomologyData.homologyIso_leftHomologyData, cyclesIsoLeftHomology_inv_hom_id, leftHomology_ext_iff, leftHomologyFunctorOpNatIso_hom_app, isIso_leftHomologyMap_of_iso, mapLeftHomologyIso_hom_naturality_assoc, π_leftRightHomologyComparison_ι, leftHomologyMapIso_hom, LeftHomologyData.homologyIso_hom_comp_leftHomologyIso_inv, rightHomologyFunctorOpNatIso_inv_app, leftHomologyIso_inv_naturality, instEpiLeftHomologyπ, cyclesIsoLeftHomology_hom, leftHomologyFunctor_obj, leftHomologyData_H, leftHomologyFunctorOpNatIso_inv_app, LeftHomologyData.π_comp_leftHomologyIso_inv, LeftHomologyData.leftHomologyIso_hom_comp_homologyIso_inv_assoc, leftHomologyMap_zero, liftCycles_leftHomologyπ_eq_zero_of_boundary, leftRightHomologyComparison_fac_assoc, leftHomologyMap_id, leftHomologyMap_smul, mapLeftHomologyIso_inv_naturality, leftHomologyMap_comp_assoc, mapLeftHomologyIso_inv_naturality_assoc, leftHomologyMap_neg, cyclesIsoLeftHomology_inv_hom_id_assoc
leftHomologyData 📖	CompOp	2 math math: LeftHomologyData.homologyIso_leftHomologyData, leftHomologyData_H
leftHomologyFunctor 📖	CompOp	9 math math: leftHomologyπNatTrans_app, leftHomologyFunctor_additive, rightHomologyFunctorOpNatIso_hom_app, leftHomologyFunctorOpNatIso_hom_app, rightHomologyFunctorOpNatIso_inv_app, leftHomologyFunctor_obj, leftHomologyFunctorOpNatIso_inv_app, leftHomologyFunctor_linear, leftHomologyFunctor_map
leftHomologyIsCokernel 📖	CompOp	—
leftHomologyIsoCokernelLift 📖	CompOp	—
leftHomologyMap 📖	CompOp	29 math math: leftHomologyMap_comp, leftHomologyMap_sub, leftHomologyMap_op, mapLeftHomologyIso_hom_naturality, leftHomologyMapIso_inv, leftHomologyMap_add, leftHomologyIso_hom_naturality, leftHomologyIso_hom_naturality_assoc, leftHomologyIso_inv_naturality_assoc, leftHomologyπ_naturality_assoc, leftHomologyMap_nullHomotopic, instIsIsoLeftHomologyMapOfEpiτ₁Ofτ₂OfMonoτ₃, LeftHomologyMapData.leftHomologyMap_comm, LeftHomologyMapData.leftHomologyMap_eq, leftHomologyπ_naturality, rightHomologyMap_op, Homotopy.leftHomologyMap_congr, isIso_leftHomologyMap_of_iso, mapLeftHomologyIso_hom_naturality_assoc, leftHomologyMapIso_hom, leftHomologyIso_inv_naturality, leftHomologyMap_zero, leftHomologyMap_id, leftHomologyMap_smul, mapLeftHomologyIso_inv_naturality, leftHomologyMap_comp_assoc, leftHomologyFunctor_map, mapLeftHomologyIso_inv_naturality_assoc, leftHomologyMap_neg
leftHomologyMap' 📖	CompOp	29 math math: leftHomologyMap'_sub, leftHomologyMap'_comp, LeftHomologyData.map_leftHomologyMap', leftHomologyMap'_neg, isIso_leftHomologyMap'_of_isIso, leftHomologyMap'_comp_assoc, rightHomologyMap'_op, Homotopy.leftHomologyMap'_congr, leftHomologyMapIso'_hom, leftHomologyπ_naturality', leftHomologyπ_naturality'_assoc, leftHomologyMap'_nullHomotopic, LeftHomologyData.leftHomologyIso_hom_naturality_assoc, leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap', LeftHomologyData.leftHomologyIso_hom_naturality, LeftHomologyData.leftHomologyIso_inv_naturality_assoc, leftHomologyMap'_id, instIsIsoLeftHomologyMap'OfEpiτ₁Ofτ₂OfMonoτ₃, leftHomologyMapIso'_inv, leftRightHomologyComparison'_naturality_assoc, LeftHomologyMapData.leftHomologyMap'_eq, leftRightHomologyComparison'_naturality, LeftHomologyData.leftHomologyIso_inv_naturality, quasiIso_iff_isIso_leftHomologyMap', leftRightHomologyComparison'_compatibility, leftHomologyMap'_zero, leftHomologyMap'_add, leftHomologyMap'_smul, leftHomologyMap'_op
leftHomologyMapData 📖	CompOp	—
leftHomologyMapIso 📖	CompOp	2 math math: leftHomologyMapIso_inv, leftHomologyMapIso_hom
leftHomologyMapIso' 📖	CompOp	2 math math: leftHomologyMapIso'_hom, leftHomologyMapIso'_inv
leftHomologyπ 📖	CompOp	23 math math: LeftHomologyData.leftHomologyπ_comp_leftHomologyIso_hom, isIso_leftHomologyπ, leftHomologyπNatTrans_app, cyclesIsoLeftHomology_hom_inv_id_assoc, toCycles_comp_leftHomologyπ_assoc, LeftHomologyData.π_comp_leftHomologyIso_inv_assoc, LeftHomologyData.leftHomologyπ_comp_leftHomologyIso_hom_assoc, homologyπ_comp_leftHomologyIso_inv, leftHomologyπ_naturality_assoc, liftCycles_leftHomologyπ_eq_zero_of_boundary_assoc, π_leftRightHomologyComparison_ι_assoc, leftHomologyπ_naturality, cyclesIsoLeftHomology_hom_inv_id, toCycles_comp_leftHomologyπ, homologyπ_comp_leftHomologyIso_inv_assoc, cyclesIsoLeftHomology_inv_hom_id, leftHomology_ext_iff, π_leftRightHomologyComparison_ι, instEpiLeftHomologyπ, cyclesIsoLeftHomology_hom, LeftHomologyData.π_comp_leftHomologyIso_inv, liftCycles_leftHomologyπ_eq_zero_of_boundary, cyclesIsoLeftHomology_inv_hom_id_assoc
leftHomologyπNatTrans 📖	CompOp	1 math math: leftHomologyπNatTrans_app
liftCycles 📖	CompOp	16 math math: liftCycles_comp_cyclesMap_assoc, comp_liftCycles_assoc, liftCycles_comp_cyclesMap, comp_liftCycles, liftCycles_leftHomologyπ_eq_zero_of_boundary_assoc, liftCycles_i, LeftHomologyData.lift_K_comp_cyclesIso_inv_assoc, eq_liftCycles_homologyπ_up_to_refinements, liftCycles_i_assoc, LeftHomologyData.lift_K_comp_cyclesIso_inv, liftCycles_homologyπ_eq_zero_of_boundary, LeftHomologyData.liftCycles_comp_cyclesIso_hom_assoc, liftCycles_leftHomologyπ_eq_zero_of_boundary, cyclesIsoKernel_inv, LeftHomologyData.liftCycles_comp_cyclesIso_hom, quasiIso_iff_isIso_liftCycles
liftLeftHomology 📖	CompOp	—
toCycles 📖	CompOp	24 math math: toCycles_comp_homologyπ, toCycles_comp_homologyπ_assoc, toCyclesNatTrans_app, toCycles_comp_leftHomologyπ_assoc, Exact.epi_toCycles, fromOpcycles_op_cyclesOpIso_inv_assoc, toCycles_i_assoc, opcyclesOpIso_hom_toCycles_op_assoc, exact_iff_epi_toCycles, toCycles_moduleCatCyclesIso_hom, LeftHomologyData.canonical_f', toCycles_comp_leftHomologyπ, toCycles_naturality_assoc, HomologicalComplex.toCycles_cyclesIsoSc'_hom_assoc, toCycles_i, toCycles_moduleCatCyclesIso_hom_apply, HomologicalComplex.toCycles_cyclesIsoSc'_hom, HomologyData.ofEpiMonoFactorisation.f'_eq, toCycles_moduleCatCyclesIso_hom_assoc_apply, opcyclesOpIso_hom_toCycles_op, toCycles_moduleCatCyclesIso_hom_assoc, Exact.isIso_toCycles, fromOpcycles_op_cyclesOpIso_inv, toCycles_naturality
toCyclesNatTrans 📖	CompOp	1 math math: toCyclesNatTrans_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_liftCycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ X₃ g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	cycles liftCycles	—	cycles_ext CategoryTheory.Category.assoc liftCycles_i
comp_liftCycles_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ X₃ g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	cycles liftCycles	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_liftCycles
cyclesFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.ShortComplex instCategory cyclesFunctor cyclesMap	—	—
cyclesFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.ShortComplex instCategory cyclesFunctor cycles	—	—
cyclesIsoKernel_hom 📖	mathematical	—	CategoryTheory.Iso.hom cycles CategoryTheory.Limits.kernel X₂ X₃ g cyclesIsoKernel CategoryTheory.Limits.kernel.lift iCycles	—	—
cyclesIsoKernel_inv 📖	mathematical	—	CategoryTheory.Iso.inv cycles CategoryTheory.Limits.kernel X₂ X₃ g cyclesIsoKernel liftCycles CategoryTheory.Limits.kernel.ι	—	—
cyclesIsoLeftHomology_hom 📖	mathematical	f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Iso.hom cycles leftHomology cyclesIsoLeftHomology leftHomologyπ	—	—
cyclesIsoLeftHomology_hom_inv_id 📖	mathematical	f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp cycles leftHomology leftHomologyπ CategoryTheory.Iso.inv cyclesIsoLeftHomology CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.hom_inv_id
cyclesIsoLeftHomology_hom_inv_id_assoc 📖	mathematical	f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp cycles leftHomology leftHomologyπ CategoryTheory.Iso.inv cyclesIsoLeftHomology	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' cyclesIsoLeftHomology_hom_inv_id
cyclesIsoLeftHomology_inv_hom_id 📖	mathematical	f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp leftHomology cycles CategoryTheory.Iso.inv cyclesIsoLeftHomology leftHomologyπ CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.inv_hom_id
cyclesIsoLeftHomology_inv_hom_id_assoc 📖	mathematical	f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp leftHomology cycles CategoryTheory.Iso.inv cyclesIsoLeftHomology leftHomologyπ	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' cyclesIsoLeftHomology_inv_hom_id
cyclesIsoX₂_hom 📖	mathematical	g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Iso.hom cycles cyclesIsoX₂ iCycles	—	—
cyclesIsoX₂_hom_inv_id 📖	mathematical	g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp cycles iCycles CategoryTheory.Iso.inv cyclesIsoX₂ CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.hom_inv_id
cyclesIsoX₂_hom_inv_id_assoc 📖	mathematical	g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp cycles iCycles CategoryTheory.Iso.inv cyclesIsoX₂	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' cyclesIsoX₂_hom_inv_id
cyclesIsoX₂_inv_hom_id 📖	mathematical	g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp cycles CategoryTheory.Iso.inv cyclesIsoX₂ iCycles CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.inv_hom_id
cyclesIsoX₂_inv_hom_id_assoc 📖	mathematical	g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp cycles CategoryTheory.Iso.inv cyclesIsoX₂ iCycles	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' cyclesIsoX₂_inv_hom_id
cyclesMap'_comp 📖	mathematical	—	cyclesMap' CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory LeftHomologyData.K	—	LeftHomologyMapData.cyclesMap'_eq LeftHomologyMapData.comp_φK
cyclesMap'_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct LeftHomologyData.K cyclesMap' CategoryTheory.ShortComplex instCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesMap'_comp
cyclesMap'_i 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct LeftHomologyData.K X₂ cyclesMap' LeftHomologyData.i Hom.τ₂	—	LeftHomologyMapData.commi
cyclesMap'_i_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct LeftHomologyData.K cyclesMap' X₂ LeftHomologyData.i Hom.τ₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesMap'_i
cyclesMap'_id 📖	mathematical	—	cyclesMap' CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory LeftHomologyData.K	—	LeftHomologyMapData.cyclesMap'_eq
cyclesMap'_zero 📖	mathematical	—	cyclesMap' Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instZeroHom LeftHomologyData.K CategoryTheory.Limits.HasZeroMorphisms.zero	—	LeftHomologyMapData.cyclesMap'_eq
cyclesMapIso'_hom 📖	mathematical	—	CategoryTheory.Iso.hom LeftHomologyData.K cyclesMapIso' cyclesMap' CategoryTheory.ShortComplex instCategory	—	—
cyclesMapIso'_inv 📖	mathematical	—	CategoryTheory.Iso.inv LeftHomologyData.K cyclesMapIso' cyclesMap' CategoryTheory.ShortComplex instCategory	—	—
cyclesMapIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom cycles cyclesMapIso cyclesMap CategoryTheory.ShortComplex instCategory	—	—
cyclesMapIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv cycles cyclesMapIso cyclesMap CategoryTheory.ShortComplex instCategory	—	—
cyclesMap_comp 📖	mathematical	—	cyclesMap CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory cycles	—	cyclesMap'_comp
cyclesMap_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles cyclesMap CategoryTheory.ShortComplex instCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesMap_comp
cyclesMap_i 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles X₂ cyclesMap iCycles Hom.τ₂	—	cyclesMap'_i
cyclesMap_i_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles cyclesMap X₂ iCycles Hom.τ₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesMap_i
cyclesMap_id 📖	mathematical	—	cyclesMap CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory cycles	—	cyclesMap'_id
cyclesMap_zero 📖	mathematical	—	cyclesMap Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instZeroHom cycles CategoryTheory.Limits.HasZeroMorphisms.zero	—	cyclesMap'_zero
cycles_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles X₂ iCycles	—	—	—
cycles_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles X₂ iCycles	—	CategoryTheory.cancel_mono instMonoICycles
f'_cyclesMap' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ LeftHomologyData.K LeftHomologyData.f' cyclesMap' Hom.τ₁	—	CategoryTheory.cancel_mono LeftHomologyData.instMonoI CategoryTheory.Category.assoc cyclesMap'_i LeftHomologyData.f'_i_assoc LeftHomologyData.f'_i Hom.comm₁₂
f'_cyclesMap'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ LeftHomologyData.K LeftHomologyData.f' cyclesMap' Hom.τ₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' f'_cyclesMap'
hasLeftHomology_of_epi_of_isIso_of_mono 📖	mathematical	—	HasLeftHomology	—	HasLeftHomology.mk'
hasLeftHomology_of_epi_of_isIso_of_mono' 📖	mathematical	—	HasLeftHomology	—	HasLeftHomology.mk'
hasLeftHomology_of_iso 📖	mathematical	—	HasLeftHomology	—	hasLeftHomology_of_epi_of_isIso_of_mono CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso instIsIsoτ₁ CategoryTheory.Iso.isIso_hom instIsIsoτ₂ CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso instIsIsoτ₃
iCyclesNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ShortComplex instCategory cyclesFunctor π₂ iCyclesNatTrans iCycles	—	—
iCycles_g 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles X₂ X₃ iCycles g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	LeftHomologyData.wi
iCycles_g_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles X₂ iCycles X₃ g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' iCycles_g
instEpiLeftHomologyπ 📖	mathematical	—	CategoryTheory.Epi cycles leftHomology leftHomologyπ	—	LeftHomologyData.instEpiπ
instIsIsoLeftHomologyMap'OfEpiτ₁Ofτ₂OfMonoτ₃ 📖	mathematical	—	CategoryTheory.IsIso LeftHomologyData.H leftHomologyMap'	—	LeftHomologyMapData.leftHomologyMap'_eq CategoryTheory.IsIso.id leftHomologyMap'_comp CategoryTheory.Category.comp_id CategoryTheory.IsIso.comp_isIso isIso_leftHomologyMap'_of_isIso
instIsIsoLeftHomologyMapOfEpiτ₁Ofτ₂OfMonoτ₃ 📖	mathematical	—	CategoryTheory.IsIso leftHomology leftHomologyMap	—	instIsIsoLeftHomologyMap'OfEpiτ₁Ofτ₂OfMonoτ₃
instMonoICycles 📖	mathematical	—	CategoryTheory.Mono cycles X₂ iCycles	—	LeftHomologyData.instMonoI
isIso_cyclesMap'_of_isIso 📖	mathematical	—	CategoryTheory.IsIso LeftHomologyData.K cyclesMap'	—	CategoryTheory.Iso.isIso_hom
isIso_cyclesMap'_of_isIso_of_mono 📖	mathematical	—	CategoryTheory.IsIso LeftHomologyData.K cyclesMap'	—	CategoryTheory.Category.assoc CategoryTheory.cancel_mono Hom.comm₂₃ CategoryTheory.IsIso.inv_hom_id_assoc LeftHomologyData.wi CategoryTheory.Limits.zero_comp LeftHomologyData.instMonoI LeftHomologyData.liftK_i cyclesMap'_i_assoc CategoryTheory.IsIso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp cyclesMap'_i LeftHomologyData.liftK_i_assoc CategoryTheory.IsIso.inv_hom_id
isIso_cyclesMap_of_isIso_of_mono 📖	mathematical	—	CategoryTheory.IsIso cycles cyclesMap	—	isIso_cyclesMap_of_isIso_of_mono'
isIso_cyclesMap_of_isIso_of_mono' 📖	mathematical	—	CategoryTheory.IsIso cycles cyclesMap	—	isIso_cyclesMap'_of_isIso_of_mono
isIso_cyclesMap_of_iso 📖	mathematical	—	CategoryTheory.IsIso cycles cyclesMap	—	CategoryTheory.Iso.isIso_hom
isIso_iCycles 📖	mathematical	g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.IsIso cycles iCycles	—	LeftHomologyData.isIso_i
isIso_leftHomologyMap'_of_isIso 📖	mathematical	—	CategoryTheory.IsIso LeftHomologyData.H leftHomologyMap'	—	CategoryTheory.Iso.isIso_hom
isIso_leftHomologyMap_of_iso 📖	mathematical	—	CategoryTheory.IsIso leftHomology leftHomologyMap	—	CategoryTheory.Iso.isIso_hom
isIso_leftHomologyπ 📖	mathematical	f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.IsIso cycles leftHomology leftHomologyπ	—	LeftHomologyData.isIso_π
isoCyclesOfIsLimit_hom_iCycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair X₂ X₃ g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero cycles CategoryTheory.Iso.hom isoCyclesOfIsLimit iCycles CategoryTheory.Limits.Fork.ι	—	CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp iCycles_g
isoCyclesOfIsLimit_hom_iCycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair X₂ X₃ g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero cycles CategoryTheory.Iso.hom isoCyclesOfIsLimit iCycles CategoryTheory.Limits.Fork.ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoCyclesOfIsLimit_hom_iCycles
isoCyclesOfIsLimit_inv_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair X₂ X₃ g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Iso.inv isoCyclesOfIsLimit CategoryTheory.Limits.Fork.ι iCycles	—	CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_inv_comp iCycles_g
isoCyclesOfIsLimit_inv_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair X₂ X₃ g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Iso.inv isoCyclesOfIsLimit CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair.zero CategoryTheory.Limits.Fork.ι iCycles	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoCyclesOfIsLimit_inv_ι
leftHomologyData_H 📖	mathematical	—	LeftHomologyData.H leftHomologyData leftHomology	—	—
leftHomologyFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.ShortComplex instCategory leftHomologyFunctor leftHomologyMap	—	—
leftHomologyFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.ShortComplex instCategory leftHomologyFunctor leftHomology	—	—
leftHomologyMap'_comp 📖	mathematical	—	leftHomologyMap' CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory LeftHomologyData.H	—	LeftHomologyMapData.leftHomologyMap'_eq LeftHomologyMapData.comp_φH
leftHomologyMap'_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct LeftHomologyData.H leftHomologyMap' CategoryTheory.ShortComplex instCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftHomologyMap'_comp
leftHomologyMap'_id 📖	mathematical	—	leftHomologyMap' CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory LeftHomologyData.H	—	LeftHomologyMapData.leftHomologyMap'_eq
leftHomologyMap'_zero 📖	mathematical	—	leftHomologyMap' Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instZeroHom LeftHomologyData.H CategoryTheory.Limits.HasZeroMorphisms.zero	—	LeftHomologyMapData.leftHomologyMap'_eq
leftHomologyMapIso'_hom 📖	mathematical	—	CategoryTheory.Iso.hom LeftHomologyData.H leftHomologyMapIso' leftHomologyMap' CategoryTheory.ShortComplex instCategory	—	—
leftHomologyMapIso'_inv 📖	mathematical	—	CategoryTheory.Iso.inv LeftHomologyData.H leftHomologyMapIso' leftHomologyMap' CategoryTheory.ShortComplex instCategory	—	—
leftHomologyMapIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom leftHomology leftHomologyMapIso leftHomologyMap CategoryTheory.ShortComplex instCategory	—	—
leftHomologyMapIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv leftHomology leftHomologyMapIso leftHomologyMap CategoryTheory.ShortComplex instCategory	—	—
leftHomologyMap_comp 📖	mathematical	—	leftHomologyMap CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory leftHomology	—	leftHomologyMap'_comp
leftHomologyMap_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct leftHomology leftHomologyMap CategoryTheory.ShortComplex instCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftHomologyMap_comp
leftHomologyMap_id 📖	mathematical	—	leftHomologyMap CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory leftHomology	—	leftHomologyMap'_id
leftHomologyMap_zero 📖	mathematical	—	leftHomologyMap Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instZeroHom leftHomology CategoryTheory.Limits.HasZeroMorphisms.zero	—	leftHomologyMap'_zero
leftHomology_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles leftHomology leftHomologyπ	—	—	—
leftHomology_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles leftHomology leftHomologyπ	—	CategoryTheory.cancel_epi instEpiLeftHomologyπ
leftHomologyπNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ShortComplex instCategory cyclesFunctor leftHomologyFunctor leftHomologyπNatTrans leftHomologyπ	—	—
leftHomologyπ_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles leftHomology leftHomologyπ leftHomologyMap cyclesMap	—	leftHomologyπ_naturality'
leftHomologyπ_naturality' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct LeftHomologyData.K LeftHomologyData.H LeftHomologyData.π leftHomologyMap' cyclesMap'	—	LeftHomologyMapData.commπ
leftHomologyπ_naturality'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct LeftHomologyData.K LeftHomologyData.H LeftHomologyData.π leftHomologyMap' cyclesMap'	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftHomologyπ_naturality'
leftHomologyπ_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles leftHomology leftHomologyπ leftHomologyMap cyclesMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftHomologyπ_naturality
liftCycles_comp_cyclesMap 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ X₃ g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	cycles liftCycles cyclesMap Hom.τ₂	—	cycles_ext CategoryTheory.Category.assoc cyclesMap_i liftCycles_i_assoc liftCycles_i
liftCycles_comp_cyclesMap_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ X₃ g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	cycles liftCycles cyclesMap Hom.τ₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' liftCycles_comp_cyclesMap
liftCycles_i 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ X₃ g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	cycles liftCycles iCycles	—	LeftHomologyData.liftK_i
liftCycles_i_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ X₃ g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	cycles liftCycles iCycles	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' liftCycles_i
liftCycles_leftHomologyπ_eq_zero_of_boundary 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ X₂ f	cycles leftHomology liftCycles leftHomologyπ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	LeftHomologyData.liftK_π_eq_zero_of_boundary
liftCycles_leftHomologyπ_eq_zero_of_boundary_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ X₂ f	cycles liftCycles leftHomology leftHomologyπ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' liftCycles_leftHomologyπ_eq_zero_of_boundary
toCyclesNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ShortComplex instCategory π₁ cyclesFunctor toCyclesNatTrans toCycles	—	—
toCycles_comp_leftHomologyπ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ cycles leftHomology toCycles leftHomologyπ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	liftCycles_leftHomologyπ_eq_zero_of_boundary CategoryTheory.Category.id_comp
toCycles_comp_leftHomologyπ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ cycles toCycles leftHomology leftHomologyπ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toCycles_comp_leftHomologyπ
toCycles_i 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ cycles X₂ toCycles iCycles f	—	LeftHomologyData.f'_i
toCycles_i_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ cycles toCycles X₂ iCycles f	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toCycles_i
toCycles_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ cycles toCycles cyclesMap Hom.τ₁	—	f'_cyclesMap'
toCycles_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ cycles toCycles cyclesMap Hom.τ₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toCycles_naturality

CategoryTheory.ShortComplex.HasLeftHomology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData	—	—
hasCokernel 📖	mathematical	—	CategoryTheory.Limits.HasCokernel CategoryTheory.ShortComplex.X₁ CategoryTheory.Limits.kernel CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g CategoryTheory.Limits.kernel.lift CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.zero	—	CategoryTheory.ShortComplex.zero CategoryTheory.Limits.kernel.condition CategoryTheory.Limits.comp_zero CategoryTheory.ShortComplex.LeftHomologyData.wi CategoryTheory.Limits.IsLimit.lift_comp_conePointUniqueUpToIso_hom CategoryTheory.Category.id_comp CategoryTheory.Limits.zero_comp CategoryTheory.Limits.hasColimit_of_iso CategoryTheory.ShortComplex.LeftHomologyData.f'_π
hasKernel 📖	mathematical	—	CategoryTheory.Limits.HasKernel CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	CategoryTheory.ShortComplex.LeftHomologyData.wi
mk' 📖	mathematical	—	CategoryTheory.ShortComplex.HasLeftHomology	—	—
of_hasCokernel 📖	mathematical	—	CategoryTheory.ShortComplex.HasLeftHomology Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.comp_zero	—	mk' CategoryTheory.Limits.comp_zero
of_hasKernel 📖	mathematical	—	CategoryTheory.ShortComplex.HasLeftHomology Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.zero_comp	—	mk' CategoryTheory.Limits.zero_comp
of_hasKernel_of_hasCokernel 📖	mathematical	—	CategoryTheory.ShortComplex.HasLeftHomology	—	CategoryTheory.ShortComplex.zero mk'
of_zeros 📖	mathematical	—	CategoryTheory.ShortComplex.HasLeftHomology Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.zero_comp	—	mk' CategoryTheory.Limits.zero_comp

CategoryTheory.ShortComplex.LeftHomologyData

Definitions

Name	Category	Theorems
H 📖	CompOp	167 math math: CategoryTheory.ShortComplex.HomologyData.exact_iff, π_descH_assoc, CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork_iso, leftHomologyπ_comp_leftHomologyIso_hom, groupHomology.π_comp_H2Iso_hom_assoc, CategoryTheory.ShortComplex.HomologyData.canonical_iso_hom, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom, ofHasKernelOfHasCokernel_H, CategoryTheory.ShortComplex.leftHomologyMap'_sub, CategoryTheory.ShortComplex.leftHomologyMap'_comp, groupCohomology.π_comp_H1Iso_hom_assoc, CategoryTheory.ShortComplex.LeftHomologyMapData.id_φH, HomologicalComplex.extend.homologyData'_left_H, map_leftHomologyMap', CategoryTheory.ShortComplex.leftHomologyMap'_neg, CategoryTheory.ShortComplex.LeftHomologyMapData.map_φH, f'_π_assoc, unop_ι, π_comp_homologyIso_inv, map_π, groupHomology.π_comp_H1Iso_inv, CategoryTheory.ShortComplex.homologyMap'_zero, CategoryTheory.ShortComplex.homologyMap'_comp, leftHomologyIso_hom_comp_homologyIso_inv, ofAbelian_H, CategoryTheory.ShortComplex.isIso_leftHomologyMap'_of_isIso, CategoryTheory.ShortComplex.HomologyData.right_homologyIso_eq_left_homologyIso_trans_iso, CategoryTheory.ShortComplex.leftRightHomologyComparison'_fac, CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι, CategoryTheory.ShortComplex.homologyMap'_nullHomotopic, CategoryTheory.ShortComplex.LeftHomologyMapData.op_φH, CategoryTheory.ShortComplex.LeftHomologyMapData.smul_φH, CategoryTheory.ShortComplex.homologyMap'_sub, CategoryTheory.ShortComplex.HomologyData.map_homologyMap', groupHomology.π_comp_H2Iso_inv_assoc, CategoryTheory.ShortComplex.isIso_leftRightHomologyComparison', CategoryTheory.ShortComplex.homologyMap'_add, CategoryTheory.ShortComplex.Exact.condition, CategoryTheory.ShortComplex.Splitting.leftHomologyData_H, ofIsLimitKernelFork_H, op_H, CategoryTheory.ShortComplex.leftHomologyMap'_comp_assoc, CategoryTheory.ShortComplex.LeftHomologyMapData.homologyMap_comm, CategoryTheory.ShortComplex.homologyMap'_op, CategoryTheory.ShortComplex.quasiIso_iff_isIso_homologyMap', CategoryTheory.ShortComplex.HomologyData.canonical_left_H, CategoryTheory.ShortComplex.homologyMap'_neg, CategoryTheory.ShortComplex.LeftHomologyMapData.neg_φH, groupCohomology.π_comp_H1Iso_hom, exact_map_iff, CategoryTheory.ShortComplex.HomologyData.comm_assoc, π_comp_leftHomologyIso_inv_assoc, CategoryTheory.ShortComplex.isIso_leftRightHomologyComparison'_of_homologyData, leftHomologyπ_comp_leftHomologyIso_hom_assoc, groupHomology.π_comp_H2Iso_hom, copy_π, CategoryTheory.ShortComplex.HomologyData.ofHasCokernel_iso, CategoryTheory.ShortComplex.LeftHomologyMapData.homologyMap_eq, CategoryTheory.ShortComplex.leftHomologyMapIso'_hom, CategoryTheory.ShortComplex.LeftHomologyMapData.commπ, CategoryTheory.ShortComplex.homologyMap'_id, CategoryTheory.ShortComplex.LeftHomologyMapData.quasiIso_map_iff, f'_π, CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono'_φH, CategoryTheory.ShortComplex.leftHomologyπ_naturality', wπ_assoc, CategoryTheory.ShortComplex.LeftHomologyMapData.comp_φH, CategoryTheory.ShortComplex.LeftHomologyMapData.add_φH, CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap_comm, CategoryTheory.ShortComplex.leftHomologyπ_naturality'_assoc, CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap_eq, CategoryTheory.ShortComplex.leftRightHomologyComparison_eq, homologyπ_comp_homologyIso_hom_assoc, HomologicalComplex.extend.leftHomologyData_H, ofIsColimitCokernelCofork_H, CategoryTheory.ShortComplex.RightHomologyData.op_H, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData_H, CategoryTheory.ShortComplex.leftHomologyMap'_nullHomotopic, mapLeftHomologyIso_eq, leftHomologyIso_hom_naturality_assoc, CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap', leftHomologyIso_hom_naturality, CategoryTheory.ShortComplex.comp_homologyMap_comp_assoc, ofHasCokernel_H, CategoryTheory.ShortComplex.LeftHomologyMapData.zero_φH, CategoryTheory.ShortComplex.HomologyData.left_homologyIso_eq_right_homologyIso_trans_iso_symm, copy_H, leftHomologyIso_inv_naturality_assoc, CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι_assoc, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_descH_hom, CategoryTheory.ShortComplex.homologyMapIso'_hom, wπ, π_comp_homologyIso_inv_assoc, ofEpiOfIsIsoOfMono'_H, homologyIso_hom_comp_leftHomologyIso_inv_assoc, canonical_H, CategoryTheory.ShortComplex.isIso_homologyMap'_of_epi_of_isIso_of_mono, groupCohomology.π_comp_H2Iso_hom_assoc, CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_liftH, CategoryTheory.ShortComplex.HomologyMapData.comm, CategoryTheory.ShortComplex.HomologyMapData.comm_assoc, CategoryTheory.ShortComplex.homologyMap'_smul, unop_H, CategoryTheory.ShortComplex.leftHomologyMap'_id, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation_iso, groupHomology.π_comp_H1Iso_hom_assoc, liftK_π_eq_zero_of_boundary, groupHomology.π_comp_H2Iso_inv, CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp_φH, CochainComplex.HomComplex.leftHomologyData_H_coe, CategoryTheory.ShortComplex.instIsIsoLeftHomologyMap'OfEpiτ₁Ofτ₂OfMonoτ₃, CategoryTheory.ShortComplex.LeftHomologyMapData.unop_φH, CategoryTheory.ShortComplex.leftHomologyMapIso'_inv, CategoryTheory.ShortComplex.leftRightHomologyComparison'_naturality_assoc, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc, CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork_iso, CategoryTheory.ShortComplex.HomologyData.canonical_iso_inv, ofZeros_H, CategoryTheory.ShortComplex.HomologyData.ofZeros_iso, ofEpiOfIsIsoOfMono_H, π_descH, CochainComplex.HomComplex.leftHomologyData'_H_coe, mapHomologyIso_eq, isIso_π, homologyIso_hom_comp_leftHomologyIso_inv, CategoryTheory.ShortComplex.map_leftRightHomologyComparison', exact_iff, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_assoc, CategoryTheory.ShortComplex.LeftHomologyMapData.quasiIso_iff, CategoryTheory.ShortComplex.HomologyData.unop_iso, CategoryTheory.ShortComplex.HomologyData.op_iso, CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono_φH, CategoryTheory.ShortComplex.HomologyData.map_iso, groupHomology.π_comp_H1Iso_hom, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_H, CategoryTheory.ShortComplex.leftRightHomologyComparison'_naturality, homologyπ_comp_homologyIso_hom, instEpiπ, leftHomologyIso_inv_naturality, CategoryTheory.ShortComplex.HomologyData.ofIso_left_H, CategoryTheory.ShortComplex.leftHomologyData_H, CategoryTheory.ShortComplex.quasiIso_iff_isIso_leftHomologyMap', CategoryTheory.ShortComplex.isIso_homologyMap'_of_isIso, π_comp_leftHomologyIso_inv, CategoryTheory.ShortComplex.RightHomologyData.unop_H, CategoryTheory.ShortComplex.HomologyData.ofIsIsoLeftRightHomologyComparison'_iso, CategoryTheory.ShortComplex.comp_homologyMap_comp, CategoryTheory.ShortComplex.HomologyData.comm, leftHomologyIso_hom_comp_homologyIso_inv_assoc, CategoryTheory.ShortComplex.LeftHomologyMapData.commπ_assoc, CategoryTheory.ShortComplex.leftRightHomologyComparison'_compatibility, CategoryTheory.ShortComplex.abLeftHomologyData_H_coe, CategoryTheory.ShortComplex.homologyMapIso'_inv, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π, CategoryTheory.ShortComplex.leftHomologyMap'_zero, map_H, CategoryTheory.ShortComplex.HomologyData.leftRightHomologyComparison'_eq, CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_H, CategoryTheory.ShortComplex.leftHomologyMap'_add, groupHomology.π_comp_H1Iso_inv_assoc, CategoryTheory.ShortComplex.HomologyData.ofHasKernel_iso, CategoryTheory.ShortComplex.leftRightHomologyComparison'_fac_assoc, liftK_π_eq_zero_of_boundary_assoc, CategoryTheory.ShortComplex.leftHomologyMap'_smul, op_ι, groupCohomology.π_comp_H2Iso_hom, CategoryTheory.ShortComplex.leftHomologyMap'_op
K 📖	CompOp	163 math math: leftHomologyπ_comp_leftHomologyIso_hom, op_g', CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom, groupCohomology.toCocycles_comp_isoCocycles₁_hom, CategoryTheory.ShortComplex.LeftHomologyMapData.unop_φQ, unop_p, ofAbelian_K, cyclesIso_inv_comp_iCycles_assoc, liftK_i_assoc, liftK_i, CategoryTheory.ShortComplex.LeftHomologyMapData.id_φK, groupCohomology.mapCocycles₂_comp_i, ofZeros_f', exact_iff_epi_f', ofHasKernelOfHasCokernel_K, CategoryTheory.ShortComplex.LeftHomologyMapData.commf', ofEpiOfIsIsoOfMono'_i, f'_π_assoc, unop_ι, π_comp_homologyIso_inv, CochainComplex.HomComplex.leftHomologyData_K_coe, instMonoI, map_π, CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φK, groupHomology.π_comp_H1Iso_inv, CategoryTheory.ShortComplex.isIso_cyclesMap'_of_isIso_of_mono, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData_K, CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι, isIso_i, IsPreservedBy.f', CategoryTheory.ShortComplex.cyclesMap'_comp_assoc, IsPreservedBy.hf', CategoryTheory.ShortComplex.cyclesMap'_sub, CategoryTheory.ShortComplex.Splitting.leftHomologyData_K, groupHomology.π_comp_H2Iso_inv_assoc, ofZeros_K, groupCohomology.toCocycles_comp_isoCocycles₂_hom, groupHomology.mapCycles₁_comp_i, CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_descH, map_i, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_assoc, CategoryTheory.ShortComplex.HomologyData.ofIso_left_i, CategoryTheory.ShortComplex.HomologyData.canonical_left_K, CategoryTheory.ShortComplex.cyclesMap'_comp, map_cyclesMap', groupHomology.mapCycles₂_comp_i, CategoryTheory.ShortComplex.cyclesMapIso'_inv, CategoryTheory.ShortComplex.LeftHomologyMapData.op_φQ, CategoryTheory.ShortComplex.HomologyData.comm_assoc, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i, π_comp_leftHomologyIso_inv_assoc, leftHomologyπ_comp_leftHomologyIso_hom_assoc, copy_i, CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_K, CategoryTheory.ShortComplex.RightHomologyData.op_K, copy_π, CategoryTheory.ShortComplex.abLeftHomologyData_K_coe, map_K, f'_i, CategoryTheory.ShortComplex.LeftHomologyMapData.commπ, ofEpiOfIsIsoOfMono'_K, f'_π, ofHasCokernel_K, op_Q, CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono'_φK, CategoryTheory.ShortComplex.Exact.shortExact, cyclesIso_hom_comp_i_assoc, CategoryTheory.ShortComplex.leftHomologyπ_naturality', CategoryTheory.ShortComplex.moduleCatLeftHomologyData_liftK_hom, wπ_assoc, CategoryTheory.ShortComplex.leftHomologyπ_naturality'_assoc, groupCohomology.isoCocycles₁_inv_comp_iCocycles, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom, CategoryTheory.ShortComplex.LeftHomologyMapData.natTransApp_φK, ofEpiOfIsIsoOfMono'_f', ofEpiOfIsIsoOfMono_K, CategoryTheory.ShortComplex.cyclesMap'_zero, homologyπ_comp_homologyIso_hom_assoc, CategoryTheory.ShortComplex.exact_iff_i_p_zero, wi, groupHomology.toCycles_comp_isoCycles₂_hom, CategoryTheory.ShortComplex.cyclesMap'_smul, CategoryTheory.ShortComplex.comp_homologyMap_comp_assoc, CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap_comm, CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι_assoc, HomologicalComplex.extend.homologyData'_left_i, copy_K, wπ, π_comp_homologyIso_inv_assoc, CategoryTheory.ShortComplex.Exact.epi_f', CategoryTheory.ShortComplex.LeftHomologyMapData.zero_φK, CategoryTheory.ShortComplex.f'_cyclesMap', op_p, f'_i_assoc, CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_liftH, lift_K_comp_cyclesIso_inv_assoc, CategoryTheory.ShortComplex.HomologyData.exact_iff_i_p_zero, CategoryTheory.ShortComplex.RightHomologyData.unop_K, liftK_π_eq_zero_of_boundary, groupHomology.π_comp_H2Iso_inv, ofIsColimitCokernelCofork_K, mapCyclesIso_eq, CategoryTheory.ShortComplex.Exact.isIso_f', groupCohomology.isoCocycles₂_inv_comp_iCocycles, HomologicalComplex.extend.leftHomologyData_i, CochainComplex.HomComplex.leftHomologyData'_K_coe, CategoryTheory.ShortComplex.LeftHomologyMapData.commi_assoc, CategoryTheory.ShortComplex.cyclesMap'_i_assoc, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles, ofIsLimitKernelFork_K, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_f'_hom, cyclesIso_hom_comp_i, CategoryTheory.ShortComplex.LeftHomologyMapData.smul_φK, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc, CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono_φK, CategoryTheory.ShortComplex.cyclesMapIso'_hom, CategoryTheory.ShortComplex.LeftHomologyMapData.neg_φK, unop_Q, CategoryTheory.ShortComplex.cyclesMap'_id, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_K, isIso_π, HomologicalComplex.extend.leftHomologyData_K, CategoryTheory.ShortComplex.LeftHomologyMapData.comp_φK, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_assoc, CategoryTheory.ShortComplex.LeftHomologyMapData.commf'_assoc, groupHomology.isoCycles₁_inv_comp_iCycles, groupHomology.toCycles_comp_isoCycles₁_hom, CategoryTheory.ShortComplex.cyclesMap'_add, groupHomology.isoCycles₂_inv_comp_iCycles, CategoryTheory.ShortComplex.LeftHomologyMapData.add_φK, ofIsLimitKernelFork_f', lift_K_comp_cyclesIso_inv, homologyπ_comp_homologyIso_hom, instEpiπ, HomologicalComplex.extend.homologyData'_left_K, CategoryTheory.ShortComplex.isIso_cyclesMap'_of_isIso, map_f', ofEpiOfIsIsoOfMono_i, CategoryTheory.ShortComplex.cyclesMap'_neg, wi_assoc, CategoryTheory.ShortComplex.cyclesMap'_i, π_comp_leftHomologyIso_inv, CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap_eq, liftCycles_comp_cyclesIso_hom_assoc, CategoryTheory.ShortComplex.HomologyData.ofIso_left_K, CategoryTheory.ShortComplex.LeftHomologyMapData.commi, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_assoc, CategoryTheory.ShortComplex.comp_homologyMap_comp, CategoryTheory.ShortComplex.f'_cyclesMap'_assoc, CategoryTheory.ShortComplex.HomologyData.comm, CategoryTheory.ShortComplex.LeftHomologyMapData.commπ_assoc, τ₁_ofEpiOfIsIsoOfMono_f', unop_g', CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π, groupHomology.π_comp_H1Iso_inv_assoc, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_assoc, liftCycles_comp_cyclesIso_hom, liftK_π_eq_zero_of_boundary_assoc, groupCohomology.mapCocycles₁_comp_i, op_ι, canonical_K, CategoryTheory.ShortComplex.LeftHomologyMapData.map_φK, cyclesIso_inv_comp_iCycles
copy 📖	CompOp	4 math math: copy_i, copy_π, copy_H, copy_K
cyclesIso 📖	CompOp	19 math math: leftHomologyπ_comp_leftHomologyIso_hom, cyclesIso_inv_comp_iCycles_assoc, π_comp_homologyIso_inv, π_comp_leftHomologyIso_inv_assoc, leftHomologyπ_comp_leftHomologyIso_hom_assoc, cyclesIso_hom_comp_i_assoc, homologyπ_comp_homologyIso_hom_assoc, CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap_comm, π_comp_homologyIso_inv_assoc, lift_K_comp_cyclesIso_inv_assoc, mapCyclesIso_eq, cyclesIso_hom_comp_i, lift_K_comp_cyclesIso_inv, homologyπ_comp_homologyIso_hom, π_comp_leftHomologyIso_inv, CategoryTheory.ShortComplex.LeftHomologyMapData.cyclesMap_eq, liftCycles_comp_cyclesIso_hom_assoc, liftCycles_comp_cyclesIso_hom, cyclesIso_inv_comp_iCycles
descH 📖	CompOp	5 math math: π_descH_assoc, CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_descH, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_descH_hom, CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_liftH, π_descH
f' 📖	CompOp	36 math math: op_g', groupCohomology.toCocycles_comp_isoCocycles₁_hom, ofZeros_f', exact_iff_epi_f', CategoryTheory.ShortComplex.LeftHomologyMapData.commf', f'_π_assoc, groupHomology.toCycles_comp_isoCycles₂_hom_assoc, IsPreservedBy.f', IsPreservedBy.hf', groupCohomology.toCocycles_comp_isoCocycles₂_hom, groupHomology.toCycles_comp_isoCycles₁_hom_assoc, CategoryTheory.ShortComplex.RightHomologyData.unop_f', f'_i, f'_π, groupCohomology.toCocycles_comp_isoCocycles₁_hom_assoc, CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom, ofEpiOfIsIsoOfMono'_f', CategoryTheory.ShortComplex.abLeftHomologyData_f', canonical_f', ofIsColimitCokernelCofork_f', groupHomology.toCycles_comp_isoCycles₂_hom, CategoryTheory.ShortComplex.Exact.epi_f', CategoryTheory.ShortComplex.f'_cyclesMap', f'_i_assoc, groupCohomology.toCocycles_comp_isoCocycles₂_hom_assoc, CategoryTheory.ShortComplex.RightHomologyData.op_f', CategoryTheory.ShortComplex.Exact.isIso_f', CategoryTheory.ShortComplex.moduleCatLeftHomologyData_f'_hom, CategoryTheory.ShortComplex.LeftHomologyMapData.commf'_assoc, groupHomology.toCycles_comp_isoCycles₁_hom, ofIsLimitKernelFork_f', map_f', CategoryTheory.ShortComplex.toCycles_moduleCatCyclesIso_hom_assoc, CategoryTheory.ShortComplex.f'_cyclesMap'_assoc, τ₁_ofEpiOfIsIsoOfMono_f', unop_g'
hi 📖	CompOp	2 math math: wπ_assoc, wπ
hπ 📖	CompOp	—
hπ' 📖	CompOp	—
i 📖	CompOp	83 math math: CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData_i, unop_p, cyclesIso_inv_comp_iCycles_assoc, liftK_i_assoc, liftK_i, CategoryTheory.ShortComplex.HomologyData.canonical_left_i, groupCohomology.mapCocycles₂_comp_i, canonical_i, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_i_hom, ofEpiOfIsIsoOfMono'_i, instMonoI, CategoryTheory.ShortComplex.RightHomologyData.unop_i, CochainComplex.HomComplex.leftHomologyData'_i, CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι, isIso_i, groupCohomology.mapCocycles₂_comp_i_assoc, CochainComplex.HomComplex.leftHomologyData_i_hom_apply, groupHomology.mapCycles₁_comp_i, ofHasKernelOfHasCokernel_i, CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_descH, ofAbelian_i, map_i, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i_assoc, CategoryTheory.ShortComplex.HomologyData.ofIso_left_i, groupHomology.mapCycles₂_comp_i, CategoryTheory.ShortComplex.HomologyData.comm_assoc, CategoryTheory.ShortComplex.moduleCatCyclesIso_hom_i, ofIsLimitKernelFork_i, copy_i, groupCohomology.isoCocycles₂_hom_comp_i, f'_i, CategoryTheory.ShortComplex.Exact.shortExact, cyclesIso_hom_comp_i_assoc, wπ_assoc, ofZeros_i, groupCohomology.isoCocycles₁_inv_comp_iCocycles, CategoryTheory.ShortComplex.exact_iff_i_p_zero, wi, CategoryTheory.ShortComplex.comp_homologyMap_comp_assoc, CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι_assoc, HomologicalComplex.extend.homologyData'_left_i, wπ, op_p, groupCohomology.mapCocycles₁_comp_i_assoc, CategoryTheory.ShortComplex.abLeftHomologyData_i, f'_i_assoc, CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_liftH, CategoryTheory.ShortComplex.HomologyData.exact_iff_i_p_zero, groupHomology.isoCycles₂_inv_comp_iCycles_assoc, groupHomology.isoCycles₁_inv_comp_iCycles_assoc, groupCohomology.isoCocycles₂_inv_comp_iCocycles, HomologicalComplex.extend.leftHomologyData_i, CategoryTheory.ShortComplex.LeftHomologyMapData.commi_assoc, CategoryTheory.ShortComplex.Splitting.leftHomologyData_i, CategoryTheory.ShortComplex.cyclesMap'_i_assoc, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles, cyclesIso_hom_comp_i, groupHomology.mapCycles₂_comp_i_assoc, groupCohomology.isoCocycles₁_hom_comp_i, groupHomology.isoCycles₁_hom_comp_i_assoc, groupHomology.isoCycles₁_inv_comp_iCycles, CategoryTheory.ShortComplex.RightHomologyData.op_i, groupHomology.isoCycles₂_hom_comp_i, groupHomology.isoCycles₂_inv_comp_iCycles, groupCohomology.isoCocycles₁_inv_comp_iCocycles_assoc, ofEpiOfIsIsoOfMono_i, groupHomology.isoCycles₁_hom_comp_i, wi_assoc, CategoryTheory.ShortComplex.cyclesMap'_i, CategoryTheory.ShortComplex.LeftHomologyMapData.commi, ofIsColimitCokernelCofork_i, CategoryTheory.ShortComplex.comp_homologyMap_comp, CategoryTheory.ShortComplex.HomologyData.comm, CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_i, groupCohomology.isoCocycles₂_hom_comp_i_assoc, groupCohomology.isoCocycles₁_hom_comp_i_assoc, groupHomology.mapCycles₁_comp_i_assoc, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_assoc, groupCohomology.mapCocycles₁_comp_i, groupHomology.isoCycles₂_hom_comp_i_assoc, ofHasCokernel_i, groupCohomology.isoCocycles₂_inv_comp_iCocycles_assoc, cyclesIso_inv_comp_iCycles
leftHomologyIso 📖	CompOp	12 math math: leftHomologyπ_comp_leftHomologyIso_hom, leftHomologyIso_hom_comp_homologyIso_inv, π_comp_leftHomologyIso_inv_assoc, leftHomologyπ_comp_leftHomologyIso_hom_assoc, CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap_comm, CategoryTheory.ShortComplex.LeftHomologyMapData.leftHomologyMap_eq, CategoryTheory.ShortComplex.leftRightHomologyComparison_eq, mapLeftHomologyIso_eq, homologyIso_hom_comp_leftHomologyIso_inv_assoc, homologyIso_hom_comp_leftHomologyIso_inv, π_comp_leftHomologyIso_inv, leftHomologyIso_hom_comp_homologyIso_inv_assoc
liftH 📖	CompOp	—
liftK 📖	CompOp	9 math math: liftK_i_assoc, liftK_i, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_liftK_hom, lift_K_comp_cyclesIso_inv_assoc, liftK_π_eq_zero_of_boundary, lift_K_comp_cyclesIso_inv, liftCycles_comp_cyclesIso_hom_assoc, liftCycles_comp_cyclesIso_hom, liftK_π_eq_zero_of_boundary_assoc
ofEpiOfIsIsoOfMono 📖	CompOp	8 math math: ofEpiOfIsIsoOfMono_K, CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono_φK, ofEpiOfIsIsoOfMono_H, CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono_φH, ofEpiOfIsIsoOfMono_i, τ₁_ofEpiOfIsIsoOfMono_f', ofEpiOfIsIsoOfMono_π, CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono_left
ofEpiOfIsIsoOfMono' 📖	CompOp	8 math math: ofEpiOfIsIsoOfMono'_i, CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono'_left, ofEpiOfIsIsoOfMono'_K, CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono'_φK, CategoryTheory.ShortComplex.LeftHomologyMapData.ofEpiOfIsIsoOfMono'_φH, ofEpiOfIsIsoOfMono'_f', ofEpiOfIsIsoOfMono'_H, ofEpiOfIsIsoOfMono'_π
ofHasCokernel 📖	CompOp	6 math math: ofHasCokernel_π, CategoryTheory.ShortComplex.HomologyData.ofHasCokernel_iso, ofHasCokernel_K, ofHasCokernel_H, CategoryTheory.ShortComplex.HomologyData.ofHasCokernel_left, ofHasCokernel_i
ofHasKernel 📖	CompOp	2 math math: CategoryTheory.ShortComplex.HomologyData.ofHasKernel_left, CategoryTheory.ShortComplex.HomologyData.ofHasKernel_iso
ofHasKernelOfHasCokernel 📖	CompOp	4 math math: ofHasKernelOfHasCokernel_H, ofHasKernelOfHasCokernel_K, ofHasKernelOfHasCokernel_i, ofHasKernelOfHasCokernel_π
ofIsColimitCokernelCofork 📖	CompOp	11 math math: CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork_iso, CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φK, ofIsColimitCokernelCofork_π, ofIsColimitCokernelCofork_H, ofIsColimitCokernelCofork_f', ofIsColimitCokernelCofork_K, CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork_left, CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsColimitCokernelCofork_φK, ofIsColimitCokernelCofork_i, CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φH, CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsColimitCokernelCofork_φH
ofIsLimitKernelFork 📖	CompOp	11 math math: CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork_left, ofIsLimitKernelFork_H, ofIsLimitKernelFork_i, CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_φH, ofIsLimitKernelFork_K, CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork_iso, ofIsLimitKernelFork_π, CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsLimitKernelFork_φK, CategoryTheory.ShortComplex.LeftHomologyMapData.ofIsLimitKernelFork_φH, ofIsLimitKernelFork_f', CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_φK
ofIso 📖	CompOp	—
ofZeros 📖	CompOp	13 math math: CategoryTheory.ShortComplex.HomologyData.ofZeros_left, ofZeros_f', CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φK, ofZeros_K, CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros_φK, ofZeros_i, CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_φH, ofZeros_H, CategoryTheory.ShortComplex.HomologyData.ofZeros_iso, ofZeros_π, CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_φK, CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φH, CategoryTheory.ShortComplex.LeftHomologyMapData.ofZeros_φH
π 📖	CompOp	70 math math: π_descH_assoc, leftHomologyπ_comp_leftHomologyIso_hom, groupHomology.π_comp_H2Iso_hom_assoc, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom, HomologicalComplex.extend.leftHomologyData_π, groupCohomology.π_comp_H1Iso_hom_assoc, CategoryTheory.ShortComplex.HomologyData.canonical_left_π, f'_π_assoc, unop_ι, π_comp_homologyIso_inv, map_π, groupHomology.π_comp_H1Iso_inv, ofHasCokernel_π, CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι, ofIsColimitCokernelCofork_π, CochainComplex.HomComplex.leftHomologyData_π_hom_apply, groupHomology.π_comp_H2Iso_inv_assoc, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.leftHomologyData_π, CategoryTheory.ShortComplex.abLeftHomologyData_π, groupCohomology.π_comp_H1Iso_hom, CategoryTheory.ShortComplex.HomologyData.comm_assoc, π_comp_leftHomologyIso_inv_assoc, leftHomologyπ_comp_leftHomologyIso_hom_assoc, groupHomology.π_comp_H2Iso_hom, copy_π, CategoryTheory.ShortComplex.LeftHomologyMapData.commπ, f'_π, CategoryTheory.ShortComplex.leftHomologyπ_naturality', wπ_assoc, CategoryTheory.ShortComplex.leftHomologyπ_naturality'_assoc, CategoryTheory.ShortComplex.Splitting.leftHomologyData_π, homologyπ_comp_homologyIso_hom_assoc, CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_π, CategoryTheory.ShortComplex.comp_homologyMap_comp_assoc, CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι_assoc, wπ, π_comp_homologyIso_inv_assoc, ofEpiOfIsIsoOfMono'_π, canonical_π, ofAbelian_π, groupCohomology.π_comp_H2Iso_hom_assoc, groupHomology.π_comp_H1Iso_hom_assoc, liftK_π_eq_zero_of_boundary, groupHomology.π_comp_H2Iso_inv, CategoryTheory.ShortComplex.HomologyData.ofIso_left_π, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π_assoc, ofHasKernelOfHasCokernel_π, π_descH, isIso_π, ofIsLimitKernelFork_π, CategoryTheory.ShortComplex.π_moduleCatCyclesIso_hom_assoc, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_π_hom, CochainComplex.HomComplex.leftHomologyData'_π, HomologicalComplex.extend.homologyData'_left_π, ofZeros_π, groupHomology.π_comp_H1Iso_hom, homologyπ_comp_homologyIso_hom, instEpiπ, CategoryTheory.ShortComplex.RightHomologyData.unop_π, π_comp_leftHomologyIso_inv, CategoryTheory.ShortComplex.comp_homologyMap_comp, CategoryTheory.ShortComplex.HomologyData.comm, CategoryTheory.ShortComplex.LeftHomologyMapData.commπ_assoc, CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_π, ofEpiOfIsIsoOfMono_π, groupHomology.π_comp_H1Iso_inv_assoc, liftK_π_eq_zero_of_boundary_assoc, op_ι, CategoryTheory.ShortComplex.RightHomologyData.op_π, groupCohomology.π_comp_H2Iso_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
copy_H 📖	mathematical	—	H copy	—	—
copy_K 📖	mathematical	—	K copy	—	—
copy_i 📖	mathematical	—	i copy CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct K CategoryTheory.ShortComplex.X₂ CategoryTheory.Iso.hom	—	—
copy_π 📖	mathematical	—	π copy CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct K CategoryTheory.Iso.hom H CategoryTheory.Iso.inv	—	—
cyclesIso_hom_comp_i 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.cycles K CategoryTheory.ShortComplex.X₂ CategoryTheory.Iso.hom cyclesIso i CategoryTheory.ShortComplex.iCycles	—	CategoryTheory.ShortComplex.cyclesMap'_i CategoryTheory.Category.comp_id
cyclesIso_hom_comp_i_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.cycles K CategoryTheory.Iso.hom cyclesIso CategoryTheory.ShortComplex.X₂ i CategoryTheory.ShortComplex.iCycles	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesIso_hom_comp_i
cyclesIso_inv_comp_iCycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct K CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.X₂ CategoryTheory.Iso.inv cyclesIso CategoryTheory.ShortComplex.iCycles i	—	cyclesIso_hom_comp_i CategoryTheory.Iso.inv_hom_id_assoc
cyclesIso_inv_comp_iCycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct K CategoryTheory.ShortComplex.cycles CategoryTheory.Iso.inv cyclesIso CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.iCycles i	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesIso_inv_comp_iCycles
f'_i 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ K CategoryTheory.ShortComplex.X₂ f' i CategoryTheory.ShortComplex.f	—	liftK_i CategoryTheory.ShortComplex.zero
f'_i_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ K f' CategoryTheory.ShortComplex.X₂ i CategoryTheory.ShortComplex.f	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' f'_i
f'_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ K H f' π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	wπ
f'_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ K f' H π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' f'_π
instEpiπ 📖	mathematical	—	CategoryTheory.Epi K H π	—	CategoryTheory.Limits.Cofork.IsColimit.hom_ext CategoryTheory.ShortComplex.zero wi wπ
instMonoI 📖	mathematical	—	CategoryTheory.Mono K CategoryTheory.ShortComplex.X₂ i	—	CategoryTheory.Limits.Fork.IsLimit.hom_ext wi
isIso_i 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.IsIso K i	—	CategoryTheory.Category.id_comp CategoryTheory.cancel_mono instMonoI CategoryTheory.Category.assoc liftK_i CategoryTheory.Category.comp_id
isIso_π 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.IsIso K H π	—	f'_π CategoryTheory.cancel_mono instMonoI CategoryTheory.Category.comp_id f'_i CategoryTheory.Limits.zero_comp CategoryTheory.cancel_epi instEpiπ CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker'
leftHomologyπ_comp_leftHomologyIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.leftHomology H CategoryTheory.ShortComplex.leftHomologyπ CategoryTheory.Iso.hom leftHomologyIso K cyclesIso π	—	CategoryTheory.ShortComplex.leftHomologyπ_naturality'
leftHomologyπ_comp_leftHomologyIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.leftHomology CategoryTheory.ShortComplex.leftHomologyπ H CategoryTheory.Iso.hom leftHomologyIso K cyclesIso π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftHomologyπ_comp_leftHomologyIso_hom
liftCycles_comp_cyclesIso_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.ShortComplex.cycles K CategoryTheory.ShortComplex.liftCycles CategoryTheory.Iso.hom cyclesIso liftK	—	CategoryTheory.cancel_mono instMonoI CategoryTheory.Category.assoc cyclesIso_hom_comp_i CategoryTheory.ShortComplex.liftCycles_i liftK_i
liftCycles_comp_cyclesIso_hom_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.liftCycles K CategoryTheory.Iso.hom cyclesIso liftK	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' liftCycles_comp_cyclesIso_hom
liftK_i 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	K liftK i	—	CategoryTheory.Limits.IsLimit.fac wi
liftK_i_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	K liftK i	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' liftK_i
liftK_π_eq_zero_of_boundary 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	K H liftK π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc f'_π CategoryTheory.Limits.comp_zero liftK.congr_simp CategoryTheory.cancel_mono instMonoI liftK_i f'_i
liftK_π_eq_zero_of_boundary_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	K liftK H π Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' liftK_π_eq_zero_of_boundary
lift_K_comp_cyclesIso_inv 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	K CategoryTheory.ShortComplex.cycles liftK CategoryTheory.Iso.inv cyclesIso CategoryTheory.ShortComplex.liftCycles	—	liftCycles_comp_cyclesIso_hom CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
lift_K_comp_cyclesIso_inv_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	K liftK CategoryTheory.ShortComplex.cycles CategoryTheory.Iso.inv cyclesIso CategoryTheory.ShortComplex.liftCycles	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_K_comp_cyclesIso_inv
ofEpiOfIsIsoOfMono'_H 📖	mathematical	—	H ofEpiOfIsIsoOfMono'	—	—
ofEpiOfIsIsoOfMono'_K 📖	mathematical	—	K ofEpiOfIsIsoOfMono'	—	—
ofEpiOfIsIsoOfMono'_f' 📖	mathematical	—	f' ofEpiOfIsIsoOfMono' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ K CategoryTheory.ShortComplex.Hom.τ₁	—	CategoryTheory.cancel_mono instMonoI f'_i ofEpiOfIsIsoOfMono'_i CategoryTheory.Category.assoc f'_i_assoc CategoryTheory.ShortComplex.Hom.comm₁₂_assoc CategoryTheory.IsIso.hom_inv_id CategoryTheory.Category.comp_id
ofEpiOfIsIsoOfMono'_i 📖	mathematical	—	i ofEpiOfIsIsoOfMono' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct K CategoryTheory.ShortComplex.X₂ CategoryTheory.inv CategoryTheory.ShortComplex.Hom.τ₂	—	—
ofEpiOfIsIsoOfMono'_π 📖	mathematical	—	π ofEpiOfIsIsoOfMono'	—	—
ofEpiOfIsIsoOfMono_H 📖	mathematical	—	H ofEpiOfIsIsoOfMono	—	—
ofEpiOfIsIsoOfMono_K 📖	mathematical	—	K ofEpiOfIsIsoOfMono	—	—
ofEpiOfIsIsoOfMono_i 📖	mathematical	—	i ofEpiOfIsIsoOfMono CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct K CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.Hom.τ₂	—	—
ofEpiOfIsIsoOfMono_π 📖	mathematical	—	π ofEpiOfIsIsoOfMono	—	—
ofHasCokernel_H 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	H ofHasCokernel CategoryTheory.Limits.cokernel CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f	—	—
ofHasCokernel_K 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	K ofHasCokernel	—	—
ofHasCokernel_i 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	i ofHasCokernel CategoryTheory.CategoryStruct.id	—	—
ofHasCokernel_π 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	π ofHasCokernel CategoryTheory.Limits.cokernel.π CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f	—	—
ofHasKernelOfHasCokernel_H 📖	mathematical	—	H ofHasKernelOfHasCokernel CategoryTheory.Limits.cokernel CategoryTheory.ShortComplex.X₁ CategoryTheory.Limits.kernel CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g CategoryTheory.Limits.kernel.lift CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.zero	—	CategoryTheory.ShortComplex.zero
ofHasKernelOfHasCokernel_K 📖	mathematical	—	K ofHasKernelOfHasCokernel CategoryTheory.Limits.kernel CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	CategoryTheory.ShortComplex.zero
ofHasKernelOfHasCokernel_i 📖	mathematical	—	i ofHasKernelOfHasCokernel CategoryTheory.Limits.kernel.ι CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	CategoryTheory.ShortComplex.zero
ofHasKernelOfHasCokernel_π 📖	mathematical	—	π ofHasKernelOfHasCokernel CategoryTheory.Limits.cokernel.π CategoryTheory.ShortComplex.X₁ CategoryTheory.Limits.kernel CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g CategoryTheory.Limits.kernel.lift CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.zero	—	CategoryTheory.ShortComplex.zero
ofIsColimitCokernelCofork_H 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	H ofIsColimitCokernelCofork CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f	—	—
ofIsColimitCokernelCofork_K 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	K ofIsColimitCokernelCofork	—	—
ofIsColimitCokernelCofork_f' 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	f' ofIsColimitCokernelCofork CategoryTheory.ShortComplex.f	—	—
ofIsColimitCokernelCofork_i 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	i ofIsColimitCokernelCofork CategoryTheory.CategoryStruct.id	—	—
ofIsColimitCokernelCofork_π 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	π ofIsColimitCokernelCofork CategoryTheory.Limits.Cofork.π CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f	—	—
ofIsLimitKernelFork_H 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	H ofIsLimitKernelFork CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	—
ofIsLimitKernelFork_K 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	K ofIsLimitKernelFork CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	—
ofIsLimitKernelFork_f' 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	f' ofIsLimitKernelFork K	—	CategoryTheory.cancel_mono instMonoI f'_i CategoryTheory.Limits.zero_comp
ofIsLimitKernelFork_i 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	i ofIsLimitKernelFork CategoryTheory.Limits.Fork.ι CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	—
ofIsLimitKernelFork_π 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	π ofIsLimitKernelFork CategoryTheory.CategoryStruct.id CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	—
ofZeros_H 📖	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₃	H ofZeros	—	—
ofZeros_K 📖	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₃	K ofZeros	—	—
ofZeros_f' 📖	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₃	f' ofZeros K	—	CategoryTheory.cancel_mono instMonoI CategoryTheory.Limits.zero_comp f'_i
ofZeros_i 📖	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₃	i ofZeros CategoryTheory.CategoryStruct.id	—	—
ofZeros_π 📖	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₃	π ofZeros CategoryTheory.CategoryStruct.id	—	—
wi 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct K CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ i CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
wi_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct K CategoryTheory.ShortComplex.X₂ i CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' wi
wπ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.KernelFork.ofι CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.zero K i wi H CategoryTheory.Limits.IsLimit.lift hi π	—	—
wπ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.KernelFork.ofι CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.zero K i wi CategoryTheory.Limits.IsLimit.lift hi H π	—	CategoryTheory.ShortComplex.zero wi CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' wπ
π_comp_leftHomologyIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct K H CategoryTheory.ShortComplex.leftHomology π CategoryTheory.Iso.inv leftHomologyIso CategoryTheory.ShortComplex.cycles cyclesIso CategoryTheory.ShortComplex.leftHomologyπ	—	CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id leftHomologyπ_comp_leftHomologyIso_hom
π_comp_leftHomologyIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct K H π CategoryTheory.ShortComplex.leftHomology CategoryTheory.Iso.inv leftHomologyIso CategoryTheory.ShortComplex.cycles cyclesIso CategoryTheory.ShortComplex.leftHomologyπ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_comp_leftHomologyIso_inv
π_descH 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ K f' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	H π descH	—	CategoryTheory.Limits.IsColimit.fac CategoryTheory.ShortComplex.zero wi wπ
π_descH_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ K f' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	H π descH	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_descH
τ₁_ofEpiOfIsIsoOfMono_f' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ K ofEpiOfIsIsoOfMono CategoryTheory.ShortComplex.Hom.τ₁ f'	—	CategoryTheory.cancel_mono instMonoI CategoryTheory.Category.assoc f'_i ofEpiOfIsIsoOfMono_i f'_i_assoc CategoryTheory.ShortComplex.Hom.comm₁₂

CategoryTheory.ShortComplex.LeftHomologyMapData

Definitions

Name	Category	Theorems
comp 📖	CompOp	3 math math: CategoryTheory.ShortComplex.HomologyMapData.comp_left, comp_φH, comp_φK
compatibilityOfZerosOfIsColimitCokernelCofork 📖	CompOp	2 math math: compatibilityOfZerosOfIsColimitCokernelCofork_φK, compatibilityOfZerosOfIsColimitCokernelCofork_φH
compatibilityOfZerosOfIsLimitKernelFork 📖	CompOp	3 math math: CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_left, compatibilityOfZerosOfIsLimitKernelFork_φH, compatibilityOfZerosOfIsLimitKernelFork_φK
id 📖	CompOp	3 math math: id_φK, id_φH, CategoryTheory.ShortComplex.HomologyMapData.id_left
instInhabited 📖	CompOp	—
instUnique 📖	CompOp	—
ofEpiOfIsIsoOfMono 📖	CompOp	2 math math: ofEpiOfIsIsoOfMono_φK, ofEpiOfIsIsoOfMono_φH
ofEpiOfIsIsoOfMono' 📖	CompOp	2 math math: ofEpiOfIsIsoOfMono'_φK, ofEpiOfIsIsoOfMono'_φH
ofIsColimitCokernelCofork 📖	CompOp	3 math math: ofIsColimitCokernelCofork_φK, CategoryTheory.ShortComplex.HomologyMapData.ofIsColimitCokernelCofork_left, ofIsColimitCokernelCofork_φH
ofIsLimitKernelFork 📖	CompOp	3 math math: CategoryTheory.ShortComplex.HomologyMapData.ofIsLimitKernelFork_left, ofIsLimitKernelFork_φK, ofIsLimitKernelFork_φH
ofZeros 📖	CompOp	3 math math: ofZeros_φK, CategoryTheory.ShortComplex.HomologyMapData.ofZeros_left, ofZeros_φH
zero 📖	CompOp	3 math math: CategoryTheory.ShortComplex.HomologyMapData.zero_left, zero_φH, zero_φK
φH 📖	CompOp	33 math math: id_φH, CategoryTheory.ShortComplex.RightHomologyMapData.op_φH, map_φH, op_φH, smul_φH, CategoryTheory.ShortComplex.HomologyMapData.congr_left_φH, homologyMap_comm, neg_φH, homologyMap_eq, commπ, quasiIso_map_iff, ofEpiOfIsIsoOfMono'_φH, comp_φH, add_φH, leftHomologyMap_comm, leftHomologyMap_eq, compatibilityOfZerosOfIsLimitKernelFork_φH, zero_φH, CategoryTheory.ShortComplex.HomologyMapData.comm, CategoryTheory.ShortComplex.HomologyMapData.comm_assoc, congr_φH, natTransApp_φH, CategoryTheory.ShortComplex.HomologyMapData.homologyMap'_eq, unop_φH, leftHomologyMap'_eq, quasiIso_iff, ofIsLimitKernelFork_φH, ofEpiOfIsIsoOfMono_φH, commπ_assoc, compatibilityOfZerosOfIsColimitCokernelCofork_φH, ofZeros_φH, CategoryTheory.ShortComplex.RightHomologyMapData.unop_φH, ofIsColimitCokernelCofork_φH
φK 📖	CompOp	30 math math: unop_φQ, id_φK, commf', compatibilityOfZerosOfIsColimitCokernelCofork_φK, CategoryTheory.ShortComplex.RightHomologyMapData.op_φK, op_φQ, CategoryTheory.ShortComplex.RightHomologyMapData.unop_φK, commπ, ofEpiOfIsIsoOfMono'_φK, ofZeros_φK, natTransApp_φK, CategoryTheory.ShortComplex.HomologyMapData.cyclesMap'_eq, cyclesMap_comm, zero_φK, commi_assoc, smul_φK, ofEpiOfIsIsoOfMono_φK, neg_φK, comp_φK, congr_φK, ofIsLimitKernelFork_φK, commf'_assoc, add_φK, ofIsColimitCokernelCofork_φK, cyclesMap_eq, commi, compatibilityOfZerosOfIsLimitKernelFork_φK, commπ_assoc, cyclesMap'_eq, map_φK

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commf' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.LeftHomologyData.K CategoryTheory.ShortComplex.LeftHomologyData.f' φK CategoryTheory.ShortComplex.Hom.τ₁	—	—
commf'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.LeftHomologyData.K CategoryTheory.ShortComplex.LeftHomologyData.f' φK CategoryTheory.ShortComplex.Hom.τ₁	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' commf'
commi 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.LeftHomologyData.K CategoryTheory.ShortComplex.X₂ φK CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.Hom.τ₂	—	—
commi_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.LeftHomologyData.K φK CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.Hom.τ₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' commi
commπ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.LeftHomologyData.K CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.ShortComplex.LeftHomologyData.π φH φK	—	—
commπ_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.LeftHomologyData.K CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.ShortComplex.LeftHomologyData.π φH φK	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' commπ
comp_φH 📖	mathematical	—	φH CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory comp CategoryTheory.ShortComplex.LeftHomologyData.H	—	—
comp_φK 📖	mathematical	—	φK CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory comp CategoryTheory.ShortComplex.LeftHomologyData.K	—	—
compatibilityOfZerosOfIsColimitCokernelCofork_φH 📖	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₃	φH CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.LeftHomologyData.ofZeros CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork compatibilityOfZerosOfIsColimitCokernelCofork CategoryTheory.Limits.Cofork.π	—	—
compatibilityOfZerosOfIsColimitCokernelCofork_φK 📖	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₃	φK CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.LeftHomologyData.ofZeros CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork compatibilityOfZerosOfIsColimitCokernelCofork CategoryTheory.ShortComplex.LeftHomologyData.K	—	—
compatibilityOfZerosOfIsLimitKernelFork_φH 📖	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₃	φH CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork CategoryTheory.ShortComplex.LeftHomologyData.ofZeros compatibilityOfZerosOfIsLimitKernelFork CategoryTheory.Limits.Fork.ι	—	—
compatibilityOfZerosOfIsLimitKernelFork_φK 📖	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₃	φK CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork CategoryTheory.ShortComplex.LeftHomologyData.ofZeros compatibilityOfZerosOfIsLimitKernelFork CategoryTheory.Limits.Fork.ι	—	—
congr_φH 📖	mathematical	—	φH	—	—
congr_φK 📖	mathematical	—	φK	—	—
cyclesMap'_eq 📖	mathematical	—	CategoryTheory.ShortComplex.cyclesMap' φK	—	congr_φK instSubsingleton
cyclesMap_comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.LeftHomologyData.K CategoryTheory.ShortComplex.cyclesMap CategoryTheory.Iso.hom CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso φK	—	cyclesMap_eq CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
cyclesMap_eq 📖	mathematical	—	CategoryTheory.ShortComplex.cyclesMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.LeftHomologyData.K CategoryTheory.Iso.hom CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso φK CategoryTheory.Iso.inv	—	cyclesMap'_eq CategoryTheory.ShortComplex.cyclesMap'_comp CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
id_φH 📖	mathematical	—	φH CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory id CategoryTheory.ShortComplex.LeftHomologyData.H	—	—
id_φK 📖	mathematical	—	φK CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory id CategoryTheory.ShortComplex.LeftHomologyData.K	—	—
instSubsingleton 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyMapData	—	CategoryTheory.cancel_mono CategoryTheory.ShortComplex.LeftHomologyData.instMonoI commi CategoryTheory.cancel_epi CategoryTheory.ShortComplex.LeftHomologyData.instEpiπ commπ
leftHomologyMap'_eq 📖	mathematical	—	CategoryTheory.ShortComplex.leftHomologyMap' φH	—	congr_φH instSubsingleton
leftHomologyMap_comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.leftHomology CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.ShortComplex.leftHomologyMap CategoryTheory.Iso.hom CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso φH	—	leftHomologyMap_eq CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
leftHomologyMap_eq 📖	mathematical	—	CategoryTheory.ShortComplex.leftHomologyMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.leftHomology CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.Iso.hom CategoryTheory.ShortComplex.LeftHomologyData.leftHomologyIso φH CategoryTheory.Iso.inv	—	leftHomologyMap'_eq CategoryTheory.ShortComplex.leftHomologyMap'_comp CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
ofEpiOfIsIsoOfMono'_φH 📖	mathematical	—	φH CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' ofEpiOfIsIsoOfMono' CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.LeftHomologyData.H	—	—
ofEpiOfIsIsoOfMono'_φK 📖	mathematical	—	φK CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono' ofEpiOfIsIsoOfMono' CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.LeftHomologyData.K	—	—
ofEpiOfIsIsoOfMono_φH 📖	mathematical	—	φH CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono ofEpiOfIsIsoOfMono CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.LeftHomologyData.H	—	—
ofEpiOfIsIsoOfMono_φK 📖	mathematical	—	φK CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono ofEpiOfIsIsoOfMono CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.LeftHomologyData.K	—	—
ofIsColimitCokernelCofork_φH 📖	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.π	φH CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork ofIsColimitCokernelCofork	—	—
ofIsColimitCokernelCofork_φK 📖	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.π	φK CategoryTheory.ShortComplex.LeftHomologyData.ofIsColimitCokernelCofork ofIsColimitCokernelCofork	—	—
ofIsLimitKernelFork_φH 📖	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.τ₂	φH CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork ofIsLimitKernelFork	—	—
ofIsLimitKernelFork_φK 📖	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.τ₂	φK CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork ofIsLimitKernelFork	—	—
ofZeros_φH 📖	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₃	φH CategoryTheory.ShortComplex.LeftHomologyData.ofZeros ofZeros CategoryTheory.ShortComplex.Hom.τ₂	—	—
ofZeros_φK 📖	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₃	φK CategoryTheory.ShortComplex.LeftHomologyData.ofZeros ofZeros CategoryTheory.ShortComplex.Hom.τ₂	—	—
zero_φH 📖	mathematical	—	φH Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instZeroHom zero CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
zero_φK 📖	mathematical	—	φK Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instZeroHom zero CategoryTheory.ShortComplex.LeftHomologyData.K CategoryTheory.Limits.HasZeroMorphisms.zero	—	—

---

← Back to Index