RightHomology

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

Statistics

Metric	Count
Definitions HasRightHomology, op, unop, op, unop, RightHomologyData, H, Q, copy, descH, descQ, g', hp, hι, hι', liftH, ofEpiOfIsIsoOfMono, ofEpiOfIsIsoOfMono', ofHasCokernel, ofHasCokernelOfHasKernel, ofHasKernel, ofIsColimitCokernelCofork, ofIsLimitKernelFork, ofIso, ofZeros, op, opcyclesIso, p, rightHomologyIso, unop, ι, RightHomologyMapData, comp, compatibilityOfZerosOfIsColimitCokernelCofork, compatibilityOfZerosOfIsLimitKernelFork, id, instInhabited, instUnique, ofEpiOfIsIsoOfMono, ofEpiOfIsIsoOfMono', ofIsColimitCokernelCofork, ofIsLimitKernelFork, ofZeros, op, unop, zero, φH, φQ, cyclesOpIso, descOpcycles, descRightHomology, fromOpcycles, fromOpcyclesNatTrans, isoOpcyclesOfIsColimit, leftHomologyFunctorOpNatIso, leftHomologyOpIso, opcycles, opcyclesFunctor, opcyclesIsCokernel, opcyclesIsoCokernel, opcyclesIsoRightHomology, opcyclesIsoX₂, opcyclesMap, opcyclesMap', opcyclesMapIso, opcyclesMapIso', opcyclesOpIso, pOpcycles, pOpcyclesNatTrans, rightHomology, rightHomologyData, rightHomologyFunctor, rightHomologyFunctorOpNatIso, rightHomologyIsKernel, rightHomologyIsoKernelDesc, rightHomologyMap, rightHomologyMap', rightHomologyMapData, rightHomologyMapIso, rightHomologyMapIso', rightHomologyOpIso, rightHomologyι, rightHomologyιNatTrans	83
Theorems condition, hasCokernel, hasKernel, mk', of_hasCokernel, of_hasCokernel_of_hasKernel, of_hasKernel, of_zeros, op_H, op_Q, op_g', op_p, op_ι, unop_H, unop_Q, unop_g', unop_p, unop_ι, op_φH, op_φQ, unop_φH, unop_φQ, copy_H, copy_Q, copy_p, copy_ι, instEpiP, instMonoι, isIso_p, isIso_ι, liftH_ι, liftH_ι_assoc, ofEpiOfIsIsoOfMono'_H, ofEpiOfIsIsoOfMono'_Q, ofEpiOfIsIsoOfMono'_g'_τ₃, ofEpiOfIsIsoOfMono'_p, ofEpiOfIsIsoOfMono'_ι, ofEpiOfIsIsoOfMono_H, ofEpiOfIsIsoOfMono_Q, ofEpiOfIsIsoOfMono_g', ofEpiOfIsIsoOfMono_p, ofEpiOfIsIsoOfMono_ι, ofHasCokernelOfHasKernel_H, ofHasCokernelOfHasKernel_Q, ofHasCokernelOfHasKernel_p, ofHasCokernelOfHasKernel_ι, ofHasKernel_H, ofHasKernel_Q, ofHasKernel_p, ofHasKernel_ι, ofIsColimitCokernelCofork_H, ofIsColimitCokernelCofork_Q, ofIsColimitCokernelCofork_g', ofIsColimitCokernelCofork_p, ofIsColimitCokernelCofork_ι, ofIsLimitKernelFork_H, ofIsLimitKernelFork_Q, ofIsLimitKernelFork_g', ofIsLimitKernelFork_p, ofIsLimitKernelFork_ι, ofZeros_H, ofZeros_Q, ofZeros_g', ofZeros_p, ofZeros_ι, op_H, op_K, op_f', op_i, op_π, opcyclesIso_hom_comp_descQ, opcyclesIso_inv_comp_descOpcycles, opcyclesIso_inv_comp_descOpcycles_assoc, pOpcycles_comp_opcyclesIso_hom, pOpcycles_comp_opcyclesIso_hom_assoc, p_comp_opcyclesIso_inv, p_comp_opcyclesIso_inv_assoc, p_descQ, p_descQ_assoc, p_g', p_g'_assoc, rightHomologyIso_hom_comp_ι, rightHomologyIso_hom_comp_ι_assoc, rightHomologyIso_inv_comp_rightHomologyι, rightHomologyIso_inv_comp_rightHomologyι_assoc, unop_H, unop_K, unop_f', unop_i, unop_π, wp, wp_assoc, wι, wι_assoc, ι_descQ_eq_zero_of_boundary, ι_descQ_eq_zero_of_boundary_assoc, ι_g', ι_g'_assoc, commg', commg'_assoc, commp, commp_assoc, commι, commι_assoc, comp_φH, comp_φQ, compatibilityOfZerosOfIsColimitCokernelCofork_φH, compatibilityOfZerosOfIsColimitCokernelCofork_φQ, compatibilityOfZerosOfIsLimitKernelFork_φH, compatibilityOfZerosOfIsLimitKernelFork_φQ, congr_φH, congr_φQ, id_φH, id_φQ, instSubsingleton, ofEpiOfIsIsoOfMono'_φH, ofEpiOfIsIsoOfMono'_φQ, ofEpiOfIsIsoOfMono_φH, ofEpiOfIsIsoOfMono_φQ, ofIsColimitCokernelCofork_φH, ofIsColimitCokernelCofork_φQ, ofIsLimitKernelFork_φH, ofIsLimitKernelFork_φQ, ofZeros_φH, ofZeros_φQ, op_φH, op_φK, opcyclesMap'_eq, opcyclesMap_comm, opcyclesMap_eq, rightHomologyMap'_eq, rightHomologyMap_comm, rightHomologyMap_eq, unop_φH, unop_φK, zero_φH, zero_φQ, cyclesOpIso_hom_naturality, cyclesOpIso_hom_naturality_assoc, cyclesOpIso_inv_naturality, cyclesOpIso_inv_naturality_assoc, cyclesOpIso_inv_op_iCycles, cyclesOpIso_inv_op_iCycles_assoc, descOpcycles_comp, descOpcycles_comp_assoc, f_pOpcycles, f_pOpcycles_assoc, fromOpcyclesNatTrans_app, fromOpcycles_naturality, fromOpcycles_naturality_assoc, fromOpcycles_op_cyclesOpIso_inv, fromOpcycles_op_cyclesOpIso_inv_assoc, hasLeftHomology_iff_op, hasLeftHomology_iff_unop, hasRightHomology_iff_op, hasRightHomology_iff_unop, hasRightHomology_of_epi_of_isIso_of_mono, hasRightHomology_of_epi_of_isIso_of_mono', hasRightHomology_of_iso, instEpiPOpcycles, instHasLeftHomologyOppositeOpOfHasRightHomology, instHasRightHomologyOppositeOpOfHasLeftHomology, instIsIsoRightHomologyMap'OfEpiτ₁Ofτ₂OfMonoτ₃, instIsIsoRightHomologyMapOfEpiτ₁Ofτ₂OfMonoτ₃, instMonoRightHomologyι, isIso_opcyclesMap'_of_isIso, isIso_opcyclesMap'_of_isIso_of_epi, isIso_opcyclesMap_of_isIso_of_epi, isIso_opcyclesMap_of_isIso_of_epi', isIso_opcyclesMap_of_iso, isIso_pOpcycles, isIso_rightHomologyMap'_of_isIso, isIso_rightHomologyMap_of_iso, isIso_rightHomologyι, leftHomologyFunctorOpNatIso_hom_app, leftHomologyFunctorOpNatIso_inv_app, leftHomologyMap'_op, leftHomologyMap_op, op_pOpcycles_opcyclesOpIso_hom, op_pOpcycles_opcyclesOpIso_hom_assoc, opcyclesFunctor_map, opcyclesFunctor_obj, opcyclesIsoCokernel_hom, opcyclesIsoCokernel_inv, opcyclesIsoRightHomology_hom_inv_id, opcyclesIsoRightHomology_hom_inv_id_assoc, opcyclesIsoRightHomology_inv, opcyclesIsoRightHomology_inv_hom_id, opcyclesIsoRightHomology_inv_hom_id_assoc, opcyclesIsoX₂_hom_inv_id, opcyclesIsoX₂_hom_inv_id_assoc, opcyclesIsoX₂_inv, opcyclesIsoX₂_inv_hom_id, opcyclesIsoX₂_inv_hom_id_assoc, opcyclesMap'_comp, opcyclesMap'_comp_assoc, opcyclesMap'_g', opcyclesMap'_g'_assoc, opcyclesMap'_id, opcyclesMap'_zero, opcyclesMapIso'_hom, opcyclesMapIso'_inv, opcyclesMapIso_hom, opcyclesMapIso_inv, opcyclesMap_comp, opcyclesMap_comp_descOpcycles, opcyclesMap_comp_descOpcycles_assoc, opcyclesMap_id, opcyclesMap_zero, opcyclesOpIso_hom_naturality, opcyclesOpIso_hom_naturality_assoc, opcyclesOpIso_hom_toCycles_op, opcyclesOpIso_hom_toCycles_op_assoc, opcyclesOpIso_inv_naturality, opcyclesOpIso_inv_naturality_assoc, opcycles_ext, opcycles_ext_iff, pOpcyclesNatTrans_app, pOpcycles_π_isoOpcyclesOfIsColimit_inv, pOpcycles_π_isoOpcyclesOfIsColimit_inv_assoc, p_descOpcycles, p_descOpcycles_assoc, p_fromOpcycles, p_fromOpcycles_assoc, p_opcyclesMap, p_opcyclesMap', p_opcyclesMap'_assoc, p_opcyclesMap_assoc, rightHomologyData_H, rightHomologyFunctorOpNatIso_hom_app, rightHomologyFunctorOpNatIso_inv_app, rightHomologyFunctor_map, rightHomologyFunctor_obj, rightHomologyMap'_comp, rightHomologyMap'_comp_assoc, rightHomologyMap'_id, rightHomologyMap'_op, rightHomologyMap'_zero, rightHomologyMapIso'_hom, rightHomologyMapIso'_inv, rightHomologyMapIso_hom, rightHomologyMapIso_inv, rightHomologyMap_comp, rightHomologyMap_id, rightHomologyMap_op, rightHomologyMap_zero, rightHomology_ext, rightHomology_ext_iff, rightHomologyιNatTrans_app, rightHomologyι_comp_fromOpcycles, rightHomologyι_comp_fromOpcycles_assoc, rightHomologyι_descOpcycles_π_eq_zero_of_boundary, rightHomologyι_descOpcycles_π_eq_zero_of_boundary_assoc, rightHomologyι_naturality, rightHomologyι_naturality', rightHomologyι_naturality'_assoc, rightHomologyι_naturality_assoc, π_isoOpcyclesOfIsColimit_hom, π_isoOpcyclesOfIsColimit_hom_assoc	259
Total	342

CategoryTheory.ShortComplex

Definitions

Name	Category	Theorems
HasRightHomology 📖	CompData	16 math math: hasRightHomology_iff_op, hasLeftHomology_iff_op, hasLeftHomology_iff_unop, hasRightHomology_of_epi_of_isIso_of_mono', hasRightHomology_of_preserves', hasRightHomology_of_preserves, HasRightHomology.of_hasCokernel, hasRightHomology_iff_unop, HasRightHomology.mk', HasRightHomology.of_hasKernel, hasRightHomology_of_epi_of_isIso_of_mono, hasRightHomology_of_iso, hasRightHomology_of_hasHomology, HasRightHomology.of_hasCokernel_of_hasKernel, HasRightHomology.of_zeros, instHasRightHomologyOppositeOpOfHasLeftHomology
RightHomologyData 📖	CompData	1 math math: HasRightHomology.condition
RightHomologyMapData 📖	CompData	1 math math: RightHomologyMapData.instSubsingleton
cyclesOpIso 📖	CompOp	8 math math: cyclesOpIso_inv_op_iCycles_assoc, cyclesOpIso_hom_naturality, fromOpcycles_op_cyclesOpIso_inv_assoc, cyclesOpIso_inv_naturality, cyclesOpIso_inv_op_iCycles, cyclesOpIso_inv_naturality_assoc, fromOpcycles_op_cyclesOpIso_inv, cyclesOpIso_hom_naturality_assoc
descOpcycles 📖	CompOp	15 math math: opcyclesMap_comp_descOpcycles, quasiIso_iff_isIso_descOpcycles, homologyι_descOpcycles_eq_zero_of_boundary, rightHomologyι_descOpcycles_π_eq_zero_of_boundary, opcyclesIsoCokernel_hom, descOpcycles_comp_assoc, p_descOpcycles_assoc, RightHomologyData.opcyclesIso_hom_comp_descQ, rightHomologyι_descOpcycles_π_eq_zero_of_boundary_assoc, homologyι_descOpcycles_eq_zero_of_boundary_assoc, RightHomologyData.opcyclesIso_inv_comp_descOpcycles_assoc, RightHomologyData.opcyclesIso_inv_comp_descOpcycles, p_descOpcycles, opcyclesMap_comp_descOpcycles_assoc, descOpcycles_comp
descRightHomology 📖	CompOp	—
fromOpcycles 📖	CompOp	20 math math: fromOpcycles_naturality, HomologicalComplex.opcyclesIsoSc'_inv_fromOpcycles, HomologicalComplex.opcyclesIsoSc'_inv_fromOpcycles_assoc, p_fromOpcycles, HomologyData.ofEpiMonoFactorisation.g'_eq, homologyι_comp_fromOpcycles_assoc, fromOpcycles_naturality_assoc, fromOpcycles_op_cyclesOpIso_inv_assoc, opcyclesOpIso_hom_toCycles_op_assoc, rightHomologyι_comp_fromOpcycles_assoc, RightHomologyData.canonical_g', Exact.mono_fromOpcycles, homologyι_comp_fromOpcycles, exact_iff_mono_fromOpcycles, fromOpcyclesNatTrans_app, opcyclesOpIso_hom_toCycles_op, rightHomologyι_comp_fromOpcycles, p_fromOpcycles_assoc, fromOpcycles_op_cyclesOpIso_inv, Exact.isIso_fromOpcycles
fromOpcyclesNatTrans 📖	CompOp	1 math math: fromOpcyclesNatTrans_app
isoOpcyclesOfIsColimit 📖	CompOp	11 math math: pOpcycles_π_isoOpcyclesOfIsColimit_inv_assoc, HomologyData.ofEpiMonoFactorisation.isoHomology_inv_homologyι_assoc, HomologyData.ofEpiMonoFactorisation.isoImage_ι, HomologyData.ofEpiMonoFactorisation.g'_eq, HomologyData.ofEpiMonoFactorisation.isoHomology_inv_homologyι, pOpcycles_π_isoOpcyclesOfIsColimit_inv, HomologyData.ofEpiMonoFactorisation.isoHomology_hom_comp_ι_assoc, π_isoOpcyclesOfIsColimit_hom_assoc, HomologyData.ofEpiMonoFactorisation.isoHomology_hom_comp_ι, π_isoOpcyclesOfIsColimit_hom, HomologyData.ofEpiMonoFactorisation.isoImage_ι_assoc
leftHomologyFunctorOpNatIso 📖	CompOp	2 math math: leftHomologyFunctorOpNatIso_hom_app, leftHomologyFunctorOpNatIso_inv_app
leftHomologyOpIso 📖	CompOp	3 math math: rightHomologyMap_op, rightHomologyFunctorOpNatIso_hom_app, rightHomologyFunctorOpNatIso_inv_app
opcycles 📖	CompOp	150 math math: opcyclesMap_smul, pOpcycles_comp_moduleCatOpcyclesIso_hom_apply, homologyι_naturality, fromOpcycles_naturality, opcyclesIsoRightHomology_hom_inv_id, cyclesOpIso_inv_op_iCycles_assoc, pOpcycles_π_isoOpcyclesOfIsColimit_inv_assoc, opcyclesMap_comp_descOpcycles, homology_π_ι_assoc, HomologicalComplex.pOpcycles_opcyclesIsoSc'_hom, RightHomologyData.canonical_Q, HomologicalComplex.opcyclesIsoSc'_inv_fromOpcycles, mapOpcyclesIso_hom_naturality_assoc, RightHomologyData.p_comp_opcyclesIso_inv, exact_iff_iCycles_pOpcycles_zero, opcyclesMap_sub, groupHomology.comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top, RightHomologyData.rightHomologyIso_hom_comp_ι, HomologicalComplex.opcyclesIsoSc'_inv_fromOpcycles_assoc, opcyclesIsoRightHomology_inv_hom_id_assoc, RightHomologyData.homologyIso_inv_comp_homologyι, HomologyData.ofEpiMonoFactorisation.isoHomology_inv_homologyι_assoc, HomologicalComplex.pOpcycles_opcyclesIsoSc'_inv_assoc, op_pOpcycles_opcyclesOpIso_hom, HomologyData.ofEpiMonoFactorisation.isoImage_ι, CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles_fac_assoc, RightHomologyData.homologyIso_hom_comp_ι, p_fromOpcycles, HomologicalComplex.pOpcycles_opcyclesIsoSc'_inv, mapOpcyclesIso_inv_naturality, cyclesOpIso_hom_naturality, pOpcycles_comp_moduleCatOpcyclesIso_hom, isIso_pOpcycles, homology_π_ι, homologyι_naturality_assoc, opcyclesOpIso_hom_naturality_assoc, opcyclesMap_add, HomologyData.canonical_right_Q, instEpiPOpcycles, HomologyData.ofEpiMonoFactorisation.g'_eq, RightHomologyData.mapOpcyclesIso_eq, RightHomologyMapData.opcyclesMap_comm, moduleCat_pOpcycles_eq_zero_iff, opcyclesIsoCokernel_inv, op_pOpcycles_opcyclesOpIso_hom_assoc, RightHomologyData.p_comp_opcyclesIso_inv_assoc, homologyι_comp_fromOpcycles_assoc, HomologicalComplex.homologyIsoSc'_hom_ι_assoc, quasiIso_iff_isIso_descOpcycles, HomologyData.ofEpiMonoFactorisation.isoHomology_inv_homologyι, CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles_hom_fac_assoc, CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles_hom_fac, fromOpcycles_naturality_assoc, opcyclesMap_neg, opcyclesMapIso_inv, fromOpcycles_op_cyclesOpIso_inv_assoc, homologyι_descOpcycles_eq_zero_of_boundary, CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles_fac, opcyclesOpIso_hom_toCycles_op_assoc, rightHomologyι_comp_fromOpcycles_assoc, opcyclesOpIso_hom_naturality, rightHomologyι_descOpcycles_π_eq_zero_of_boundary, opcyclesIsoRightHomology_inv_hom_id, rightHomologyIso_hom_comp_homologyι, cyclesOpIso_inv_naturality, opcyclesIsoCokernel_hom, isIso_homologyι, RightHomologyData.homologyIso_hom_comp_ι_assoc, opcyclesIsoX₂_inv_hom_id_assoc, RightHomologyData.pOpcycles_comp_opcyclesIso_hom, opcyclesMapIso_hom, π_leftRightHomologyComparison_ι_assoc, RightHomologyData.homologyIso_inv_comp_homologyι_assoc, homologyι_comp_asIsoHomologyι_inv, descOpcycles_comp_assoc, opcyclesOpIso_inv_naturality, pOpcycles_comp_moduleCatOpcyclesIso_hom_assoc, Exact.mono_fromOpcycles, isIso_rightHomologyι, RightHomologyData.rightHomologyIso_hom_comp_ι_assoc, opcyclesIsoX₂_inv_hom_id, p_descOpcycles_assoc, RightHomologyData.opcyclesIso_hom_comp_descQ, opcyclesMap_zero, opcyclesMap_comp, pOpcycles_π_isoOpcyclesOfIsColimit_inv, p_opcyclesMap_assoc, isIso_opcyclesMap_of_iso, rightHomologyι_descOpcycles_π_eq_zero_of_boundary_assoc, homologyIsoImageICyclesCompPOpcycles_ι, π_homologyMap_ι_assoc, HomologicalComplex.homologyIsoSc'_inv_ι, homologyι_comp_fromOpcycles, opcyclesIsoX₂_hom_inv_id_assoc, HomologicalComplex.pOpcycles_opcyclesIsoSc'_hom_assoc, RightHomologyData.rightHomologyIso_inv_comp_rightHomologyι_assoc, HomologyData.ofEpiMonoFactorisation.isoHomology_hom_comp_ι_assoc, homologyι_descOpcycles_eq_zero_of_boundary_assoc, isIso_opcyclesMap_of_isIso_of_epi', rightHomologyIso_hom_comp_homologyι_assoc, π_leftRightHomologyComparison_ι, asIsoHomologyι_hom, opcyclesFunctor_obj, mapOpcyclesIso_inv_naturality_assoc, opcyclesIsoX₂_inv, exact_iff_mono_fromOpcycles, opcyclesIsoRightHomology_hom_inv_id_assoc, opcyclesIsoRightHomology_inv, π_isoOpcyclesOfIsColimit_hom_assoc, moduleCat_pOpcycles_eq_iff, RightHomologyData.rightHomologyIso_inv_comp_rightHomologyι, HomologicalComplex.homologyIsoSc'_inv_ι_assoc, RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc, isIso_opcyclesMap_of_isIso_of_epi, rightHomology_ext_iff, opcyclesOpIso_hom_toCycles_op, rightHomologyι_comp_fromOpcycles, RightHomologyMapData.opcyclesMap_eq, mapOpcyclesIso_hom_naturality, cyclesOpIso_inv_op_iCycles, cyclesOpIso_inv_naturality_assoc, instMonoRightHomologyι, p_fromOpcycles_assoc, opcyclesMap_id, RightHomologyData.opcyclesIso_inv_comp_descOpcycles_assoc, fromOpcycles_op_cyclesOpIso_inv, HomologicalComplex.homologyIsoSc'_hom_ι, RightHomologyData.opcyclesIso_inv_comp_descOpcycles, rightHomologyι_naturality, instMonoHomologyι, HomologyData.ofEpiMonoFactorisation.isoHomology_hom_comp_ι, opcyclesOpIso_inv_naturality_assoc, homologyι_comp_asIsoHomologyι_inv_assoc, π_isoOpcyclesOfIsColimit_hom, opcyclesIsoX₂_hom_inv_id, HomologyData.ofEpiMonoFactorisation.isoImage_ι_assoc, homologyIsoImageICyclesCompPOpcycles_ι_assoc, Exact.isIso_fromOpcycles, p_opcyclesMap, p_descOpcycles, opcycles_ext_iff, asIsoHomologyι_inv_comp_homologyι_assoc, opcyclesMap_comp_descOpcycles_assoc, rightHomologyι_naturality_assoc, f_pOpcycles, descOpcycles_comp, f_pOpcycles_assoc, π_homologyMap_ι, cyclesOpIso_hom_naturality_assoc, asIsoHomologyι_inv_comp_homologyι
opcyclesFunctor 📖	CompOp	7 math math: rightHomologyιNatTrans_app, opcyclesFunctor_linear, opcyclesFunctor_additive, opcyclesFunctor_map, opcyclesFunctor_obj, fromOpcyclesNatTrans_app, pOpcyclesNatTrans_app
opcyclesIsCokernel 📖	CompOp	—
opcyclesIsoCokernel 📖	CompOp	2 math math: opcyclesIsoCokernel_inv, opcyclesIsoCokernel_hom
opcyclesIsoRightHomology 📖	CompOp	5 math math: opcyclesIsoRightHomology_hom_inv_id, opcyclesIsoRightHomology_inv_hom_id_assoc, opcyclesIsoRightHomology_inv_hom_id, opcyclesIsoRightHomology_hom_inv_id_assoc, opcyclesIsoRightHomology_inv
opcyclesIsoX₂ 📖	CompOp	5 math math: opcyclesIsoX₂_inv_hom_id_assoc, opcyclesIsoX₂_inv_hom_id, opcyclesIsoX₂_hom_inv_id_assoc, opcyclesIsoX₂_inv, opcyclesIsoX₂_hom_inv_id
opcyclesMap 📖	CompOp	37 math math: opcyclesMap_smul, homologyι_naturality, fromOpcycles_naturality, opcyclesMap_comp_descOpcycles, mapOpcyclesIso_hom_naturality_assoc, opcyclesMap_sub, mapOpcyclesIso_inv_naturality, cyclesOpIso_hom_naturality, homologyι_naturality_assoc, opcyclesOpIso_hom_naturality_assoc, opcyclesMap_add, RightHomologyMapData.opcyclesMap_comm, fromOpcycles_naturality_assoc, opcyclesMap_neg, opcyclesMapIso_inv, opcyclesOpIso_hom_naturality, cyclesOpIso_inv_naturality, opcyclesMapIso_hom, opcyclesOpIso_inv_naturality, opcyclesMap_zero, opcyclesMap_comp, p_opcyclesMap_assoc, isIso_opcyclesMap_of_iso, opcyclesFunctor_map, isIso_opcyclesMap_of_isIso_of_epi', mapOpcyclesIso_inv_naturality_assoc, isIso_opcyclesMap_of_isIso_of_epi, RightHomologyMapData.opcyclesMap_eq, mapOpcyclesIso_hom_naturality, cyclesOpIso_inv_naturality_assoc, opcyclesMap_id, rightHomologyι_naturality, opcyclesOpIso_inv_naturality_assoc, p_opcyclesMap, opcyclesMap_comp_descOpcycles_assoc, rightHomologyι_naturality_assoc, cyclesOpIso_hom_naturality_assoc
opcyclesMap' 📖	CompOp	21 math math: opcyclesMap'_g', opcyclesMap'_sub, opcyclesMap'_g'_assoc, rightHomologyι_naturality'_assoc, RightHomologyMapData.opcyclesMap'_eq, opcyclesMapIso'_inv, opcyclesMap'_id, isIso_opcyclesMap'_of_isIso, HomologyMapData.opcyclesMap'_eq, p_opcyclesMap', opcyclesMap'_comp_assoc, rightHomologyι_naturality', opcyclesMapIso'_hom, isIso_opcyclesMap'_of_isIso_of_epi, opcyclesMap'_add, p_opcyclesMap'_assoc, RightHomologyData.map_opcyclesMap', opcyclesMap'_comp, opcyclesMap'_neg, opcyclesMap'_smul, opcyclesMap'_zero
opcyclesMapIso 📖	CompOp	2 math math: opcyclesMapIso_inv, opcyclesMapIso_hom
opcyclesMapIso' 📖	CompOp	2 math math: opcyclesMapIso'_inv, opcyclesMapIso'_hom
opcyclesOpIso 📖	CompOp	8 math math: op_pOpcycles_opcyclesOpIso_hom, opcyclesOpIso_hom_naturality_assoc, op_pOpcycles_opcyclesOpIso_hom_assoc, opcyclesOpIso_hom_toCycles_op_assoc, opcyclesOpIso_hom_naturality, opcyclesOpIso_inv_naturality, opcyclesOpIso_hom_toCycles_op, opcyclesOpIso_inv_naturality_assoc
pOpcycles 📖	CompOp	57 math math: pOpcycles_comp_moduleCatOpcyclesIso_hom_apply, cyclesOpIso_inv_op_iCycles_assoc, pOpcycles_π_isoOpcyclesOfIsColimit_inv_assoc, homology_π_ι_assoc, HomologicalComplex.pOpcycles_opcyclesIsoSc'_hom, RightHomologyData.p_comp_opcyclesIso_inv, exact_iff_iCycles_pOpcycles_zero, groupHomology.comap_coinvariantsKer_pOpcycles_range_subtype_pOpcycles_eq_top, HomologicalComplex.pOpcycles_opcyclesIsoSc'_inv_assoc, op_pOpcycles_opcyclesOpIso_hom, HomologyData.ofEpiMonoFactorisation.isoImage_ι, CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles_fac_assoc, p_fromOpcycles, HomologicalComplex.pOpcycles_opcyclesIsoSc'_inv, pOpcycles_comp_moduleCatOpcyclesIso_hom, isIso_pOpcycles, homology_π_ι, instEpiPOpcycles, moduleCat_pOpcycles_eq_zero_iff, opcyclesIsoCokernel_inv, op_pOpcycles_opcyclesOpIso_hom_assoc, RightHomologyData.p_comp_opcyclesIso_inv_assoc, CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles_hom_fac_assoc, CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles_hom_fac, CategoryTheory.ComposableArrows.IsComplex.opcyclesToCycles_fac, HomologyData.canonical_right_p, opcyclesIsoX₂_inv_hom_id_assoc, RightHomologyData.pOpcycles_comp_opcyclesIso_hom, π_leftRightHomologyComparison_ι_assoc, pOpcycles_comp_moduleCatOpcyclesIso_hom_assoc, opcyclesIsoX₂_inv_hom_id, p_descOpcycles_assoc, RightHomologyData.canonical_p, pOpcycles_π_isoOpcyclesOfIsColimit_inv, p_opcyclesMap_assoc, homologyIsoImageICyclesCompPOpcycles_ι, π_homologyMap_ι_assoc, opcyclesIsoX₂_hom_inv_id_assoc, HomologicalComplex.pOpcycles_opcyclesIsoSc'_hom_assoc, π_leftRightHomologyComparison_ι, opcyclesIsoX₂_inv, π_isoOpcyclesOfIsColimit_hom_assoc, moduleCat_pOpcycles_eq_iff, RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc, cyclesOpIso_inv_op_iCycles, p_fromOpcycles_assoc, pOpcyclesNatTrans_app, π_isoOpcyclesOfIsColimit_hom, opcyclesIsoX₂_hom_inv_id, HomologyData.ofEpiMonoFactorisation.isoImage_ι_assoc, homologyIsoImageICyclesCompPOpcycles_ι_assoc, p_opcyclesMap, p_descOpcycles, opcycles_ext_iff, f_pOpcycles, f_pOpcycles_assoc, π_homologyMap_ι
pOpcyclesNatTrans 📖	CompOp	1 math math: pOpcyclesNatTrans_app
rightHomology 📖	CompOp	63 math math: rightHomologyMap_id, opcyclesIsoRightHomology_hom_inv_id, RightHomologyData.homologyIso_hom_comp_rightHomologyIso_inv, RightHomologyData.rightHomologyIso_hom_comp_ι, opcyclesIsoRightHomology_inv_hom_id_assoc, isIso_leftRightHomologyComparison, leftRightHomologyComparison_fac, leftHomologyMap_op, rightHomologyMapIso_inv, rightHomologyFunctor_obj, mapRightHomologyIso_inv_naturality, RightHomologyData.homologyIso_hom_comp_rightHomologyIso_inv_assoc, RightHomologyMapData.rightHomologyMap_eq, rightHomologyMap_comp, rightHomologyι_comp_fromOpcycles_assoc, rightHomologyι_descOpcycles_π_eq_zero_of_boundary, rightHomologyIso_inv_naturality_assoc, opcyclesIsoRightHomology_inv_hom_id, rightHomologyIso_hom_comp_homologyι, mapRightHomologyIso_hom_naturality, RightHomologyMapData.rightHomologyMap_comm, mapRightHomologyIso_inv_naturality_assoc, leftRightHomologyComparison_eq, rightHomologyMap_zero, π_leftRightHomologyComparison_ι_assoc, rightHomologyMapIso_hom, RightHomologyData.rightHomologyIso_hom_comp_homologyIso_inv_assoc, isIso_rightHomologyMap_of_iso, isIso_rightHomologyι, RightHomologyData.rightHomologyIso_hom_comp_ι_assoc, rightHomologyMap_sub, rightHomologyMap_op, rightHomologyFunctorOpNatIso_hom_app, RightHomologyData.mapRightHomologyIso_eq, rightHomologyMap_nullHomotopic, rightHomologyIso_hom_naturality_assoc, rightHomologyMap_add, rightHomologyι_descOpcycles_π_eq_zero_of_boundary_assoc, leftHomologyFunctorOpNatIso_hom_app, rightHomologyData_H, RightHomologyData.rightHomologyIso_inv_comp_rightHomologyι_assoc, rightHomologyIso_hom_comp_homologyι_assoc, π_leftRightHomologyComparison_ι, rightHomologyMap_neg, rightHomologyIso_inv_naturality, rightHomologyFunctorOpNatIso_inv_app, mapRightHomologyIso_hom_naturality_assoc, opcyclesIsoRightHomology_hom_inv_id_assoc, opcyclesIsoRightHomology_inv, exact_iff_isZero_rightHomology, RightHomologyData.rightHomologyIso_inv_comp_rightHomologyι, rightHomology_ext_iff, rightHomologyι_comp_fromOpcycles, rightHomologyIso_hom_naturality, leftHomologyFunctorOpNatIso_inv_app, RightHomologyData.rightHomologyIso_hom_comp_homologyIso_inv, rightHomologyMap_smul, instMonoRightHomologyι, instIsIsoRightHomologyMapOfEpiτ₁Ofτ₂OfMonoτ₃, rightHomologyι_naturality, leftRightHomologyComparison_fac_assoc, RightHomologyData.homologyIso_rightHomologyData, rightHomologyι_naturality_assoc
rightHomologyData 📖	CompOp	2 math math: rightHomologyData_H, RightHomologyData.homologyIso_rightHomologyData
rightHomologyFunctor 📖	CompOp	9 math math: rightHomologyιNatTrans_app, rightHomologyFunctor_linear, rightHomologyFunctor_obj, rightHomologyFunctor_additive, rightHomologyFunctorOpNatIso_hom_app, leftHomologyFunctorOpNatIso_hom_app, rightHomologyFunctorOpNatIso_inv_app, leftHomologyFunctorOpNatIso_inv_app, rightHomologyFunctor_map
rightHomologyFunctorOpNatIso 📖	CompOp	2 math math: rightHomologyFunctorOpNatIso_hom_app, rightHomologyFunctorOpNatIso_inv_app
rightHomologyIsKernel 📖	CompOp	—
rightHomologyIsoKernelDesc 📖	CompOp	—
rightHomologyMap 📖	CompOp	28 math math: rightHomologyMap_id, leftHomologyMap_op, rightHomologyMapIso_inv, mapRightHomologyIso_inv_naturality, RightHomologyMapData.rightHomologyMap_eq, rightHomologyMap_comp, rightHomologyIso_inv_naturality_assoc, mapRightHomologyIso_hom_naturality, RightHomologyMapData.rightHomologyMap_comm, mapRightHomologyIso_inv_naturality_assoc, rightHomologyMap_zero, rightHomologyMapIso_hom, isIso_rightHomologyMap_of_iso, rightHomologyMap_sub, rightHomologyMap_op, rightHomologyMap_nullHomotopic, rightHomologyIso_hom_naturality_assoc, rightHomologyMap_add, rightHomologyMap_neg, rightHomologyIso_inv_naturality, mapRightHomologyIso_hom_naturality_assoc, Homotopy.rightHomologyMap_congr, rightHomologyIso_hom_naturality, rightHomologyMap_smul, instIsIsoRightHomologyMapOfEpiτ₁Ofτ₂OfMonoτ₃, rightHomologyFunctor_map, rightHomologyι_naturality, rightHomologyι_naturality_assoc
rightHomologyMap' 📖	CompOp	29 math math: quasiIso_iff_isIso_rightHomologyMap', RightHomologyData.rightHomologyIso_inv_naturality_assoc, rightHomologyι_naturality'_assoc, rightHomologyMap'_id, RightHomologyData.rightHomologyIso_hom_naturality, Homotopy.rightHomologyMap'_congr, RightHomologyData.rightHomologyIso_inv_naturality, RightHomologyData.map_rightHomologyMap', rightHomologyMap'_op, rightHomologyMap'_add, rightHomologyMapIso'_inv, RightHomologyMapData.rightHomologyMap'_eq, rightHomologyMap'_nullHomotopic, rightHomologyι_naturality', leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap', instIsIsoRightHomologyMap'OfEpiτ₁Ofτ₂OfMonoτ₃, isIso_rightHomologyMap'_of_isIso, rightHomologyMap'_comp, rightHomologyMap'_sub, rightHomologyMapIso'_hom, rightHomologyMap'_comp_assoc, leftRightHomologyComparison'_naturality_assoc, RightHomologyData.rightHomologyIso_hom_naturality_assoc, rightHomologyMap'_neg, leftRightHomologyComparison'_naturality, rightHomologyMap'_smul, leftRightHomologyComparison'_compatibility, rightHomologyMap'_zero, leftHomologyMap'_op
rightHomologyMapData 📖	CompOp	—
rightHomologyMapIso 📖	CompOp	2 math math: rightHomologyMapIso_inv, rightHomologyMapIso_hom
rightHomologyMapIso' 📖	CompOp	2 math math: rightHomologyMapIso'_inv, rightHomologyMapIso'_hom
rightHomologyOpIso 📖	CompOp	3 math math: leftHomologyMap_op, leftHomologyFunctorOpNatIso_hom_app, leftHomologyFunctorOpNatIso_inv_app
rightHomologyι 📖	CompOp	23 math math: opcyclesIsoRightHomology_hom_inv_id, RightHomologyData.rightHomologyIso_hom_comp_ι, rightHomologyιNatTrans_app, opcyclesIsoRightHomology_inv_hom_id_assoc, rightHomologyι_comp_fromOpcycles_assoc, rightHomologyι_descOpcycles_π_eq_zero_of_boundary, opcyclesIsoRightHomology_inv_hom_id, rightHomologyIso_hom_comp_homologyι, π_leftRightHomologyComparison_ι_assoc, isIso_rightHomologyι, RightHomologyData.rightHomologyIso_hom_comp_ι_assoc, rightHomologyι_descOpcycles_π_eq_zero_of_boundary_assoc, RightHomologyData.rightHomologyIso_inv_comp_rightHomologyι_assoc, rightHomologyIso_hom_comp_homologyι_assoc, π_leftRightHomologyComparison_ι, opcyclesIsoRightHomology_hom_inv_id_assoc, opcyclesIsoRightHomology_inv, RightHomologyData.rightHomologyIso_inv_comp_rightHomologyι, rightHomology_ext_iff, rightHomologyι_comp_fromOpcycles, instMonoRightHomologyι, rightHomologyι_naturality, rightHomologyι_naturality_assoc
rightHomologyιNatTrans 📖	CompOp	1 math math: rightHomologyιNatTrans_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cyclesOpIso_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite cycles CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasLeftHomologyOppositeOpOfHasRightHomology Opposite.op opcycles cyclesMap opMap CategoryTheory.Iso.hom cyclesOpIso CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver opcyclesMap	—	instHasLeftHomologyOppositeOpOfHasRightHomology CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id cyclesOpIso_inv_naturality CategoryTheory.Iso.hom_inv_id_assoc
cyclesOpIso_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite cycles CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasLeftHomologyOppositeOpOfHasRightHomology cyclesMap opMap Opposite.op opcycles CategoryTheory.Iso.hom cyclesOpIso Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver opcyclesMap	—	instHasLeftHomologyOppositeOpOfHasRightHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesOpIso_hom_naturality
cyclesOpIso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op opcycles cycles CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasLeftHomologyOppositeOpOfHasRightHomology Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver opcyclesMap CategoryTheory.Iso.inv cyclesOpIso cyclesMap opMap	—	instHasLeftHomologyOppositeOpOfHasRightHomology CategoryTheory.cancel_mono instMonoICycles CategoryTheory.Category.assoc cyclesOpIso_inv_op_iCycles cyclesMap_i cyclesOpIso_inv_op_iCycles_assoc CategoryTheory.op_comp p_opcyclesMap opMap_τ₂
cyclesOpIso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite Opposite.op opcycles Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver opcyclesMap cycles CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasLeftHomologyOppositeOpOfHasRightHomology CategoryTheory.Iso.inv cyclesOpIso cyclesMap opMap	—	instHasLeftHomologyOppositeOpOfHasRightHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesOpIso_inv_naturality
cyclesOpIso_inv_op_iCycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op opcycles cycles CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasLeftHomologyOppositeOpOfHasRightHomology X₂ CategoryTheory.Iso.inv cyclesOpIso iCycles Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver pOpcycles	—	instHasLeftHomologyOppositeOpOfHasRightHomology LeftHomologyData.cyclesIso_hom_comp_i CategoryTheory.Iso.inv_hom_id_assoc
cyclesOpIso_inv_op_iCycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite Opposite.op opcycles cycles CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasLeftHomologyOppositeOpOfHasRightHomology CategoryTheory.Iso.inv cyclesOpIso X₂ iCycles Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver pOpcycles	—	instHasLeftHomologyOppositeOpOfHasRightHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesOpIso_inv_op_iCycles
descOpcycles_comp 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ X₂ f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	opcycles descOpcycles	—	CategoryTheory.cancel_epi instEpiPOpcycles p_descOpcycles_assoc p_descOpcycles
descOpcycles_comp_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ X₂ f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	opcycles descOpcycles	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' descOpcycles_comp
f_pOpcycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ X₂ opcycles f pOpcycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	RightHomologyData.wp
f_pOpcycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ X₂ f opcycles pOpcycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' f_pOpcycles
fromOpcyclesNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ShortComplex instCategory opcyclesFunctor π₃ fromOpcyclesNatTrans fromOpcycles	—	—
fromOpcycles_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles X₃ opcyclesMap fromOpcycles Hom.τ₃	—	opcyclesMap'_g'
fromOpcycles_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles opcyclesMap X₃ fromOpcycles Hom.τ₃	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fromOpcycles_naturality
fromOpcycles_op_cyclesOpIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op X₃ opcycles cycles CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasLeftHomologyOppositeOpOfHasRightHomology Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver fromOpcycles CategoryTheory.Iso.inv cyclesOpIso toCycles	—	instHasLeftHomologyOppositeOpOfHasRightHomology CategoryTheory.cancel_mono instMonoICycles CategoryTheory.Category.assoc toCycles_i LeftHomologyData.cyclesIso_inv_comp_iCycles RightHomologyData.op_i CategoryTheory.op_comp RightHomologyData.p_g' op_f
fromOpcycles_op_cyclesOpIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite Opposite.op X₃ opcycles Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver fromOpcycles cycles CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasLeftHomologyOppositeOpOfHasRightHomology CategoryTheory.Iso.inv cyclesOpIso toCycles	—	instHasLeftHomologyOppositeOpOfHasRightHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' fromOpcycles_op_cyclesOpIso_inv
hasLeftHomology_iff_op 📖	mathematical	—	HasLeftHomology HasRightHomology Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite op	—	instHasRightHomologyOppositeOpOfHasLeftHomology HasLeftHomology.mk'
hasLeftHomology_iff_unop 📖	mathematical	—	HasLeftHomology Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite HasRightHomology unop	—	hasRightHomology_iff_op
hasRightHomology_iff_op 📖	mathematical	—	HasRightHomology HasLeftHomology Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite op	—	instHasLeftHomologyOppositeOpOfHasRightHomology HasRightHomology.mk'
hasRightHomology_iff_unop 📖	mathematical	—	HasRightHomology Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite HasLeftHomology unop	—	hasLeftHomology_iff_op
hasRightHomology_of_epi_of_isIso_of_mono 📖	mathematical	—	HasRightHomology	—	HasRightHomology.mk'
hasRightHomology_of_epi_of_isIso_of_mono' 📖	mathematical	—	HasRightHomology	—	HasRightHomology.mk'
hasRightHomology_of_iso 📖	mathematical	—	HasRightHomology	—	hasRightHomology_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τ₃
instEpiPOpcycles 📖	mathematical	—	CategoryTheory.Epi X₂ opcycles pOpcycles	—	RightHomologyData.instEpiP
instHasLeftHomologyOppositeOpOfHasRightHomology 📖	mathematical	—	HasLeftHomology Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite op	—	HasLeftHomology.mk'
instHasRightHomologyOppositeOpOfHasLeftHomology 📖	mathematical	—	HasRightHomology Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite op	—	HasRightHomology.mk'
instIsIsoRightHomologyMap'OfEpiτ₁Ofτ₂OfMonoτ₃ 📖	mathematical	—	CategoryTheory.IsIso RightHomologyData.H rightHomologyMap'	—	rightHomologyMap'_comp CategoryTheory.Category.comp_id CategoryTheory.IsIso.comp_isIso RightHomologyMapData.rightHomologyMap'_eq CategoryTheory.IsIso.id isIso_rightHomologyMap'_of_isIso
instIsIsoRightHomologyMapOfEpiτ₁Ofτ₂OfMonoτ₃ 📖	mathematical	—	CategoryTheory.IsIso rightHomology rightHomologyMap	—	instIsIsoRightHomologyMap'OfEpiτ₁Ofτ₂OfMonoτ₃
instMonoRightHomologyι 📖	mathematical	—	CategoryTheory.Mono rightHomology opcycles rightHomologyι	—	RightHomologyData.instMonoι
isIso_opcyclesMap'_of_isIso 📖	mathematical	—	CategoryTheory.IsIso RightHomologyData.Q opcyclesMap'	—	CategoryTheory.Iso.isIso_hom
isIso_opcyclesMap'_of_isIso_of_epi 📖	mathematical	—	CategoryTheory.IsIso RightHomologyData.Q opcyclesMap'	—	CategoryTheory.cancel_epi Hom.comm₁₂_assoc CategoryTheory.IsIso.hom_inv_id_assoc RightHomologyData.wp CategoryTheory.Limits.comp_zero RightHomologyData.instEpiP p_opcyclesMap'_assoc RightHomologyData.p_descQ CategoryTheory.Category.comp_id RightHomologyData.p_descQ_assoc CategoryTheory.Category.assoc p_opcyclesMap' CategoryTheory.IsIso.inv_hom_id_assoc
isIso_opcyclesMap_of_isIso_of_epi 📖	mathematical	—	CategoryTheory.IsIso opcycles opcyclesMap	—	isIso_opcyclesMap_of_isIso_of_epi'
isIso_opcyclesMap_of_isIso_of_epi' 📖	mathematical	—	CategoryTheory.IsIso opcycles opcyclesMap	—	isIso_opcyclesMap'_of_isIso_of_epi
isIso_opcyclesMap_of_iso 📖	mathematical	—	CategoryTheory.IsIso opcycles opcyclesMap	—	CategoryTheory.Iso.isIso_hom
isIso_pOpcycles 📖	mathematical	f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.IsIso opcycles pOpcycles	—	RightHomologyData.isIso_p
isIso_rightHomologyMap'_of_isIso 📖	mathematical	—	CategoryTheory.IsIso RightHomologyData.H rightHomologyMap'	—	CategoryTheory.Iso.isIso_hom
isIso_rightHomologyMap_of_iso 📖	mathematical	—	CategoryTheory.IsIso rightHomology rightHomologyMap	—	CategoryTheory.Iso.isIso_hom
isIso_rightHomologyι 📖	mathematical	g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.IsIso rightHomology opcycles rightHomologyι	—	RightHomologyData.isIso_ι
leftHomologyFunctorOpNatIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.ShortComplex CategoryTheory.Category.opposite instCategory CategoryTheory.Functor.op leftHomologyFunctor CategoryTheory.Functor.comp CategoryTheory.Limits.hasZeroMorphismsOpposite opFunctor rightHomologyFunctor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category leftHomologyFunctorOpNatIso CategoryTheory.Iso.inv rightHomology op Opposite.unop Opposite.op leftHomology rightHomologyOpIso	—	—
leftHomologyFunctorOpNatIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.ShortComplex CategoryTheory.Category.opposite instCategory CategoryTheory.Functor.comp CategoryTheory.Limits.hasZeroMorphismsOpposite opFunctor rightHomologyFunctor CategoryTheory.Functor.op leftHomologyFunctor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category leftHomologyFunctorOpNatIso CategoryTheory.Iso.hom rightHomology op Opposite.unop Opposite.op leftHomology rightHomologyOpIso	—	—
leftHomologyMap'_op 📖	mathematical	—	Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct LeftHomologyData.H leftHomologyMap' rightHomologyMap' Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite op opMap LeftHomologyData.op	—	LeftHomologyMapData.leftHomologyMap'_eq RightHomologyMapData.rightHomologyMap'_eq
leftHomologyMap_op 📖	mathematical	—	Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct leftHomology leftHomologyMap CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite Opposite.op rightHomology CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasRightHomologyOppositeOpOfHasLeftHomology CategoryTheory.Iso.inv rightHomologyOpIso rightHomologyMap opMap CategoryTheory.Iso.hom	—	instHasRightHomologyOppositeOpOfHasLeftHomology leftHomologyMap'_op CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
op_pOpcycles_opcyclesOpIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct X₂ CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite op opcycles instHasRightHomologyOppositeOpOfHasLeftHomology Opposite.op cycles pOpcycles CategoryTheory.Iso.hom opcyclesOpIso Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver iCycles	—	instHasRightHomologyOppositeOpOfHasLeftHomology RightHomologyData.p_comp_opcyclesIso_inv CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
op_pOpcycles_opcyclesOpIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite X₂ CategoryTheory.Limits.hasZeroMorphismsOpposite op opcycles instHasRightHomologyOppositeOpOfHasLeftHomology pOpcycles Opposite.op cycles CategoryTheory.Iso.hom opcyclesOpIso Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver iCycles	—	instHasRightHomologyOppositeOpOfHasLeftHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' op_pOpcycles_opcyclesOpIso_hom
opcyclesFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.ShortComplex instCategory opcyclesFunctor opcyclesMap	—	—
opcyclesFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.ShortComplex instCategory opcyclesFunctor opcycles	—	—
opcyclesIsoCokernel_hom 📖	mathematical	—	CategoryTheory.Iso.hom opcycles CategoryTheory.Limits.cokernel X₁ X₂ f opcyclesIsoCokernel descOpcycles CategoryTheory.Limits.cokernel.π	—	—
opcyclesIsoCokernel_inv 📖	mathematical	—	CategoryTheory.Iso.inv opcycles CategoryTheory.Limits.cokernel X₁ X₂ f opcyclesIsoCokernel CategoryTheory.Limits.cokernel.desc pOpcycles	—	—
opcyclesIsoRightHomology_hom_inv_id 📖	mathematical	g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp opcycles rightHomology CategoryTheory.Iso.hom opcyclesIsoRightHomology rightHomologyι CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.hom_inv_id
opcyclesIsoRightHomology_hom_inv_id_assoc 📖	mathematical	g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp opcycles rightHomology CategoryTheory.Iso.hom opcyclesIsoRightHomology rightHomologyι	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' opcyclesIsoRightHomology_hom_inv_id
opcyclesIsoRightHomology_inv 📖	mathematical	g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Iso.inv opcycles rightHomology opcyclesIsoRightHomology rightHomologyι	—	—
opcyclesIsoRightHomology_inv_hom_id 📖	mathematical	g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp rightHomology opcycles rightHomologyι CategoryTheory.Iso.hom opcyclesIsoRightHomology CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.inv_hom_id
opcyclesIsoRightHomology_inv_hom_id_assoc 📖	mathematical	g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₂ X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp rightHomology opcycles rightHomologyι CategoryTheory.Iso.hom opcyclesIsoRightHomology	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' opcyclesIsoRightHomology_inv_hom_id
opcyclesIsoX₂_hom_inv_id 📖	mathematical	f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp opcycles CategoryTheory.Iso.hom opcyclesIsoX₂ pOpcycles CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.hom_inv_id
opcyclesIsoX₂_hom_inv_id_assoc 📖	mathematical	f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp opcycles CategoryTheory.Iso.hom opcyclesIsoX₂ pOpcycles	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' opcyclesIsoX₂_hom_inv_id
opcyclesIsoX₂_inv 📖	mathematical	f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.Iso.inv opcycles opcyclesIsoX₂ pOpcycles	—	—
opcyclesIsoX₂_inv_hom_id 📖	mathematical	f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp opcycles pOpcycles CategoryTheory.Iso.hom opcyclesIsoX₂ CategoryTheory.CategoryStruct.id	—	CategoryTheory.Iso.inv_hom_id
opcyclesIsoX₂_inv_hom_id_assoc 📖	mathematical	f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X₁ X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.CategoryStruct.comp opcycles pOpcycles CategoryTheory.Iso.hom opcyclesIsoX₂	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' opcyclesIsoX₂_inv_hom_id
opcyclesMap'_comp 📖	mathematical	—	opcyclesMap' CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory RightHomologyData.Q	—	RightHomologyMapData.opcyclesMap'_eq RightHomologyMapData.comp_φQ
opcyclesMap'_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct RightHomologyData.Q opcyclesMap' CategoryTheory.ShortComplex instCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesMap'_comp
opcyclesMap'_g' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct RightHomologyData.Q X₃ opcyclesMap' RightHomologyData.g' Hom.τ₃	—	CategoryTheory.cancel_epi RightHomologyData.instEpiP p_opcyclesMap'_assoc RightHomologyData.p_g' Hom.comm₂₃ RightHomologyData.p_g'_assoc
opcyclesMap'_g'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct RightHomologyData.Q opcyclesMap' X₃ RightHomologyData.g' Hom.τ₃	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesMap'_g'
opcyclesMap'_id 📖	mathematical	—	opcyclesMap' CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory RightHomologyData.Q	—	RightHomologyMapData.opcyclesMap'_eq
opcyclesMap'_zero 📖	mathematical	—	opcyclesMap' Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instZeroHom RightHomologyData.Q CategoryTheory.Limits.HasZeroMorphisms.zero	—	RightHomologyMapData.opcyclesMap'_eq
opcyclesMapIso'_hom 📖	mathematical	—	CategoryTheory.Iso.hom RightHomologyData.Q opcyclesMapIso' opcyclesMap' CategoryTheory.ShortComplex instCategory	—	—
opcyclesMapIso'_inv 📖	mathematical	—	CategoryTheory.Iso.inv RightHomologyData.Q opcyclesMapIso' opcyclesMap' CategoryTheory.ShortComplex instCategory	—	—
opcyclesMapIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom opcycles opcyclesMapIso opcyclesMap CategoryTheory.ShortComplex instCategory	—	—
opcyclesMapIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv opcycles opcyclesMapIso opcyclesMap CategoryTheory.ShortComplex instCategory	—	—
opcyclesMap_comp 📖	mathematical	—	opcyclesMap CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory opcycles	—	opcyclesMap'_comp
opcyclesMap_comp_descOpcycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ X₂ f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	opcycles opcyclesMap descOpcycles Hom.τ₂	—	CategoryTheory.cancel_epi instEpiPOpcycles p_opcyclesMap_assoc p_descOpcycles
opcyclesMap_comp_descOpcycles_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ X₂ f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	opcycles opcyclesMap descOpcycles Hom.τ₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesMap_comp_descOpcycles
opcyclesMap_id 📖	mathematical	—	opcyclesMap CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory opcycles	—	opcyclesMap'_id
opcyclesMap_zero 📖	mathematical	—	opcyclesMap Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instZeroHom opcycles CategoryTheory.Limits.HasZeroMorphisms.zero	—	opcyclesMap'_zero
opcyclesOpIso_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite opcycles CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasRightHomologyOppositeOpOfHasLeftHomology Opposite.op cycles opcyclesMap opMap CategoryTheory.Iso.hom opcyclesOpIso CategoryTheory.CategoryStruct.opposite Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver cyclesMap	—	instHasRightHomologyOppositeOpOfHasLeftHomology CategoryTheory.cancel_epi instEpiPOpcycles p_opcyclesMap_assoc opMap_τ₂ op_pOpcycles_opcyclesOpIso_hom op_pOpcycles_opcyclesOpIso_hom_assoc CategoryTheory.op_comp cyclesMap_i
opcyclesOpIso_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite opcycles CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasRightHomologyOppositeOpOfHasLeftHomology opcyclesMap opMap Opposite.op cycles CategoryTheory.Iso.hom opcyclesOpIso Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver cyclesMap	—	instHasRightHomologyOppositeOpOfHasLeftHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesOpIso_hom_naturality
opcyclesOpIso_hom_toCycles_op 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct opcycles CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasRightHomologyOppositeOpOfHasLeftHomology Opposite.op cycles X₁ CategoryTheory.Iso.hom opcyclesOpIso Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver toCycles fromOpcycles	—	instHasRightHomologyOppositeOpOfHasLeftHomology CategoryTheory.cancel_epi instEpiPOpcycles p_fromOpcycles RightHomologyData.pOpcycles_comp_opcyclesIso_hom_assoc LeftHomologyData.op_p CategoryTheory.op_comp LeftHomologyData.f'_i op_g
opcyclesOpIso_hom_toCycles_op_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite opcycles CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasRightHomologyOppositeOpOfHasLeftHomology Opposite.op cycles CategoryTheory.Iso.hom opcyclesOpIso X₁ Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver toCycles fromOpcycles	—	instHasRightHomologyOppositeOpOfHasLeftHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesOpIso_hom_toCycles_op
opcyclesOpIso_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op cycles opcycles CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasRightHomologyOppositeOpOfHasLeftHomology Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver cyclesMap CategoryTheory.Iso.inv opcyclesOpIso opcyclesMap opMap	—	instHasRightHomologyOppositeOpOfHasLeftHomology CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.hom_inv_id_assoc opcyclesOpIso_hom_naturality_assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id
opcyclesOpIso_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite Opposite.op cycles Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver cyclesMap opcycles CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasRightHomologyOppositeOpOfHasLeftHomology CategoryTheory.Iso.inv opcyclesOpIso opcyclesMap opMap	—	instHasRightHomologyOppositeOpOfHasLeftHomology CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesOpIso_inv_naturality
opcycles_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ opcycles pOpcycles	—	—	—
opcycles_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ opcycles pOpcycles	—	CategoryTheory.cancel_epi instEpiPOpcycles
pOpcyclesNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ShortComplex instCategory π₂ opcyclesFunctor pOpcyclesNatTrans pOpcycles	—	—
pOpcycles_π_isoOpcyclesOfIsColimit_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ opcycles CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair X₁ f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero pOpcycles CategoryTheory.Iso.inv isoOpcyclesOfIsColimit CategoryTheory.Limits.Cofork.π	—	CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv f_pOpcycles
pOpcycles_π_isoOpcyclesOfIsColimit_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ opcycles pOpcycles CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair X₁ f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Iso.inv isoOpcyclesOfIsColimit CategoryTheory.Limits.Cofork.π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pOpcycles_π_isoOpcyclesOfIsColimit_inv
p_descOpcycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ X₂ f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	opcycles pOpcycles descOpcycles	—	RightHomologyData.p_descQ
p_descOpcycles_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₁ X₂ f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	opcycles pOpcycles descOpcycles	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p_descOpcycles
p_fromOpcycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ opcycles X₃ pOpcycles fromOpcycles g	—	RightHomologyData.p_g'
p_fromOpcycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ opcycles pOpcycles X₃ fromOpcycles g	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p_fromOpcycles
p_opcyclesMap 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ opcycles pOpcycles opcyclesMap Hom.τ₂	—	p_opcyclesMap'
p_opcyclesMap' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ RightHomologyData.Q RightHomologyData.p opcyclesMap' Hom.τ₂	—	RightHomologyMapData.commp
p_opcyclesMap'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ RightHomologyData.Q RightHomologyData.p opcyclesMap' Hom.τ₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p_opcyclesMap'
p_opcyclesMap_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ opcycles pOpcycles opcyclesMap Hom.τ₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p_opcyclesMap
rightHomologyData_H 📖	mathematical	—	RightHomologyData.H rightHomologyData rightHomology	—	—
rightHomologyFunctorOpNatIso_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.ShortComplex CategoryTheory.Category.opposite instCategory CategoryTheory.Functor.op rightHomologyFunctor CategoryTheory.Functor.comp CategoryTheory.Limits.hasZeroMorphismsOpposite opFunctor leftHomologyFunctor CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category rightHomologyFunctorOpNatIso CategoryTheory.Iso.inv leftHomology op Opposite.unop Opposite.op rightHomology leftHomologyOpIso	—	—
rightHomologyFunctorOpNatIso_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CategoryTheory.ShortComplex CategoryTheory.Category.opposite instCategory CategoryTheory.Functor.comp CategoryTheory.Limits.hasZeroMorphismsOpposite opFunctor leftHomologyFunctor CategoryTheory.Functor.op rightHomologyFunctor CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category rightHomologyFunctorOpNatIso CategoryTheory.Iso.hom leftHomology op Opposite.unop Opposite.op rightHomology leftHomologyOpIso	—	—
rightHomologyFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.ShortComplex instCategory rightHomologyFunctor rightHomologyMap	—	—
rightHomologyFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.ShortComplex instCategory rightHomologyFunctor rightHomology	—	—
rightHomologyMap'_comp 📖	mathematical	—	rightHomologyMap' CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory RightHomologyData.H	—	RightHomologyMapData.rightHomologyMap'_eq RightHomologyMapData.comp_φH
rightHomologyMap'_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct RightHomologyData.H rightHomologyMap' CategoryTheory.ShortComplex instCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightHomologyMap'_comp
rightHomologyMap'_id 📖	mathematical	—	rightHomologyMap' CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory RightHomologyData.H	—	RightHomologyMapData.rightHomologyMap'_eq
rightHomologyMap'_op 📖	mathematical	—	Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct RightHomologyData.H rightHomologyMap' leftHomologyMap' Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite op opMap RightHomologyData.op	—	RightHomologyMapData.rightHomologyMap'_eq LeftHomologyMapData.leftHomologyMap'_eq
rightHomologyMap'_zero 📖	mathematical	—	rightHomologyMap' Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instZeroHom RightHomologyData.H CategoryTheory.Limits.HasZeroMorphisms.zero	—	RightHomologyMapData.rightHomologyMap'_eq
rightHomologyMapIso'_hom 📖	mathematical	—	CategoryTheory.Iso.hom RightHomologyData.H rightHomologyMapIso' rightHomologyMap' CategoryTheory.ShortComplex instCategory	—	—
rightHomologyMapIso'_inv 📖	mathematical	—	CategoryTheory.Iso.inv RightHomologyData.H rightHomologyMapIso' rightHomologyMap' CategoryTheory.ShortComplex instCategory	—	—
rightHomologyMapIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom rightHomology rightHomologyMapIso rightHomologyMap CategoryTheory.ShortComplex instCategory	—	—
rightHomologyMapIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv rightHomology rightHomologyMapIso rightHomologyMap CategoryTheory.ShortComplex instCategory	—	—
rightHomologyMap_comp 📖	mathematical	—	rightHomologyMap CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory rightHomology	—	rightHomologyMap'_comp
rightHomologyMap_id 📖	mathematical	—	rightHomologyMap CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct instCategory rightHomology	—	rightHomologyMap'_id
rightHomologyMap_op 📖	mathematical	—	Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct rightHomology rightHomologyMap CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite Opposite.op leftHomology CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite op instHasLeftHomologyOppositeOpOfHasRightHomology CategoryTheory.Iso.inv leftHomologyOpIso leftHomologyMap opMap CategoryTheory.Iso.hom	—	instHasLeftHomologyOppositeOpOfHasRightHomology rightHomologyMap'_op CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
rightHomologyMap_zero 📖	mathematical	—	rightHomologyMap Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instZeroHom rightHomology CategoryTheory.Limits.HasZeroMorphisms.zero	—	rightHomologyMap'_zero
rightHomology_ext 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct rightHomology opcycles rightHomologyι	—	—	—
rightHomology_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct rightHomology opcycles rightHomologyι	—	CategoryTheory.cancel_mono instMonoRightHomologyι
rightHomologyιNatTrans_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ShortComplex instCategory rightHomologyFunctor opcyclesFunctor rightHomologyιNatTrans rightHomologyι	—	—
rightHomologyι_comp_fromOpcycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct rightHomology opcycles X₃ rightHomologyι fromOpcycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	rightHomologyι_descOpcycles_π_eq_zero_of_boundary CategoryTheory.Category.comp_id
rightHomologyι_comp_fromOpcycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct rightHomology opcycles rightHomologyι X₃ fromOpcycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightHomologyι_comp_fromOpcycles
rightHomologyι_descOpcycles_π_eq_zero_of_boundary 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ X₃ g	rightHomology opcycles rightHomologyι descOpcycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	RightHomologyData.ι_descQ_eq_zero_of_boundary
rightHomologyι_descOpcycles_π_eq_zero_of_boundary_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X₂ X₃ g	rightHomology opcycles rightHomologyι descOpcycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightHomologyι_descOpcycles_π_eq_zero_of_boundary
rightHomologyι_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct rightHomology opcycles rightHomologyMap rightHomologyι opcyclesMap	—	rightHomologyι_naturality'
rightHomologyι_naturality' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct RightHomologyData.H RightHomologyData.Q rightHomologyMap' RightHomologyData.ι opcyclesMap'	—	RightHomologyMapData.commι
rightHomologyι_naturality'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct RightHomologyData.H rightHomologyMap' RightHomologyData.Q RightHomologyData.ι opcyclesMap'	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightHomologyι_naturality'
rightHomologyι_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct rightHomology rightHomologyMap opcycles rightHomologyι opcyclesMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightHomologyι_naturality
π_isoOpcyclesOfIsColimit_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair X₁ X₂ f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt opcycles CategoryTheory.Limits.Cofork.π CategoryTheory.Iso.hom isoOpcyclesOfIsColimit pOpcycles	—	CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_hom f_pOpcycles
π_isoOpcyclesOfIsColimit_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair X₁ X₂ f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.WalkingParallelPair.one CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cofork.π opcycles CategoryTheory.Iso.hom isoOpcyclesOfIsColimit pOpcycles	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_isoOpcyclesOfIsColimit_hom

CategoryTheory.ShortComplex.HasRightHomology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
condition 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData	—	—
hasCokernel 📖	mathematical	—	CategoryTheory.Limits.HasCokernel CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	—	CategoryTheory.ShortComplex.RightHomologyData.wp
hasKernel 📖	mathematical	—	CategoryTheory.Limits.HasKernel CategoryTheory.Limits.cokernel CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.cokernel.desc CategoryTheory.ShortComplex.g CategoryTheory.ShortComplex.zero	—	CategoryTheory.ShortComplex.zero CategoryTheory.ShortComplex.RightHomologyData.wp CategoryTheory.Limits.coequalizer.hom_ext CategoryTheory.Category.comp_id CategoryTheory.Limits.cokernel.π_desc CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom_assoc CategoryTheory.ShortComplex.RightHomologyData.p_g' CategoryTheory.Limits.comp_zero CategoryTheory.Limits.hasLimit_of_iso CategoryTheory.ShortComplex.RightHomologyData.ι_g'
mk' 📖	mathematical	—	CategoryTheory.ShortComplex.HasRightHomology	—	—
of_hasCokernel 📖	mathematical	—	CategoryTheory.ShortComplex.HasRightHomology Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.comp_zero	—	mk' CategoryTheory.Limits.comp_zero
of_hasCokernel_of_hasKernel 📖	mathematical	—	CategoryTheory.ShortComplex.HasRightHomology	—	CategoryTheory.ShortComplex.zero mk'
of_hasKernel 📖	mathematical	—	CategoryTheory.ShortComplex.HasRightHomology Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.zero_comp	—	mk' CategoryTheory.Limits.zero_comp
of_zeros 📖	mathematical	—	CategoryTheory.ShortComplex.HasRightHomology 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
op 📖	CompOp	9 math math: op_g', CategoryTheory.ShortComplex.LeftHomologyMapData.op_φH, CategoryTheory.ShortComplex.HomologyData.op_right, op_H, CategoryTheory.ShortComplex.LeftHomologyMapData.op_φQ, op_Q, op_p, op_ι, CategoryTheory.ShortComplex.leftHomologyMap'_op
unop 📖	CompOp	8 math math: CategoryTheory.ShortComplex.LeftHomologyMapData.unop_φQ, unop_p, unop_ι, unop_H, CategoryTheory.ShortComplex.LeftHomologyMapData.unop_φH, unop_Q, CategoryTheory.ShortComplex.HomologyData.unop_right, unop_g'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op_H 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.H Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.ShortComplex.op op Opposite.op H	—	—
op_Q 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.Q Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.ShortComplex.op op Opposite.op K	—	—
op_g' 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.g' Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.ShortComplex.op op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ K f'	—	—
op_p 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.p Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.ShortComplex.op op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct K CategoryTheory.ShortComplex.X₂ i	—	—
op_ι 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.ι Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.ShortComplex.op op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct K H π	—	—
unop_H 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.H CategoryTheory.ShortComplex.unop unop Opposite.unop H Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite	—	—
unop_Q 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.Q CategoryTheory.ShortComplex.unop unop Opposite.unop K Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite	—	—
unop_g' 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.g' CategoryTheory.ShortComplex.unop unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite K f'	—	—
unop_p 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.p CategoryTheory.ShortComplex.unop unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct K Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.ShortComplex.X₂ i	—	—
unop_ι 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.ι CategoryTheory.ShortComplex.unop unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct K Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite H π	—	—

CategoryTheory.ShortComplex.LeftHomologyMapData

Definitions

Name	Category	Theorems
op 📖	CompOp	3 math math: op_φH, op_φQ, CategoryTheory.ShortComplex.HomologyMapData.op_right
unop 📖	CompOp	3 math math: unop_φQ, CategoryTheory.ShortComplex.HomologyMapData.unop_right, unop_φH

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
op_φH 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyMapData.φH Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.ShortComplex.op CategoryTheory.ShortComplex.opMap CategoryTheory.ShortComplex.LeftHomologyData.op op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.LeftHomologyData.H φH	—	—
op_φQ 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyMapData.φQ Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.ShortComplex.op CategoryTheory.ShortComplex.opMap CategoryTheory.ShortComplex.LeftHomologyData.op op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.LeftHomologyData.K φK	—	—
unop_φH 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyMapData.φH CategoryTheory.ShortComplex.unop CategoryTheory.ShortComplex.unopMap CategoryTheory.ShortComplex.LeftHomologyData.unop unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.LeftHomologyData.H Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite φH	—	—
unop_φQ 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyMapData.φQ CategoryTheory.ShortComplex.unop CategoryTheory.ShortComplex.unopMap CategoryTheory.ShortComplex.LeftHomologyData.unop unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.LeftHomologyData.K Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite φK	—	—

CategoryTheory.ShortComplex.RightHomologyData

Definitions

Name	Category	Theorems
H 📖	CompOp	124 math math: map_ι, ι_g', CategoryTheory.ShortComplex.HomologyData.ofIso_right_H, CategoryTheory.ShortComplex.quasiIso_iff_isIso_rightHomologyMap', CategoryTheory.ShortComplex.RightHomologyMapData.neg_φH, ofAbelian_H, homologyIso_hom_comp_rightHomologyIso_inv, CategoryTheory.ShortComplex.RightHomologyMapData.op_φH, CategoryTheory.ShortComplex.RightHomologyMapData.homologyMap_eq, rightHomologyIso_hom_comp_ι, rightHomologyIso_inv_naturality_assoc, CategoryTheory.ShortComplex.rightHomologyι_naturality'_assoc, homologyIso_inv_comp_homologyι, liftH_ι, CategoryTheory.ShortComplex.HomologyData.right_homologyIso_eq_left_homologyIso_trans_iso, CategoryTheory.ShortComplex.RightHomologyMapData.id_φH, CategoryTheory.ShortComplex.leftRightHomologyComparison'_fac, CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι, map_H, CategoryTheory.ShortComplex.rightHomologyMap'_id, homologyIso_hom_comp_ι, CategoryTheory.ShortComplex.RightHomologyMapData.quasiIso_map_iff, CategoryTheory.ShortComplex.isIso_leftRightHomologyComparison', rightHomologyIso_hom_naturality, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData_H, CategoryTheory.ShortComplex.HomologyData.canonical_right_H, exact_iff, CategoryTheory.ShortComplex.LeftHomologyData.op_H, CategoryTheory.ShortComplex.RightHomologyMapData.homologyMap_comm, CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_descH, rightHomologyIso_inv_naturality, wι_assoc, CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_H, ofZeros_H, CategoryTheory.ShortComplex.homologyMap'_op, map_rightHomologyMap', ofIsColimitCokernelCofork_H, copy_ι, CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono'_φH, CategoryTheory.ShortComplex.RightHomologyMapData.zero_φH, homologyIso_hom_comp_rightHomologyIso_inv_assoc, CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap_eq, CategoryTheory.ShortComplex.HomologyData.comm_assoc, CategoryTheory.ShortComplex.isIso_leftRightHomologyComparison'_of_homologyData, CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp_φH, CategoryTheory.ShortComplex.rightHomologyMap'_op, CategoryTheory.ShortComplex.rightHomologyMap'_add, CategoryTheory.ShortComplex.rightHomologyMapIso'_inv, CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap_comm, ofHasCokernelOfHasKernel_H, CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono_φH, ι_descQ_eq_zero_of_boundary_assoc, HomologicalComplex.extend.homologyData'_right_H, homologyIso_hom_comp_ι_assoc, CategoryTheory.ShortComplex.leftRightHomologyComparison_eq, CategoryTheory.ShortComplex.rightHomologyMap'_nullHomotopic, wι, CategoryTheory.ShortComplex.rightHomologyι_naturality', homologyIso_inv_comp_homologyι_assoc, op_H, ofEpiOfIsIsoOfMono'_H, CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap', CategoryTheory.ShortComplex.comp_homologyMap_comp_assoc, rightHomologyIso_hom_comp_homologyIso_inv_assoc, CategoryTheory.ShortComplex.HomologyData.left_homologyIso_eq_right_homologyIso_trans_iso_symm, CategoryTheory.ShortComplex.instIsIsoRightHomologyMap'OfEpiτ₁Ofτ₂OfMonoτ₃, CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι_assoc, CategoryTheory.ShortComplex.RightHomologyMapData.comp_φH, CategoryTheory.ShortComplex.isIso_rightHomologyMap'_of_isIso, CategoryTheory.ShortComplex.RightHomologyMapData.smul_φH, ι_g'_assoc, rightHomologyIso_hom_comp_ι_assoc, instMonoι, CategoryTheory.ShortComplex.rightHomologyMap'_comp, CategoryTheory.ShortComplex.rightHomologyMap'_sub, mapRightHomologyIso_eq, CategoryTheory.ShortComplex.HomologyMapData.comm, CategoryTheory.ShortComplex.HomologyMapData.comm_assoc, CategoryTheory.ShortComplex.LeftHomologyData.unop_H, isIso_ι, exact_map_iff, HomologicalComplex.extend.rightHomologyData_H, CategoryTheory.ShortComplex.rightHomologyMapIso'_hom, HomologicalComplex.truncGE.rightHomologyMapData_φH, CategoryTheory.ShortComplex.rightHomologyMap'_comp_assoc, CategoryTheory.ShortComplex.RightHomologyMapData.commι, CategoryTheory.ShortComplex.rightHomologyData_H, rightHomologyIso_inv_comp_rightHomologyι_assoc, CategoryTheory.ShortComplex.leftRightHomologyComparison'_naturality_assoc, rightHomologyIso_hom_naturality_assoc, CategoryTheory.ShortComplex.RightHomologyMapData.add_φH, CategoryTheory.ShortComplex.map_leftRightHomologyComparison', canonical_H, CategoryTheory.ShortComplex.HomologyData.unop_iso, CategoryTheory.ShortComplex.rightHomologyMap'_neg, CategoryTheory.ShortComplex.HomologyData.op_iso, liftH_ι_assoc, ofHasKernel_H, CategoryTheory.ShortComplex.HomologyData.map_iso, ι_descQ_eq_zero_of_boundary, CategoryTheory.ShortComplex.leftRightHomologyComparison'_naturality, rightHomologyIso_inv_comp_rightHomologyι, CategoryTheory.ShortComplex.RightHomologyMapData.map_φH, unop_π, CategoryTheory.ShortComplex.rightHomologyMap'_smul, rightHomologyIso_hom_comp_homologyIso_inv, unop_H, ofIsLimitKernelFork_H, CategoryTheory.ShortComplex.Splitting.rightHomologyData_H, CategoryTheory.ShortComplex.HomologyData.ofIsIsoLeftRightHomologyComparison'_iso, CategoryTheory.ShortComplex.comp_homologyMap_comp, CategoryTheory.ShortComplex.HomologyData.comm, CategoryTheory.ShortComplex.leftRightHomologyComparison'_compatibility, CategoryTheory.ShortComplex.rightHomologyMap'_zero, CategoryTheory.ShortComplex.HomologyData.exact_iff', CategoryTheory.ShortComplex.HomologyData.leftRightHomologyComparison'_eq, ofEpiOfIsIsoOfMono_H, CategoryTheory.ShortComplex.leftRightHomologyComparison'_fac_assoc, CategoryTheory.ShortComplex.RightHomologyMapData.commι_assoc, CategoryTheory.ShortComplex.RightHomologyMapData.unop_φH, copy_H, op_π, mapHomologyIso'_eq, CategoryTheory.ShortComplex.RightHomologyMapData.quasiIso_iff
Q 📖	CompOp	131 math math: map_ι, CategoryTheory.ShortComplex.HomologyData.ofIso_right_p, ι_g', canonical_Q, IsPreservedBy.hg', ofZeros_Q, wp, p_comp_opcyclesIso_inv, wp_assoc, CategoryTheory.ShortComplex.RightHomologyMapData.natTransApp_φQ, CategoryTheory.ShortComplex.opcyclesMap'_g', CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData_Q, CategoryTheory.ShortComplex.opcyclesMap'_sub, CategoryTheory.ShortComplex.RightHomologyMapData.neg_φQ, rightHomologyIso_hom_comp_ι, CategoryTheory.ShortComplex.opcyclesMap'_g'_assoc, CategoryTheory.ShortComplex.rightHomologyι_naturality'_assoc, ofEpiOfIsIsoOfMono'_Q, homologyIso_inv_comp_homologyι, CategoryTheory.ShortComplex.opcyclesMapIso'_inv, unop_i, p_g'_assoc, copy_p, map_g', CategoryTheory.ShortComplex.opcyclesMap'_id, CategoryTheory.ShortComplex.isIso_opcyclesMap'_of_isIso, CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι, CategoryTheory.ShortComplex.RightHomologyMapData.op_φK, homologyIso_hom_comp_ι, CategoryTheory.ShortComplex.HomologyData.ofIso_right_Q, CategoryTheory.ShortComplex.RightHomologyMapData.commg'_assoc, CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_descH, wι_assoc, copy_Q, ofEpiOfIsIsoOfMono_Q, ofEpiOfIsIsoOfMono'_g'_τ₃, CategoryTheory.ShortComplex.HomologyData.canonical_right_Q, mapOpcyclesIso_eq, instEpiP, ofIsColimitCokernelCofork_Q, CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap_comm, copy_ι, p_comp_opcyclesIso_inv_assoc, CategoryTheory.ShortComplex.RightHomologyMapData.unop_φK, ofAbelian_Q, CategoryTheory.ShortComplex.HomologyData.comm_assoc, CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono'_φQ, CategoryTheory.ShortComplex.Splitting.rightHomologyData_Q, op_K, ofIsLimitKernelFork_Q, CategoryTheory.ShortComplex.RightHomologyMapData.comp_φQ, CategoryTheory.ShortComplex.p_opcyclesMap', CategoryTheory.ShortComplex.RightHomologyMapData.commg', map_Q, unop_f', CategoryTheory.ShortComplex.LeftHomologyData.op_Q, p_descQ_assoc, p_descQ, CategoryTheory.ShortComplex.Exact.shortExact, CategoryTheory.ShortComplex.opcyclesMap'_comp_assoc, IsPreservedBy.g', ofEpiOfIsIsoOfMono_g', CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_Q, ι_descQ_eq_zero_of_boundary_assoc, homologyIso_hom_comp_ι_assoc, CategoryTheory.ShortComplex.RightHomologyMapData.id_φQ, HomologicalComplex.extend.rightHomologyData_p, wι, CategoryTheory.ShortComplex.exact_iff_i_p_zero, pOpcycles_comp_opcyclesIso_hom, CategoryTheory.ShortComplex.rightHomologyι_naturality', homologyIso_inv_comp_homologyι_assoc, CategoryTheory.ShortComplex.comp_homologyMap_comp_assoc, HomologicalComplex.extend.rightHomologyData_g', HomologicalComplex.extend.homologyData'_right_p, CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι_assoc, ofEpiOfIsIsoOfMono_p, exact_iff_mono_g', CategoryTheory.ShortComplex.opcyclesMapIso'_hom, ι_g'_assoc, map_p, rightHomologyIso_hom_comp_ι_assoc, instMonoι, CategoryTheory.ShortComplex.Exact.isIso_g', CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_liftH, opcyclesIso_hom_comp_descQ, CategoryTheory.ShortComplex.HomologyData.exact_iff_i_p_zero, unop_K, ofHasKernel_Q, CategoryTheory.ShortComplex.RightHomologyMapData.zero_φQ, isIso_ι, op_f', CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_φQ, isIso_p, CategoryTheory.ShortComplex.RightHomologyMapData.commι, CategoryTheory.ShortComplex.isIso_opcyclesMap'_of_isIso_of_epi, rightHomologyIso_inv_comp_rightHomologyι_assoc, ofHasCokernelOfHasKernel_Q, CategoryTheory.ShortComplex.LeftHomologyData.unop_Q, HomologicalComplex.extend.homologyData'_right_Q, CategoryTheory.ShortComplex.RightHomologyMapData.smul_φQ, op_i, CategoryTheory.ShortComplex.RightHomologyMapData.commp_assoc, ι_descQ_eq_zero_of_boundary, rightHomologyIso_inv_comp_rightHomologyι, pOpcycles_comp_opcyclesIso_hom_assoc, CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap_eq, unop_π, CategoryTheory.ShortComplex.opcyclesMap'_add, CategoryTheory.ShortComplex.Exact.mono_g', CategoryTheory.ShortComplex.p_opcyclesMap'_assoc, ofZeros_g', CategoryTheory.ShortComplex.comp_homologyMap_comp, map_opcyclesMap', CategoryTheory.ShortComplex.HomologyData.comm, CategoryTheory.ShortComplex.opcyclesMap'_comp, opcyclesIso_inv_comp_descOpcycles_assoc, ofIsColimitCokernelCofork_g', opcyclesIso_inv_comp_descOpcycles, CategoryTheory.ShortComplex.RightHomologyMapData.map_φQ, HomologicalComplex.extend.rightHomologyData_Q, CategoryTheory.ShortComplex.opcyclesMap'_neg, ofEpiOfIsIsoOfMono'_p, CategoryTheory.ShortComplex.RightHomologyMapData.commι_assoc, CategoryTheory.ShortComplex.RightHomologyMapData.add_φQ, CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono_φQ, CategoryTheory.ShortComplex.opcyclesMap'_smul, CategoryTheory.ShortComplex.RightHomologyMapData.commp, op_π, CategoryTheory.ShortComplex.opcyclesMap'_zero, p_g'
copy 📖	CompOp	4 math math: copy_p, copy_Q, copy_ι, copy_H
descH 📖	CompOp	—
descQ 📖	CompOp	7 math math: p_descQ_assoc, p_descQ, ι_descQ_eq_zero_of_boundary_assoc, opcyclesIso_hom_comp_descQ, ι_descQ_eq_zero_of_boundary, opcyclesIso_inv_comp_descOpcycles_assoc, opcyclesIso_inv_comp_descOpcycles
g' 📖	CompOp	26 math math: CategoryTheory.ShortComplex.LeftHomologyData.op_g', ι_g', IsPreservedBy.hg', CategoryTheory.ShortComplex.opcyclesMap'_g', CategoryTheory.ShortComplex.opcyclesMap'_g'_assoc, p_g'_assoc, map_g', CategoryTheory.ShortComplex.RightHomologyMapData.commg'_assoc, ofEpiOfIsIsoOfMono'_g'_τ₃, CategoryTheory.ShortComplex.RightHomologyMapData.commg', unop_f', HomologicalComplex.truncGE'.homologyData_right_g', IsPreservedBy.g', ofEpiOfIsIsoOfMono_g', canonical_g', HomologicalComplex.extend.rightHomologyData_g', exact_iff_mono_g', ι_g'_assoc, CategoryTheory.ShortComplex.Exact.isIso_g', op_f', CategoryTheory.ShortComplex.Exact.mono_g', ofZeros_g', ofIsColimitCokernelCofork_g', CategoryTheory.ShortComplex.LeftHomologyData.unop_g', ofIsLimitKernelFork_g', p_g'
hp 📖	CompOp	2 math math: wι_assoc, wι
hι 📖	CompOp	—
hι' 📖	CompOp	—
liftH 📖	CompOp	4 math math: liftH_ι, CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_descH, CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_liftH, liftH_ι_assoc
ofEpiOfIsIsoOfMono 📖	CompOp	8 math math: ofEpiOfIsIsoOfMono_Q, CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono_φH, ofEpiOfIsIsoOfMono_g', CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono_right, ofEpiOfIsIsoOfMono_p, ofEpiOfIsIsoOfMono_H, CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono_φQ, ofEpiOfIsIsoOfMono_ι
ofEpiOfIsIsoOfMono' 📖	CompOp	8 math math: ofEpiOfIsIsoOfMono'_Q, ofEpiOfIsIsoOfMono'_ι, ofEpiOfIsIsoOfMono'_g'_τ₃, CategoryTheory.ShortComplex.HomologyData.ofEpiOfIsIsoOfMono'_right, CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono'_φH, CategoryTheory.ShortComplex.RightHomologyMapData.ofEpiOfIsIsoOfMono'_φQ, ofEpiOfIsIsoOfMono'_H, ofEpiOfIsIsoOfMono'_p
ofHasCokernel 📖	CompOp	1 math math: CategoryTheory.ShortComplex.HomologyData.ofHasCokernel_right
ofHasCokernelOfHasKernel 📖	CompOp	4 math math: ofHasCokernelOfHasKernel_p, ofHasCokernelOfHasKernel_H, ofHasCokernelOfHasKernel_ι, ofHasCokernelOfHasKernel_Q
ofHasKernel 📖	CompOp	5 math math: ofHasKernel_p, CategoryTheory.ShortComplex.HomologyData.ofHasKernel_right, ofHasKernel_Q, ofHasKernel_ι, ofHasKernel_H
ofIsColimitCokernelCofork 📖	CompOp	10 math math: CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φH, ofIsColimitCokernelCofork_Q, ofIsColimitCokernelCofork_H, CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork_right, ofIsColimitCokernelCofork_p, ofIsColimitCokernelCofork_ι, CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φQ, CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork_φH, ofIsColimitCokernelCofork_g', CategoryTheory.ShortComplex.RightHomologyMapData.ofIsColimitCokernelCofork_φQ
ofIsLimitKernelFork 📖	CompOp	10 math math: CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_φH, CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork_φH, ofIsLimitKernelFork_Q, ofIsLimitKernelFork_p, CategoryTheory.ShortComplex.RightHomologyMapData.ofIsLimitKernelFork_φQ, CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork_right, CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_φQ, ofIsLimitKernelFork_ι, ofIsLimitKernelFork_H, ofIsLimitKernelFork_g'
ofIso 📖	CompOp	—
ofZeros 📖	CompOp	12 math math: ofZeros_Q, CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φH, CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_φH, ofZeros_H, CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros_φQ, ofZeros_p, ofZeros_ι, CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_φQ, CategoryTheory.ShortComplex.RightHomologyMapData.ofZeros_φH, CategoryTheory.ShortComplex.HomologyData.ofZeros_right, CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsColimitCokernelCofork_φQ, ofZeros_g'
op 📖	CompOp	9 math math: CategoryTheory.ShortComplex.RightHomologyMapData.op_φH, CategoryTheory.ShortComplex.RightHomologyMapData.op_φK, op_K, CategoryTheory.ShortComplex.rightHomologyMap'_op, op_H, CategoryTheory.ShortComplex.HomologyData.op_left, op_f', op_i, op_π
opcyclesIso 📖	CompOp	18 math math: p_comp_opcyclesIso_inv, rightHomologyIso_hom_comp_ι, homologyIso_inv_comp_homologyι, homologyIso_hom_comp_ι, mapOpcyclesIso_eq, CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap_comm, p_comp_opcyclesIso_inv_assoc, homologyIso_hom_comp_ι_assoc, pOpcycles_comp_opcyclesIso_hom, homologyIso_inv_comp_homologyι_assoc, rightHomologyIso_hom_comp_ι_assoc, opcyclesIso_hom_comp_descQ, rightHomologyIso_inv_comp_rightHomologyι_assoc, rightHomologyIso_inv_comp_rightHomologyι, pOpcycles_comp_opcyclesIso_hom_assoc, CategoryTheory.ShortComplex.RightHomologyMapData.opcyclesMap_eq, opcyclesIso_inv_comp_descOpcycles_assoc, opcyclesIso_inv_comp_descOpcycles
p 📖	CompOp	51 math math: ofHasCokernelOfHasKernel_p, CategoryTheory.ShortComplex.HomologyData.ofIso_right_p, CategoryTheory.ShortComplex.LeftHomologyData.unop_p, wp, p_comp_opcyclesIso_inv, wp_assoc, unop_i, p_g'_assoc, copy_p, CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι, ofHasKernel_p, CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_descH, wι_assoc, instEpiP, CategoryTheory.ShortComplex.Splitting.rightHomologyData_p, p_comp_opcyclesIso_inv_assoc, CategoryTheory.ShortComplex.HomologyData.comm_assoc, CategoryTheory.ShortComplex.p_opcyclesMap', p_descQ_assoc, p_descQ, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData_p, CategoryTheory.ShortComplex.Exact.shortExact, CategoryTheory.ShortComplex.HomologyData.canonical_right_p, ofIsColimitCokernelCofork_p, ofIsLimitKernelFork_p, HomologicalComplex.extend.rightHomologyData_p, ofZeros_p, wι, CategoryTheory.ShortComplex.exact_iff_i_p_zero, pOpcycles_comp_opcyclesIso_hom, CategoryTheory.ShortComplex.comp_homologyMap_comp_assoc, ofAbelian_p, HomologicalComplex.extend.homologyData'_right_p, CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι_assoc, ofEpiOfIsIsoOfMono_p, map_p, CategoryTheory.ShortComplex.LeftHomologyData.op_p, CategoryTheory.ShortComplex.leftRightHomologyComparison'_eq_liftH, canonical_p, CategoryTheory.ShortComplex.HomologyData.exact_iff_i_p_zero, isIso_p, op_i, CategoryTheory.ShortComplex.RightHomologyMapData.commp_assoc, CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_p, pOpcycles_comp_opcyclesIso_hom_assoc, CategoryTheory.ShortComplex.p_opcyclesMap'_assoc, CategoryTheory.ShortComplex.comp_homologyMap_comp, CategoryTheory.ShortComplex.HomologyData.comm, ofEpiOfIsIsoOfMono'_p, CategoryTheory.ShortComplex.RightHomologyMapData.commp, p_g'
rightHomologyIso 📖	CompOp	12 math math: homologyIso_hom_comp_rightHomologyIso_inv, rightHomologyIso_hom_comp_ι, homologyIso_hom_comp_rightHomologyIso_inv_assoc, CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap_eq, CategoryTheory.ShortComplex.RightHomologyMapData.rightHomologyMap_comm, CategoryTheory.ShortComplex.leftRightHomologyComparison_eq, rightHomologyIso_hom_comp_homologyIso_inv_assoc, rightHomologyIso_hom_comp_ι_assoc, mapRightHomologyIso_eq, rightHomologyIso_inv_comp_rightHomologyι_assoc, rightHomologyIso_inv_comp_rightHomologyι, rightHomologyIso_hom_comp_homologyIso_inv
unop 📖	CompOp	8 math math: unop_i, CategoryTheory.ShortComplex.RightHomologyMapData.unop_φK, CategoryTheory.ShortComplex.HomologyData.unop_left, unop_f', unop_K, unop_π, unop_H, CategoryTheory.ShortComplex.RightHomologyMapData.unop_φH
ι 📖	CompOp	50 math math: map_ι, ι_g', rightHomologyIso_hom_comp_ι, CategoryTheory.ShortComplex.rightHomologyι_naturality'_assoc, CategoryTheory.ShortComplex.LeftHomologyData.unop_ι, homologyIso_inv_comp_homologyι, liftH_ι, CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι, CategoryTheory.ShortComplex.Splitting.rightHomologyData_ι, ofEpiOfIsIsoOfMono'_ι, homologyIso_hom_comp_ι, wι_assoc, canonical_ι, copy_ι, CategoryTheory.ShortComplex.HomologyData.comm_assoc, ι_descQ_eq_zero_of_boundary_assoc, homologyIso_hom_comp_ι_assoc, CategoryTheory.ShortComplex.HomologyData.ofIso_right_ι, wι, CategoryTheory.ShortComplex.rightHomologyι_naturality', homologyIso_inv_comp_homologyι_assoc, CategoryTheory.ShortComplex.comp_homologyMap_comp_assoc, HomologicalComplex.extend.rightHomologyData_ι, CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι_assoc, ofAbelian_ι, CategoryTheory.ShortComplex.HomologyData.canonical_right_ι, ι_g'_assoc, rightHomologyIso_hom_comp_ι_assoc, instMonoι, ofHasCokernelOfHasKernel_ι, isIso_ι, ofZeros_ι, CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_ι, HomologicalComplex.extend.homologyData'_right_ι, CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.rightHomologyData_ι, ofIsLimitKernelFork_ι, CategoryTheory.ShortComplex.RightHomologyMapData.commι, rightHomologyIso_inv_comp_rightHomologyι_assoc, ofHasKernel_ι, ofIsColimitCokernelCofork_ι, liftH_ι_assoc, ι_descQ_eq_zero_of_boundary, rightHomologyIso_inv_comp_rightHomologyι, unop_π, CategoryTheory.ShortComplex.comp_homologyMap_comp, CategoryTheory.ShortComplex.HomologyData.comm, CategoryTheory.ShortComplex.RightHomologyMapData.commι_assoc, CategoryTheory.ShortComplex.LeftHomologyData.op_ι, op_π, ofEpiOfIsIsoOfMono_ι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
copy_H 📖	mathematical	—	H copy	—	—
copy_Q 📖	mathematical	—	Q copy	—	—
copy_p 📖	mathematical	—	p copy CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ Q CategoryTheory.Iso.inv	—	—
copy_ι 📖	mathematical	—	ι copy CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct H CategoryTheory.Iso.hom Q CategoryTheory.Iso.inv	—	—
instEpiP 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.ShortComplex.X₂ Q p	—	CategoryTheory.Limits.Cofork.IsColimit.hom_ext wp
instMonoι 📖	mathematical	—	CategoryTheory.Mono H Q ι	—	CategoryTheory.Limits.Fork.IsLimit.hom_ext CategoryTheory.ShortComplex.zero wp wι
isIso_p 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.IsIso Q p	—	CategoryTheory.Category.comp_id p_descQ CategoryTheory.cancel_epi instEpiP p_descQ_assoc CategoryTheory.Category.id_comp
isIso_ι 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.IsIso H Q ι	—	ι_g' CategoryTheory.cancel_epi instEpiP CategoryTheory.Category.id_comp p_g' CategoryTheory.Limits.comp_zero CategoryTheory.cancel_mono instMonoι CategoryTheory.Category.assoc CategoryTheory.Category.comp_id
liftH_ι 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Q CategoryTheory.ShortComplex.X₃ g' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	H liftH ι	—	CategoryTheory.Limits.IsLimit.fac CategoryTheory.ShortComplex.zero wp wι
liftH_ι_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Q CategoryTheory.ShortComplex.X₃ g' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	H liftH ι	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' liftH_ι
ofEpiOfIsIsoOfMono'_H 📖	mathematical	—	H ofEpiOfIsIsoOfMono'	—	—
ofEpiOfIsIsoOfMono'_Q 📖	mathematical	—	Q ofEpiOfIsIsoOfMono'	—	—
ofEpiOfIsIsoOfMono'_g'_τ₃ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Q ofEpiOfIsIsoOfMono' CategoryTheory.ShortComplex.X₃ g' CategoryTheory.ShortComplex.Hom.τ₃	—	CategoryTheory.cancel_epi instEpiP p_g'_assoc ofEpiOfIsIsoOfMono'_p CategoryTheory.Category.assoc p_g' CategoryTheory.ShortComplex.Hom.comm₂₃
ofEpiOfIsIsoOfMono'_p 📖	mathematical	—	p ofEpiOfIsIsoOfMono' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ Q CategoryTheory.ShortComplex.Hom.τ₂	—	—
ofEpiOfIsIsoOfMono'_ι 📖	mathematical	—	ι ofEpiOfIsIsoOfMono'	—	—
ofEpiOfIsIsoOfMono_H 📖	mathematical	—	H ofEpiOfIsIsoOfMono	—	—
ofEpiOfIsIsoOfMono_Q 📖	mathematical	—	Q ofEpiOfIsIsoOfMono	—	—
ofEpiOfIsIsoOfMono_g' 📖	mathematical	—	g' ofEpiOfIsIsoOfMono CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Q CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.Hom.τ₃	—	CategoryTheory.ShortComplex.LeftHomologyData.ofEpiOfIsIsoOfMono'_f'
ofEpiOfIsIsoOfMono_p 📖	mathematical	—	p ofEpiOfIsIsoOfMono CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ Q CategoryTheory.inv CategoryTheory.ShortComplex.Hom.τ₂	—	CategoryTheory.isIso_unop CategoryTheory.unop_inv
ofEpiOfIsIsoOfMono_ι 📖	mathematical	—	ι ofEpiOfIsIsoOfMono	—	—
ofHasCokernelOfHasKernel_H 📖	mathematical	—	H ofHasCokernelOfHasKernel CategoryTheory.Limits.kernel CategoryTheory.Limits.cokernel CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.cokernel.desc CategoryTheory.ShortComplex.g CategoryTheory.ShortComplex.zero	—	CategoryTheory.ShortComplex.zero
ofHasCokernelOfHasKernel_Q 📖	mathematical	—	Q ofHasCokernelOfHasKernel CategoryTheory.Limits.cokernel CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	—	CategoryTheory.ShortComplex.zero
ofHasCokernelOfHasKernel_p 📖	mathematical	—	p ofHasCokernelOfHasKernel CategoryTheory.Limits.cokernel.π CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	—	CategoryTheory.ShortComplex.zero
ofHasCokernelOfHasKernel_ι 📖	mathematical	—	ι ofHasCokernelOfHasKernel CategoryTheory.Limits.kernel.ι CategoryTheory.Limits.cokernel CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.cokernel.desc CategoryTheory.ShortComplex.g CategoryTheory.ShortComplex.zero	—	CategoryTheory.ShortComplex.zero
ofHasKernel_H 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	H ofHasKernel CategoryTheory.Limits.kernel CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	—
ofHasKernel_Q 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	Q ofHasKernel	—	—
ofHasKernel_p 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	p ofHasKernel CategoryTheory.CategoryStruct.id	—	—
ofHasKernel_ι 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	ι ofHasKernel CategoryTheory.Limits.kernel.ι CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	—
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_Q 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	Q ofIsColimitCokernelCofork CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f	—	—
ofIsColimitCokernelCofork_g' 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	g' ofIsColimitCokernelCofork Q	—	CategoryTheory.cancel_epi instEpiP p_g' CategoryTheory.Limits.comp_zero
ofIsColimitCokernelCofork_p 📖	mathematical	CategoryTheory.ShortComplex.g Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.Limits.HasZeroMorphisms.zero	p ofIsColimitCokernelCofork CategoryTheory.Limits.Cofork.π CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.f	—	—
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.CategoryStruct.id CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair 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_Q 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	Q ofIsLimitKernelFork	—	—
ofIsLimitKernelFork_g' 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	g' ofIsLimitKernelFork CategoryTheory.ShortComplex.g	—	CategoryTheory.cancel_epi instEpiP p_g' ofIsLimitKernelFork_p CategoryTheory.Category.id_comp
ofIsLimitKernelFork_p 📖	mathematical	CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Limits.HasZeroMorphisms.zero	p ofIsLimitKernelFork CategoryTheory.CategoryStruct.id	—	—
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.Limits.Fork.ι 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_Q 📖	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₃	Q ofZeros	—	—
ofZeros_g' 📖	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₃	g' ofZeros Q	—	CategoryTheory.cancel_epi instEpiP CategoryTheory.Limits.comp_zero p_g'
ofZeros_p 📖	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₃	p 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	—	—
op_H 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.H Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.ShortComplex.op op Opposite.op H	—	—
op_K 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.K Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.ShortComplex.op op Opposite.op Q	—	—
op_f' 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.f' Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.ShortComplex.op op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Q CategoryTheory.ShortComplex.X₃ g'	—	—
op_i 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.i Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.ShortComplex.op op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ Q p	—	—
op_π 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.π Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.ShortComplex.op op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct H Q ι	—	—
opcyclesIso_hom_comp_descQ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	CategoryTheory.ShortComplex.opcycles Q CategoryTheory.Iso.hom opcyclesIso descQ CategoryTheory.ShortComplex.descOpcycles	—	opcyclesIso_inv_comp_descOpcycles CategoryTheory.Iso.hom_inv_id_assoc
opcyclesIso_inv_comp_descOpcycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	Q CategoryTheory.ShortComplex.opcycles CategoryTheory.Iso.inv opcyclesIso CategoryTheory.ShortComplex.descOpcycles descQ	—	CategoryTheory.cancel_epi instEpiP p_comp_opcyclesIso_inv_assoc CategoryTheory.ShortComplex.p_descOpcycles p_descQ
opcyclesIso_inv_comp_descOpcycles_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	Q CategoryTheory.ShortComplex.opcycles CategoryTheory.Iso.inv opcyclesIso CategoryTheory.ShortComplex.descOpcycles descQ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesIso_inv_comp_descOpcycles
pOpcycles_comp_opcyclesIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.opcycles Q CategoryTheory.ShortComplex.pOpcycles CategoryTheory.Iso.hom opcyclesIso p	—	p_comp_opcyclesIso_inv CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
pOpcycles_comp_opcyclesIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.pOpcycles Q CategoryTheory.Iso.hom opcyclesIso p	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' pOpcycles_comp_opcyclesIso_hom
p_comp_opcyclesIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ Q CategoryTheory.ShortComplex.opcycles p CategoryTheory.Iso.inv opcyclesIso CategoryTheory.ShortComplex.pOpcycles	—	CategoryTheory.ShortComplex.p_opcyclesMap' CategoryTheory.Category.id_comp
p_comp_opcyclesIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ Q p CategoryTheory.ShortComplex.opcycles CategoryTheory.Iso.inv opcyclesIso CategoryTheory.ShortComplex.pOpcycles	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p_comp_opcyclesIso_inv
p_descQ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	Q p descQ	—	CategoryTheory.Limits.IsColimit.fac wp
p_descQ_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	Q p descQ	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p_descQ
p_g' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ Q CategoryTheory.ShortComplex.X₃ p g' CategoryTheory.ShortComplex.g	—	p_descQ CategoryTheory.ShortComplex.zero
p_g'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ Q p CategoryTheory.ShortComplex.X₃ g' CategoryTheory.ShortComplex.g	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p_g'
rightHomologyIso_hom_comp_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.rightHomology H Q CategoryTheory.Iso.hom rightHomologyIso ι CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.rightHomologyι opcyclesIso	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Iso.isIso_inv CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.cancel_epi CategoryTheory.epi_of_strongEpi CategoryTheory.strongEpi_of_isIso CategoryTheory.Iso.inv_hom_id_assoc rightHomologyIso_inv_comp_rightHomologyι
rightHomologyIso_hom_comp_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.rightHomology H CategoryTheory.Iso.hom rightHomologyIso Q ι CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.rightHomologyι opcyclesIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightHomologyIso_hom_comp_ι
rightHomologyIso_inv_comp_rightHomologyι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct H CategoryTheory.ShortComplex.rightHomology CategoryTheory.ShortComplex.opcycles CategoryTheory.Iso.inv rightHomologyIso CategoryTheory.ShortComplex.rightHomologyι Q ι opcyclesIso	—	CategoryTheory.ShortComplex.rightHomologyι_naturality'
rightHomologyIso_inv_comp_rightHomologyι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct H CategoryTheory.ShortComplex.rightHomology CategoryTheory.Iso.inv rightHomologyIso CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.rightHomologyι Q ι opcyclesIso	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightHomologyIso_inv_comp_rightHomologyι
unop_H 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.ShortComplex.unop unop Opposite.unop H Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite	—	—
unop_K 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.K CategoryTheory.ShortComplex.unop unop Opposite.unop Q Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite	—	—
unop_f' 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.f' CategoryTheory.ShortComplex.unop unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Q Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.ShortComplex.X₃ g'	—	—
unop_i 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.unop unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite Q p	—	—
unop_π 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.π CategoryTheory.ShortComplex.unop unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct H Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite Q ι	—	—
wp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ Q CategoryTheory.ShortComplex.f p Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
wp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f Q p Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' wp
wι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct H Q CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.CokernelCofork.ofπ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g CategoryTheory.ShortComplex.zero ι CategoryTheory.Limits.IsColimit.desc p wp hp	—	—
wι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct H Q ι CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Limits.CokernelCofork.ofπ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g CategoryTheory.ShortComplex.zero CategoryTheory.Limits.IsColimit.desc p wp hp	—	CategoryTheory.ShortComplex.zero wp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' wι
ι_descQ_eq_zero_of_boundary 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	H Q ι descQ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	ι_g'_assoc CategoryTheory.Limits.zero_comp descQ.congr_simp CategoryTheory.cancel_epi instEpiP p_descQ p_g'_assoc
ι_descQ_eq_zero_of_boundary_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	H Q ι descQ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_descQ_eq_zero_of_boundary
ι_g' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct H Q CategoryTheory.ShortComplex.X₃ ι g' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	wι
ι_g'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct H Q ι CategoryTheory.ShortComplex.X₃ g' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_g'

CategoryTheory.ShortComplex.RightHomologyMapData

Definitions

Name	Category	Theorems
comp 📖	CompOp	3 math math: CategoryTheory.ShortComplex.HomologyMapData.comp_right, comp_φQ, comp_φH
compatibilityOfZerosOfIsColimitCokernelCofork 📖	CompOp	2 math math: compatibilityOfZerosOfIsColimitCokernelCofork_φH, compatibilityOfZerosOfIsColimitCokernelCofork_φQ
compatibilityOfZerosOfIsLimitKernelFork 📖	CompOp	3 math math: compatibilityOfZerosOfIsLimitKernelFork_φH, compatibilityOfZerosOfIsLimitKernelFork_φQ, CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsLimitKernelFork_right
id 📖	CompOp	3 math math: id_φH, CategoryTheory.ShortComplex.HomologyMapData.id_right, id_φQ
instInhabited 📖	CompOp	—
instUnique 📖	CompOp	—
ofEpiOfIsIsoOfMono 📖	CompOp	2 math math: ofEpiOfIsIsoOfMono_φH, ofEpiOfIsIsoOfMono_φQ
ofEpiOfIsIsoOfMono' 📖	CompOp	2 math math: ofEpiOfIsIsoOfMono'_φH, ofEpiOfIsIsoOfMono'_φQ
ofIsColimitCokernelCofork 📖	CompOp	3 math math: CategoryTheory.ShortComplex.HomologyMapData.ofIsColimitCokernelCofork_right, ofIsColimitCokernelCofork_φH, ofIsColimitCokernelCofork_φQ
ofIsLimitKernelFork 📖	CompOp	3 math math: ofIsLimitKernelFork_φH, CategoryTheory.ShortComplex.HomologyMapData.ofIsLimitKernelFork_right, ofIsLimitKernelFork_φQ
ofZeros 📖	CompOp	3 math math: ofZeros_φQ, ofZeros_φH, CategoryTheory.ShortComplex.HomologyMapData.ofZeros_right
op 📖	CompOp	3 math math: CategoryTheory.ShortComplex.HomologyMapData.op_left, op_φH, op_φK
unop 📖	CompOp	3 math math: unop_φK, unop_φH, CategoryTheory.ShortComplex.HomologyMapData.unop_left
zero 📖	CompOp	3 math math: zero_φH, CategoryTheory.ShortComplex.HomologyMapData.zero_right, zero_φQ
φH 📖	CompOp	32 math math: neg_φH, op_φH, homologyMap_eq, compatibilityOfZerosOfIsColimitCokernelCofork_φH, compatibilityOfZerosOfIsLimitKernelFork_φH, id_φH, CategoryTheory.ShortComplex.LeftHomologyMapData.op_φH, quasiIso_map_iff, ofIsLimitKernelFork_φH, homologyMap_comm, congr_φH, ofEpiOfIsIsoOfMono'_φH, zero_φH, rightHomologyMap_eq, natTransApp_φH, rightHomologyMap_comm, ofEpiOfIsIsoOfMono_φH, rightHomologyMap'_eq, comp_φH, smul_φH, CategoryTheory.ShortComplex.HomologyMapData.comm, CategoryTheory.ShortComplex.HomologyMapData.comm_assoc, HomologicalComplex.truncGE.rightHomologyMapData_φH, CategoryTheory.ShortComplex.LeftHomologyMapData.unop_φH, commι, ofZeros_φH, add_φH, map_φH, ofIsColimitCokernelCofork_φH, commι_assoc, unop_φH, quasiIso_iff
φQ 📖	CompOp	31 math math: HomologicalComplex.truncGE.rightHomologyMapData_φQ, CategoryTheory.ShortComplex.LeftHomologyMapData.unop_φQ, natTransApp_φQ, neg_φQ, opcyclesMap'_eq, op_φK, CategoryTheory.ShortComplex.HomologyMapData.opcyclesMap'_eq, commg'_assoc, opcyclesMap_comm, ofZeros_φQ, CategoryTheory.ShortComplex.LeftHomologyMapData.op_φQ, unop_φK, ofEpiOfIsIsoOfMono'_φQ, comp_φQ, commg', id_φQ, ofIsLimitKernelFork_φQ, zero_φQ, congr_φQ, compatibilityOfZerosOfIsLimitKernelFork_φQ, commι, smul_φQ, compatibilityOfZerosOfIsColimitCokernelCofork_φQ, commp_assoc, opcyclesMap_eq, map_φQ, ofIsColimitCokernelCofork_φQ, commι_assoc, add_φQ, ofEpiOfIsIsoOfMono_φQ, commp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commg' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.RightHomologyData.Q CategoryTheory.ShortComplex.X₃ φQ CategoryTheory.ShortComplex.RightHomologyData.g' CategoryTheory.ShortComplex.Hom.τ₃	—	—
commg'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.RightHomologyData.Q φQ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.RightHomologyData.g' CategoryTheory.ShortComplex.Hom.τ₃	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' commg'
commp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.RightHomologyData.Q CategoryTheory.ShortComplex.RightHomologyData.p φQ CategoryTheory.ShortComplex.Hom.τ₂	—	—
commp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.RightHomologyData.Q CategoryTheory.ShortComplex.RightHomologyData.p φQ CategoryTheory.ShortComplex.Hom.τ₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' commp
commι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.RightHomologyData.H CategoryTheory.ShortComplex.RightHomologyData.Q φH CategoryTheory.ShortComplex.RightHomologyData.ι φQ	—	—
commι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.RightHomologyData.H φH CategoryTheory.ShortComplex.RightHomologyData.Q CategoryTheory.ShortComplex.RightHomologyData.ι φQ	—	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.RightHomologyData.H	—	—
comp_φQ 📖	mathematical	—	φQ CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory comp CategoryTheory.ShortComplex.RightHomologyData.Q	—	—
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.RightHomologyData.ofZeros CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork compatibilityOfZerosOfIsColimitCokernelCofork CategoryTheory.Limits.Cofork.π	—	—
compatibilityOfZerosOfIsColimitCokernelCofork_φQ 📖	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₃	φQ CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.RightHomologyData.ofZeros CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork compatibilityOfZerosOfIsColimitCokernelCofork CategoryTheory.Limits.Cofork.π	—	—
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.RightHomologyData.ofIsLimitKernelFork CategoryTheory.ShortComplex.RightHomologyData.ofZeros compatibilityOfZerosOfIsLimitKernelFork CategoryTheory.Limits.Fork.ι	—	—
compatibilityOfZerosOfIsLimitKernelFork_φQ 📖	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₃	φQ CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork CategoryTheory.ShortComplex.RightHomologyData.ofZeros compatibilityOfZerosOfIsLimitKernelFork CategoryTheory.ShortComplex.RightHomologyData.Q	—	—
congr_φH 📖	mathematical	—	φH	—	—
congr_φQ 📖	mathematical	—	φQ	—	—
id_φH 📖	mathematical	—	φH CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory id CategoryTheory.ShortComplex.RightHomologyData.H	—	—
id_φQ 📖	mathematical	—	φQ CategoryTheory.CategoryStruct.id CategoryTheory.ShortComplex CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory id CategoryTheory.ShortComplex.RightHomologyData.Q	—	—
instSubsingleton 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyMapData	—	CategoryTheory.cancel_epi CategoryTheory.ShortComplex.RightHomologyData.instEpiP commp CategoryTheory.cancel_mono CategoryTheory.ShortComplex.RightHomologyData.instMonoι commι
ofEpiOfIsIsoOfMono'_φH 📖	mathematical	—	φH CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' ofEpiOfIsIsoOfMono' CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.RightHomologyData.H	—	—
ofEpiOfIsIsoOfMono'_φQ 📖	mathematical	—	φQ CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono' ofEpiOfIsIsoOfMono' CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.RightHomologyData.Q	—	—
ofEpiOfIsIsoOfMono_φH 📖	mathematical	—	φH CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono ofEpiOfIsIsoOfMono CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.RightHomologyData.H	—	—
ofEpiOfIsIsoOfMono_φQ 📖	mathematical	—	φQ CategoryTheory.ShortComplex.RightHomologyData.ofEpiOfIsIsoOfMono ofEpiOfIsIsoOfMono CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.RightHomologyData.Q	—	—
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.RightHomologyData.ofIsColimitCokernelCofork ofIsColimitCokernelCofork	—	—
ofIsColimitCokernelCofork_φQ 📖	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.π	φQ CategoryTheory.ShortComplex.RightHomologyData.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.RightHomologyData.ofIsLimitKernelFork ofIsLimitKernelFork	—	—
ofIsLimitKernelFork_φQ 📖	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.τ₂	φQ CategoryTheory.ShortComplex.RightHomologyData.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.RightHomologyData.ofZeros ofZeros CategoryTheory.ShortComplex.Hom.τ₂	—	—
ofZeros_φQ 📖	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₃	φQ CategoryTheory.ShortComplex.RightHomologyData.ofZeros ofZeros CategoryTheory.ShortComplex.Hom.τ₂	—	—
op_φH 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyMapData.φH Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.ShortComplex.op CategoryTheory.ShortComplex.opMap CategoryTheory.ShortComplex.RightHomologyData.op op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.RightHomologyData.H φH	—	—
op_φK 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyMapData.φK Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite CategoryTheory.ShortComplex.op CategoryTheory.ShortComplex.opMap CategoryTheory.ShortComplex.RightHomologyData.op op Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.RightHomologyData.Q φQ	—	—
opcyclesMap'_eq 📖	mathematical	—	CategoryTheory.ShortComplex.opcyclesMap' φQ	—	congr_φQ instSubsingleton
opcyclesMap_comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.RightHomologyData.Q CategoryTheory.ShortComplex.opcyclesMap CategoryTheory.Iso.hom CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso φQ	—	opcyclesMap_eq CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
opcyclesMap_eq 📖	mathematical	—	CategoryTheory.ShortComplex.opcyclesMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.RightHomologyData.Q CategoryTheory.Iso.hom CategoryTheory.ShortComplex.RightHomologyData.opcyclesIso φQ CategoryTheory.Iso.inv	—	opcyclesMap'_eq CategoryTheory.ShortComplex.opcyclesMap'_comp CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
rightHomologyMap'_eq 📖	mathematical	—	CategoryTheory.ShortComplex.rightHomologyMap' φH	—	congr_φH instSubsingleton
rightHomologyMap_comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.rightHomology CategoryTheory.ShortComplex.RightHomologyData.H CategoryTheory.ShortComplex.rightHomologyMap CategoryTheory.Iso.hom CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso φH	—	rightHomologyMap_eq CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
rightHomologyMap_eq 📖	mathematical	—	CategoryTheory.ShortComplex.rightHomologyMap CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.rightHomology CategoryTheory.ShortComplex.RightHomologyData.H CategoryTheory.Iso.hom CategoryTheory.ShortComplex.RightHomologyData.rightHomologyIso φH CategoryTheory.Iso.inv	—	rightHomologyMap'_eq CategoryTheory.ShortComplex.rightHomologyMap'_comp CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
unop_φH 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyMapData.φH CategoryTheory.ShortComplex.unop CategoryTheory.ShortComplex.unopMap CategoryTheory.ShortComplex.RightHomologyData.unop unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.RightHomologyData.H Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite φH	—	—
unop_φK 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyMapData.φK CategoryTheory.ShortComplex.unop CategoryTheory.ShortComplex.unopMap CategoryTheory.ShortComplex.RightHomologyData.unop unop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.RightHomologyData.Q Opposite CategoryTheory.Category.opposite CategoryTheory.Limits.hasZeroMorphismsOpposite φQ	—	—
zero_φH 📖	mathematical	—	φH Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instZeroHom zero CategoryTheory.ShortComplex.RightHomologyData.H CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
zero_φQ 📖	mathematical	—	φQ Quiver.Hom CategoryTheory.ShortComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.instZeroHom zero CategoryTheory.ShortComplex.RightHomologyData.Q CategoryTheory.Limits.HasZeroMorphisms.zero	—	—

---

← Back to Index