Page

📁 Source: Mathlib/Algebra/Homology/SpectralObject/Page.lean

Statistics

Metric	Count
Definitions E, EIsoH, EToCycles, cokernelSequenceCyclesE, cokernelSequenceCyclesEIso, cokernelSequenceE, cokernelSequenceOpcyclesE, cyclesIso, cyclesIsoH, descE, homologyDataIdId, instEpiπE, instMonoιE, kernelSequenceCyclesE, kernelSequenceE, kernelSequenceOpcyclesE, kernelSequenceOpcyclesEIso, leftHomologyDataShortComplex, liftE, map, opcyclesIso, opcyclesIsoH, opcyclesToE, rightHomologyDataShortComplex, shortComplex, shortComplexMap, shortComplexOpcyclesThreeδ₂Toδ₁, ιE, πE	29
Theorems EIsoH_hom_naturality, EIsoH_hom_opcyclesIsoH_inv, EIsoH_hom_opcyclesIsoH_inv_assoc, EToCycles_i, EToCycles_i_assoc, cokernelSequenceCyclesEIso_hom_τ₁, cokernelSequenceCyclesEIso_hom_τ₂, cokernelSequenceCyclesEIso_hom_τ₃, cokernelSequenceCyclesEIso_inv_τ₁, cokernelSequenceCyclesEIso_inv_τ₂, cokernelSequenceCyclesEIso_inv_τ₃, cokernelSequenceCyclesE_X₁, cokernelSequenceCyclesE_X₂, cokernelSequenceCyclesE_X₃, cokernelSequenceCyclesE_exact, cokernelSequenceCyclesE_f, cokernelSequenceCyclesE_g, cokernelSequenceE_X₁, cokernelSequenceE_X₂, cokernelSequenceE_X₃, cokernelSequenceE_exact, cokernelSequenceE_f, cokernelSequenceE_g, cokernelSequenceOpcyclesE_X₁, cokernelSequenceOpcyclesE_X₂, cokernelSequenceOpcyclesE_X₃, cokernelSequenceOpcyclesE_exact, cokernelSequenceOpcyclesE_f, cokernelSequenceOpcyclesE_g, cyclesIsoH_hom_EIsoH_inv, cyclesIsoH_hom_EIsoH_inv_assoc, cyclesIsoH_hom_inv_id, cyclesIsoH_hom_inv_id_assoc, cyclesIsoH_inv, cyclesIsoH_inv_hom_id, cyclesIsoH_inv_hom_id_assoc, cyclesIso_hom_i, cyclesIso_hom_i_assoc, cyclesIso_inv_cyclesMap, cyclesIso_inv_cyclesMap_assoc, cyclesIso_inv_i, cyclesIso_inv_i_assoc, homologyDataIdId_iso_hom, homologyDataIdId_iso_inv, homologyDataIdId_left_H, homologyDataIdId_left_K, homologyDataIdId_left_i, homologyDataIdId_left_π, homologyDataIdId_right_H, homologyDataIdId_right_Q, homologyDataIdId_right_p, homologyDataIdId_right_ι, instEpiGCokernelSequenceCyclesE, instEpiGCokernelSequenceE, instEpiGCokernelSequenceOpcyclesE, instEpiGShortComplexOpcyclesThreeδ₂Toδ₁, instEpiOpcyclesToE, instMonoEToCycles, instMonoFKernelSequenceCyclesE, instMonoFKernelSequenceE, instMonoFKernelSequenceOpcyclesE, instMonoFShortComplexOpcyclesThreeδ₂Toδ₁, isIso_map, isZero_E_of_isZero_H, isZero_H_obj_of_isIso, kernelSequenceCyclesE_X₁, kernelSequenceCyclesE_X₂, kernelSequenceCyclesE_X₃, kernelSequenceCyclesE_exact, kernelSequenceCyclesE_f, kernelSequenceCyclesE_g, kernelSequenceE_X₁, kernelSequenceE_X₂, kernelSequenceE_X₃, kernelSequenceE_exact, kernelSequenceE_f, kernelSequenceE_g, kernelSequenceOpcyclesEIso_hom_τ₁, kernelSequenceOpcyclesEIso_hom_τ₂, kernelSequenceOpcyclesEIso_hom_τ₃, kernelSequenceOpcyclesEIso_inv_τ₁, kernelSequenceOpcyclesEIso_inv_τ₂, kernelSequenceOpcyclesEIso_inv_τ₃, kernelSequenceOpcyclesE_X₁, kernelSequenceOpcyclesE_X₂, kernelSequenceOpcyclesE_X₃, kernelSequenceOpcyclesE_exact, kernelSequenceOpcyclesE_f, kernelSequenceOpcyclesE_g, leftHomologyDataShortComplex_H, leftHomologyDataShortComplex_K, leftHomologyDataShortComplex_f', leftHomologyDataShortComplex_i, leftHomologyDataShortComplex_π, liftE_ιE_fromOpcycles, liftE_ιE_fromOpcycles_assoc, map_comp, map_comp_assoc, map_id, map_ιE, map_ιE_assoc, opcyclesIsoH_hom, opcyclesIsoH_hom_inv_id, opcyclesIsoH_hom_inv_id_assoc, opcyclesIsoH_inv_hom_id, opcyclesIsoH_inv_hom_id_assoc, opcyclesIso_hom_δFromOpcycles, opcyclesIso_hom_δFromOpcycles_assoc, opcyclesMap_opcyclesIso_hom, opcyclesMap_opcyclesIso_hom_assoc, opcyclesMap_threeδ₂Toδ₁_opcyclesToE, opcyclesMap_threeδ₂Toδ₁_opcyclesToE_assoc, opcyclesToE_map, opcyclesToE_map_assoc, opcyclesToE_ιE, opcyclesToE_ιE_assoc, p_opcyclesIso_hom, p_opcyclesIso_hom_assoc, p_opcyclesIso_inv, p_opcyclesIso_inv_assoc, p_opcyclesToE, p_opcyclesToE_assoc, rightHomologyDataShortComplex_H, rightHomologyDataShortComplex_Q, rightHomologyDataShortComplex_g', rightHomologyDataShortComplex_p, rightHomologyDataShortComplex_ι, shortComplexMap_comp, shortComplexMap_comp_assoc, shortComplexMap_id, shortComplexMap_τ₁, shortComplexMap_τ₂, shortComplexMap_τ₃, shortComplexOpcyclesThreeδ₂Toδ₁_X₁, shortComplexOpcyclesThreeδ₂Toδ₁_X₂, shortComplexOpcyclesThreeδ₂Toδ₁_X₃, shortComplexOpcyclesThreeδ₂Toδ₁_exact, shortComplexOpcyclesThreeδ₂Toδ₁_f, shortComplexOpcyclesThreeδ₂Toδ₁_g, shortComplexOpcyclesThreeδ₂Toδ₁_shortExact, shortComplex_X₁, shortComplex_X₂, shortComplex_X₃, shortComplex_f, shortComplex_g, toCycles_πE_descE, toCycles_πE_descE_assoc, δToCycles_cyclesIso_inv, δToCycles_cyclesIso_inv_assoc, δToCycles_πE, δToCycles_πE_assoc, δ_eq_zero_of_isIso₁, δ_eq_zero_of_isIso₂, ιE_δFromOpcycles, ιE_δFromOpcycles_assoc, πE_EToCycles, πE_EToCycles_assoc, πE_map, πE_map_assoc, πE_ιE, πE_ιE_assoc	161
Total	190

CategoryTheory.Abelian.SpectralObject

Definitions

Name	Category	Theorems
E 📖	CompOp	114 math math: isoMapFourδ₄Toδ₄'_inv_hom_id, isoMapFourδ₄Toδ₄'_inv_hom_id_assoc, instMonoEToCycles, EIsoH_hom_opcyclesIsoH_inv_assoc, opcyclesMap_threeδ₂Toδ₁_opcyclesToE_assoc, opcyclesToE_map, isZero_E_of_isZero_H, dKernelSequence_X₂, isIso_map_fourδ₄Toδ₃_of_isZero, mapFourδ₄Toδ₃'_comp_assoc, instEpiMapFourδ₄Toδ₃, toCycles_πE_d, cokernelSequenceCyclesEIso_inv_τ₃, δToCycles_πE, kernelSequenceCyclesE_X₁, SpectralSequence.HomologyData.kf_w, d_ιE_fromOpcycles, πE_EToCycles, toCycles_πE_d_assoc, isIso_map, shortComplexOpcyclesThreeδ₂Toδ₁_X₃, cyclesIsoH_hom_EIsoH_inv, dCokernelSequence_X₂, dHomologyData_iso_inv, kernelSequenceOpcyclesE_X₁, EToCycles_i_assoc, map_fourδ₁Toδ₀_d, SpectralSequence.HomologyData.kfSc_f, πE_ιE, cokernelSequenceOpcyclesE_X₃, mapFourδ₄Toδ₃'_comp, d_d, πE_EIsoH_hom_assoc, d_EIsoH_hom, πE_map_assoc, map_fourδ₁Toδ₀_d_assoc, cokernelSequenceE_g, kernelSequenceE_X₁, p_opcyclesToE, dKernelSequence_X₃, ιE_δFromOpcycles_assoc, liftE_ιE_fromOpcycles, dHomologyData_right_Q, cokernelSequenceCyclesEIso_hom_τ₃, dHomologyData_left_H, map_ιE_assoc, isoMapFourδ₁Toδ₀'_hom_inv_id, δToCycles_πE_assoc, toCycles_πE_descE_assoc, cyclesIsoH_hom_EIsoH_inv_assoc, πE_EIsoH_hom, πE_d_ιE_assoc, kernelSequenceE_f, d_map_fourδ₄Toδ₃, isoMapFourδ₁Toδ₀'_inv_hom_id, d_ιE_fromOpcycles_assoc, dCokernelSequence_X₁, d_map_fourδ₄Toδ₃_assoc, mapFourδ₁Toδ₀'_comp_assoc, d_EIsoH_hom_assoc, cokernelSequenceCyclesE_X₃, opcyclesToE_map_assoc, SpectralSequence.HomologyData.isIso_mapFourδ₁Toδ₀', dHomologyData_right_H, map_comp, isoMapFourδ₁Toδ₀'_hom_inv_id_assoc, πE_ιE_assoc, isoMapFourδ₁Toδ₀'_inv_hom_id_assoc, mono_map, mapFourδ₁Toδ₀'_comp, dHomologyData_left_K, isoMapFourδ₄Toδ₄'_hom_inv_id, SpectralSequence.pageD_eq, πE_EToCycles_assoc, isIso_mapFourδ₁Toδ₀', isIso_map_fourδ₁Toδ₀_of_isZero, cokernelSequenceE_X₃, mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃', ιE_δFromOpcycles, opcyclesToE_ιE, d_d_assoc, EToCycles_i, map_ιE, dShortComplex_X₃, SpectralSequence.HomologyData.kfSc_X₁, dKernelSequence_X₁, opcyclesToE_ιE_assoc, instMonoMapFourδ₁Toδ₀, dHomologyData_iso_hom, instEpiOpcyclesToE, p_opcyclesToE_assoc, dCokernelSequence_X₃, isIso_mapFourδ₂Toδ₁', EIsoH_hom_opcyclesIsoH_inv, map_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃_assoc, dShortComplex_X₂, epi_map, toCycles_πE_descE, EIsoH_hom_naturality, isIso_mapFourδ₄Toδ₃', πE_map, liftE_ιE_fromOpcycles_assoc, isIso_map_fourδ₄Toδ₃, map_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃, map_comp_assoc, isoMapFourδ₁Toδ₀'_hom, isIso_map_fourδ₁Toδ₀, isoMapFourδ₄Toδ₄'_hom_inv_id_assoc, dShortComplex_X₁, mapFourδ₁Toδ₀'_mapFourδ₃Toδ₃'_assoc, opcyclesMap_threeδ₂Toδ₁_opcyclesToE, isoMapFourδ₄Toδ₃'_hom, πE_d_ιE, map_id
EIsoH 📖	CompOp	9 math math: EIsoH_hom_opcyclesIsoH_inv_assoc, cyclesIsoH_hom_EIsoH_inv, πE_EIsoH_hom_assoc, d_EIsoH_hom, cyclesIsoH_hom_EIsoH_inv_assoc, πE_EIsoH_hom, d_EIsoH_hom_assoc, EIsoH_hom_opcyclesIsoH_inv, EIsoH_hom_naturality
EToCycles 📖	CompOp	6 math math: instMonoEToCycles, πE_EToCycles, EToCycles_i_assoc, kernelSequenceCyclesE_f, πE_EToCycles_assoc, EToCycles_i
cokernelSequenceCyclesE 📖	CompOp	13 math math: cokernelSequenceCyclesEIso_hom_τ₁, cokernelSequenceCyclesEIso_inv_τ₃, cokernelSequenceCyclesE_exact, cokernelSequenceCyclesEIso_hom_τ₃, cokernelSequenceCyclesE_g, cokernelSequenceCyclesE_X₁, cokernelSequenceCyclesEIso_hom_τ₂, cokernelSequenceCyclesE_f, cokernelSequenceCyclesEIso_inv_τ₁, cokernelSequenceCyclesE_X₂, cokernelSequenceCyclesE_X₃, instEpiGCokernelSequenceCyclesE, cokernelSequenceCyclesEIso_inv_τ₂
cokernelSequenceCyclesEIso 📖	CompOp	6 math math: cokernelSequenceCyclesEIso_hom_τ₁, cokernelSequenceCyclesEIso_inv_τ₃, cokernelSequenceCyclesEIso_hom_τ₃, cokernelSequenceCyclesEIso_hom_τ₂, cokernelSequenceCyclesEIso_inv_τ₁, cokernelSequenceCyclesEIso_inv_τ₂
cokernelSequenceE 📖	CompOp	7 math math: cokernelSequenceE_g, cokernelSequenceE_X₂, cokernelSequenceE_exact, cokernelSequenceE_X₃, instEpiGCokernelSequenceE, cokernelSequenceE_X₁, cokernelSequenceE_f
cokernelSequenceOpcyclesE 📖	CompOp	7 math math: cokernelSequenceOpcyclesE_exact, cokernelSequenceOpcyclesE_X₃, instEpiGCokernelSequenceOpcyclesE, cokernelSequenceOpcyclesE_X₂, cokernelSequenceOpcyclesE_X₁, cokernelSequenceOpcyclesE_g, cokernelSequenceOpcyclesE_f
cyclesIso 📖	CompOp	10 math math: cyclesIso_inv_i_assoc, δToCycles_cyclesIso_inv_assoc, cyclesIso_hom_i, cyclesIso_hom_i_assoc, cyclesIso_inv_cyclesMap_assoc, cokernelSequenceCyclesEIso_hom_τ₂, δToCycles_cyclesIso_inv, cyclesIso_inv_i, cokernelSequenceCyclesEIso_inv_τ₂, cyclesIso_inv_cyclesMap
cyclesIsoH 📖	CompOp	9 math math: cyclesIsoH_hom_EIsoH_inv, πE_EIsoH_hom_assoc, cyclesIsoH_inv_hom_id, cyclesIsoH_inv_hom_id_assoc, cyclesIsoH_hom_EIsoH_inv_assoc, πE_EIsoH_hom, cyclesIsoH_hom_inv_id_assoc, cyclesIsoH_hom_inv_id, cyclesIsoH_inv
descE 📖	CompOp	2 math math: toCycles_πE_descE_assoc, toCycles_πE_descE
homologyDataIdId 📖	CompOp	10 math math: homologyDataIdId_left_π, homologyDataIdId_left_i, homologyDataIdId_left_H, homologyDataIdId_iso_inv, homologyDataIdId_iso_hom, homologyDataIdId_right_p, homologyDataIdId_right_ι, homologyDataIdId_left_K, homologyDataIdId_right_H, homologyDataIdId_right_Q
instEpiπE 📖	CompOp	—
instMonoιE 📖	CompOp	—
kernelSequenceCyclesE 📖	CompOp	7 math math: kernelSequenceCyclesE_X₁, instMonoFKernelSequenceCyclesE, kernelSequenceCyclesE_g, kernelSequenceCyclesE_f, kernelSequenceCyclesE_exact, kernelSequenceCyclesE_X₂, kernelSequenceCyclesE_X₃
kernelSequenceE 📖	CompOp	7 math math: instMonoFKernelSequenceE, kernelSequenceE_exact, kernelSequenceE_g, kernelSequenceE_X₁, kernelSequenceE_f, kernelSequenceE_X₂, kernelSequenceE_X₃
kernelSequenceOpcyclesE 📖	CompOp	13 math math: instMonoFKernelSequenceOpcyclesE, kernelSequenceOpcyclesE_X₁, kernelSequenceOpcyclesE_X₃, kernelSequenceOpcyclesEIso_inv_τ₂, kernelSequenceOpcyclesEIso_hom_τ₃, kernelSequenceOpcyclesE_exact, kernelSequenceOpcyclesEIso_hom_τ₂, kernelSequenceOpcyclesE_X₂, kernelSequenceOpcyclesE_f, kernelSequenceOpcyclesEIso_inv_τ₁, kernelSequenceOpcyclesEIso_inv_τ₃, kernelSequenceOpcyclesEIso_hom_τ₁, kernelSequenceOpcyclesE_g
kernelSequenceOpcyclesEIso 📖	CompOp	6 math math: kernelSequenceOpcyclesEIso_inv_τ₂, kernelSequenceOpcyclesEIso_hom_τ₃, kernelSequenceOpcyclesEIso_hom_τ₂, kernelSequenceOpcyclesEIso_inv_τ₁, kernelSequenceOpcyclesEIso_inv_τ₃, kernelSequenceOpcyclesEIso_hom_τ₁
leftHomologyDataShortComplex 📖	CompOp	5 math math: leftHomologyDataShortComplex_H, leftHomologyDataShortComplex_f', leftHomologyDataShortComplex_π, leftHomologyDataShortComplex_i, leftHomologyDataShortComplex_K
liftE 📖	CompOp	2 math math: liftE_ιE_fromOpcycles, liftE_ιE_fromOpcycles_assoc
map 📖	CompOp	33 math math: opcyclesToE_map, isIso_map_fourδ₄Toδ₃_of_isZero, instEpiMapFourδ₄Toδ₃, isIso_map, dHomologyData_iso_inv, map_fourδ₁Toδ₀_d, πE_map_assoc, map_fourδ₁Toδ₀_d_assoc, dHomologyData_left_i, map_ιE_assoc, d_map_fourδ₄Toδ₃, d_map_fourδ₄Toδ₃_assoc, dHomologyData_right_ι, opcyclesToE_map_assoc, map_comp, dHomologyData_right_p, mono_map, isIso_map_fourδ₁Toδ₀_of_isZero, map_ιE, dKernelSequence_f, dHomologyData_left_π, instMonoMapFourδ₁Toδ₀, dHomologyData_iso_hom, dCokernelSequence_g, map_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃_assoc, epi_map, EIsoH_hom_naturality, πE_map, isIso_map_fourδ₄Toδ₃, map_fourδ₁Toδ₀_EMap_fourδ₄Toδ₃, map_comp_assoc, isIso_map_fourδ₁Toδ₀, map_id
opcyclesIso 📖	CompOp	10 math math: opcyclesIso_hom_δFromOpcycles, p_opcyclesIso_inv, kernelSequenceOpcyclesEIso_inv_τ₂, p_opcyclesIso_hom, p_opcyclesIso_hom_assoc, kernelSequenceOpcyclesEIso_hom_τ₂, p_opcyclesIso_inv_assoc, opcyclesIso_hom_δFromOpcycles_assoc, opcyclesMap_opcyclesIso_hom_assoc, opcyclesMap_opcyclesIso_hom
opcyclesIsoH 📖	CompOp	7 math math: EIsoH_hom_opcyclesIsoH_inv_assoc, opcyclesIsoH_hom, opcyclesIsoH_inv_hom_id_assoc, opcyclesIsoH_inv_hom_id, opcyclesIsoH_hom_inv_id, EIsoH_hom_opcyclesIsoH_inv, opcyclesIsoH_hom_inv_id_assoc
opcyclesToE 📖	CompOp	11 math math: opcyclesMap_threeδ₂Toδ₁_opcyclesToE_assoc, opcyclesToE_map, p_opcyclesToE, opcyclesToE_map_assoc, opcyclesToE_ιE, opcyclesToE_ιE_assoc, instEpiOpcyclesToE, shortComplexOpcyclesThreeδ₂Toδ₁_g, p_opcyclesToE_assoc, cokernelSequenceOpcyclesE_g, opcyclesMap_threeδ₂Toδ₁_opcyclesToE
rightHomologyDataShortComplex 📖	CompOp	5 math math: rightHomologyDataShortComplex_ι, rightHomologyDataShortComplex_H, rightHomologyDataShortComplex_g', rightHomologyDataShortComplex_Q, rightHomologyDataShortComplex_p
shortComplex 📖	CompOp	59 math math: leftHomologyDataShortComplex_H, homologyDataIdId_left_π, cokernelSequenceCyclesEIso_hom_τ₁, cyclesIso_inv_i_assoc, cokernelSequenceCyclesEIso_inv_τ₃, shortComplex_X₂, opcyclesIso_hom_δFromOpcycles, homologyDataIdId_left_i, homologyDataIdId_left_H, δToCycles_cyclesIso_inv_assoc, cyclesIso_hom_i, homologyDataIdId_iso_inv, cyclesIso_hom_i_assoc, leftHomologyDataShortComplex_f', shortComplex_g, cyclesIso_inv_cyclesMap_assoc, homologyDataIdId_iso_hom, p_opcyclesIso_inv, kernelSequenceOpcyclesEIso_inv_τ₂, rightHomologyDataShortComplex_ι, homologyDataIdId_right_p, rightHomologyDataShortComplex_H, shortComplexMap_id, cokernelSequenceCyclesEIso_hom_τ₃, kernelSequenceOpcyclesEIso_hom_τ₃, p_opcyclesIso_hom, shortComplexMap_comp_assoc, p_opcyclesIso_hom_assoc, homologyDataIdId_right_ι, cokernelSequenceCyclesEIso_hom_τ₂, cokernelSequenceCyclesEIso_inv_τ₁, kernelSequenceOpcyclesEIso_hom_τ₂, shortComplex_f, leftHomologyDataShortComplex_π, leftHomologyDataShortComplex_i, p_opcyclesIso_inv_assoc, shortComplexMap_τ₂, homologyDataIdId_left_K, shortComplexMap_τ₃, δToCycles_cyclesIso_inv, rightHomologyDataShortComplex_g', opcyclesIso_hom_δFromOpcycles_assoc, homologyDataIdId_right_H, shortComplexMap_τ₁, rightHomologyDataShortComplex_Q, shortComplex_X₁, opcyclesMap_opcyclesIso_hom_assoc, homologyDataIdId_right_Q, shortComplex_X₃, rightHomologyDataShortComplex_p, kernelSequenceOpcyclesEIso_inv_τ₁, cyclesIso_inv_i, kernelSequenceOpcyclesEIso_inv_τ₃, cokernelSequenceCyclesEIso_inv_τ₂, shortComplexMap_comp, cyclesIso_inv_cyclesMap, leftHomologyDataShortComplex_K, kernelSequenceOpcyclesEIso_hom_τ₁, opcyclesMap_opcyclesIso_hom
shortComplexMap 📖	CompOp	10 math math: cyclesIso_inv_cyclesMap_assoc, shortComplexMap_id, shortComplexMap_comp_assoc, shortComplexMap_τ₂, shortComplexMap_τ₃, shortComplexMap_τ₁, opcyclesMap_opcyclesIso_hom_assoc, shortComplexMap_comp, cyclesIso_inv_cyclesMap, opcyclesMap_opcyclesIso_hom
shortComplexOpcyclesThreeδ₂Toδ₁ 📖	CompOp	9 math math: shortComplexOpcyclesThreeδ₂Toδ₁_X₃, shortComplexOpcyclesThreeδ₂Toδ₁_exact, instEpiGShortComplexOpcyclesThreeδ₂Toδ₁, instMonoFShortComplexOpcyclesThreeδ₂Toδ₁, shortComplexOpcyclesThreeδ₂Toδ₁_shortExact, shortComplexOpcyclesThreeδ₂Toδ₁_g, shortComplexOpcyclesThreeδ₂Toδ₁_f, shortComplexOpcyclesThreeδ₂Toδ₁_X₁, shortComplexOpcyclesThreeδ₂Toδ₁_X₂
ιE 📖	CompOp	20 math math: EIsoH_hom_opcyclesIsoH_inv_assoc, d_ιE_fromOpcycles, EToCycles_i_assoc, πE_ιE, ιE_δFromOpcycles_assoc, liftE_ιE_fromOpcycles, map_ιE_assoc, πE_d_ιE_assoc, kernelSequenceE_f, d_ιE_fromOpcycles_assoc, πE_ιE_assoc, ιE_δFromOpcycles, opcyclesToE_ιE, EToCycles_i, map_ιE, kernelSequenceOpcyclesE_f, opcyclesToE_ιE_assoc, EIsoH_hom_opcyclesIsoH_inv, liftE_ιE_fromOpcycles_assoc, πE_d_ιE
πE 📖	CompOp	22 math math: toCycles_πE_d, δToCycles_πE, πE_EToCycles, toCycles_πE_d_assoc, cyclesIsoH_hom_EIsoH_inv, πE_ιE, πE_EIsoH_hom_assoc, πE_map_assoc, cokernelSequenceE_g, p_opcyclesToE, δToCycles_πE_assoc, toCycles_πE_descE_assoc, cyclesIsoH_hom_EIsoH_inv_assoc, cokernelSequenceCyclesE_g, πE_EIsoH_hom, πE_d_ιE_assoc, πE_ιE_assoc, πE_EToCycles_assoc, p_opcyclesToE_assoc, toCycles_πE_descE, πE_map, πE_d_ιE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
EIsoH_hom_naturality 📖	mathematical	Quiver.Hom CategoryTheory.ComposableArrows CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₃ CategoryTheory.CategoryStruct.id CategoryTheory.ComposableArrows.homMk₃ CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows.mk₁ CategoryTheory.ComposableArrows.naturality'	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E CategoryTheory.CategoryStruct.id CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ map CategoryTheory.Iso.hom EIsoH CategoryTheory.Functor.map	—	CategoryTheory.ComposableArrows.naturality' CategoryTheory.ShortComplex.LeftHomologyMapData.homologyMap_comm CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ComposableArrows.hom_ext₁
EIsoH_hom_opcyclesIsoH_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E CategoryTheory.CategoryStruct.id CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ opcycles CategoryTheory.Iso.hom EIsoH CategoryTheory.Iso.inv opcyclesIsoH ιE	—	CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.comp_id CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv CategoryTheory.Iso.inv_hom_id_assoc instEpiPOpcycles p_opcyclesIso_inv_assoc CategoryTheory.ShortComplex.RightHomologyData.pOpcycles_comp_opcyclesIso_hom p_fromOpcycles CategoryTheory.Functor.map_id CategoryTheory.ComposableArrows.hom_ext₁ CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc opcyclesIsoH_hom opcyclesIsoH_inv_hom_id CategoryTheory.ShortComplex.HomologyData.left_homologyIso_eq_right_homologyIso_trans_iso_symm CategoryTheory.ShortComplex.RightHomologyData.homologyIso_hom_comp_ι
EIsoH_hom_opcyclesIsoH_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E CategoryTheory.CategoryStruct.id CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Iso.hom EIsoH opcycles CategoryTheory.Iso.inv opcyclesIsoH ιE	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' EIsoH_hom_opcyclesIsoH_inv
EToCycles_i 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E cycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ EToCycles iCycles opcycles ιE fromOpcycles	—	liftCycles_i
EToCycles_i_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E cycles EToCycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ iCycles opcycles ιE fromOpcycles	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' EToCycles_i
cokernelSequenceCyclesEIso_hom_τ₁ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceCyclesE CategoryTheory.ShortComplex.X₁ shortComplex CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.homology CategoryTheory.ShortComplex.toCycles CategoryTheory.ShortComplex.homologyπ CategoryTheory.Iso.hom CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.toCycles_comp_homologyπ cokernelSequenceCyclesEIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.toCycles_comp_homologyπ
cokernelSequenceCyclesEIso_hom_τ₂ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceCyclesE CategoryTheory.ShortComplex.X₁ shortComplex CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.homology CategoryTheory.ShortComplex.toCycles CategoryTheory.ShortComplex.homologyπ CategoryTheory.Iso.hom CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.toCycles_comp_homologyπ cokernelSequenceCyclesEIso CategoryTheory.Iso.inv cycles cyclesIso	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.toCycles_comp_homologyπ
cokernelSequenceCyclesEIso_hom_τ₃ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceCyclesE CategoryTheory.ShortComplex.X₁ shortComplex CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.homology CategoryTheory.ShortComplex.toCycles CategoryTheory.ShortComplex.homologyπ CategoryTheory.Iso.hom CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.toCycles_comp_homologyπ cokernelSequenceCyclesEIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct E	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.toCycles_comp_homologyπ
cokernelSequenceCyclesEIso_inv_τ₁ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₁ shortComplex CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.homology CategoryTheory.ShortComplex.toCycles CategoryTheory.ShortComplex.homologyπ cokernelSequenceCyclesE CategoryTheory.Iso.inv CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.toCycles_comp_homologyπ cokernelSequenceCyclesEIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.toCycles_comp_homologyπ
cokernelSequenceCyclesEIso_inv_τ₂ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₁ shortComplex CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.homology CategoryTheory.ShortComplex.toCycles CategoryTheory.ShortComplex.homologyπ cokernelSequenceCyclesE CategoryTheory.Iso.inv CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.toCycles_comp_homologyπ cokernelSequenceCyclesEIso CategoryTheory.Iso.hom cycles cyclesIso	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.toCycles_comp_homologyπ
cokernelSequenceCyclesEIso_inv_τ₃ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.X₁ shortComplex CategoryTheory.ShortComplex.cycles CategoryTheory.ShortComplex.homology CategoryTheory.ShortComplex.toCycles CategoryTheory.ShortComplex.homologyπ cokernelSequenceCyclesE CategoryTheory.Iso.inv CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.toCycles_comp_homologyπ cokernelSequenceCyclesEIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct E	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.toCycles_comp_homologyπ
cokernelSequenceCyclesE_X₁ 📖	mathematical	—	CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceCyclesE CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
cokernelSequenceCyclesE_X₂ 📖	mathematical	—	CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceCyclesE cycles	—	—
cokernelSequenceCyclesE_X₃ 📖	mathematical	—	CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceCyclesE E	—	—
cokernelSequenceCyclesE_exact 📖	mathematical	—	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceCyclesE	—	CategoryTheory.ShortComplex.exact_of_iso CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.toCycles_comp_homologyπ CategoryTheory.ShortComplex.exact_of_g_is_cokernel
cokernelSequenceCyclesE_f 📖	mathematical	—	CategoryTheory.ShortComplex.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceCyclesE δToCycles	—	—
cokernelSequenceCyclesE_g 📖	mathematical	—	CategoryTheory.ShortComplex.g CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceCyclesE πE	—	—
cokernelSequenceE_X₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceE CategoryTheory.Limits.biprod CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
cokernelSequenceE_X₂ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceE CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
cokernelSequenceE_X₃ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceE E	—	—
cokernelSequenceE_exact 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceE	—	CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements CategoryTheory.ShortComplex.Exact.exact_up_to_refinements cokernelSequenceCyclesE_exact CategoryTheory.Category.assoc exact₂ CategoryTheory.Preadditive.sub_comp δ_toCycles sub_self toCycles_i CategoryTheory.Limits.zero_comp CategoryTheory.eq_whisker CategoryTheory.epi_comp CategoryTheory.Limits.biprod.lift_desc CategoryTheory.Preadditive.comp_sub sub_add_cancel
cokernelSequenceE_f 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceE CategoryTheory.Limits.biprod.desc CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₂Toδ₁ δ	—	—
cokernelSequenceE_g 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.g CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceE CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles E toCycles πE	—	—
cokernelSequenceOpcyclesE_X₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceOpcyclesE CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
cokernelSequenceOpcyclesE_X₂ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceOpcyclesE opcycles	—	—
cokernelSequenceOpcyclesE_X₃ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceOpcyclesE E	—	—
cokernelSequenceOpcyclesE_exact 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceOpcyclesE	—	CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements CategoryTheory.surjective_up_to_refinements_of_epi instEpiPOpcycles CategoryTheory.ShortComplex.Exact.exact_up_to_refinements cokernelSequenceE_exact CategoryTheory.Category.assoc p_opcyclesToE CategoryTheory.Limits.comp_zero CategoryTheory.eq_whisker CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Abelian.hasBinaryBiproducts CategoryTheory.Limits.biprod.hom_ext CategoryTheory.Preadditive.add_comp CategoryTheory.Limits.BinaryBicone.inl_fst CategoryTheory.Category.comp_id CategoryTheory.Limits.BinaryBicone.inr_fst add_zero CategoryTheory.Limits.BinaryBicone.inl_snd CategoryTheory.Limits.BinaryBicone.inr_snd zero_add CategoryTheory.epi_comp Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.biprod.inl_desc CategoryTheory.Limits.biprod.inr_desc δ_pOpcycles
cokernelSequenceOpcyclesE_f 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceOpcyclesE CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ opcycles CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₂Toδ₁ pOpcycles	—	—
cokernelSequenceOpcyclesE_g 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.g CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceOpcyclesE opcyclesToE	—	—
cyclesIsoH_hom_EIsoH_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.CategoryStruct.id CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ E CategoryTheory.Iso.hom cyclesIsoH CategoryTheory.Iso.inv EIsoH πE	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.id_comp CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id instMonoICycles cyclesIso_hom_i CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles toCycles_i CategoryTheory.Functor.map_id CategoryTheory.ComposableArrows.hom_ext₁ CategoryTheory.cancel_epi CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv cyclesIsoH_inv cyclesIsoH_inv_hom_id_assoc CategoryTheory.ShortComplex.LeftHomologyData.instEpiπ CategoryTheory.ShortComplex.LeftHomologyData.π_comp_homologyIso_inv
cyclesIsoH_hom_EIsoH_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.CategoryStruct.id CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Iso.hom cyclesIsoH E CategoryTheory.Iso.inv EIsoH πE	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesIsoH_hom_EIsoH_inv
cyclesIsoH_hom_inv_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.CategoryStruct.id CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Iso.hom cyclesIsoH toCycles	—	cyclesIsoH_inv CategoryTheory.Iso.hom_inv_id
cyclesIsoH_hom_inv_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.CategoryStruct.id CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Iso.hom cyclesIsoH toCycles	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' cyclesIsoH_hom_inv_id
cyclesIsoH_inv 📖	mathematical	—	CategoryTheory.Iso.inv cycles CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cyclesIsoH toCycles	—	CategoryTheory.cancel_mono instMonoICycles toCycles_i CategoryTheory.Category.assoc CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian cyclesIso_hom_i CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles CategoryTheory.ComposableArrows.hom_ext₁
cyclesIsoH_inv_hom_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles CategoryTheory.CategoryStruct.id toCycles CategoryTheory.Iso.hom cyclesIsoH	—	cyclesIsoH_inv CategoryTheory.Iso.inv_hom_id
cyclesIsoH_inv_hom_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles CategoryTheory.CategoryStruct.id toCycles CategoryTheory.Iso.hom cyclesIsoH	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' cyclesIsoH_inv_hom_id
cyclesIso_hom_i 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.cycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian cycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Iso.hom cyclesIso iCycles CategoryTheory.ShortComplex.iCycles	—	CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_hom_comp_i
cyclesIso_hom_i_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.cycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian cycles CategoryTheory.Iso.hom cyclesIso CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ iCycles CategoryTheory.ShortComplex.iCycles	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesIso_hom_i
cyclesIso_inv_cyclesMap 📖	mathematical	CategoryTheory.ComposableArrows.homMk₂ CategoryTheory.ComposableArrows.mk₂ CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₃ CategoryTheory.ComposableArrows.naturality'	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.ShortComplex.cycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Iso.inv cyclesIso CategoryTheory.ShortComplex.cyclesMap shortComplexMap cyclesMap	—	CategoryTheory.ComposableArrows.naturality' CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.cancel_mono CategoryTheory.ShortComplex.instMonoICycles CategoryTheory.Category.assoc CategoryTheory.ShortComplex.cyclesMap_i cyclesIso_inv_i_assoc cyclesIso_inv_i cyclesMap_i
cyclesIso_inv_cyclesMap_assoc 📖	mathematical	CategoryTheory.ComposableArrows.homMk₂ CategoryTheory.ComposableArrows.mk₂ CategoryTheory.NatTrans.app Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₃ CategoryTheory.ComposableArrows.naturality'	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.ShortComplex.cycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Iso.inv cyclesIso CategoryTheory.ShortComplex.cyclesMap shortComplexMap cyclesMap	—	CategoryTheory.ComposableArrows.naturality' CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesIso_inv_cyclesMap
cyclesIso_inv_i 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.ShortComplex.cycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.X₂ CategoryTheory.Iso.inv cyclesIso CategoryTheory.ShortComplex.iCycles iCycles	—	CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso_inv_comp_iCycles
cyclesIso_inv_i_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.ShortComplex.cycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Iso.inv cyclesIso CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.iCycles iCycles	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cyclesIso_inv_i
homologyDataIdId_iso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.LeftHomologyData.ofZeros CategoryTheory.ShortComplex.HomologyData.iso homologyDataIdId CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
homologyDataIdId_iso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.LeftHomologyData.ofZeros CategoryTheory.ShortComplex.HomologyData.iso homologyDataIdId CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
homologyDataIdId_left_H 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.HomologyData.left homologyDataIdId CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
homologyDataIdId_left_K 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.K CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.HomologyData.left homologyDataIdId CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
homologyDataIdId_left_i 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.HomologyData.left homologyDataIdId CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
homologyDataIdId_left_π 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.π CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.HomologyData.left homologyDataIdId CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
homologyDataIdId_right_H 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.H CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.HomologyData.right homologyDataIdId CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
homologyDataIdId_right_Q 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.Q CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.HomologyData.right homologyDataIdId CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
homologyDataIdId_right_p 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.p CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.HomologyData.right homologyDataIdId CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
homologyDataIdId_right_ι 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.ι CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.HomologyData.right homologyDataIdId CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
instEpiGCokernelSequenceCyclesE 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceCyclesE CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	—
instEpiGCokernelSequenceE 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Epi CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceE CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	CategoryTheory.epi_comp instEpiToCycles
instEpiGCokernelSequenceOpcyclesE 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Epi CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive cokernelSequenceOpcyclesE CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	instEpiOpcyclesToE
instEpiGShortComplexOpcyclesThreeδ₂Toδ₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Epi CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplexOpcyclesThreeδ₂Toδ₁ CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.g	—	instEpiOpcyclesToE
instEpiOpcyclesToE 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Epi opcycles E opcyclesToE	—	CategoryTheory.epi_of_epi_fac CategoryTheory.epi_comp instEpiToCycles p_opcyclesToE
instMonoEToCycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Mono E cycles EToCycles	—	CategoryTheory.mono_of_mono_fac CategoryTheory.mono_comp instMonoFromOpcycles EToCycles_i
instMonoFKernelSequenceCyclesE 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Mono CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceCyclesE CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	—	instMonoEToCycles
instMonoFKernelSequenceE 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Mono CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceE CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	—	CategoryTheory.mono_comp instMonoFromOpcycles
instMonoFKernelSequenceOpcyclesE 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceOpcyclesE CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	—	—
instMonoFShortComplexOpcyclesThreeδ₂Toδ₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.Mono CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplexOpcyclesThreeδ₂Toδ₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	—	CategoryTheory.Preadditive.mono_iff_cancel_zero CategoryTheory.eq_whisker CategoryTheory.Category.assoc CategoryTheory.Limits.zero_comp CategoryTheory.Category.comp_id CategoryTheory.Functor.map_id opcyclesMap_fromOpcycles CategoryTheory.cancel_mono instMonoFromOpcycles
isIso_map 📖	mathematical	—	CategoryTheory.IsIso E map	—	CategoryTheory.ShortComplex.isIso_of_isIso CategoryTheory.ShortComplex.QuasiIso.isIso CategoryTheory.ShortComplex.quasiIso_of_isIso
isZero_E_of_isZero_H 📖	mathematical	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	CategoryTheory.Limits.IsZero E	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.exact_iff_isZero_homology CategoryTheory.ShortComplex.exact_of_isZero_X₂
isZero_H_obj_of_isIso 📖	mathematical	—	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	CategoryTheory.Category.id_comp CategoryTheory.Limits.IsZero.of_iso CategoryTheory.Category.comp_id zero₂ CategoryTheory.Limits.IsZero.iff_id_eq_zero CategoryTheory.Functor.map_id CategoryTheory.Functor.map_comp CategoryTheory.ComposableArrows.hom_ext₁
kernelSequenceCyclesE_X₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceCyclesE E	—	—
kernelSequenceCyclesE_X₂ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceCyclesE cycles	—	—
kernelSequenceCyclesE_X₃ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceCyclesE CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
kernelSequenceCyclesE_exact 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceCyclesE	—	CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements CategoryTheory.ShortComplex.Exact.exact_up_to_refinements kernelSequenceE_exact CategoryTheory.Category.assoc CategoryTheory.Limits.biprod.hom_ext CategoryTheory.Limits.biprod.lift_fst CategoryTheory.Limits.zero_comp CategoryTheory.Limits.biprod.lift_snd iCycles_δ CategoryTheory.Limits.comp_zero CategoryTheory.cancel_mono instMonoICycles EToCycles_i
kernelSequenceCyclesE_f 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceCyclesE EToCycles	—	—
kernelSequenceCyclesE_g 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.g CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceCyclesE CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ iCycles CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₁Toδ₀	—	—
kernelSequenceE_X₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceE E	—	—
kernelSequenceE_X₂ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceE CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
kernelSequenceE_X₃ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceE CategoryTheory.Limits.biprod CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
kernelSequenceE_exact 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceE	—	CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements CategoryTheory.Category.assoc CategoryTheory.Limits.biprod.lift_fst CategoryTheory.Limits.zero_comp CategoryTheory.eq_whisker CategoryTheory.ShortComplex.Exact.exact_up_to_refinements kernelSequenceOpcyclesE_exact fromOpcyles_δ liftOpcycles_fromOpcycles_assoc CategoryTheory.Limits.biprod.lift_snd Mathlib.Tactic.Reassoc.eq_whisker' liftOpcycles_fromOpcycles
kernelSequenceE_f 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceE CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E opcycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ ιE fromOpcycles	—	—
kernelSequenceE_g 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.g CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceE CategoryTheory.Limits.biprod.lift CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₁Toδ₀ δ	—	—
kernelSequenceOpcyclesEIso_hom_τ₁ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceOpcyclesE CategoryTheory.ShortComplex.homology shortComplex CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.homologyι CategoryTheory.ShortComplex.fromOpcycles CategoryTheory.Iso.hom CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.homologyι_comp_fromOpcycles kernelSequenceOpcyclesEIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.homologyι_comp_fromOpcycles
kernelSequenceOpcyclesEIso_hom_τ₂ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceOpcyclesE CategoryTheory.ShortComplex.homology shortComplex CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.homologyι CategoryTheory.ShortComplex.fromOpcycles CategoryTheory.Iso.hom CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.homologyι_comp_fromOpcycles kernelSequenceOpcyclesEIso CategoryTheory.Iso.inv opcycles opcyclesIso	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.homologyι_comp_fromOpcycles
kernelSequenceOpcyclesEIso_hom_τ₃ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceOpcyclesE CategoryTheory.ShortComplex.homology shortComplex CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.homologyι CategoryTheory.ShortComplex.fromOpcycles CategoryTheory.Iso.hom CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.homologyι_comp_fromOpcycles kernelSequenceOpcyclesEIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.homologyι_comp_fromOpcycles
kernelSequenceOpcyclesEIso_inv_τ₁ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.homology shortComplex CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.homologyι CategoryTheory.ShortComplex.fromOpcycles kernelSequenceOpcyclesE CategoryTheory.Iso.inv CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.homologyι_comp_fromOpcycles kernelSequenceOpcyclesEIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.homologyι_comp_fromOpcycles
kernelSequenceOpcyclesEIso_inv_τ₂ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.homology shortComplex CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.homologyι CategoryTheory.ShortComplex.fromOpcycles kernelSequenceOpcyclesE CategoryTheory.Iso.inv CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.homologyι_comp_fromOpcycles kernelSequenceOpcyclesEIso CategoryTheory.Iso.hom opcycles opcyclesIso	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.homologyι_comp_fromOpcycles
kernelSequenceOpcyclesEIso_inv_τ₃ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.homology shortComplex CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.X₃ CategoryTheory.ShortComplex.homologyι CategoryTheory.ShortComplex.fromOpcycles kernelSequenceOpcyclesE CategoryTheory.Iso.inv CategoryTheory.ShortComplex CategoryTheory.ShortComplex.instCategory CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.homologyι_comp_fromOpcycles kernelSequenceOpcyclesEIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.homologyι_comp_fromOpcycles
kernelSequenceOpcyclesE_X₁ 📖	mathematical	—	CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceOpcyclesE E	—	—
kernelSequenceOpcyclesE_X₂ 📖	mathematical	—	CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceOpcyclesE opcycles	—	—
kernelSequenceOpcyclesE_X₃ 📖	mathematical	—	CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceOpcyclesE CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
kernelSequenceOpcyclesE_exact 📖	mathematical	—	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceOpcyclesE	—	CategoryTheory.ShortComplex.exact_of_iso CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.homologyι_comp_fromOpcycles CategoryTheory.ShortComplex.exact_of_f_is_kernel
kernelSequenceOpcyclesE_f 📖	mathematical	—	CategoryTheory.ShortComplex.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceOpcyclesE ιE	—	—
kernelSequenceOpcyclesE_g 📖	mathematical	—	CategoryTheory.ShortComplex.g CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive kernelSequenceOpcyclesE δFromOpcycles	—	—
leftHomologyDataShortComplex_H 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex leftHomologyDataShortComplex CategoryTheory.Limits.cokernel CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles δToCycles	—	—
leftHomologyDataShortComplex_K 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.K CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex leftHomologyDataShortComplex cycles	—	—
leftHomologyDataShortComplex_f' 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.f' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex leftHomologyDataShortComplex δToCycles	—	CategoryTheory.ShortComplex.zero CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory kernelSequenceCycles_exact instMonoFKernelSequenceCycles CategoryTheory.Limits.Fork.IsLimit.hom_ext δToCycles_iCycles CategoryTheory.Limits.IsLimit.fac
leftHomologyDataShortComplex_i 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex leftHomologyDataShortComplex iCycles	—	—
leftHomologyDataShortComplex_π 📖	mathematical	—	CategoryTheory.ShortComplex.LeftHomologyData.π CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex leftHomologyDataShortComplex CategoryTheory.Limits.cokernel.π CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles δToCycles	—	—
liftE_ιE_fromOpcycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₁Toδ₀ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive δ	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ liftE opcycles ιE fromOpcycles	—	CategoryTheory.ShortComplex.Exact.lift_f CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory kernelSequenceE_exact
liftE_ιE_fromOpcycles_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₁Toδ₀ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive δ	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E liftE opcycles ιE CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ fromOpcycles	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' liftE_ιE_fromOpcycles
map_comp 📖	mathematical	—	map CategoryTheory.CategoryStruct.comp CategoryTheory.ComposableArrows CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₃ E	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian shortComplexMap_comp CategoryTheory.ShortComplex.homologyMap_comp
map_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E map CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₃	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_comp
map_id 📖	mathematical	—	map CategoryTheory.CategoryStruct.id CategoryTheory.ComposableArrows CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₃ E	—	shortComplexMap_id CategoryTheory.ShortComplex.homologyMap_id
map_ιE 📖	mathematical	Quiver.Hom CategoryTheory.ComposableArrows CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₂ CategoryTheory.ComposableArrows.homMk₂ CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows.mk₃ CategoryTheory.ComposableArrows.naturality'	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E opcycles map ιE opcyclesMap	—	CategoryTheory.ComposableArrows.naturality' CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.homologyι_naturality_assoc opcyclesMap_opcyclesIso_hom CategoryTheory.Category.assoc
map_ιE_assoc 📖	mathematical	Quiver.Hom CategoryTheory.ComposableArrows CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₂ CategoryTheory.ComposableArrows.homMk₂ CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows.mk₃ CategoryTheory.ComposableArrows.naturality'	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E map opcycles ιE opcyclesMap	—	CategoryTheory.ComposableArrows.naturality' CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_ιE
opcyclesIsoH_hom 📖	mathematical	—	CategoryTheory.Iso.hom opcycles CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ opcyclesIsoH fromOpcycles	—	CategoryTheory.cancel_epi instEpiPOpcycles p_fromOpcycles CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian p_opcyclesIso_inv_assoc CategoryTheory.ShortComplex.RightHomologyData.pOpcycles_comp_opcyclesIso_hom CategoryTheory.ComposableArrows.hom_ext₁
opcyclesIsoH_hom_inv_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles CategoryTheory.CategoryStruct.id CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ fromOpcycles CategoryTheory.Iso.inv opcyclesIsoH	—	opcyclesIsoH_hom CategoryTheory.Iso.hom_inv_id
opcyclesIsoH_hom_inv_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles CategoryTheory.CategoryStruct.id CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ fromOpcycles CategoryTheory.Iso.inv opcyclesIsoH	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' opcyclesIsoH_hom_inv_id
opcyclesIsoH_inv_hom_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ opcycles CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv opcyclesIsoH fromOpcycles	—	opcyclesIsoH_hom CategoryTheory.Iso.inv_hom_id
opcyclesIsoH_inv_hom_id_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ opcycles CategoryTheory.CategoryStruct.id CategoryTheory.Iso.inv opcyclesIsoH fromOpcycles	—	CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' opcyclesIsoH_inv_hom_id
opcyclesIso_hom_δFromOpcycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.opcycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian opcycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Iso.hom opcyclesIso δFromOpcycles CategoryTheory.ShortComplex.fromOpcycles	—	CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.cancel_epi CategoryTheory.ShortComplex.instEpiPOpcycles p_opcyclesIso_hom_assoc pOpcycles_δFromOpcycles CategoryTheory.ShortComplex.p_fromOpcycles
opcyclesIso_hom_δFromOpcycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.opcycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian opcycles CategoryTheory.Iso.hom opcyclesIso CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ δFromOpcycles CategoryTheory.ShortComplex.fromOpcycles	—	CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesIso_hom_δFromOpcycles
opcyclesMap_opcyclesIso_hom 📖	mathematical	Quiver.Hom CategoryTheory.ComposableArrows CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₂ CategoryTheory.ComposableArrows.homMk₂ CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows.mk₃ CategoryTheory.ComposableArrows.naturality'	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.opcycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian opcycles CategoryTheory.ShortComplex.opcyclesMap shortComplexMap CategoryTheory.Iso.hom opcyclesIso opcyclesMap	—	CategoryTheory.ComposableArrows.naturality' CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.cancel_epi CategoryTheory.ShortComplex.instEpiPOpcycles CategoryTheory.ShortComplex.p_opcyclesMap_assoc p_opcyclesIso_hom p_opcyclesIso_hom_assoc p_opcyclesMap
opcyclesMap_opcyclesIso_hom_assoc 📖	mathematical	Quiver.Hom CategoryTheory.ComposableArrows CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₂ CategoryTheory.ComposableArrows.homMk₂ CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows.mk₃ CategoryTheory.ComposableArrows.naturality'	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.opcycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.opcyclesMap shortComplexMap opcycles CategoryTheory.Iso.hom opcyclesIso opcyclesMap	—	CategoryTheory.ComposableArrows.naturality' CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesMap_opcyclesIso_hom
opcyclesMap_threeδ₂Toδ₁_opcyclesToE 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles E opcyclesMap CategoryTheory.ComposableArrows.threeδ₂Toδ₁ opcyclesToE Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.cancel_epi instEpiPOpcycles CategoryTheory.Limits.comp_zero p_opcyclesMap_assoc CategoryTheory.ComposableArrows.naturality' p_opcyclesToE H_map_twoδ₂Toδ₁_toCycles_assoc CategoryTheory.Limits.zero_comp
opcyclesMap_threeδ₂Toδ₁_opcyclesToE_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles opcyclesMap CategoryTheory.ComposableArrows.threeδ₂Toδ₁ E opcyclesToE Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesMap_threeδ₂Toδ₁_opcyclesToE
opcyclesToE_map 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₂ CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows.mk₃	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles E opcyclesToE map opcyclesMap	—	CategoryTheory.cancel_mono CategoryTheory.Category.assoc opcyclesToE_ιE CategoryTheory.cancel_epi instEpiPOpcycles p_opcyclesToE_assoc CategoryTheory.ComposableArrows.naturality' πE_map_assoc πE_ιE cyclesMap_i_assoc toCycles_i_assoc p_opcyclesMap_assoc p_opcyclesMap CategoryTheory.Functor.map_comp_assoc CategoryTheory.ComposableArrows.hom_ext₁ CategoryTheory.ComposableArrows.homMk₁.congr_simp CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
opcyclesToE_map_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Functor.obj Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₂ CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows.mk₃	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles E opcyclesToE map opcyclesMap	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesToE_map
opcyclesToE_ιE 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles E opcyclesToE ιE opcyclesMap CategoryTheory.ComposableArrows.threeδ₁Toδ₀	—	CategoryTheory.cancel_epi instEpiPOpcycles p_opcyclesToE_assoc πE_ιE toCycles_i_assoc p_opcyclesMap CategoryTheory.ComposableArrows.naturality'
opcyclesToE_ιE_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct opcycles E opcyclesToE ιE opcyclesMap CategoryTheory.ComposableArrows.threeδ₁Toδ₀	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' opcyclesToE_ιE
p_opcyclesIso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian opcycles CategoryTheory.ShortComplex.pOpcycles CategoryTheory.Iso.hom opcyclesIso pOpcycles	—	CategoryTheory.ShortComplex.RightHomologyData.pOpcycles_comp_opcyclesIso_hom CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian
p_opcyclesIso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.ShortComplex.opcycles CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.pOpcycles opcycles CategoryTheory.Iso.hom opcyclesIso pOpcycles	—	CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p_opcyclesIso_hom
p_opcyclesIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ opcycles CategoryTheory.ShortComplex.opcycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian pOpcycles CategoryTheory.Iso.inv opcyclesIso CategoryTheory.ShortComplex.pOpcycles	—	CategoryTheory.ShortComplex.RightHomologyData.p_comp_opcyclesIso_inv CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian
p_opcyclesIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ opcycles pOpcycles CategoryTheory.ShortComplex.opcycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Iso.inv opcyclesIso CategoryTheory.ShortComplex.pOpcycles	—	CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p_opcyclesIso_inv
p_opcyclesToE 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ opcycles E pOpcycles opcyclesToE cycles toCycles πE	—	p_descOpcycles
p_opcyclesToE_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ opcycles pOpcycles E opcyclesToE cycles toCycles πE	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p_opcyclesToE
rightHomologyDataShortComplex_H 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.H CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex rightHomologyDataShortComplex CategoryTheory.Limits.kernel opcycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ δFromOpcycles	—	—
rightHomologyDataShortComplex_Q 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.Q CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex rightHomologyDataShortComplex opcycles	—	—
rightHomologyDataShortComplex_g' 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.g' CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex rightHomologyDataShortComplex δFromOpcycles	—	CategoryTheory.ShortComplex.zero CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory cokernelSequenceOpcycles_exact instEpiGCokernelSequenceOpcycles CategoryTheory.Limits.Cofork.IsColimit.hom_ext pOpcycles_δFromOpcycles CategoryTheory.Limits.IsColimit.fac
rightHomologyDataShortComplex_p 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.p CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex rightHomologyDataShortComplex pOpcycles	—	—
rightHomologyDataShortComplex_ι 📖	mathematical	—	CategoryTheory.ShortComplex.RightHomologyData.ι CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex rightHomologyDataShortComplex CategoryTheory.Limits.kernel.ι opcycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ δFromOpcycles	—	—
shortComplexMap_comp 📖	mathematical	—	shortComplexMap CategoryTheory.CategoryStruct.comp CategoryTheory.ComposableArrows CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₃ CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.instCategory shortComplex	—	CategoryTheory.ShortComplex.hom_ext CategoryTheory.Functor.map_comp CategoryTheory.ComposableArrows.hom_ext₁
shortComplexMap_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.instCategory shortComplex shortComplexMap CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₃	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' shortComplexMap_comp
shortComplexMap_id 📖	mathematical	—	shortComplexMap CategoryTheory.CategoryStruct.id CategoryTheory.ComposableArrows CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₃ CategoryTheory.ShortComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.ShortComplex.instCategory shortComplex	—	CategoryTheory.ShortComplex.hom_ext CategoryTheory.ComposableArrows.hom_ext₁ CategoryTheory.Functor.map_id
shortComplexMap_τ₁ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex shortComplexMap CategoryTheory.Functor.map CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.ComposableArrows.homMk₁ CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows.mk₃	—	—
shortComplexMap_τ₂ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex shortComplexMap CategoryTheory.Functor.map CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.ComposableArrows.homMk₁ CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows.mk₃	—	—
shortComplexMap_τ₃ 📖	mathematical	—	CategoryTheory.ShortComplex.Hom.τ₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex shortComplexMap CategoryTheory.Functor.map CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.ComposableArrows.homMk₁ CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows.mk₃	—	—
shortComplexOpcyclesThreeδ₂Toδ₁_X₁ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplexOpcyclesThreeδ₂Toδ₁ opcycles	—	—
shortComplexOpcyclesThreeδ₂Toδ₁_X₂ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplexOpcyclesThreeδ₂Toδ₁ opcycles	—	—
shortComplexOpcyclesThreeδ₂Toδ₁_X₃ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplexOpcyclesThreeδ₂Toδ₁ E	—	—
shortComplexOpcyclesThreeδ₂Toδ₁_exact 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.Exact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplexOpcyclesThreeδ₂Toδ₁	—	CategoryTheory.Category.comp_id p_opcyclesMap CategoryTheory.ComposableArrows.naturality' CategoryTheory.Category.id_comp CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono instEpiPOpcycles CategoryTheory.IsIso.id CategoryTheory.instMonoId cokernelSequenceOpcyclesE_exact
shortComplexOpcyclesThreeδ₂Toδ₁_f 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplexOpcyclesThreeδ₂Toδ₁ opcyclesMap CategoryTheory.ComposableArrows.threeδ₂Toδ₁	—	—
shortComplexOpcyclesThreeδ₂Toδ₁_g 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.g CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplexOpcyclesThreeδ₂Toδ₁ opcyclesToE	—	—
shortComplexOpcyclesThreeδ₂Toδ₁_shortExact 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.ShortComplex.ShortExact CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplexOpcyclesThreeδ₂Toδ₁	—	shortComplexOpcyclesThreeδ₂Toδ₁_exact instMonoFShortComplexOpcyclesThreeδ₂Toδ₁ instEpiGShortComplexOpcyclesThreeδ₂Toδ₁
shortComplex_X₁ 📖	mathematical	—	CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
shortComplex_X₂ 📖	mathematical	—	CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
shortComplex_X₃ 📖	mathematical	—	CategoryTheory.ShortComplex.X₃ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁	—	—
shortComplex_f 📖	mathematical	—	CategoryTheory.ShortComplex.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex δ	—	—
shortComplex_g 📖	mathematical	—	CategoryTheory.ShortComplex.g CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex δ	—	—
toCycles_πE_descE 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₂Toδ₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive δ	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles toCycles E πE descE	—	CategoryTheory.Category.assoc CategoryTheory.ShortComplex.Exact.g_desc CategoryTheory.balanced_of_strongMonoCategory CategoryTheory.strongMonoCategory_of_regularMonoCategory CategoryTheory.regularMonoCategoryOfNormalMonoCategory CategoryTheory.Abelian.toIsNormalMonoCategory cokernelSequenceE_exact
toCycles_πE_descE_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Functor.map CategoryTheory.ComposableArrows.twoδ₂Toδ₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive δ	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles toCycles E πE descE	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toCycles_πE_descE
δToCycles_cyclesIso_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles CategoryTheory.ShortComplex.cycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian δToCycles CategoryTheory.Iso.inv cyclesIso CategoryTheory.ShortComplex.toCycles	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.cancel_mono CategoryTheory.ShortComplex.instMonoICycles CategoryTheory.Category.assoc cyclesIso_inv_i δToCycles_iCycles CategoryTheory.ShortComplex.toCycles_i
δToCycles_cyclesIso_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles δToCycles CategoryTheory.ShortComplex.cycles CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive shortComplex CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Iso.inv cyclesIso CategoryTheory.ShortComplex.toCycles	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δToCycles_cyclesIso_inv
δToCycles_πE 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles E δToCycles πE Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian δToCycles_cyclesIso_inv_assoc CategoryTheory.ShortComplex.toCycles_comp_homologyπ
δToCycles_πE_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ cycles δToCycles E πE Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' δToCycles_πE
δ_eq_zero_of_isIso₁ 📖	mathematical	—	δ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Functor.map_isIso CategoryTheory.ComposableArrows.instIsIsoOfNatNatTwoδ₁Toδ₀ zero₃
δ_eq_zero_of_isIso₂ 📖	mathematical	—	δ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Functor.map_isIso CategoryTheory.ComposableArrows.instIsIsoOfNatNatTwoδ₂Toδ₁ zero₁
ιE_δFromOpcycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E opcycles CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ ιE δFromOpcycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Category.assoc CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian opcyclesIso_hom_δFromOpcycles CategoryTheory.ShortComplex.homologyι_comp_fromOpcycles
ιE_δFromOpcycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct E opcycles ιE CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ δFromOpcycles Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιE_δFromOpcycles
πE_EToCycles 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles E πE EToCycles cyclesMap CategoryTheory.ComposableArrows.threeδ₃Toδ₂	—	CategoryTheory.cancel_mono instMonoICycles CategoryTheory.Category.assoc EToCycles_i πE_ιE_assoc p_fromOpcycles cyclesMap_i CategoryTheory.ComposableArrows.naturality'
πE_EToCycles_assoc 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles E πE EToCycles cyclesMap CategoryTheory.ComposableArrows.threeδ₃Toδ₂	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' πE_EToCycles
πE_map 📖	mathematical	Quiver.Hom CategoryTheory.ComposableArrows CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₂ CategoryTheory.ComposableArrows.homMk₂ CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows.mk₃ CategoryTheory.ComposableArrows.naturality'	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles E πE map cyclesMap	—	CategoryTheory.ComposableArrows.naturality' CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Category.assoc CategoryTheory.ShortComplex.homologyπ_naturality cyclesIso_inv_cyclesMap_assoc
πE_map_assoc 📖	mathematical	Quiver.Hom CategoryTheory.ComposableArrows CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder CategoryTheory.ComposableArrows.mk₂ CategoryTheory.ComposableArrows.homMk₂ CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows.mk₃ CategoryTheory.ComposableArrows.naturality'	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles E πE map cyclesMap	—	CategoryTheory.ComposableArrows.naturality' CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' πE_map
πE_ιE 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles E opcycles πE ιE CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ iCycles pOpcycles	—	CategoryTheory.Category.assoc CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.ShortComplex.hasRightHomology_of_hasHomology CategoryTheory.ShortComplex.homology_π_ι_assoc p_opcyclesIso_hom cyclesIso_inv_i_assoc
πE_ιE_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct cycles E πE opcycles ιE CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder H CategoryTheory.ComposableArrows.mk₁ iCycles pOpcycles	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' πE_ιE

---

← Back to Index