HomologicalComplex

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

Statistics

Metric	Count
Definitions ChainComplex, mk, mk', mk'XIso, mkAux, mkHom, mkHomAux, mkXIso, of, ofHom, mk, mk', mkAux, mkHom, mkHomAux, of, ofHom, f, isoApp, isoOfComponents, next, prev, sqFrom, sqTo, X, XIsoOfEq, comp, d, dFrom, dTo, eval, forget, forgetEval, id, instCategory, instHasZeroMorphisms, instInhabitedHom, instInhabitedOfHasZeroObject, instZeroHom, xNext, xNextIso, xNextIsoSelf, xPrev, xPrevIso, xPrevIsoSelf, zero	46
Theorems mk'_X_0, mk'_X_1, mk'_congr_succ'_d, mk'_d, mk'_d_1_0, mkAux_eq_shortComplex_mk_d_comp_d, mkHom_f_0, mkHom_f_1, mkHom_f_succ_succ, mk_X_0, mk_X_1, mk_X_2, mk_congr_succ_X₃, mk_congr_succ_d₂, mk_d, mk_d_1_0, mk_d_2_1, next, next_nat_succ, next_nat_zero, ofHom_f, of_d, of_d_ne, of_x, prev, mk'_X_0, mk'_X_1, mk'_d_1_0, mkHom_f_0, mkHom_f_1, mkHom_f_succ_succ, mk_X_0, mk_X_1, mk_X_2, mk_d_1_0, mk_d_2_0, next, ofHom_f, of_d, of_d_ne, of_x, prev, prev_nat_succ, prev_nat_zero, comm, comm', comm_assoc, comm_from, comm_from_apply, comm_from_assoc, comm_to, comm_to_apply, comm_to_assoc, ext, ext_iff, isIso_of_components, isoApp_hom, isoApp_inv, isoOfComponents_app, isoOfComponents_hom_f, isoOfComponents_inv_f, next_eq, prev_eq, sqFrom_comp, sqFrom_id, sqFrom_left, sqFrom_right, sqTo_left, sqTo_right, XIsoOfEq_hom_comp_XIsoOfEq_hom, XIsoOfEq_hom_comp_XIsoOfEq_hom_assoc, XIsoOfEq_hom_comp_XIsoOfEq_inv, XIsoOfEq_hom_comp_XIsoOfEq_inv_assoc, XIsoOfEq_hom_comp_d, XIsoOfEq_hom_comp_d_assoc, XIsoOfEq_hom_naturality, XIsoOfEq_hom_naturality_assoc, XIsoOfEq_inv_comp_XIsoOfEq_hom, XIsoOfEq_inv_comp_XIsoOfEq_hom_assoc, XIsoOfEq_inv_comp_XIsoOfEq_inv, XIsoOfEq_inv_comp_XIsoOfEq_inv_assoc, XIsoOfEq_inv_comp_d, XIsoOfEq_inv_comp_d_assoc, XIsoOfEq_inv_naturality, XIsoOfEq_inv_naturality_assoc, XIsoOfEq_rfl, comp_f, comp_f_assoc, congr_hom, dFrom_comp_xNextIso, dFrom_comp_xNextIsoSelf, dFrom_comp_xNextIsoSelf_assoc, dFrom_comp_xNextIso_assoc, dFrom_eq, dFrom_eq_zero, dTo_comp_dFrom, dTo_eq, dTo_eq_zero, d_comp_XIsoOfEq_hom, d_comp_XIsoOfEq_hom_assoc, d_comp_XIsoOfEq_inv, d_comp_XIsoOfEq_inv_assoc, d_comp_d, d_comp_d', d_comp_d_assoc, d_comp_eqToHom, epi_of_epi_f, eqToHom_comp_d, eqToHom_f, eval_map, eval_obj, ext, forgetEval_hom_app, forgetEval_inv_app, forget_map, forget_obj, hom_ext, hom_ext_iff, hom_f_injective, id_f, image_eq_image, image_to_eq_image, instFaithfulGradedObjectForget, instHasZeroObject, instPreservesZeroMorphismsEval, isZero_zero, kernel_eq_kernel, kernel_from_eq_kernel, mono_of_mono_f, shape, xPrevIsoSelf_comp_dTo, xPrevIsoSelf_comp_dTo_assoc, xPrevIso_comp_dTo, xPrevIso_comp_dTo_assoc, zero_f	135
Total	181

ChainComplex

Definitions

Name	Category	Theorems
mk 📖	CompOp	—
mk' 📖	CompOp	4 math math: mk'_X_0, mk'_d, mk'_X_1, mk'_d_1_0
mk'XIso 📖	CompOp	1 math math: mk'_d
mkAux 📖	CompOp	1 math math: mkAux_eq_shortComplex_mk_d_comp_d
mkHom 📖	CompOp	3 math math: mkHom_f_0, mkHom_f_1, mkHom_f_succ_succ
mkHomAux 📖	CompOp	—
mkXIso 📖	CompOp	1 math math: mk_d
of 📖	CompOp	5 math math: ofHom_f, of_x, of_d, of_d_ne, map_chain_complex_of
ofHom 📖	CompOp	1 math math: ofHom_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk'_X_0 📖	mathematical	—	HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne mk'	—	AddRightCancelSemigroup.toIsRightCancelAdd
mk'_X_1 📖	mathematical	—	HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne mk'	—	AddRightCancelSemigroup.toIsRightCancelAdd
mk'_congr_succ'_d 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.eqToHom	—	CategoryTheory.Category.id_comp
mk'_d 📖	mathematical	—	HomologicalComplex.d ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne mk' CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Iso.hom mk'XIso	—	AddRightCancelSemigroup.toIsRightCancelAdd mk_d_2_1 mk'_congr_succ'_d mk_d_1_0 mk_d
mk'_d_1_0 📖	mathematical	—	HomologicalComplex.d ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne mk'	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.id_comp
mkAux_eq_shortComplex_mk_d_comp_d 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	mkAux HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne HomologicalComplex.d HomologicalComplex.d_comp_d	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.d_comp_d CategoryTheory.ShortComplex.zero CategoryTheory.Category.id_comp
mkHom_f_0 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne HomologicalComplex.d	HomologicalComplex.Hom.f mkHom	—	AddRightCancelSemigroup.toIsRightCancelAdd
mkHom_f_1 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne HomologicalComplex.d	HomologicalComplex.Hom.f mkHom	—	AddRightCancelSemigroup.toIsRightCancelAdd
mkHom_f_succ_succ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne HomologicalComplex.d	HomologicalComplex.Hom.f mkHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.Hom.comm	—	AddRightCancelSemigroup.toIsRightCancelAdd
mk_X_0 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne	—	AddRightCancelSemigroup.toIsRightCancelAdd
mk_X_1 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne	—	AddRightCancelSemigroup.toIsRightCancelAdd
mk_X_2 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.X ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne	—	AddRightCancelSemigroup.toIsRightCancelAdd
mk_congr_succ_X₃ 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex.f CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
mk_congr_succ_d₂ 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.CategoryStruct.comp CategoryTheory.ShortComplex.f CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.eqToHom	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
mk_d 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.d ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne HomologicalComplex.X CategoryTheory.ShortComplex.X₁ HomologicalComplex.d_comp_d CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f CategoryTheory.Iso.hom mkXIso	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.d_comp_d mkAux_eq_shortComplex_mk_d_comp_d mk_congr_succ_d₂ CategoryTheory.eqToHom_refl CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
mk_d_1_0 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.d ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.id_comp
mk_d_2_1 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.d ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.id_comp
next 📖	mathematical	—	ComplexShape.next ComplexShape.down AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid SubNegMonoid.toSub	—	ComplexShape.next_eq' AddRightCancelSemigroup.toIsRightCancelAdd sub_add_cancel
next_nat_succ 📖	mathematical	—	ComplexShape.next ComplexShape.down AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne	—	ComplexShape.next_eq' AddRightCancelSemigroup.toIsRightCancelAdd
next_nat_zero 📖	mathematical	—	ComplexShape.next ComplexShape.down AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne	—	AddRightCancelSemigroup.toIsRightCancelAdd
ofHom_f 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.Hom.f ComplexShape.down AddRightCancelSemigroup.toIsRightCancelAdd of ofHom	—	AddRightCancelSemigroup.toIsRightCancelAdd
of_d 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.d ComplexShape.down AddRightCancelSemigroup.toIsRightCancelAdd of	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.id_comp
of_d_ne 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.d ComplexShape.down AddRightCancelSemigroup.toIsRightCancelAdd of HomologicalComplex.X	—	AddRightCancelSemigroup.toIsRightCancelAdd
of_x 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.X ComplexShape.down AddRightCancelSemigroup.toIsRightCancelAdd of	—	AddRightCancelSemigroup.toIsRightCancelAdd
prev 📖	mathematical	—	ComplexShape.prev ComplexShape.down AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd	—	ComplexShape.prev_eq' AddRightCancelSemigroup.toIsRightCancelAdd

CochainComplex

Definitions

Name	Category	Theorems
mk 📖	CompOp	—
mk' 📖	CompOp	3 math math: mk'_X_0, mk'_X_1, mk'_d_1_0
mkAux 📖	CompOp	—
mkHom 📖	CompOp	3 math math: mkHom_f_succ_succ, mkHom_f_1, mkHom_f_0
mkHomAux 📖	CompOp	—
of 📖	CompOp	4 math math: of_d, of_d_ne, of_x, ofHom_f
ofHom 📖	CompOp	1 math math: ofHom_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk'_X_0 📖	mathematical	—	HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne mk'	—	AddRightCancelSemigroup.toIsRightCancelAdd
mk'_X_1 📖	mathematical	—	HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne mk'	—	AddRightCancelSemigroup.toIsRightCancelAdd
mk'_d_1_0 📖	mathematical	—	HomologicalComplex.d ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne mk'	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.comp_id
mkHom_f_0 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne HomologicalComplex.d	HomologicalComplex.Hom.f mkHom	—	AddRightCancelSemigroup.toIsRightCancelAdd
mkHom_f_1 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne HomologicalComplex.d	HomologicalComplex.Hom.f mkHom	—	AddRightCancelSemigroup.toIsRightCancelAdd
mkHom_f_succ_succ 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne HomologicalComplex.d	HomologicalComplex.Hom.f mkHom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.Hom.comm	—	AddRightCancelSemigroup.toIsRightCancelAdd
mk_X_0 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne	—	AddRightCancelSemigroup.toIsRightCancelAdd
mk_X_1 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne	—	AddRightCancelSemigroup.toIsRightCancelAdd
mk_X_2 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne	—	AddRightCancelSemigroup.toIsRightCancelAdd
mk_d_1_0 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.d ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.comp_id
mk_d_2_0 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.d ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.comp_id
next 📖	mathematical	—	ComplexShape.next ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd	—	ComplexShape.next_eq' AddRightCancelSemigroup.toIsRightCancelAdd
ofHom_f 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.Hom.f ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd of ofHom	—	AddRightCancelSemigroup.toIsRightCancelAdd
of_d 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.d ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd of	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.comp_id
of_d_ne 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.d ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd of HomologicalComplex.X	—	AddRightCancelSemigroup.toIsRightCancelAdd
of_x 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	HomologicalComplex.X ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd of	—	AddRightCancelSemigroup.toIsRightCancelAdd
prev 📖	mathematical	—	ComplexShape.prev ComplexShape.up AddSemigroup.toAdd AddMonoid.toAddSemigroup SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid SubNegMonoid.toSub	—	ComplexShape.prev_eq' AddRightCancelSemigroup.toIsRightCancelAdd sub_add_cancel
prev_nat_succ 📖	mathematical	—	ComplexShape.prev ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne	—	ComplexShape.prev_eq' AddRightCancelSemigroup.toIsRightCancelAdd
prev_nat_zero 📖	mathematical	—	ComplexShape.prev ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne	—	AddRightCancelSemigroup.toIsRightCancelAdd

HomologicalComplex

Definitions

Name	Category	Theorems
X 📖	CompOp	1141 math math: CategoryTheory.InjectiveResolution.injective, CategoryTheory.InjectiveResolution.Hom.hom'_f, pOpcycles_restrictionOpcyclesIso_hom_assoc, eqToHom_f, CochainComplex.mappingConeCompTriangleh_comm₁_assoc, extendSingleIso_inv_f, restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv, evalCompCoyonedaCorepresentableByDoubleId_homEquiv_apply, AlgebraicTopology.DoldKan.P_f_0_eq, singleMapHomologicalComplex_hom_app_ne, ChainComplex.truncate_map_f, AlgebraicTopology.DoldKan.PInfty_f_add_QInfty_f, CategoryTheory.NatIso.mapHomologicalComplex_inv_app_f, dFrom_comp_xNextIsoSelf, CochainComplex.HomComplex.Cochain.fromSingleMk_neg, ComplexShape.Embedding.isIso_liftExtend_f_iff, CochainComplex.mappingCone.inl_v_descCochain_v_assoc, rightUnitor'_inv, CategoryTheory.Functor.mapHomologicalComplexIdIso_hom_app_f, groupCohomology.toCocycles_comp_isoCocycles₁_hom, mapBifunctor.ι_D₂, mapBifunctor₁₂.ι_D₃_assoc, isZero_single_obj_X, HomologicalComplex₂.totalFlipIso_hom_f_D₁, singleMapHomologicalComplex_hom_app_self, double_d_eq_zero₀, truncGE.rightHomologyMapData_φQ, mapBifunctor₁₂.d_eq, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_d, singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, AlgebraicTopology.DoldKan.σ_comp_PInfty_assoc, XIsoOfEq_hom_comp_XIsoOfEq_hom, dFrom_eq_zero, alternatingConst_iCycles_odd_comp_assoc, CochainComplex.mappingCone.inr_f_d_assoc, pOpcycles_opcyclesToCycles_iCycles_assoc, CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_map_f_f, Hom.comm_from_apply, CochainComplex.HomComplex.Cochain.δ_single, pOpcycles_opcyclesIsoSc'_hom, groupCohomology.π_comp_H0IsoOfIsTrivial_hom_assoc, pOpcycles_singleObjOpcyclesSelfIso_inv, prevD_comp_left, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_X, AlgebraicTopology.DoldKan.HigherFacesVanish.inclusionOfMooreComplexMap, opcyclesIsoSc'_inv_fromOpcycles, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp_assoc, singleObjOpcyclesSelfIso_hom, singleObjCyclesSelfIso_inv_iCycles, groupCohomology.cocyclesIso₀_hom_comp_f, CategoryTheory.InjectiveResolution.ι'_f_zero, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_map_f_f, CochainComplex.mappingCone.liftCochain_v_snd_v_assoc, extend.d_comp_eq_zero_iff, CochainComplex.augmentTruncate_inv_f_zero, groupCohomology.eq_d₀₁_comp_inv, ChainComplex.mkAux_eq_shortComplex_mk_d_comp_d, CochainComplex.mappingCone.inr_f_fst_v, CochainComplex.isStrictlyLE_iff, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.map_f_f, homotopyCofiber.inlX_fstX, mapBifunctor.ι_D₂_assoc, op_d, homotopyCofiber.inrX_fstX_assoc, CochainComplex.HomComplex.Cochain.fromSingleEquiv_fromSingleMk, opSymm_d, groupCohomology.eq_d₁₂_comp_inv, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀', Homotopy.nullHomotopicMap_comp, toCycles_i, shortComplexFunctor'_obj_X₁, CategoryTheory.ProjectiveResolution.lift_commutes_zero_assoc, homotopyCofiber.inrCompHomotopy_hom_desc_hom_assoc, groupHomology.eq_d₃₂_comp_inv, HomologicalComplex₂.shiftFunctor₂XXIso_refl, AlgebraicTopology.DoldKan.HigherFacesVanish.of_P, CochainComplex.mappingCone.liftCochain_v_snd_v, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₂, mapBifunctor.ι_D₁_assoc, leftUnitor'_inv_comm, SimplicialObject.Splitting.PInfty_comp_πSummand_id, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₃, ComplexShape.Embedding.liftExtend.comm_assoc, dTo_eq_zero, HomologicalComplex₂.comm_f, isZero_stupidTrunc_X, ChainComplex.mk'_X_0, CochainComplex.mk'_X_0, mapBifunctor₂₃.ι_D₃, CochainComplex.mappingCone.homologySequenceδ_triangleh, CategoryTheory.Functor.mapHomologicalComplex_obj_d, restriction.sc'Iso_inv_τ₃, mapBifunctor₂₃.d₂_eq, Hom.comm_to_apply, opcyclesIsoSc'_inv_fromOpcycles_assoc, groupHomology.comp_d₂₁_eq, instMonoICycles, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_assoc, CategoryTheory.Functor.mapHomologicalComplex_map_f, groupHomology.toCycles_comp_isoCycles₂_hom_assoc, Homotopy.nullHomotopicMap_f_eq_zero, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_succ, HomologicalComplex₂.totalAux.d₂_eq, CochainComplex.mappingCone.d_snd_v, p_fromOpcycles, HomologicalComplex₂.D₂_totalShift₁XIso_hom_assoc, CochainComplex.HomComplex.Cochain.δ_fromSingleMk, CochainComplex.HomComplex.Cochain.map_v, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_p_f, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂, HomologicalComplex₂.D₂_totalShift₂XIso_hom_assoc, CochainComplex.truncate_obj_X, HomologicalComplex₂.d_f_comp_d_f, add_f_apply, extend_op_d_assoc, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles, ChainComplex.mk_X_2, groupCohomology.comp_d₁₂_eq, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.comp_p_d, HomologicalComplex₂.d₁_eq_zero', CategoryTheory.InjectiveResolution.of_def, Homotopy.extend_hom_eq, homotopyCofiber.inrX_sndX_assoc, CategoryTheory.ProjectiveResolution.cochainComplex_d, CochainComplex.HomComplex.Cochain.toSingleMk_neg, CochainComplex.HomComplex.Cochain.ofHom_v_comp_d, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂_assoc, unopInverse_map, Hom.next_eq, CategoryTheory.NatTrans.mapHomologicalComplex_app_f, CochainComplex.cm5b.fac, groupCohomology.dArrowIso₀₁_inv_right, mapBifunctor₂₃.d₃_eq, natIsoSc'_inv_app_τ₂, CochainComplex.HomComplex.Cochain.toSingleMk_v, groupCohomology.eq_d₂₃_comp_inv_assoc, CategoryTheory.InjectiveResolution.complex_d_comp, restrictionCyclesIso_hom_iCycles, CochainComplex.ConnectData.cochainComplex_X, homotopyCofiber.desc_f', single_obj_d, Rep.standardComplex.d_eq, CategoryTheory.InjectiveResolution.desc_commutes_zero_assoc, XIsoOfEq_hom_comp_d_assoc, truncLE'_d_eq_toCycles, Homotopy.prevD_succ_cochainComplex, d_toCycles_assoc, HomologicalComplex₂.ιTotalOrZero_map_assoc, asFunctor_obj_X, CochainComplex.ι_mapBifunctorShift₂Iso_hom_f_assoc, HomologicalComplex₂.ιTotal_map, xPrevIsoSelf_comp_dTo, CochainComplex.homotopyUnop_hom_eq, CochainComplex.HomComplex.Cochain.toSingleMk_add, HomologicalComplex₂.ι_totalShift₁Iso_hom_f_assoc, ι_mapBifunctorAssociatorX_hom, mapBifunctor₁₂.ι_D₁_assoc, CochainComplex.mappingCone.inr_f_d, instHasMapProdObjGradedObjectFunctorMapBifunctorXπ, HomologicalComplex₂.ι_D₁_assoc, groupHomology.chainsMap_id_f_map_mono, CochainComplex.HomComplex.δ_v, d_comp_d_assoc, CochainComplex.HomComplex.Cochain.comp_v, forgetEval_hom_app, HomologicalComplex₂.ιTotal_totalFlipIso_f_inv_assoc, CochainComplex.fromSingle₀Equiv_apply_coe, instEpiFπTruncGE, CochainComplex.HomComplex.Cochain.comp_zero_cochain_v, CochainComplex.mappingCone.inr_f_descShortComplex_f_assoc, CochainComplex.HomComplex.Cochain.neg_v, shortComplexFunctor'_map_τ₂, CochainComplex.HomComplex.Cochain.sub_v, groupHomology.d₁₀ArrowIso_hom_left, XIsoOfEq_inv_naturality_assoc, CochainComplex.mappingCone.liftCochain_v_descCochain_v, Homotopy.nullHomotopicMap'_f_eq_zero, CochainComplex.mappingCone.lift_f_fst_v, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand_assoc, CochainComplex.mappingCone.inl_v_triangle_mor₃_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_p, HomologicalComplex₂.d₂_eq_zero, AlgebraicTopology.DoldKan.PInfty_f_naturality_assoc, mapBifunctorMapHomotopy.comm₁, HomologicalComplex₂.ι_totalShift₁Iso_inv_f, extendSingleIso_inv_f_assoc, natIsoSc'_inv_app_τ₃, XIsoOfEq_inv_comp_XIsoOfEq_inv, homotopyCofiber_X, HomologicalComplex₂.ι_totalDesc_assoc, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comm_f_assoc, instHasTensorXTensorUnit_1, CochainComplex.mappingCone.inr_triangleδ, CochainComplex.HomComplex.Cochain.ofHoms_comp, groupCohomology.cocyclesIso₀_inv_comp_iCocycles, XIsoOfEq_inv_naturality, XIsoOfEq_rfl, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d, fromOpcycles_d_assoc, restriction_d_eq, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_p_f, dTo_eq, CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_X_d, AlgebraicTopology.DoldKan.comp_P_eq_self_iff, natIsoSc'_hom_app_τ₃, CochainComplex.mappingCone.id_X, CategoryTheory.ProjectiveResolution.instProjectiveXNatOfComplex, CochainComplex.HomComplex.Cochain.single_zero, CochainComplex.mappingCone.inr_descShortComplex_assoc, groupHomology.chainsMap_f_3_comp_chainsIso₃, instEpiFOfHasFiniteColimits, instIsIsoFRestrictionToTruncGE'OfIsStrictlySupported, ChainComplex.single₀ObjXSelf, groupHomology.eq_d₂₁_comp_inv, mapBifunctor₁₂.hom_ext_iff, mapBifunctor₂₃.ι_mapBifunctor₂₃Desc, CochainComplex.mappingConeCompHomotopyEquiv_comm₂_assoc, Hom.sqFrom_comp, CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id, groupCohomology.dArrowIso₀₁_hom_right, shortComplexFunctor_obj_X₂, extendCyclesIso_inv_iCycles_assoc, groupCohomology.toCocycles_comp_isoCocycles₂_hom, mapBifunctor₁₂.ι_mapBifunctor₁₂Desc, mapBifunctor₁₂.ι_D₂_assoc, CochainComplex.HomComplex.Cochain.fromSingleMk_postcomp, mapBifunctor₂₃.ιOrZero_eq_zero, homotopyCofiber.inrX_d_assoc, mapBifunctor.hom_ext_iff, sub_f_apply, CochainComplex.mappingCone.d_snd_v'_assoc, ι_mapBifunctorDesc, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_assoc, Homotopy.map_nullHomotopicMap', AlgebraicTopology.karoubi_alternatingFaceMapComplex_d, d_pOpcycles, HomologicalComplex₂.flipEquivalenceUnitIso_hom_app_f_f, CochainComplex.shiftFunctorZero_inv_app_f, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comp_d_assoc, fromOpcycles_eq_zero, AlgebraicTopology.DoldKan.PInfty_f_comp_QInfty_f_assoc, ChainComplex.toSingle₀Equiv_apply_coe, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self_assoc, extendMap_f, HomologicalComplex₂.ι_totalShift₂Iso_inv_f_assoc, AlgebraicTopology.DoldKan.P_f_idem_assoc, HomologicalComplex₂.d_comm, pOpcycles_restrictionOpcyclesIso_inv, extend.mapX_some, IsStrictlySupported.isZero, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroZero_assoc, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.comp_p_d_assoc, restriction.sc'Iso_inv_τ₁, CochainComplex.HomComplex.Cochain.zero_cochain_comp_v, CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id_assoc, homotopyCofiber.inrCompHomotopy_hom_desc_hom, HomologicalComplex₂.d_f_comp_d_f_assoc, homotopyCofiber.inlX_sndX_assoc, Hom.isoOfComponents_inv_f, CochainComplex.of_d_ne, mapBifunctorAssociatorX_hom_D₂, homologyι_comp_fromOpcycles, groupCohomology.comp_d₂₃_eq, restriction_X, CochainComplex.HomComplex.Cochain.toSingleMk_v_eq_zero, HomologicalComplex₂.ι_D₂, AlgebraicTopology.DoldKan.QInfty_f_0, isZero_double_X, CategoryTheory.InjectiveResolution.ι_f_succ, prevD_eq_toPrev_dTo, CochainComplex.isStrictlyGE_iff, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, Homotopy.nullHomotopicMap'_comp, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_assoc, instMonoFιTruncLE, HomologicalComplex₂.total.mapAux.d₁_mapMap, CochainComplex.mappingCone.lift_f_fst_v_assoc, cyclesIsoSc'_inv_iCycles_assoc, mapBifunctorMapHomotopy.zero₁, Homotopy.dNext_zero_chainComplex, mapBifunctor₂₃.d₃_eq_zero, CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d_assoc, groupHomology.chainsMap_f_single, HomologicalComplex₂.d₁_eq, groupCohomology.π_comp_H0IsoOfIsTrivial_hom, opcyclesToCycles_iCycles_assoc, Homotopy.prevD_chainComplex, groupCohomology.cochainsMap_f_map_epi, groupCohomology.comp_d₀₁_eq, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_map_f_f, single_obj_X_self, CochainComplex.HomComplex.Cochain.zero_v, AlgebraicTopology.DoldKan.map_Hσ, instMonoFTruncLE'ToRestriction, id_f, singleMapHomologicalComplex_inv_app_self, restrictionMap_f'_assoc, CochainComplex.isZero_of_isStrictlyLE, mapBifunctor₁₂.d₂_eq_zero, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_1, HomologicalComplex₂.XXIsoOfEq_hom_ιTotal_assoc, extendSingleIso_hom_f_assoc, restrictionToTruncGE'.comm_assoc, iCycles_d, mapBifunctor₁₂.ιOrZero_eq_zero, prevD_nat, CategoryTheory.InjectiveResolution.extMk_zero, dTo_comp_dFrom, AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_f, CochainComplex.shiftFunctor_obj_X, CochainComplex.mappingConeCompHomotopyEquiv_comm₁, groupCohomology.dArrowIso₀₁_inv_left, CategoryTheory.Functor.mapHomologicalComplex_obj_X, d_comp_eqToHom, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂, CochainComplex.mk'_X_1, restrictionToTruncGE'.comm, CochainComplex.HomComplex.Cochain.fromSingleMk_v, instHasMapProdObjGradedObjectFunctorMapBifunctorXMapBifunctorMapObjπ, CochainComplex.HomComplex.Cochain.fromSingleMk_add, HomologicalComplex₂.totalFlipIsoX_hom_D₂_assoc, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq_zero, XIsoOfEq_hom_comp_d, CategoryTheory.ProjectiveResolution.Hom.hom'_f_assoc, HomologicalComplex₂.XXIsoOfEq_rfl, dgoToHomologicalComplex_obj_X, CochainComplex.mappingCone.ext_from_iff, ChainComplex.augmentTruncate_inv_f_succ, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₁, HomologicalComplex₂.ι_D₂_assoc, CochainComplex.HomComplex.Cocycle.toSingleMk_zero, units_smul_f_apply, CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv, p_opcyclesMap, AlgebraicTopology.DoldKan.PInfty_comp_map_mono_eq_zero, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero'_assoc, homotopyCofiber.inrX_fstX, CochainComplex.HomComplex.Cochain.leftUnshift_v, CategoryTheory.NatIso.mapHomologicalComplex_hom_app_f, CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_X_X, CochainComplex.mappingConeCompHomotopyEquiv_comm₁_assoc, coconeOfHasColimitEval_pt_X, restriction.sc'Iso_hom_τ₂, singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom, mapBifunctor₂₃.ι_D₁, leftUnitor'_inv_comm_assoc, SimplicialObject.Splitting.cofan_inj_comp_PInfty_eq_zero, opcyclesOpIso_hom_toCycles_op, mapBifunctor₂₃.ι_mapBifunctor₂₃Desc_assoc, SimplicialObject.Splitting.ιSummand_comp_d_comp_πSummand_eq_zero, groupHomology.chainsMap_f_map_epi, Homotopy.nullHomotopicMap_f, d_toCycles, mapBifunctorAssociatorX_hom_D₃_assoc, unop_X, opFunctor_map_f, groupCohomology.isoCocycles₂_hom_comp_i, cyclesIsoSc'_inv_iCycles, CochainComplex.mappingCone.inr_f_snd_v, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map_f_f, CochainComplex.mappingConeCompTriangle_mor₃_naturality, groupHomology.comp_d₁₀_eq, d_pOpcycles_assoc, CategoryTheory.ProjectiveResolution.of_def, HomologicalComplex₂.totalAux.d₂_eq', Homotopy.zero, CategoryTheory.ProjectiveResolution.π'_f_zero_assoc, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_p_f, truncLE'Map_f_eq_cyclesMap, CategoryTheory.ProjectiveResolution.π_f_succ, HomologicalComplex₂.totalAux.d₁_eq, groupCohomology.dArrowIso₀₁_hom_left, HomologicalComplex₂.D₁_totalShift₂XIso_hom_assoc, homotopyCofiber.sndX_inrX_assoc, HomologicalComplex₂.shiftFunctor₁XXIso_refl, xPrevIso_comp_dTo, Homotopy.extend.hom_eq_zero₁, ComplexShape.Embedding.epi_liftExtend_f_iff, prevD_eq, mapBifunctor.d₂_eq, groupHomology.toCycles_comp_isoCycles₁_hom_assoc, AlgebraicTopology.DoldKan.P_f_idem, HomologicalComplex₂.ι_totalDesc, CochainComplex.mappingCone.ext_to_iff, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀, HomologicalComplex₂.total.mapAux.d₂_mapMap_assoc, CochainComplex.ConnectData.restrictionLEIso_inv_f, ι_mapBifunctorFlipIso_inv_assoc, extend_single_d, CochainComplex.mappingCone.inr_f_desc_f, mapBifunctor.d₁_eq_zero, groupCohomology.cocyclesIso₀_inv_comp_iCocycles_assoc, Homotopy.map_nullHomotopicMap, HomologicalComplex₂.d₁_eq_zero, zsmul_f_apply, HomologicalComplex₂.flip_X_X, cyclesMap_i_assoc, CategoryTheory.ProjectiveResolution.Hom.hom'_f, CochainComplex.singleFunctor_obj_d, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero', mapBifunctor₂₃.ι_D₂, AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, Hom.isoOfComponents_hom_f, CochainComplex.HomComplex.Cochain.rightUnshift_v, SimplicialObject.Splitting.nondegComplex_X, extend_d_to_eq_zero, CategoryTheory.ProjectiveResolution.Hom.hom_f_zero_comp_π_f_zero_assoc, CochainComplex.mappingCone.inl_v_desc_f_assoc, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₂, nsmul_f_apply, CochainComplex.shiftFunctorAdd'_inv_app_f', groupHomology.d₁₀ArrowIso_inv_right, truncGE'_d_eq, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_d_f, CategoryTheory.Functor.mapBifunctorHomologicalComplex_map_app_f_f, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_0, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_inv_f_f, prevD_eq_zero, AlgebraicTopology.DoldKan.QInfty_f_naturality_assoc, fromOpcycles_op_cyclesOpIso_inv_assoc, CategoryTheory.Functor.mapCochainComplexShiftIso_inv_app_f, CochainComplex.shiftFunctorAdd'_inv_app_f, HomologicalComplex₂.D₁_totalShift₁XIso_hom_assoc, Homotopy.extend.homAux_eq, ChainComplex.mk_X_0, CochainComplex.mappingCone.liftCochain_v_fst_v, CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d, groupHomology.chainsMap_id_f_map_epi, isZero_extend_X, mapBifunctor₁₂.ι_D₁, homotopyCofiber.inlX_desc_f_assoc, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, CochainComplex.HomComplex.Cochain.fromSingleMk_zero, CochainComplex.mappingCone.decomp_from, CochainComplex.mappingCone.inl_v_triangle_mor₃_f_assoc, AlgebraicTopology.DoldKan.map_PInfty_f, unopSymm_X, eval_obj, homotopyCofiber.d_fstX, CochainComplex.ConnectData.X_zero, groupCohomology.cochainsMap_id_f_map_mono, shortComplexFunctor_map_τ₁, CochainComplex.mappingCone.inr_triangleδ_assoc, CochainComplex.cm5b.instIsStrictlyGEBiprodIntMappingConeIdIOfHAddOfNat, CochainComplex.of_x, comp_f, CochainComplex.mappingCone.inl_v_snd_v_assoc, XIsoOfEq_hom_comp_XIsoOfEq_inv_assoc, ι_mapBifunctorAssociatorX_hom_assoc, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp, CategoryTheory.Functor.mapHomotopy_hom, ιOrZero_mapBifunctorAssociatorX_hom, extend.rightHomologyData.d_comp_desc_eq_zero_iff, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_X_d, shortComplexFunctor'_obj_X₂, CochainComplex.HomComplex.Cochain.ofHoms_v_comp_d, CochainComplex.mappingCone.inr_f_triangle_mor₃_f, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id, CategoryTheory.Functor.mapHomologicalComplexIdIso_inv_app_f, homotopyCofiber.inrX_desc_f, Homotopy.compRight_hom, CochainComplex.cm5b.fac_assoc, AlgebraicTopology.DoldKan.Hσ_eq_zero, CochainComplex.ConnectData.d₀_comp, tensor_unit_d₂, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_hom_f_f, groupCohomology.toCocycles_comp_isoCocycles₁_hom_assoc, CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv, CochainComplex.shiftFunctorZero'_hom_app_f, HomologicalComplex₂.flipEquivalenceUnitIso_inv_app_f_f, CategoryTheory.ProjectiveResolution.lift_commutes_zero, groupCohomology.isoCocycles₁_inv_comp_iCocycles, mapBifunctorAssociatorX_hom_D₂_assoc, homologyι_comp_fromOpcycles_assoc, groupHomology.eq_d₂₁_comp_inv_assoc, HomologicalComplex₂.d₂_eq_zero', shortComplexFunctor_map_τ₃, CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero_comp, HomologicalComplex₂.ι_totalShift₁Iso_inv_f_assoc, HomologicalComplex₂.ιTotal_totalFlipIso_f_hom_assoc, d_comp_d', zero_f, groupHomology.cyclesIso₀_inv_comp_iCycles, HomologicalComplex₂.XXIsoOfEq_inv_ιTotal_assoc, CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id, homotopyCofiber.inrCompHomotopy_hom_eq_zero, CochainComplex.mappingCone.d_snd_v_assoc, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_X_d, CochainComplex.shiftFunctor_map_f, isIso_truncLE'ToRestriction, CochainComplex.mappingCone.d_snd_v', extend_op_d, ComplexShape.Embedding.mono_liftExtend_f_iff, AlgebraicTopology.DoldKan.Γ₀_map_app, extend.rightHomologyData_p, Hom.comm_to, shortComplexFunctor'_obj_X₃, AlgebraicTopology.DoldKan.Q_f_0_eq, complexOfFunctorsToFunctorToComplex_map_app_f, CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero, mapBifunctor.d_eq, unopSymm_d, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_X, stupidTruncMap_stupidTruncXIso_hom_assoc, XIsoOfEq_inv_comp_XIsoOfEq_hom_assoc, CochainComplex.ConnectData.X_ofNat, Homotopy.nullHomotopicMap_f_of_not_rel_right, CochainComplex.homotopyOp_hom_eq, CochainComplex.mappingCone.inr_f_descCochain_v_assoc, AlgebraicTopology.DoldKan.QInfty_f_naturality, natIsoSc'_hom_app_τ₂, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_idem, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'_assoc, Homotopy.ofEq_hom, CochainComplex.mappingCone.d_fst_v_assoc, CochainComplex.shiftFunctorAdd_inv_app_f, CochainComplex.truncate_map_f, HomologicalComplex₂.ι_totalShift₂Iso_hom_f_assoc, ChainComplex.augmentTruncate_hom_f_succ, CochainComplex.mappingCone.map_id, groupHomology.chainsMap_id_f_hom_eq_mapRange, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₁, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₂, XIsoOfEq_hom_naturality_assoc, groupHomology.toCycles_comp_isoCycles₂_hom, ComplexShape.Embedding.liftExtend.comm, CategoryTheory.ProjectiveResolution.exact_succ, alternatingConst_iCycles_odd_comp, homotopyCofiber.inlX_sndX, CategoryTheory.ProjectiveResolution.π'_f_zero, Homotopy.ofExtend_hom, leftUnitor'_inv, HomologicalComplex₂.totalFlipIso_hom_f_D₂, dNext_comp_left, AlgebraicTopology.DoldKan.P_f_naturality_assoc, CochainComplex.mappingCone.inl_v_fst_v, forget_obj, AlgebraicTopology.DoldKan.map_P, xPrevIso_comp_dTo_assoc, homotopyCofiber.inlX_d, mapBifunctor₂₃.d₁_eq, CategoryTheory.Idempotents.DoldKan.η_inv_app_f, Homotopy.comp_nullHomotopicMap, groupHomology.chainsMap_f_map_mono, extend.rightHomologyData_g', single_map_f_self_assoc, groupHomology.eq_d₁₀_comp_inv, ι_mapBifunctorMap_assoc, homologicalComplexToDGO_map_f, CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_inv_app_f, ιMapBifunctorOrZero_eq_zero, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self, extend.homologyData'_right_p, extendCyclesIso_hom_iCycles, AlgebraicTopology.DoldKan.degeneracy_comp_PInfty_assoc, IsStrictlySupportedOutside.isZero, groupHomology.eq_d₁₀_comp_inv_assoc, CochainComplex.ConnectData.restrictionLEIso_hom_f, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comp_d, Homotopy.symm_hom, groupHomology.chainsMap_f_1_comp_chainsIso₁_assoc, extend.homologyData'_left_i, truncGE'_d_eq_fromOpcycles, CochainComplex.mappingCone.inr_f_descCochain_v, CochainComplex.ι_mapBifunctorShift₂Iso_hom_f, CochainComplex.cm5b.instQuasiIsoIntP, XIsoOfEq_hom_comp_XIsoOfEq_hom_assoc, HomologicalComplex₂.D₁_totalShift₁XIso_hom, groupCohomology.cocyclesIso₀_hom_comp_f_assoc, groupHomology.lsingle_comp_chainsMap_f, HomologicalComplex₂.D₂_totalShift₁XIso_hom, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_p, ComplexShape.Embedding.homRestrict.comm_assoc, HasHomotopyCofiber.hasBinaryBiproduct, HomologicalComplex₂.comm_f_assoc, d_comp_XIsoOfEq_inv_assoc, mapBifunctor₂₃.ι_eq, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂_assoc, CochainComplex.mappingCone.isZero_X_iff, CochainComplex.mappingCone.quasiIso_descShortComplex, HomologicalComplex₂.totalFlipIso_hom_f_D₁_assoc, Homotopy.comp_nullHomotopicMap', XIsoOfEq_inv_comp_d, CategoryTheory.ProjectiveResolution.complex_d_succ_comp, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_map_f_f, AlgebraicTopology.DoldKan.Γ₀.map_app, Homotopy.dNext_succ_chainComplex, XIsoOfEq_inv_comp_d_assoc, HomologicalComplex₂.XXIsoOfEq_inv_ιTotal, CategoryTheory.InjectiveResolution.Hom.ι_f_zero_comp_hom_f_zero, CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne_comp_assoc, groupHomology.chainsMap_f_3_comp_chainsIso₃_assoc, CochainComplex.mappingConeCompHomotopyEquiv_comm₂, CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom_assoc, groupCohomology.cocyclesMk₁_eq, mapBifunctor₁₂.ι_D₃, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_X, CochainComplex.HomComplex.δ_zero_cochain_v, CochainComplex.HomComplex.Cochain.units_smul_v, CochainComplex.HomComplex.Cochain.δ_toSingleMk, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_map_f_f, smul_f_apply, CochainComplex.cm5b.instMonoFIntI, mapBifunctorMapHomotopy.ιMapBifunctor_hom₂, mapBifunctorAssociatorX_hom_D₁, groupHomology.chainsMap_f_0_comp_chainsIso₀_assoc, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self_assoc, CochainComplex.HomComplex.Cochain.fromSingleMk_precomp, AlgebraicTopology.DoldKan.Q_f_naturality_assoc, mapBifunctor₂₃.ι_D₁_assoc, HomologicalComplex₂.ofGradedObject_X_d, singleObjCyclesSelfIso_inv_iCycles_assoc, Homotopy.compLeftId_hom, CochainComplex.HomComplex.Cocycle.fromSingleMk_zero, zero_f_apply, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃_assoc, CategoryTheory.ProjectiveResolution.extMk_zero, alternatingConst_iCycles_even_comp, d_comp_XIsoOfEq_hom_assoc, CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom, pOpcycles_extendOpcyclesIso_hom_assoc, toCycles_eq_zero, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self, homotopyCofiber.inlX_d'_assoc, CochainComplex.mappingCone.inr_f_fst_v_assoc, CategoryTheory.ProjectiveResolution.instProjectiveXIntCochainComplex, Homotopy.add_hom, CategoryTheory.InjectiveResolution.ι'_f_zero_assoc, HomologicalComplex₂.totalFlipIsoX_hom_D₁, CochainComplex.mappingCone.inl_v_d_assoc, CochainComplex.shiftFunctorZero'_inv_app_f, CochainComplex.mappingCone.inl_v_desc_f, CochainComplex.mappingCone.cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v, SimplicialObject.Splitting.PInfty_comp_πSummand_id_assoc, truncLE'_d_eq, ChainComplex.mk'_d, singleMapHomologicalComplex_inv_app_ne, pOpcycles_extendOpcyclesIso_inv, CochainComplex.isZero_of_isStrictlyGE, groupHomology.eq_d₃₂_comp_inv_assoc, shortComplexFunctor'_map_τ₁, ι_mapBifunctorDesc_assoc, homology_π_ι_assoc, instMonoFOfHasFiniteLimits, HomologicalComplex₂.ofGradedObject_X_X, CochainComplex.mappingCone.map_comp_assoc, Rep.standardComplex.d_comp_ε, groupCohomology.toCocycles_comp_isoCocycles₂_hom_assoc, single_map_f_self, ChainComplex.fromSingle₀Equiv_symm_apply_f_zero, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃_assoc, toCycles_comp_homologyπ, Homotopy.compRightId_hom, CochainComplex.HomComplex.Cochain.smul_v, homotopyCofiber.d_sndX, CochainComplex.ConnectData.X_negOne, CategoryTheory.InjectiveResolution.Hom.hom'_f_assoc, xPrevIsoSelf_comp_dTo_assoc, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₃, mapBifunctor₁₂.d₃_eq_zero, groupHomology.isoCycles₂_inv_comp_iCycles_assoc, CochainComplex.HomComplex.Cochain.fromSingleMk_sub, CochainComplex.toSingle₀Equiv_symm_apply_f_succ, CochainComplex.mappingCone.inl_v_descShortComplex_f_assoc, singleCompEvalIsoSelf_inv_app, toCycles_cyclesIsoSc'_hom_assoc, asFunctor_obj_d, ChainComplex.augmentTruncate_hom_f_zero, shortComplexFunctor_obj_X₁, HomologicalComplex₂.ιTotalOrZero_map, truncGE'Map_f_eq_opcyclesMap, kernel_from_eq_kernel, restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv, CochainComplex.cm5b.instInjectiveXIntI, CochainComplex.cm5b.instMonoIntI, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_eq_zero, groupHomology.cyclesMk₂_eq, groupHomology.chainsMap_f_1_comp_chainsIso₁, CochainComplex.ConnectData.X_negSucc, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_naturality, isZero_extend_X', groupHomology.isoCycles₁_inv_comp_iCycles_assoc, AlgebraicTopology.DoldKan.hσ'_eq, HomologicalComplex₂.d₂_eq, groupHomology.chainsMap_f_2_comp_chainsIso₂, extend_d_from_eq_zero, groupHomology.pOpcycles_comp_opcyclesIso_hom, Homotopy.extend.hom_eq_zero₂, Homotopy.nullHomotopicMap'_f_of_not_rel_left, homotopyCofiber.inlX_d', AlgebraicTopology.DoldKan.PInfty_f_0, Homotopy.nullHomotopicMap_f_of_not_rel_left, groupCohomology.eq_d₂₃_comp_inv, toCycles_comp_homologyπ_assoc, groupCohomology.cochainsMap_f_map_mono, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv, CochainComplex.mappingCone.map_comp, AlgebraicTopology.DoldKan.PInfty_f_naturality, CategoryTheory.InjectiveResolution.cochainComplex_d_assoc, AlgebraicTopology.DoldKan.hσ'_eq_zero, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand, HomologicalComplex₂.shape_f, AlgebraicTopology.DoldKan.PInfty_f_idem_assoc, ComplexShape.Embedding.liftExtend_f, groupCohomology.isoCocycles₂_inv_comp_iCocycles, homotopyCofiber.inlX_fstX_assoc, image_eq_image, CochainComplex.cm5b.i_f_comp, ComplexShape.Embedding.homRestrict.comm, CochainComplex.mappingCone.decomp_to, extend.leftHomologyData_i, inhomogeneousCochains.d_eq, image_to_eq_image, extend.comp_d_eq_zero_iff, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroOne_assoc, restrictionCyclesIso_inv_iCycles_assoc, groupCohomology.cocyclesMk₂_eq, Homotopy.trans_hom, ComplexShape.Embedding.liftExtend.f_eq, CochainComplex.mappingCone.liftCochain_v_fst_v_assoc, groupCohomology.cochainsMap_id_f_map_epi, dgoEquivHomologicalComplexCounitIso_hom_app_f, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_idem_assoc, CochainComplex.mappingCone.lift_desc_f, CochainComplex.ConnectData.restrictionGEIso_inv_f, AlgebraicTopology.DoldKan.map_Q, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀_assoc, HomologicalComplex₂.ι_totalShift₂Iso_inv_f, groupHomology.pOpcycles_comp_opcyclesIso_hom_assoc, AlgebraicTopology.DoldKan.PInfty_f_idem, pOpcycles_opcyclesIsoSc'_hom_assoc, Hom.sqTo_right, eqToHom_comp_d, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_X_X, CochainComplex.HomComplex.Cochain.leftShift_v, CochainComplex.mappingCone.desc_f, groupHomology.cyclesMk₁_eq, CochainComplex.mappingCone.d_fst_v'_assoc, CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero_comp_assoc, AlgebraicTopology.DoldKan.σ_comp_PInfty, CochainComplex.HomComplex.Cochain.toSingleMk_zero, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_X_X, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_hom_f_f, groupCohomology.isoCocycles₁_hom_comp_i, dNext_eq_dFrom_fromNext, CochainComplex.augmentTruncate_inv_f_succ, double_d, CochainComplex.mappingCone.inl_v_d, AlgebraicTopology.NormalizedMooreComplex.obj_X, CochainComplex.shiftFunctor_obj_X', Hom.sqFrom_left, CochainComplex.HomComplex.Cochain.shift_v, CochainComplex.shiftFunctorZero_hom_app_f, CategoryTheory.ProjectiveResolution.Hom.hom_f_zero_comp_π_f_zero, pOpcycles_singleObjOpcyclesSelfIso_inv_assoc, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀, AlgebraicTopology.DoldKan.N₂_obj_X_X, CochainComplex.mappingCone.inr_f_snd_v_assoc, mapBifunctorMapHomotopy.comm₁_aux, ChainComplex.linearYonedaObj_d, Hom.comm_assoc, CochainComplex.mk_X_2, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_d_f, Homotopy.smul_hom, Rep.standardComplex.x_projective, Homotopy.prevD_zero_cochainComplex, CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv_assoc, instIsIsoFTruncLE'ToRestrictionOfIsStrictlySupported, mapBifunctor.ι_D₁, HomologicalComplex₂.total.mapAux.d₂_mapMap, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃, restrictionMap_f', homotopyCofiber.inrX_d, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc, evalCompCoyonedaCorepresentableByDoubleId_homEquiv_symm_apply, HomologicalComplex₂.ιTotal_totalFlipIso_f_hom, CochainComplex.ConnectData.d₀_comp_assoc, ChainComplex.fromSingle₀Equiv_apply, CochainComplex.mappingCone.d_fst_v', CategoryTheory.InjectiveResolution.desc_commutes_zero, singleObjCyclesSelfIso_hom_assoc, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, CochainComplex.shiftFunctorAdd'_hom_app_f', CochainComplex.mappingCone.inl_v_descCochain_v, d_comp_XIsoOfEq_hom, Homotopy.comm, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply, mapBifunctor.d₁_eq', Hom.comm_from, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃_assoc, CochainComplex.augmentTruncate_hom_f_succ, CochainComplex.shiftEval_hom_app, d_comp_d, singleCompEvalIsoSelf_hom_app, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃, HomologicalComplex₂.flip_X_d, op_X, XIsoOfEq_inv_comp_XIsoOfEq_hom, mapBifunctor.d₂_eq_zero, ChainComplex.chainComplex_d_succ_succ_zero, CochainComplex.cm5b.i_f_comp_assoc, CochainComplex.HomComplex_X, d_eqToHom_assoc, coneOfHasLimitEval_pt_X, Homotopy.comp_hom, dNext_eq, CochainComplex.shiftFunctor_obj_d', Hom.sqFrom_right, CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_hom_app_f, groupHomology.isoCycles₁_hom_comp_i_assoc, mapBifunctor₂₃.d_eq, CochainComplex.mappingCone.inr_descShortComplex, CochainComplex.ι_mapBifunctorShift₁Iso_hom_f_assoc, CochainComplex.cm5b.I_d, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroOne, CategoryTheory.ProjectiveResolution.exact₀, CochainComplex.mappingCone.mapHomologicalComplexXIso'_hom, homotopyCofiber.inlX_d_assoc, pOpcycles_extendOpcyclesIso_hom, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_inv_f_f, CochainComplex.HomComplex.Cochain.d_comp_ofHom_v, AlgebraicTopology.DoldKan.karoubi_PInfty_f, mapBifunctorAssociatorX_hom_D₃, homologicalComplexToDGO_obj_obj, homotopyCofiber.desc_f, extendCyclesIso_inv_iCycles, CochainComplex.ConnectData.comp_d₀, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_X_p, ChainComplex.augmentTruncate_inv_f_zero, CochainComplex.shiftFunctorAdd_hom_app_f, restrictionCyclesIso_hom_iCycles_assoc, restriction.sc'Iso_inv_τ₂, ι_mapBifunctorFlipIso_hom, SimplicialObject.Splitting.comp_PInfty_eq_zero_iff, homology_π_ι, ChainComplex.of_x, CategoryTheory.Idempotents.DoldKan.Γ_map_app, CategoryTheory.ProjectiveResolution.projective, evalCompCoyonedaCorepresentableBySingle_homEquiv_apply, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, shortComplexFunctor'_map_τ₃, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_X, CochainComplex.mappingCone.inl_v_descShortComplex_f, homotopyCofiber.sndX_inrX, instHasMapProdObjGradedObjectFunctorMapBifunctorMapBifunctorMapObjπX, HomologicalComplex₂.ι_D₁, HomologicalComplex₂.flipEquivalenceCounitIso_inv_app_f_f, AlgebraicTopology.DoldKan.degeneracy_comp_PInfty, mapBifunctor₁₂.d₁_eq_zero, CochainComplex.HomComplex.Cochain.d_comp_ofHoms_v, CochainComplex.HomComplex.Cochain.toSingleMk_postcomp, CochainComplex.mappingCone.triangleRotateShortComplexSplitting_s, extendCyclesIso_hom_iCycles_assoc, mapBifunctor.d₂_eq_zero', Hom.sqTo_left, CochainComplex.mappingCone.inr_f_descShortComplex_f, asFunctor_map_f, Hom.comm_from_assoc, CochainComplex.toSingle₀Equiv_apply, mapBifunctorMapHomotopy.ιMapBifunctor_hom₁_assoc, CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne_comp, ComplexShape.Embedding.homRestrict_f, groupHomology.isoCycles₁_inv_comp_iCycles, CochainComplex.HomComplex.Cochain.single_v_eq_zero', CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comm_f, extend.d_eq, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₃, shortComplexFunctor_map_τ₂, CochainComplex.shiftFunctorAdd'_hom_app_f, mapBifunctor.d₂_eq', CochainComplex.mappingCone.inr_f_triangle_mor₃_f_assoc, Homotopy.compLeft_hom, isIso_restrictionToTruncGE', CochainComplex.cochainComplex_d_succ_succ_zero, truncLE'Map_f_eq, groupHomology.toCycles_comp_isoCycles₁_hom, prevD_comp_right, Hom.comm', HomologicalComplex₂.ι_totalShift₂Iso_hom_f, dFrom_comp_xNextIso_assoc, toCycles_cyclesIsoSc'_hom, fromOpcycles_op_cyclesOpIso_inv, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq, CategoryTheory.InjectiveResolution.Hom.ι_f_zero_comp_hom_f_zero_assoc, groupHomology.chainsMap_f_2_comp_chainsIso₂_assoc, pOpcycles_opcyclesToCycles_iCycles, extend_d_eq, AlgebraicTopology.DoldKan.QInfty_f_idem_assoc, mapBifunctor.d₁_eq_zero', CochainComplex.shiftFunctorComm_hom_app_f, groupCohomology.iCocycles_mk, ComplexShape.Embedding.homRestrict.f_eq, AlgebraicTopology.DoldKan.QInfty_f_idem, groupHomology.isoCycles₂_hom_comp_i, restrictionToTruncGE'.f_eq_iso_hom_iso_inv, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d_1_0, CochainComplex.mappingCone.inl_v_snd_v, p_fromOpcycles_assoc, CategoryTheory.Abelian.DoldKan.comparisonN_hom_app_f, groupHomology.isoCycles₂_inv_comp_iCycles, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_f, unit_tensor_d₁, HomologicalComplex₂.XXIsoOfEq_hom_ιTotal, ChainComplex.mk'_X_1, groupCohomology.isoCocycles₁_inv_comp_iCocycles_assoc, Hom.isoApp_inv, CochainComplex.mappingConeCompTriangle_mor₃_naturality_assoc, CategoryTheory.InjectiveResolution.exact_succ, ChainComplex.mk_d, HomologicalComplex₂.total.mapAux.d₁_mapMap_assoc, CategoryTheory.ProjectiveResolution.liftFOne_zero_comm, CochainComplex.ConnectData.comp_d₀_assoc, AlgebraicTopology.DoldKan.PInfty_f_comp_QInfty_f, CategoryTheory.InjectiveResolution.instMonoFNatι, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃, HomologicalComplex₂.d₂_eq', CategoryTheory.InjectiveResolution.comp_descHomotopyZeroZero, CochainComplex.HomComplex.Cochain.fromSingleMk_v_eq_zero, isZero_X_of_isStrictlySupported, AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id_assoc, groupHomology.d₁₀ArrowIso_hom_right, Homotopy.dNext_cochainComplex, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₂, Homotopy.nullHomotopicMap'_f, CategoryTheory.Functor.mapCochainComplexShiftIso_hom_app_f, HomologicalComplex₂.totalFlipIsoX_hom_D₂, extend.leftHomologyData.lift_d_comp_eq_zero_iff, CochainComplex.shiftEval_inv_app, mapBifunctor₂₃.ι_D₃_assoc, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_assoc, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles_assoc, pOpcycles_opcyclesToCycles, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_id, Homotopy.nullHomotopicMap'_f_of_not_rel_right, dNext_comp_right, homotopyCofiber.inlX_desc_f, fromOpcycles_d, iCycles_d_assoc, HomologicalComplex₂.d₁_eq', instHasTensorXTensorUnit, groupHomology.inhomogeneousChains.d_eq, cyclesMap_i, AlgebraicTopology.DoldKan.Γ₂_map_f_app, CochainComplex.HomComplex.Cochain.equivHomotopy_symm_apply_hom, AlgebraicTopology.DoldKan.decomposition_Q, extendMap_f_eq_zero, CategoryTheory.InjectiveResolution.exact₀, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_succ_succ, groupHomology.cyclesMk₀_eq, groupHomology.isoCycles₁_hom_comp_i, AlgebraicTopology.DoldKan.σ_comp_P_eq_zero, mapBifunctor₁₂.ι_eq, HomologicalComplex₂.toGradedObjectMap_apply, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₁, CochainComplex.mappingCone.lift_f_snd_v, HomologicalComplex₂.ιTotalOrZero_eq_zero, double_d_eq_zero₁, unop_d, XIsoOfEq_hom_comp_XIsoOfEq_inv, truncGE'.homologyι_truncGE'XIsoOpcycles_inv_d, HomologicalComplex₂.flip_d_f, truncGE'Map_f_eq, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₃, dFrom_eq, AlgebraicTopology.AlternatingFaceMapComplex.obj_X, AlgebraicTopology.DoldKan.Q_f_idem_assoc, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d_1_0_assoc, HomologicalComplex₂.D₁_totalShift₂XIso_hom, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_d_f, CochainComplex.cm5b.degreewiseEpiWithInjectiveKernel_p, CochainComplex.HomComplex.Cochain.rightShift_v, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_X_X, groupCohomology.cocyclesMk₀_eq, CochainComplex.mappingConeCompTriangleh_comm₁, AlgebraicTopology.DoldKan.Q_f_naturality, mapBifunctor₁₂.d₁_eq, groupHomology.lsingle_comp_chainsMap_f_assoc, HomologicalComplex₂.D₂_totalShift₂XIso_hom, d_comp_XIsoOfEq_inv, AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_f_assoc, ChainComplex.truncate_obj_X, CochainComplex.single₀_obj_zero, alternatingConst_X, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_map_f_f, restrictionToTruncGE'_f_eq_iso_hom_iso_inv, instEpiPOpcycles, groupHomology.cyclesIso₀_inv_comp_iCycles_assoc, CochainComplex.cm5b.instInjectiveXIntMappingConeIdI, stupidTruncMap_stupidTruncXIso_hom, groupCohomology.cochainsMap_id_f_hom_eq_compLeft, mapBifunctor₁₂.d₃_eq, AlgebraicTopology.alternatingFaceMapComplex_obj_X, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, Homotopy.extend.hom_eq, mapBifunctor₁₂.ι_D₂, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand', CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv_assoc, homotopyCofiber.d_sndX_assoc, mapBifunctor₁₂.ι_mapBifunctor₁₂Desc_assoc, CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_d_f, dNext_nat, mapBifunctorMapHomotopy.ιMapBifunctor_hom₁, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁, neg_f_apply, CategoryTheory.ProjectiveResolution.instEpiFNatπ, CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero_assoc, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_X, pOpcycles_restrictionOpcyclesIso_inv_assoc, unopFunctor_map_f, Hom.comm, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_assoc, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_d, shape, HomologicalComplex₂.flipEquivalenceCounitIso_hom_app_f_f, AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty_assoc, Homotopy.refl_hom, CochainComplex.HomComplex.Cochain.toSingleEquiv_toSingleMk, pOpcycles_extendOpcyclesIso_inv_assoc, AlgebraicTopology.DoldKan.map_hσ', CochainComplex.HomComplex.Cochain.ofHoms_zero, dFrom_comp_xNextIso, mapBifunctor₁₂.d₂_eq, groupCohomology.eq_d₁₂_comp_inv_assoc, pOpcycles_opcyclesToCycles_assoc, opcyclesOpIso_hom_toCycles_op_assoc, singleObjCyclesSelfIso_hom, restriction_d_eq_assoc, mapBifunctor₂₃.d₁_eq_zero, HomologicalComplex₂.d_comm_assoc, AlgebraicTopology.DoldKan.P_f_naturality, alternatingConst_iCycles_even_comp_assoc, dNext_eq_zero, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃, CochainComplex.mappingCone.lift_f, Rep.barComplex.d_comp_diagonalSuccIsoFree_inv_eq, groupHomology.d₁₀ArrowIso_inv_left, XIsoOfEq_hom_naturality, homotopyCofiber.inrX_sndX, AlgebraicTopology.DoldKan.factors_normalizedMooreComplex_PInfty, HomologicalComplex₂.totalAux.d₁_eq', Hom.comm_to_assoc, opcyclesToCycles_iCycles, ι_mapBifunctorFlipIso_hom_assoc, extendSingleIso_hom_f, restriction.sc'Iso_hom_τ₃, HomologicalComplex₂.total.hom_ext_iff, XIsoOfEq_inv_comp_XIsoOfEq_inv_assoc, CochainComplex.HomComplex.Cochain.add_v, d_eqToHom, CochainComplex.toSingle₀Equiv_symm_apply_f_zero, CochainComplex.mappingConeHomOfDegreewiseSplitIso_hom_f, groupCohomology.isoCocycles₂_hom_comp_i_assoc, CochainComplex.augmentTruncate_hom_f_zero, CochainComplex.mappingCone.inl_v_fst_v_assoc, comp_f_assoc, ChainComplex.single₀_obj_zero, CategoryTheory.ProjectiveResolution.cochainComplex_d_assoc, ChainComplex.of_d_ne, ChainComplex.fromSingle₀Equiv_symm_apply_f_succ, rightUnitor'_inv_comm, AlgebraicTopology.DoldKan.hσ'_naturality, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_naturality_assoc, AlgebraicTopology.DoldKan.P_add_Q_f, opInverse_map, HomologicalComplex₂.flipFunctor_map_f_f, groupCohomology.eq_d₀₁_comp_inv_assoc, dFrom_comp_xNextIsoSelf_assoc, mapBifunctorAssociatorX_hom_D₁_assoc, AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty, CochainComplex.HomComplex.Cochain.toSingleMk_sub, Hom.isoApp_hom, groupCohomology.isoCocycles₁_hom_comp_i_assoc, CategoryTheory.InjectiveResolution.descFOne_zero_comm, CategoryTheory.Abelian.DoldKan.comparisonN_inv_app_f, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₁, singleObjOpcyclesSelfIso_hom_assoc, mapBifunctor.d₁_eq, mapBifunctorMapHomotopy.ιMapBifunctor_hom₂_assoc, HomologicalComplex₂.totalFlipIsoX_hom_D₁_assoc, dgoEquivHomologicalComplexCounitIso_inv_app_f, Homotopy.nullHomotopy'_hom, AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'_assoc, CochainComplex.mappingCone.lift_f_snd_v_assoc, CochainComplex.mappingCone.mapHomologicalComplexXIso'_inv, Rep.FiniteCyclicGroup.resolution.π_f, natIsoSc'_inv_app_τ₁, restriction.sc'Iso_hom_τ₁, kernel_eq_kernel, homotopyCofiber.d_fstX_assoc, opSymm_X, CochainComplex.mappingCone.inr_f_desc_f_assoc, Hom.fAddMonoidHom_apply, CategoryTheory.InjectiveResolution.instInjectiveXIntCochainComplex, toCycles_i_assoc, CochainComplex.shiftFunctor_obj_d, CochainComplex.HomComplex.Cochain.toSingleMk_precomp, ι_mapBifunctorMap, CochainComplex.mappingCone.d_fst_v, CochainComplex.single₀ObjXSelf, CategoryTheory.InjectiveResolution.instInjectiveXNatOfCocomplex, mapBifunctor₂₃.d₂_eq_zero, CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id_assoc, ιOrZero_mapBifunctorAssociatorX_hom_assoc, homotopyCofiber.inrX_desc_f_assoc, natIsoSc'_hom_app_τ₁, extendMap_id_f, p_opcyclesMap_assoc, groupHomology.isoCycles₂_hom_comp_i_assoc, CochainComplex.mk_X_0, groupHomology.comp_d₃₂_eq, CategoryTheory.Idempotents.DoldKan.η_hom_app_f, groupHomology.chainsMap_f_0_comp_chainsIso₀, restrictionCyclesIso_inv_iCycles, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_toGradedObject, HomologicalComplex₂.ιTotal_map_assoc, ι_mapBifunctorFlipIso_inv, CochainComplex.cm5b.I_X, groupCohomology.isoCocycles₂_inv_comp_iCocycles_assoc, HomologicalComplex₂.totalFlipIso_hom_f_D₂_assoc, pOpcycles_restrictionOpcyclesIso_hom, HomologicalComplex₂.ι_totalShift₁Iso_hom_f, instEpiFRestrictionToTruncGE', forgetEval_inv_app, ChainComplex.mk_X_1, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, CochainComplex.mk_X_1, mapBifunctor₂₃.ι_D₂_assoc, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_d_f, CochainComplex.ι_mapBifunctorShift₁Iso_hom_f, shortComplexFunctor_obj_X₃, AlgebraicTopology.DoldKan.Q_f_idem, CochainComplex.HomComplex.Cochain.single_v_eq_zero, Hom.prev_eq, CategoryTheory.InjectiveResolution.cochainComplex_d, CochainComplex.mappingCone.map_δ, HomologicalComplex₂.ιTotal_totalFlipIso_f_inv, ChainComplex.linearYonedaObj_X, CochainComplex.ConnectData.restrictionGEIso_hom_f, Hom.sqFrom_id
XIsoOfEq 📖	CompOp	58 math math: XIsoOfEq_hom_comp_XIsoOfEq_hom, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₂, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₃, XIsoOfEq_hom_comp_d_assoc, CochainComplex.homotopyUnop_hom_eq, XIsoOfEq_inv_naturality_assoc, CochainComplex.XIsoOfEq_shift, natIsoSc'_inv_app_τ₃, XIsoOfEq_inv_comp_XIsoOfEq_inv, XIsoOfEq_inv_naturality, XIsoOfEq_rfl, natIsoSc'_hom_app_τ₃, CochainComplex.shiftFunctorZero_inv_app_f, XIsoOfEq_hom_comp_d, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₁, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₂, CochainComplex.shiftFunctorAdd'_inv_app_f', CochainComplex.shiftFunctorAdd'_inv_app_f, XIsoOfEq_hom_comp_XIsoOfEq_inv_assoc, CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv, CochainComplex.shiftFunctorZero'_hom_app_f, XIsoOfEq_inv_comp_XIsoOfEq_hom_assoc, CochainComplex.homotopyOp_hom_eq, CochainComplex.shiftFunctorAdd_inv_app_f, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₁, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₂, XIsoOfEq_hom_naturality_assoc, XIsoOfEq_hom_comp_XIsoOfEq_hom_assoc, d_comp_XIsoOfEq_inv_assoc, XIsoOfEq_inv_comp_d, XIsoOfEq_inv_comp_d_assoc, CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom_assoc, d_comp_XIsoOfEq_hom_assoc, CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom, CochainComplex.shiftFunctorZero'_inv_app_f, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₃, CochainComplex.shiftFunctorZero_hom_app_f, CochainComplex.shiftFunctorAdd'_hom_app_f', d_comp_XIsoOfEq_hom, CochainComplex.shiftEval_hom_app, XIsoOfEq_inv_comp_XIsoOfEq_hom, CochainComplex.shiftFunctorAdd_hom_app_f, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₃, CochainComplex.shiftFunctorAdd'_hom_app_f, CochainComplex.shiftFunctorComm_hom_app_f, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₂, CochainComplex.shiftEval_inv_app, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₁, XIsoOfEq_hom_comp_XIsoOfEq_inv, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₃, d_comp_XIsoOfEq_inv, CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv_assoc, XIsoOfEq_hom_naturality, XIsoOfEq_inv_comp_XIsoOfEq_inv_assoc, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₁, Rep.FiniteCyclicGroup.resolution.π_f, natIsoSc'_inv_app_τ₁, natIsoSc'_hom_app_τ₁
comp 📖	CompOp	—
d 📖	CompOp	325 math math: ChainComplex.truncate_map_f, double_d_eq_zero₀, mapBifunctor₁₂.d_eq, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_d, CochainComplex.mappingCone.inr_f_d_assoc, AlgebraicTopology.NormalizedMooreComplex.obj_d, pOpcycles_opcyclesToCycles_iCycles_assoc, CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_map_f_f, CochainComplex.HomComplex.Cochain.δ_single, groupCohomology.inhomogeneousCochains.d_def, extend.d_comp_eq_zero_iff, CochainComplex.augmentTruncate_inv_f_zero, groupCohomology.eq_d₀₁_comp_inv, ChainComplex.mkAux_eq_shortComplex_mk_d_comp_d, coneOfHasLimitEval_pt_d, op_d, opSymm_d, groupCohomology.eq_d₁₂_comp_inv, toCycles_i, groupHomology.eq_d₃₂_comp_inv, leftUnitor'_inv_comm, Rep.barComplex.d_def, ComplexShape.Embedding.liftExtend.comm_assoc, HomologicalComplex₂.comm_f, CategoryTheory.ProjectiveResolution.ofComplex_d_1_0, CategoryTheory.Functor.mapHomologicalComplex_obj_d, mapBifunctor₂₃.d₂_eq, groupHomology.comp_d₂₁_eq, CochainComplex.ConnectData.d_ofNat, CategoryTheory.Functor.mapHomologicalComplex_map_f, HomologicalComplex₂.totalAux.d₂_eq, CochainComplex.mappingCone.d_snd_v, p_fromOpcycles, CochainComplex.HomComplex.Cochain.δ_fromSingleMk, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_p_f, HomologicalComplex₂.d_f_comp_d_f, extend_op_d_assoc, groupCohomology.comp_d₁₂_eq, CategoryTheory.InjectiveResolution.of_def, CategoryTheory.ProjectiveResolution.cochainComplex_d, CochainComplex.HomComplex.Cochain.ofHom_v_comp_d, groupCohomology.dArrowIso₀₁_inv_right, mapBifunctor₂₃.d₃_eq, CochainComplex.ConnectData.d_zero_one, groupCohomology.eq_d₂₃_comp_inv_assoc, groupCohomology.eq_d₂₃_comp_inv_apply, CategoryTheory.InjectiveResolution.complex_d_comp, groupCohomology.eq_d₁₂_comp_inv_apply, single_obj_d, Rep.standardComplex.d_eq, AlgebraicTopology.alternatingFaceMapComplex_obj_d, XIsoOfEq_hom_comp_d_assoc, truncLE'_d_eq_toCycles, Homotopy.prevD_succ_cochainComplex, d_toCycles_assoc, CochainComplex.mappingCone.inr_f_d, CochainComplex.HomComplex.δ_v, d_comp_d_assoc, CochainComplex.fromSingle₀Equiv_apply_coe, dgoToHomologicalComplex_obj_d, shortComplexFunctor'_map_τ₂, groupHomology.d₁₀ArrowIso_hom_left, CochainComplex.of_d, mapBifunctorMapHomotopy.comm₁, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d, fromOpcycles_d_assoc, restriction_d_eq, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_p_f, dTo_eq, CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_X_d, groupHomology.eq_d₂₁_comp_inv, groupCohomology.dArrowIso₀₁_hom_right, coconeOfHasColimitEval_pt_d, homotopyCofiber.inrX_d_assoc, CochainComplex.mappingCone.d_snd_v'_assoc, AlgebraicTopology.karoubi_alternatingFaceMapComplex_d, d_pOpcycles, ChainComplex.toSingle₀Equiv_apply_coe, SimplicialObject.Splitting.nondegComplex_d, HomologicalComplex₂.d_comm, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroZero_assoc, groupHomology.inhomogeneousChains.d_def, HomologicalComplex₂.d_f_comp_d_f_assoc, ChainComplex.mk_d_1_0, CochainComplex.of_d_ne, groupCohomology.comp_d₂₃_eq, CochainComplex.ConnectData.d_negSucc, CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d_assoc, HomologicalComplex₂.d₁_eq, Homotopy.prevD_chainComplex, groupCohomology.comp_d₀₁_eq, CochainComplex.mk_d_2_0, restrictionToTruncGE'.comm_assoc, iCycles_d, prevD_nat, groupCohomology.dArrowIso₀₁_inv_left, d_comp_eqToHom, restriction_d, restrictionToTruncGE'.comm, groupHomology.eq_d₃₂_comp_inv_apply, XIsoOfEq_hom_comp_d, ChainComplex.augmentTruncate_inv_f_succ, leftUnitor'_inv_comm_assoc, SimplicialObject.Splitting.ιSummand_comp_d_comp_πSummand_eq_zero, CochainComplex.ConnectData.d_sub_two_sub_one, Homotopy.nullHomotopicMap_f, d_toCycles, groupHomology.comp_d₁₀_eq, d_pOpcycles_assoc, CategoryTheory.ProjectiveResolution.of_def, HomologicalComplex₂.totalAux.d₂_eq', CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_p_f, CategoryTheory.InjectiveResolution.ofCocomplex_d_0_1, HomologicalComplex₂.totalAux.d₁_eq, groupCohomology.dArrowIso₀₁_hom_left, xPrevIso_comp_dTo, prevD_eq, mapBifunctor.d₂_eq, groupCohomology.eq_d₀₁_comp_inv_apply, extend_single_d, CochainComplex.singleFunctor_obj_d, extend_d_to_eq_zero, groupHomology.d₁₀ArrowIso_inv_right, truncGE'_d_eq, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_d_f, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀', CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d, truncGE'.homologyData_right_g', homotopyCofiber.d_fstX, shortComplexFunctor_map_τ₁, extend.rightHomologyData.d_comp_desc_eq_zero_iff, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_X_d, CochainComplex.HomComplex.Cochain.ofHoms_v_comp_d, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_d, CochainComplex.ConnectData.d₀_comp, AlgebraicTopology.AlternatingFaceMapComplex.obj_d_eq, AlgebraicTopology.normalizedMooreComplex_objD, groupHomology.eq_d₂₁_comp_inv_assoc, shortComplexFunctor_map_τ₃, CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero_comp, d_comp_d', shortComplexFunctor_obj_f, CochainComplex.mappingCone.d_snd_v_assoc, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_X_d, CochainComplex.shiftFunctor_map_f, CochainComplex.mappingCone.d_snd_v', extend_op_d, CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero, mapBifunctor.d_eq, unopSymm_d, Homotopy.nullHomotopicMap_f_of_not_rel_right, shortComplexFunctor'_obj_g, CochainComplex.mappingCone.d_fst_v_assoc, CochainComplex.truncate_map_f, ChainComplex.augmentTruncate_hom_f_succ, ComplexShape.Embedding.liftExtend.comm, CategoryTheory.ProjectiveResolution.exact_succ, xPrevIso_comp_dTo_assoc, CochainComplex.ConnectData.cochainComplex_d, homotopyCofiber.inlX_d, mapBifunctor₂₃.d₁_eq, groupHomology.eq_d₁₀_comp_inv, homologicalComplexToDGO_map_f, groupHomology.eq_d₁₀_comp_inv_assoc, truncGE'_d_eq_fromOpcycles, ComplexShape.Embedding.homRestrict.comm_assoc, HomologicalComplex₂.comm_f_assoc, d_comp_XIsoOfEq_inv_assoc, XIsoOfEq_inv_comp_d, CategoryTheory.ProjectiveResolution.complex_d_succ_comp, Homotopy.dNext_succ_chainComplex, XIsoOfEq_inv_comp_d_assoc, CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne_comp_assoc, CochainComplex.HomComplex.δ_zero_cochain_v, CochainComplex.HomComplex.Cochain.δ_toSingleMk, HomologicalComplex₂.ofGradedObject_X_d, d_comp_XIsoOfEq_hom_assoc, CochainComplex.mappingCone.inl_v_d_assoc, truncLE'_d_eq, ChainComplex.mk'_d, groupHomology.eq_d₃₂_comp_inv_assoc, shortComplexFunctor'_map_τ₁, Rep.standardComplex.d_comp_ε, homotopyCofiber.d_sndX, alternatingConst_d, asFunctor_obj_d, ChainComplex.augmentTruncate_hom_f_zero, kernel_from_eq_kernel, HomologicalComplex₂.d₂_eq, extend_d_from_eq_zero, Homotopy.nullHomotopicMap'_f_of_not_rel_left, coconeOfHasColimitEval_ι_app_f, Homotopy.nullHomotopicMap_f_of_not_rel_left, groupCohomology.eq_d₂₃_comp_inv, CategoryTheory.InjectiveResolution.cochainComplex_d_assoc, HomologicalComplex₂.shape_f, image_eq_image, ComplexShape.Embedding.homRestrict.comm, ChainComplex.truncate_obj_d, inhomogeneousCochains.d_eq, image_to_eq_image, extend.comp_d_eq_zero_iff, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroOne_assoc, HomologicalComplex₂.ofGradedObject_d_f, eqToHom_comp_d, CochainComplex.mappingCone.d_fst_v'_assoc, CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero_comp_assoc, CochainComplex.augmentTruncate_inv_f_succ, double_d, CochainComplex.mappingCone.inl_v_d, ChainComplex.linearYonedaObj_d, Hom.comm_assoc, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_d_f, homotopyCofiber.inrX_d, evalCompCoyonedaCorepresentableByDoubleId_homEquiv_symm_apply, CochainComplex.ConnectData.d₀_comp_assoc, CochainComplex.mappingCone.d_fst_v', d_comp_XIsoOfEq_hom, mapBifunctor.d₁_eq', CochainComplex.augmentTruncate_hom_f_succ, d_comp_d, homologicalComplexToDGO_obj_d, HomologicalComplex₂.flip_X_d, ChainComplex.chainComplex_d_succ_succ_zero, d_eqToHom_assoc, dNext_eq, CochainComplex.shiftFunctor_obj_d', AlgebraicTopology.DoldKan.N₂_obj_X_d, coneOfHasLimitEval_π_app_f, mapBifunctor₂₃.d_eq, CochainComplex.cm5b.I_d, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroOne, CategoryTheory.ProjectiveResolution.exact₀, homotopyCofiber.inlX_d_assoc, homotopyCofiber_d, CochainComplex.HomComplex.Cochain.d_comp_ofHom_v, CochainComplex.ConnectData.comp_d₀, ChainComplex.augmentTruncate_inv_f_zero, shortComplexFunctor'_map_τ₃, CochainComplex.HomComplex.Cochain.d_comp_ofHoms_v, asFunctor_map_f, CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne_comp, extend.d_eq, shortComplexFunctor_map_τ₂, mapBifunctor.d₂_eq', shortComplexFunctor_obj_g, CochainComplex.cochainComplex_d_succ_succ_zero, Hom.comm', dFrom_comp_xNextIso_assoc, HomologicalComplex₂.total_d, pOpcycles_opcyclesToCycles_iCycles, extend_d_eq, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d_1_0, p_fromOpcycles_assoc, CategoryTheory.InjectiveResolution.exact_succ, ChainComplex.mk_d, CategoryTheory.ProjectiveResolution.liftFOne_zero_comm, CochainComplex.ConnectData.comp_d₀_assoc, HomologicalComplex₂.d₂_eq', CategoryTheory.InjectiveResolution.comp_descHomotopyZeroZero, groupHomology.d₁₀ArrowIso_hom_right, Homotopy.dNext_cochainComplex, Homotopy.nullHomotopicMap'_f, CochainComplex.mk'_d_1_0, extend.leftHomologyData.lift_d_comp_eq_zero_iff, Homotopy.nullHomotopicMap'_f_of_not_rel_right, ChainComplex.mk'_d_1_0, fromOpcycles_d, iCycles_d_assoc, HomologicalComplex₂.d₁_eq', groupHomology.inhomogeneousChains.d_eq, groupHomology.eq_d₂₁_comp_inv_apply, CategoryTheory.InjectiveResolution.exact₀, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_succ_succ, shortComplexFunctor'_obj_f, double_d_eq_zero₁, unop_d, truncGE'.homologyι_truncGE'XIsoOpcycles_inv_d, HomologicalComplex₂.flip_d_f, dFrom_eq, CategoryTheory.Abelian.LeftResolution.map_chainComplex_d_1_0_assoc, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_d_f, mapBifunctor₁₂.d₁_eq, d_comp_XIsoOfEq_inv, ChainComplex.of_d, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_map_f_f, mapBifunctor₁₂.d₃_eq, homotopyCofiber.d_sndX_assoc, CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_d_f, dNext_nat, CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero_assoc, CochainComplex.HomComplex.Cochain.diff_v, Hom.comm, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_d, shape, CochainComplex.truncate_obj_d, dFrom_comp_xNextIso, mapBifunctor₁₂.d₂_eq, groupCohomology.eq_d₁₂_comp_inv_assoc, restriction_d_eq_assoc, HomologicalComplex₂.d_comm_assoc, Rep.barComplex.d_comp_diagonalSuccIsoFree_inv_eq, groupHomology.d₁₀ArrowIso_inv_left, HomologicalComplex₂.totalAux.d₁_eq', d_eqToHom, CochainComplex.augmentTruncate_hom_f_zero, groupHomology.eq_d₁₀_comp_inv_apply, CategoryTheory.ProjectiveResolution.cochainComplex_d_assoc, ChainComplex.of_d_ne, CochainComplex.mk_d_1_0, rightUnitor'_inv_comm, groupCohomology.eq_d₀₁_comp_inv_assoc, CategoryTheory.InjectiveResolution.descFOne_zero_comm, mapBifunctor.d₁_eq, ChainComplex.mk_d_2_1, kernel_eq_kernel, homotopyCofiber.d_fstX_assoc, toCycles_i_assoc, CochainComplex.shiftFunctor_obj_d, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀, CochainComplex.mappingCone.d_fst_v, groupHomology.comp_d₃₂_eq, CochainComplex.HomComplex_d_hom_apply, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_d_f, CategoryTheory.InjectiveResolution.cochainComplex_d
dFrom 📖	CompOp	22 math math: dFrom_comp_xNextIsoSelf, dFrom_eq_zero, Hom.comm_from_apply, Homotopy.mkInductiveAux₃, Hom.sqFrom_comp, dTo_comp_dFrom, Homotopy.mkCoinductiveAux₂_add_one, Homotopy.mkCoinductiveAux₂_zero, kernel_from_eq_kernel, Homotopy.mkCoinductiveAux₃, dNext_eq_dFrom_fromNext, Hom.sqFrom_left, Hom.comm_from, Hom.sqFrom_right, Hom.comm_from_assoc, dFrom_comp_xNextIso_assoc, dFrom_eq, dFrom_comp_xNextIso, Homotopy.mkInductiveAux₂_zero, dFrom_comp_xNextIsoSelf_assoc, Homotopy.mkInductiveAux₂_add_one, Hom.sqFrom_id
dTo 📖	CompOp	20 math math: Homotopy.mkInductiveAux₃, dTo_eq_zero, Hom.comm_to_apply, xPrevIsoSelf_comp_dTo, dTo_eq, prevD_eq_toPrev_dTo, dTo_comp_dFrom, xPrevIso_comp_dTo, Hom.comm_to, Homotopy.mkCoinductiveAux₂_add_one, xPrevIso_comp_dTo_assoc, Homotopy.mkCoinductiveAux₂_zero, xPrevIsoSelf_comp_dTo_assoc, Homotopy.mkCoinductiveAux₃, image_to_eq_image, Hom.sqTo_right, Hom.sqTo_left, Hom.comm_to_assoc, Homotopy.mkInductiveAux₂_zero, Homotopy.mkInductiveAux₂_add_one
eval 📖	CompOp	30 math math: evalCompCoyonedaCorepresentableByDoubleId_homEquiv_apply, instPreservesFiniteLimitsEvalOfHasFiniteLimits, eval_map, forgetEval_hom_app, instIsCorepresentableCompEvalObjOppositeFunctorTypeCoyonedaOp, isSeparator_coproduct_separatingFamily, instPreservesZeroMorphismsEval, instHasLimitDiscreteWalkingPairCompPairEval, eval_obj, instPreservesColimitsOfShapeEvalOfHasColimitsOfShape, AlgebraicTopology.DoldKan.natTransPInfty_f_app, CochainComplex.mappingCone.triangleRotateShortComplexSplitting_r, singleCompEvalIsoSelf_inv_app, instPreservesLimitsOfShapeEvalOfHasLimitsOfShape, evalCompCoyonedaCorepresentableByDoubleId_homEquiv_symm_apply, CochainComplex.shiftEval_hom_app, singleCompEvalIsoSelf_hom_app, evalCompCoyonedaCorepresentableBySingle_homEquiv_symm_apply, evalCompCoyonedaCorepresentableBySingle_homEquiv_apply, CochainComplex.mappingCone.triangleRotateShortComplexSplitting_s, instPreservesFiniteColimitsEvalOfHasFiniteColimits, instPreservesBinaryBiproductEval, CochainComplex.shiftEval_inv_app, eval_additive, instHasBinaryBiproductObjEval, shortExact_iff_degreewise_shortExact, instHasColimitDiscreteWalkingPairCompPairEval, isZero_single_comp_eval, exact_iff_degreewise_exact, forgetEval_inv_app
forget 📖	CompOp	6 math math: instFaithfulGradedObjectForget, forget_map, forgetEval_hom_app, forget_obj, HomologicalComplex₂.total.forget_map, forgetEval_inv_app
forgetEval 📖	CompOp	2 math math: forgetEval_hom_app, forgetEval_inv_app
id 📖	CompOp	—
instCategory 📖	CompOp	1377 math math: AlgebraicTopology.DoldKan.natTransPInfty_app, HomotopyCategory.spectralObjectMappingCone_δ'_app, DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp, CochainComplex.acyclic_op, CategoryTheory.ShortComplex.ShortExact.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoX₃CochainComplexMapSingleFunctorOfNatX₁, AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex, eqToHom_f, CochainComplex.triangleOfDegreewiseSplit_obj₁, CochainComplex.mappingConeCompTriangleh_comm₁_assoc, extendSingleIso_inv_f, CochainComplex.HomComplex.Cochain.rightShiftAddEquiv_symm_apply, evalCompCoyonedaCorepresentableByDoubleId_homEquiv_apply, singleMapHomologicalComplex_hom_app_ne, homotopyEquivalences_le_quasiIso, ChainComplex.truncate_map_f, CategoryTheory.NatIso.mapHomologicalComplex_inv_app_f, instPreservesLimitsOfShapeSingle, CochainComplex.HomComplex.Cochain.fromSingleMk_neg, CochainComplex.mappingCone.δ_inl, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_neg, rightUnitor'_inv, ComplexShape.Embedding.truncLEFunctor_obj, CategoryTheory.Functor.mapHomologicalComplexIdIso_hom_app_f, HomotopyCategory.quotient_map_out_comp_out, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_add, DerivedCategory.right_fac, isZero_single_obj_X, CochainComplex.HomComplex.Cocycle.fromSingleMk_add, HomologicalComplex₂.totalFlipIso_hom_f_D₁, singleMapHomologicalComplex_hom_app_self, πTruncGE_naturality_assoc, singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, truncGE.rightHomologyMapData_φQ, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_d, singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom_assoc, CochainComplex.HomComplex.Cocycle.leftShiftAddEquiv_symm_apply, opcyclesMap_comp, truncLEMap_comp_assoc, CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_map_f_f, CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app_assoc, instPreservesColimitsOfShapeSingle, CochainComplex.mappingConeCompTriangle_obj₂, pOpcycles_singleObjOpcyclesSelfIso_inv, CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι, quasiIsoAt_iff_comp_right, isZero_single_obj_homology, AlgebraicTopology.DoldKan.N₁_map_f, cyclesFunctor_map, CochainComplex.HomComplex.Cocycle.equivHom_symm_apply, CochainComplex.isStrictlyGE_shift, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_X, CochainComplex.mappingCone.id, AlgebraicTopology.DoldKan.HigherFacesVanish.inclusionOfMooreComplexMap, singleObjOpcyclesSelfIso_hom, singleObjCyclesSelfIso_inv_iCycles, CochainComplex.shiftFunctorZero_eq, instIsStrictlySupportedOfNat, HomologicalComplex₂.totalShift₂Iso_hom_naturality_assoc, CategoryTheory.InjectiveResolution.ι'_f_zero, CategoryTheory.ProjectiveResolution.quasiIso, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_map_f_f, opcyclesMapIso_inv, CochainComplex.augmentTruncate_inv_f_zero, AlgebraicTopology.singularChainComplexFunctor_exactAt_of_totallyDisconnectedSpace, biprod_inr_desc_f, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.map_f_f, CochainComplex.HomComplex.Cochain.leftShift_smul, biprod_lift_fst_f_assoc, homologyι_singleObjOpcyclesSelfIso_inv_assoc, CochainComplex.HomComplex.Cochain.fromSingleEquiv_fromSingleMk, ComplexShape.Embedding.truncGE'Functor_obj, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_inv_app, AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_inv_f, Homotopy.nullHomotopicMap_comp, groupCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor, shortComplexFunctor'_obj_X₁, CochainComplex.mappingCone.triangle_mor₁, CategoryTheory.ProjectiveResolution.lift_commutes_zero_assoc, homotopyCofiber.inrCompHomotopy_hom_desc_hom_assoc, AlgebraicTopology.DoldKan.identity_N₂, HomologicalComplex₂.shiftFunctor₂XXIso_refl, AlgebraicTopology.DoldKan.PInfty_comp_QInfty, CochainComplex.IsKInjective.nonempty_homotopy_zero, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₂, unopFunctor_obj, CategoryTheory.Abelian.LeftResolution.chainComplexMap_zero, groupHomology.chainsMap_id, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₃, CochainComplex.instIsStrictlyLEObjHomologicalComplexIntUpSingle, CategoryTheory.InjectiveResolution.self_ι, HomologicalComplex₂.comm_f, CochainComplex.exactAt_op, DerivedCategory.instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso, CategoryTheory.Abelian.LeftResolution.chainComplexMap_comp, CategoryTheory.Functor.mapHomologicalComplex_linear, CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π_assoc, HomotopyCategory.isZero_quotient_obj_iff, CategoryTheory.Abelian.LeftResolution.chainComplexMap_id, CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_functor, restrictionMap_comp, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_postcomp, CategoryTheory.Functor.mapHomotopyEquiv_inv, AlgebraicTopology.DoldKan.PInfty_idem, AlgebraicTopology.DoldKan.homotopyPInftyToId_hom, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso_inv_app_f_f, CategoryTheory.Functor.mapHomologicalComplex_obj_d, HomologicalComplex₂.total.mapIso_hom, instPreservesFiniteLimitsEvalOfHasFiniteLimits, CategoryTheory.Preadditive.DoldKan.equivalence_unitIso, opcyclesOpIso_inv_naturality_assoc, CochainComplex.instLinearIntFunctorSingleFunctors, AlgebraicTopology.DoldKan.instIsIsoFunctorSimplicialObjectKaroubiNatTrans, inl_biprodXIso_inv_assoc, cyclesMap_comp_assoc, CochainComplex.mapBifunctorShift₂Iso_hom_naturality₂_assoc, instIsStableUnderRetractsQuasiIso, biprod_inr_snd_f_assoc, CategoryTheory.Functor.mapHomologicalComplex_map_f, CochainComplex.IsKProjective.homotopyZero_def, biprod_inl_snd_f_assoc, CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_succ, HomologicalComplex₂.totalAux.d₂_eq, CochainComplex.HomComplex.Cochain.rightUnshift_neg, instIsNormalEpiCategory, HomologicalComplex₂.D₂_totalShift₁XIso_hom_assoc, CochainComplex.HomComplex.Cochain.δ_fromSingleMk, CategoryTheory.Functor.mapHomotopyEquiv_homotopyHomInvId, eval_map, map_isStrictlySupported, AlgebraicTopology.DoldKan.QInfty_idem, stupidTruncMap_comp, to_single_hom_ext_iff, CochainComplex.HomComplex.Cochain.map_v, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_p_f, biprodXIso_hom_fst, HomologicalComplex₂.D₂_totalShift₂XIso_hom_assoc, CochainComplex.truncate_obj_X, HomologicalComplex₂.d_f_comp_d_f, HomologicalComplexUpToQuasiIso.instIsLocalizationHomologicalComplexCompHomotopyCategoryQuotientQhQuasiIso, HomologicalComplex₂.flipEquivalence_unitIso, add_f_apply, extend_op_d_assoc, CategoryTheory.Functor.commShiftIso_map₂CochainComplex_flip_hom_app, CochainComplex.ConnectData.map_comp_map, groupCohomology.cochainsMap_comp, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles, CategoryTheory.Functor.map_homogical_complex_additive, CochainComplex.mappingConeCompTriangle_mor₃, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.comp_p_d, HomologicalComplex₂.d₁_eq_zero', CochainComplex.HomComplex.Cochain.shift_add, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_inv, CategoryTheory.InjectiveResolution.of_def, CochainComplex.HomComplex.Cochain.comp_id, CategoryTheory.Preadditive.DoldKan.equivalence_functor, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_add, CategoryTheory.ProjectiveResolution.self_π, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_sub, singleObjCyclesSelfIso_inv_homologyπ, CochainComplex.HomComplex.Cochain.toSingleMk_neg, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂_assoc, CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁_assoc, unopInverse_map, CategoryTheory.NatTrans.mapHomologicalComplex_app_f, CochainComplex.shiftShortComplexFunctorIso_add'_hom_app, CochainComplex.HomComplex.Cochain.map_zero, CochainComplex.cm5b.fac, natIsoSc'_inv_app_τ₂, DerivedCategory.singleFunctorsPostcompQIso_inv_hom, CochainComplex.instIsCompatibleWithShiftHomologicalComplexIntUpQuasiIso, CochainComplex.HomComplex.Cochain.toSingleMk_v, unopEquivalence_functor, CochainComplex.IsKInjective.rightOrthogonal, single_obj_d, HomotopyCategory.instAdditiveHomologicalComplexQuotientHomotopicFunctor, HomotopyCategory.quotient_inverts_homotopyEquivalences, CochainComplex.IsKInjective.Qh_map_bijective, CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv_apply, AlgebraicTopology.alternatingFaceMapComplex_obj_d, CochainComplex.HomComplex.Cochain.shift_neg, CategoryTheory.InjectiveResolution.desc_commutes_zero_assoc, instFaithfulGradedObjectForget, biprod_lift_fst_f, DerivedCategory.subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE, ιTruncLE_naturality, CochainComplex.instIsIsoIntπTruncGEOfIsStrictlyGE, HomologicalComplex₂.toGradedObjectFunctor_obj, forget_map, CategoryTheory.NatTrans.mapHomologicalComplex_id, HomologicalComplex₂.ιTotalOrZero_map_assoc, asFunctor_obj_X, CochainComplex.ι_mapBifunctorShift₂Iso_hom_f_assoc, HomologicalComplex₂.ιTotal_map, CochainComplex.homotopyUnop_hom_eq, CochainComplex.HomComplex.Cochain.toSingleMk_add, CategoryTheory.NatTrans.mapHomotopyCategory_app, HomologicalComplex₂.ι_totalShift₁Iso_hom_f_assoc, CategoryTheory.Functor.mapProjectiveResolution_π, cyclesMap_id, complexOfFunctorsToFunctorToComplex_obj, opcyclesOpIso_inv_naturality, CategoryTheory.instIsIsoToRightDerivedZero', HomologicalComplex₂.ι_D₁_assoc, opEquivalence_unitIso, Rep.FiniteCyclicGroup.chainComplexFunctor_obj, CochainComplex.instIsStrictlyGEObjHomologicalComplexIntUpSingle, forgetEval_hom_app, homologyι_singleObjOpcyclesSelfIso_inv, HomologicalComplex₂.ιTotal_totalFlipIso_f_inv_assoc, CochainComplex.fromSingle₀Equiv_apply_coe, dgoToHomologicalComplex_obj_d, HomotopyCategory.quotient_map_eq_zero_iff, CochainComplex.mappingCone.inr_f_descShortComplex_f_assoc, CochainComplex.HomComplex.Cocycle.equivHomShift'_symm_apply, shortComplexFunctor'_map_τ₂, isZero_zero, CategoryTheory.Abelian.LeftResolution.exactAt_map_chainComplex_succ, CochainComplex.mappingCone.inl_v_triangle_mor₃_f, HomotopyCategory.instFullHomologicalComplexQuotient, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_p, HomologicalComplex₂.d₂_eq_zero, CochainComplex.XIsoOfEq_shift, HomologicalComplex₂.ι_totalShift₁Iso_inv_f, extendSingleIso_inv_f_assoc, AlgebraicTopology.DoldKan.instIsIsoFunctorKaroubiSimplicialObjectNatTrans, natIsoSc'_inv_app_τ₃, CochainComplex.ιTruncLE_naturality_assoc, HomologicalComplex₂.ι_totalDesc_assoc, truncGEMap_comp_assoc, HomotopyCategory.isoOfHomotopyEquiv_hom, CochainComplex.HomComplex.Cochain.rightUnshift_comp, CochainComplex.HomComplex.Cochain.rightUnshift_units_smul, AlgebraicTopology.DoldKan.N₁_obj_p, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comm_f_assoc, dgoEquivHomologicalComplex_unitIso, CochainComplex.mappingCone.inr_triangleδ, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_map_f, CategoryTheory.Preadditive.DoldKan.equivalence_counitIso, CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_eq, mapBifunctorFlipIso_hom_naturality_assoc, homotopyCofiber.inrCompHomotopy_hom, CategoryTheory.Equivalence.mapHomologicalComplex_unitIso, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_sub, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_p_f, opFunctor_obj, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_X_d, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_sub, natIsoSc'_hom_app_τ₃, instQuasiIsoAtMapOppositeSymmUnopFunctorOp, CochainComplex.πTruncGE_naturality, truncGE'Map_comp, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, CategoryTheory.InjectiveResolution.toRightDerivedZero_eq, CochainComplex.mappingCone.inr_descShortComplex_assoc, CategoryTheory.Idempotents.instIsIdempotentCompleteHomologicalComplex, ChainComplex.single₀ObjXSelf, instEpiGShortComplexTruncLE, ComplexShape.Embedding.restrictionFunctor_map, cyclesOpIso_inv_naturality_assoc, AlgebraicTopology.DoldKan.QInfty_idem_assoc, singleObjHomologySelfIso_hom_singleObjOpcyclesSelfIso_hom, CochainComplex.mappingConeCompHomotopyEquiv_comm₂_assoc, Hom.sqFrom_comp, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_sub, CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id, HomologicalComplexUpToQuasiIso.Q_inverts_homotopyEquivalences, shortComplexFunctor_obj_X₂, singleObjCyclesSelfIso_hom_naturality, cylinder.πCompι₀Homotopy.nullHomotopicMap_eq, CochainComplex.HomComplex.Cochain.fromSingleMk_postcomp, singleObjCyclesSelfIso_inv_naturality_assoc, sub_f_apply, instIsLocalizationHomologicalComplexIntUpHomotopyCategoryQuotientHomotopyEquivalences, HomotopyCategory.eq_of_homotopy, homotopyCofiber.descSigma_ext_iff, instRespectsIsoQuasiIso, Homotopy.map_nullHomotopicMap', CochainComplex.HomComplex.Cochain.shift_zero, CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_unitIso, HomologicalComplex₂.flipEquivalenceUnitIso_hom_app_f_f, CochainComplex.shiftFunctorZero_inv_app_f, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comp_d_assoc, ChainComplex.toSingle₀Equiv_apply_coe, opcyclesMap_id, CategoryTheory.Functor.mapProjectiveResolution_complex, CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_inverse, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_zero, HomologicalComplex₂.ι_totalShift₂Iso_inv_f_assoc, AlgebraicTopology.alternatingFaceMapComplex_map_f, CochainComplex.HomComplex.Cochain.leftShift_comp, HomologicalComplex₂.d_comm, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_symm_apply, CochainComplex.triangleOfDegreewiseSplit_obj₂, Rep.standardComplex.εToSingle₀_comp_eq, AlgebraicTopology.DoldKan.Γ₀'_obj, inr_biprodXIso_inv, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.comp_p_d_assoc, CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id_assoc, ChainComplex.exactAt_succ_single_obj, stupidTruncMap_id, homotopyCofiber.inrCompHomotopy_hom_desc_hom, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE, HomologicalComplex₂.d_f_comp_d_f_assoc, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso_inv, instHasFilteredColimitsOfSize, Hom.isoOfComponents_inv_f, CochainComplex.homologyFunctor_shift, CategoryTheory.Idempotents.DoldKan.hε, cyclesOpNatIso_inv_app, opcyclesFunctor_map, ChainComplex.truncateAugment_inv_f, CochainComplex.HomComplex.Cochain.toSingleMk_v_eq_zero, gradedHomologyFunctor_map, quasiIso_iff_evaluation, quasiIsoAt_comp, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyHomInvId, HomologicalComplex₂.ι_D₂, homologyMap_neg, isZero_stupidTrunc_iff, CategoryTheory.InjectiveResolution.Hom.ι_comp_hom_assoc, CategoryTheory.InjectiveResolution.ι_f_succ, CochainComplex.isKInjective_shift_iff, from_single_hom_ext_iff, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, Homotopy.nullHomotopicMap'_comp, natTransHomologyπ_app, CategoryTheory.Idempotents.DoldKan.N₂_map_isoΓ₀_hom_app_f, CochainComplex.HomComplex.Cochain.leftShift_rightShift_eq_negOnePow_rightShift_leftShift, HomologicalComplex₂.total.mapAux.d₁_mapMap, singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv_assoc, dgoEquivHomologicalComplexUnitIso_hom_app_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_hom_app_f_f, CategoryTheory.NatTrans.mapHomologicalComplex_comp, CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d_assoc, DerivedCategory.to_singleFunctor_obj_eq_zero_of_injective, opcyclesMapIso_hom, CategoryTheory.InjectiveResolution.instIsIsoToRightDerivedZero'Self, HomologicalComplex₂.d₁_eq, DerivedCategory.right_fac_of_isStrictlyLE_of_isStrictlyGE, CategoryTheory.ProjectiveResolution.Hom.hom_comp_π_assoc, CochainComplex.HomComplex.Cochain.leftShift_rightShift, cyclesMap_comp, CochainComplex.HomComplex.Cochain.ofHom_neg, CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective, CochainComplex.HomComplex.Cocycle.toSingleMk_add, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_map_f_f, homologyπ_singleObjHomologySelfIso_hom_assoc, HomologicalComplex₂.instHasTotalIntObjUpShiftFunctor₂, instQuasiIsoMapOppositeSymmUnopFunctorOp, single_obj_X_self, biprod_inr_snd_f, id_f, DerivedCategory.instLinearCochainComplexIntQ, singleMapHomologicalComplex_inv_app_self, dgoEquivHomologicalComplex_functor, AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans, ComplexShape.Embedding.instFaithfulHomologicalComplexExtendFunctor, HomologicalComplex₂.XXIsoOfEq_hom_ιTotal_assoc, extendSingleIso_hom_f_assoc, homologyMapIso_hom, AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_hom_f, instHasHomologyObjSingle, AlgebraicTopology.DoldKan.Γ₀_obj_map, groupCohomology.cochainsMap_zero, CochainComplex.instAdditiveIntFunctorSingleFunctors, CochainComplex.shiftFunctor_obj_X, CochainComplex.mappingConeCompHomotopyEquiv_comm₁, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app_f_f, instIsCorepresentableCompEvalObjOppositeFunctorTypeCoyonedaOp, CochainComplex.exactAt_succ_single_obj, CategoryTheory.Functor.mapHomologicalComplex_obj_X, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂, CochainComplex.HomComplex.Cocycle.toSingleMk_mem_coboundaries_iff, groupHomology.map_chainsFunctor_shortExact, AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty_assoc, ιTruncLE_naturality_assoc, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂, instMonoFShortComplexTruncLE, CochainComplex.HomComplex.Cochain.map_add, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc, CategoryTheory.ProjectiveResolution.extMk_hom, CochainComplex.mappingCone.triangleRotateShortComplex_X₂, CochainComplex.HomComplex.Cochain.fromSingleMk_v, CategoryTheory.Idempotents.DoldKan.equivalence_counitIso, CategoryTheory.Functor.mapHomologicalComplex_upToQuasiIso_Q_inverts_quasiIso, CochainComplex.HomComplex.Cochain.fromSingleMk_add, CochainComplex.single₀_map_f_zero, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_neg, AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_hom_app, CochainComplex.HomComplex.Cochain.shift_smul, CategoryTheory.Functor.mapHomologicalComplex_reflects_iso, CategoryTheory.Abelian.LeftResolution.chainComplexMap_comp_assoc, CochainComplex.HomComplex.Cochain.leftShiftAddEquiv_apply, HomologicalComplex₂.instHasTotalIntObjUpCompShiftFunctor₁ShiftFunctor₂, opcyclesOpIso_hom_naturality_assoc, HomologicalComplex₂.XXIsoOfEq_rfl, CochainComplex.IsKInjective.homotopyZero_def, dgoToHomologicalComplex_obj_X, ChainComplex.augmentTruncate_inv_f_succ, HomotopyCategory.instEssSurjHomologicalComplexQuotient, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₁, HomotopyCategory.quasiIso_eq_quasiIso_map_quotient, extendMap_comp_assoc, groupCohomology.cochainsMap_id_comp, restrictionMap_id, DerivedCategory.instIsIsoMapCochainComplexIntQ, HomologicalComplex₂.ι_D₂_assoc, ComplexShape.Embedding.AreComplementary.hom_ext, isIso_homologyMap_shortComplexTruncLE_g, HomotopyCategory.quot_mk_eq_quotient_map, CochainComplex.HomComplex.Cocycle.toSingleMk_zero, CochainComplex.HomComplex.Cochain.rightShiftAddEquiv_apply, units_smul_f_apply, CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv, quasiIsoAt_unopFunctor_map_iff, CochainComplex.isIso_πTruncGE_iff, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero'_assoc, CochainComplex.HomComplex.Cochain.leftUnshift_v, CategoryTheory.NatIso.mapHomologicalComplex_hom_app_f, CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_X_X, CochainComplex.mappingConeCompHomotopyEquiv_comm₁_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, ChainComplex.quasiIsoAt₀_iff, singleObjCyclesSelfIso_hom_singleObjOpcyclesSelfIso_hom, groupCohomology.cochainsMap_comp_assoc, CochainComplex.mappingCone.triangleRotateShortComplex_X₃, HomologicalComplex₂.totalFunctor_obj, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse_map, CochainComplex.HomComplex.Cochain.rightShift_leftShift, mono_of_mono_f, groupHomology.isoShortComplexH1_hom, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_zero, isSeparator_coproduct_separatingFamily, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom, CochainComplex.HomComplex.Cochain.ofHom_sub, CochainComplex.instLinearHomologicalComplexIntUpShiftFunctor, CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π, opFunctor_map_f, instIsMultiplicativeQuasiIso, instIsIsoπTruncGEOfIsStrictlySupported, CategoryTheory.ProjectiveResolution.instIsIsoFromLeftDerivedZero'Self, HomologicalComplex₂.flipFunctor_obj, CochainComplex.HomComplex.Cochain.leftUnshift_smul, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map_f_f, CochainComplex.instIsKInjectiveObjIntShiftFunctor, CochainComplex.mappingConeCompTriangle_mor₃_naturality, CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors, CochainComplex.HomComplex.Cochain.shiftLinearMap_apply, CategoryTheory.ProjectiveResolution.of_def, HomologicalComplex₂.totalAux.d₂_eq', CategoryTheory.ProjectiveResolution.π'_f_zero_assoc, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_p_f, CategoryTheory.ProjectiveResolution.π_f_succ, HomologicalComplex₂.totalAux.d₁_eq, ComplexShape.Embedding.homRestrict_precomp, instPreservesZeroMorphismsEval, HomologicalComplex₂.D₁_totalShift₂XIso_hom_assoc, CochainComplex.HomComplex.Cocycle.toSingleMk_coe, HomologicalComplex₂.shiftFunctor₁XXIso_refl, AlgebraicTopology.inclusionOfMooreComplex_app, homologyMap_id, AlgebraicTopology.DoldKan.Γ₂_obj_X_map, CochainComplex.mappingCone.triangleRotateShortComplex_X₁, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_inv_f_f, instHasLimitDiscreteWalkingPairCompPairEval, instQuasiIsoAtOppositeMapSymmOpFunctorOp, DerivedCategory.left_fac_of_isStrictlyLE_of_isStrictlyGE, CochainComplex.shiftFunctor_map_f', HomologicalComplex₂.ι_totalDesc, ComplexShape.Embedding.extendFunctor_map, AlgebraicTopology.DoldKan.PInfty_idem_assoc, HomologicalComplexUpToQuasiIso.Q_map_eq_of_homotopy, HomologicalComplex₂.total.mapAux.d₂_mapMap_assoc, CochainComplex.ConnectData.restrictionLEIso_inv_f, ι_mapBifunctorFlipIso_inv_assoc, extend_single_d, ComplexShape.Embedding.stupidTruncFunctor_map, singleObjHomologySelfIso_inv_homologyι_assoc, CategoryTheory.ProjectiveResolution.Hom.hom'_comp_π', CochainComplex.HomComplex.Cochain.rightShift_zero, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor_obj, Homotopy.map_nullHomotopicMap, HomologicalComplex₂.d₁_eq_zero, groupHomology.chainsFunctor_obj, zsmul_f_apply, HomologicalComplex₂.flip_X_X, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, CategoryTheory.Idempotents.DoldKan.equivalence_inverse, HomotopyCategory.instFullFunctorHomologicalComplexObjWhiskeringLeftQuotient, CochainComplex.singleFunctor_obj_d, biprod_lift_snd_f, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero', AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, homologyMap_add, Hom.isoOfComponents_hom_f, CochainComplex.quasiIso_shift_iff, cylinder.ι₁_π, CochainComplex.HomComplex.Cochain.rightUnshift_v, HomotopyCategory.composableArrowsFunctor_obj, singleObjCyclesSelfIso_inv_homologyπ_assoc, AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty, biprod_inl_fst_f_assoc, CategoryTheory.ProjectiveResolution.Hom.hom_f_zero_comp_π_f_zero_assoc, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₂, CategoryTheory.Functor.map₂HomologicalComplex_map_app, unopEquivalence_unitIso, nsmul_f_apply, g_shortComplexTruncLEX₃ToTruncGE, CochainComplex.shiftFunctorAdd'_inv_app_f', homotopyCofiber.inr_desc, Rep.FiniteCyclicGroup.chainComplexFunctor_map_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_d_f, CategoryTheory.Functor.mapBifunctorHomologicalComplex_map_app_f_f, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_hom_app, instHasLimitsOfShape, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_inv_f_f, opEquivalence_counitIso, HomotopyCategory.quotient_obj_surjective, inl_biprodXIso_inv, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_zero, AlgebraicTopology.DoldKan.compatibility_N₂_N₁_karoubi, CochainComplex.mappingCone.map_inr, CategoryTheory.Functor.mapCochainComplexShiftIso_inv_app_f, homotopyCofiber.inr_desc_assoc, CochainComplex.shiftFunctorAdd'_eq, mapBifunctorFlipIso_hom_naturality, mono_homologyMap_shortComplexTruncLE_g, CochainComplex.shiftFunctorAdd'_inv_app_f, HomologicalComplex₂.D₁_totalShift₁XIso_hom_assoc, truncLEMap_comp, CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d, cylinder.inrX_π_assoc, CochainComplex.truncateAugment_inv_f, CochainComplex.mapBifunctorShift₂Iso_hom_naturality₂, homologyOp_hom_naturality_assoc, homologyMap_comp, homotopyCofiber.inlX_desc_f_assoc, biprod_inl_fst_f, CochainComplex.HomComplex.Cochain.fromSingleMk_zero, CochainComplex.mappingCone.inl_v_triangle_mor₃_f_assoc, instAdditiveHomologyFunctor, AlgebraicTopology.DoldKan.P_succ, eval_obj, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, ab5OfSize, shortComplexFunctor_map_τ₁, HomologicalComplex₂.instHasTotalIntObjUpCompShiftFunctor₂ShiftFunctor₁, CochainComplex.mappingConeCompTriangle_mor₁, CochainComplex.mappingCone.inr_triangleδ_assoc, CochainComplex.cm5b.instIsStrictlyGEBiprodIntMappingConeIdIOfHAddOfNat, groupHomology.chainsMap_id_comp, CochainComplex.HomComplex.Cochain.leftShift_zero, comp_f, cylinder.ι₀_π, CategoryTheory.Functor.mapHomotopy_hom, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_zero, CategoryTheory.ProjectiveResolution.Hom.hom'_comp_π'_assoc, singleObjOpcyclesSelfIso_inv_naturality, CochainComplex.instLinearIntShiftFunctor, isIso_ιTruncLE_iff, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_X_d, cyclesOpIso_inv_naturality, AlgebraicTopology.DoldKan.N₂Γ₂_compatible_with_N₁Γ₀, SimplicialObject.Split.nondegComplexFunctor_map_f, CochainComplex.triangleOfDegreewiseSplit_mor₂, AlgebraicTopology.DoldKan.Γ₀'_map_F, quasiIso_iff_comp_left, biprod_inr_fst_f, shortComplexFunctor'_obj_X₂, opcyclesOpIso_hom_naturality, dgoEquivHomologicalComplex_counitIso, homotopyCofiber.eq_desc, truncLE'Map_id, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_d, CochainComplex.mappingCone.inr_f_triangle_mor₃_f, CochainComplex.HomComplex.Cocycle.fromSingleMk_coe, CategoryTheory.Functor.mapHomologicalComplexIdIso_inv_app_f, DerivedCategory.isLE_Q_obj_iff, Homotopy.compRight_hom, CochainComplex.cm5b.fac_assoc, ComplexShape.Embedding.homRestrict_comp_extendMap_assoc, AlgebraicTopology.normalizedMooreComplex_objD, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_hom_f_f, CochainComplex.IsKProjective.nonempty_homotopy_zero, instHasHomologyOppositeObjSymmOpFunctorOp, biprodXIso_hom_fst_assoc, CochainComplex.triangleOfDegreewiseSplit_obj₃, CochainComplex.shiftFunctorZero'_hom_app_f, CategoryTheory.InjectiveResolution.self_cocomplex, HomologicalComplex₂.flipEquivalenceUnitIso_inv_app_f_f, CategoryTheory.ProjectiveResolution.lift_commutes_zero, AlgebraicTopology.DoldKan.QInfty_comp_PInfty, AlgebraicTopology.DoldKan.Q_idem, opcyclesMap_comp_assoc, quasiIsoAt_shortComplexTruncLE_g, HomotopyCategory.instFaithfulFunctorHomologicalComplexObjWhiskeringLeftQuotient, AlgebraicTopology.DoldKan.whiskerLeft_toKaroubi_N₂Γ₂_hom, HomologicalComplex₂.d₂_eq_zero', CategoryTheory.ProjectiveResolution.leftDerived_app_eq, CochainComplex.mappingCone.triangle_mor₂, shortComplexFunctor_map_τ₃, HomologicalComplex₂.ι_totalShift₁Iso_inv_f_assoc, HomologicalComplex₂.ιTotal_totalFlipIso_f_hom_assoc, CochainComplex.HomComplex.Cocycle.leftUnshift_coe, shortComplexFunctor_obj_f, zero_f, AlgebraicTopology.normalizedMooreComplex_map, CategoryTheory.ProjectiveResolution.lift_commutes, HomologicalComplex₂.XXIsoOfEq_inv_ιTotal_assoc, CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id, cylinder.ι₀_π_assoc, homotopyCofiber.inrCompHomotopy_hom_eq_zero, AlgebraicTopology.DoldKan.Q_idem_assoc, CochainComplex.instAdditiveIntShiftFunctor, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_X_d, homologyFunctor_map, cylinder.ι₁_π_assoc, CategoryTheory.HasExt.hasSmallLocalizedShiftedHom_of_isLE_of_isGE, CochainComplex.shiftFunctor_map_f, CochainComplex.quasiIsoAt_shift_iff, HomologicalComplex₂.total.mapIso_inv, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_apply, shortComplexTruncLE_f, CochainComplex.instIsKProjectiveObjIntShiftFunctor, extend_op_d, AlgebraicTopology.DoldKan.Γ₀_map_app, CategoryTheory.HasExt.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoOfIsGEOfIsLEOfNat, CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π_assoc, shortComplexFunctor'_obj_X₃, CategoryTheory.Idempotents.DoldKan.N_obj, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_hom_app, CochainComplex.HomComplex.Cochain.rightShift_smul, complexOfFunctorsToFunctorToComplex_map_app_f, CochainComplex.HomComplex.Cochain.map_comp, CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero, cylinder.ι₀_desc, opInverse_obj, CategoryTheory.ProjectiveResolution.Hom.hom_comp_π, isGrothendieckAbelian, mkHomToSingle_f, biprodXIso_hom_snd, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_X, CochainComplex.homotopyOp_hom_eq, CochainComplex.HomComplex.Cochain.map_sub, ComplexShape.Embedding.ιTruncLENatTrans_app, shortComplexFunctor'_obj_g, natIsoSc'_hom_app_τ₂, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_idem, CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoLocalizerMorphism_functor, CochainComplex.IsKProjective.Qh_map_bijective, CategoryTheory.Equivalence.mapHomologicalComplex_functor, CochainComplex.homOfDegreewiseSplit_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_counitIso_hom, cyclesOpIso_hom_naturality_assoc, HomologicalComplex₂.flipEquivalence_counitIso, CochainComplex.shiftFunctorAdd_inv_app_f, DerivedCategory.isGE_Q_obj_iff, CochainComplex.truncate_map_f, HomologicalComplex₂.ι_totalShift₂Iso_hom_f_assoc, CategoryTheory.NatTrans.mapHomologicalComplex_naturality, ChainComplex.augmentTruncate_hom_f_succ, CochainComplex.mappingCone.map_id, CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₁, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₂, biprodXIso_hom_snd_assoc, CategoryTheory.Functor.commShiftIso_map₂CochainComplex_inv_app, quasiIso_comp, CochainComplex.mappingConeCompTriangle_obj₃, instPreservesZeroMorphismsHomologyFunctor, CategoryTheory.ProjectiveResolution.π'_f_zero, leftUnitor'_inv, HomologicalComplex₂.totalFlipIso_hom_f_D₂, forget_obj, QuasiIsoAt.quasiIso, CategoryTheory.InjectiveResolution.desc_commutes, isSeparating_separatingFamily, CategoryTheory.Idempotents.DoldKan.η_inv_app_f, CochainComplex.HomComplex.Cocycle.fromSingleMk_neg, Homotopy.comp_nullHomotopicMap, CategoryTheory.InjectiveResolution.desc_commutes_assoc, single_map_f_self_assoc, isIso_πTruncGE_iff, homologicalComplexToDGO_map_f, CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_inv_app_f, ComplexShape.Embedding.instFullHomologicalComplexExtendFunctor, CochainComplex.exists_iso_single, groupHomology.isoShortComplexH1_inv, CochainComplex.HomComplex.Cocycle.rightShiftAddEquiv_symm_apply, CochainComplex.HomComplex.Cochain.shift_units_smul, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_inv_app, CochainComplex.ConnectData.restrictionLEIso_hom_f, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comp_d, CochainComplex.shiftFunctorAdd_eq, CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv_symm_apply, CochainComplex.ι_mapBifunctorShift₂Iso_hom_f, CochainComplex.cm5b.instQuasiIsoIntP, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, HomologicalComplex₂.D₁_totalShift₁XIso_hom, πTruncGE_naturality, HomologicalComplex₂.D₂_totalShift₁XIso_hom, AlgebraicTopology.DoldKan.P_idem, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_p, ComplexShape.Embedding.instAdditiveHomologicalComplexRestrictionFunctor, ComplexShape.Embedding.homEquiv_symm_apply, HomologicalComplex₂.comm_f_assoc, cylinder.inrX_π, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, homologyMap_sub, HomologicalComplex₂.totalFlipIso_hom_f_D₁_assoc, Homotopy.comp_nullHomotopicMap', instPreservesColimitsOfShapeEvalOfHasColimitsOfShape, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_map_f_f, ComplexShape.Embedding.homEquiv_apply_coe, groupHomology.chainsMap_comp, HomologicalComplex₂.XXIsoOfEq_inv_ιTotal, AlgebraicTopology.DoldKan.natTransP_app, CategoryTheory.InjectiveResolution.Hom.ι_f_zero_comp_hom_f_zero, DerivedCategory.instIsGEObjCochainComplexIntQOfIsGE, cylinder.πCompι₀Homotopy.inrX_nullHomotopy_f, homologyπ_singleObjHomologySelfIso_hom, CategoryTheory.Functor.mapHomotopyEquiv_homotopyInvHomId, HomologicalComplex₂.total.map_comp, SimplicialObject.Split.nondegComplexFunctor_obj, cyclesOpIso_hom_naturality, CochainComplex.mappingConeCompHomotopyEquiv_comm₂, AlgebraicTopology.DoldKan.N₁_obj_X, CategoryTheory.Functor.map₂HomologicalComplex_obj_obj, instHasColimitsOfShape, AlgebraicTopology.map_alternatingFaceMapComplex, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_obj_X, CochainComplex.HomComplex.Cochain.δ_toSingleMk, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_map_f_f, smul_f_apply, CochainComplex.cm5b.instMonoFIntI, CochainComplex.HomComplex.CohomologyClass.toHom_bijective, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, AlgebraicTopology.DoldKan.Γ₀_obj_obj, CochainComplex.HomComplex.Cochain.fromSingleMk_precomp, HomologicalComplex₂.ofGradedObject_X_d, singleObjCyclesSelfIso_inv_iCycles_assoc, CochainComplex.HomComplex.Cochain.leftUnshift_add, HomologicalComplex₂.flipEquivalence_functor, Homotopy.compLeftId_hom, singleObjOpcyclesSelfIso_hom_naturality_assoc, CochainComplex.HomComplex.Cocycle.fromSingleMk_zero, zero_f_apply, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃_assoc, HomotopyCategory.instIsCompatibleWithShiftHomologicalComplexIntUpHomotopic, CochainComplex.instIsIsoIntιTruncLEOfIsStrictlyLE, natTransOpCyclesToCycles_app, CategoryTheory.Idempotents.DoldKan.Γ_obj_map, Homotopy.add_hom, CategoryTheory.InjectiveResolution.ι'_f_zero_assoc, Rep.standardComplex.quasiIso_forget₂_εToSingle₀, instMonoιTruncLE, CochainComplex.shiftFunctorZero'_inv_app_f, CochainComplex.mappingCone.cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality_assoc, inr_biprodXIso_inv_assoc, singleMapHomologicalComplex_inv_app_ne, CochainComplex.HomComplex.Cochain.rightShift_units_smul, CategoryTheory.ProjectiveResolution.self_complex, AlgebraicTopology.alternatingCofaceMapComplex_obj, CategoryTheory.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoObjCochainComplexCompSingleFunctorOfNatOfHasExt, truncLE'ToRestriction_naturality_assoc, dgoToHomologicalComplex_map_f, ComplexShape.Embedding.instPreservesZeroMorphismsHomologicalComplexExtendFunctor, DerivedCategory.exists_iso_Q_obj_of_isGE_of_isLE, ChainComplex.truncateAugment_hom_f, shortComplexFunctor'_map_τ₁, CochainComplex.HomComplex.Cochain.rightUnshift_smul, HomotopyCategory.composableArrowsFunctor_map, HomologicalComplexUpToQuasiIso.Qh_inverts_quasiIso, HomologicalComplex₂.ofGradedObject_X_X, AlgebraicTopology.DoldKan.Q_succ, AlgebraicTopology.DoldKan.natTransPInfty_f_app, instIsLocalizationHomologicalComplexDownHomotopyCategoryQuotientHomotopyEquivalences, cyclesMap_zero, CategoryTheory.Idempotents.DoldKan.Γ_obj_obj, HomologicalComplex₂.flipEquivalence_inverse, single_map_f_self, ChainComplex.fromSingle₀Equiv_symm_apply_f_zero, CochainComplex.HomComplex.Cocycle.equivHomShift'_apply, CochainComplex.instQuasiIsoIntMapHomologicalComplexUpShiftFunctor, CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom'_assoc, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃_assoc, homologyMap_zero, mapBifunctorFlipIso_flip, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_add, CategoryTheory.Equivalence.mapHomologicalComplex_counitIso, Homotopy.compRightId_hom, CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective, CochainComplex.mappingCone.triangleRotateShortComplexSplitting_r, AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_inv_app, AlgebraicTopology.DoldKan.instMonoChainComplexNatInclusionOfMooreComplexMap, extendMap_add, CategoryTheory.Abelian.DoldKan.equivalence_inverse, cyclesFunctor_obj, CochainComplex.HomComplex.Cochain.δ_shift, CochainComplex.shiftShortComplexFunctor'_hom_app_τ₃, CochainComplex.HomComplex.Cochain.fromSingleMk_sub, CochainComplex.toSingle₀Equiv_symm_apply_f_succ, CochainComplex.mappingCone.inl_v_descShortComplex_f_assoc, groupHomology.isoShortComplexH2_hom, shortComplexTruncLE_shortExact, CochainComplex.IsKProjective.leftOrthogonal, instHasTwoOutOfThreePropertyQuasiIso, singleCompEvalIsoSelf_inv_app, asFunctor_obj_d, ComplexShape.Embedding.truncLE'Functor_map, ChainComplex.augmentTruncate_hom_f_zero, DerivedCategory.from_singleFunctor_obj_eq_zero_of_projective, CategoryTheory.ProjectiveResolution.lift_commutes_assoc, shortComplexFunctor_obj_X₁, HomologicalComplex₂.ιTotalOrZero_map, restrictionMap_comp_assoc, HomotopyCategory.quotient_obj_as, HomologicalComplex₂.totalShift₁Iso_trans_totalShift₂Iso, DerivedCategory.exists_iso_Q_obj_of_isGE, CategoryTheory.Functor.commShiftIso_map₂CochainComplex_flip_inv_app, CochainComplex.cm5b.instMonoIntI, CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_apply, AlgebraicTopology.DoldKan.P_add_Q, AlgebraicTopology.DoldKan.instReflectsIsomorphismsSimplicialObjectKaroubiChainComplexNatN₁, shortComplexTruncLE_X₂, HomologicalComplex₂.d₂_eq, ChainComplex.toSingle₀Equiv_symm_apply_f_zero, CategoryTheory.ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq, ChainComplex.instHasHomologyNatObjAlternatingConst, CochainComplex.HomComplex.Cocycle.toSingleMk_sub, truncLEMap_id, ComplexShape.Embedding.πTruncGENatTrans_app, instHasFiniteColimits, ComplexShape.Embedding.truncLEFunctor_map, CochainComplex.isKProjective_iff_leftOrthogonal, HomologicalComplex₂.flip_totalFlipIso, quasiIsoAt_iff_evaluation, truncGE.rightHomologyMapData_φH, CategoryTheory.InjectiveResolution.extMk_hom, groupCohomology.isoShortComplexH1_hom, HomologicalComplex₂.total.map_comp_assoc, quasiIsoAt_iff', CochainComplex.HomComplex.Cocycle.fromSingleMk_sub, homologyFunctorSingleIso_inv_app, instPreservesLimitsOfShapeEvalOfHasLimitsOfShape, HomologicalComplex₂.shape_f, homotopy_congruence, ComplexShape.Embedding.truncLE'Functor_obj, CochainComplex.shortComplexTruncLE_shortExact, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_zero, CochainComplex.cm5b.i_f_comp, CochainComplex.HomComplex.Cochain.δ_rightUnshift, CochainComplex.mappingCone.inr_snd, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_neg, ChainComplex.truncate_obj_d, HomologicalComplexUpToQuasiIso.instIsLocalizationHomotopyCategoryQhQuasiIso, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId, CochainComplex.HomComplex.Cochain.leftUnshift_units_smul, CochainComplex.mappingCone.inl_fst, CochainComplex.quasiIsoAt₀_iff, Rep.FiniteCyclicGroup.resolution_complex, CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv_apply, singleObjHomologySelfIso_hom_naturality, gradedHomologyFunctor_obj, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₃, groupHomology.chainsFunctor_map, CochainComplex.HomComplex.Cocycle.shift_coe, CategoryTheory.Preadditive.DoldKan.equivalence_inverse, groupHomology.instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor, cylinder.ι₁_desc_assoc, dgoEquivHomologicalComplexCounitIso_hom_app_f, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_idem_assoc, CochainComplex.isStrictlyLE_shift, instQuasiIsoOppositeMapSymmOpFunctorOp, CochainComplex.ConnectData.restrictionGEIso_inv_f, restrictionToTruncGE'_naturality_assoc, singleObjHomologySelfIso_hom_naturality_assoc, CategoryTheory.NatTrans.mapHomologicalComplex_naturality_assoc, singleObjHomologySelfIso_inv_naturality_assoc, instHasBinaryBiproduct, CochainComplex.instFullIntSingleFunctor, HomologicalComplex₂.ofGradedObject_d_f, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₁, CochainComplex.HomComplex.Cochain.δ_rightShift, DerivedCategory.right_fac_of_isStrictlyLE, HomologicalComplex₂.ι_totalShift₂Iso_inv_f, CochainComplex.ConnectData.map_id, AlgebraicTopology.DoldKan.N₂_obj_p_f, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_X_X, CochainComplex.HomComplex.Cochain.leftShift_v, CochainComplex.HomComplex.Cochain.rightUnshift_add, CochainComplex.HomComplex.Cochain.toSingleMk_zero, CochainComplex.homologySequenceδ_quotient_mapTriangle_obj, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_X_X, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_hom_f_f, HomotopyCategory.homologyFunctor_shiftMap_assoc, CochainComplex.augmentTruncate_inv_f_succ, HomologicalComplex₂.totalShift₂Iso_hom_naturality, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso_hom_app_f_f, CategoryTheory.Functor.mapHomotopyCategory_map, CochainComplex.shiftFunctor_obj_X', CochainComplex.HomComplex.Cochain.shift_v, CochainComplex.shiftFunctorZero_hom_app_f, CategoryTheory.ProjectiveResolution.Hom.hom_f_zero_comp_π_f_zero, pOpcycles_singleObjOpcyclesSelfIso_inv_assoc, AlgebraicTopology.DoldKan.N₂_obj_X_X, truncGE'Map_comp_assoc, CategoryTheory.Idempotents.DoldKan.isoN₁_hom_app_f, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app, mapBifunctorMapHomotopy.comm₁_aux, ComplexShape.Embedding.instAdditiveHomologicalComplexExtendFunctor, Rep.standardComplex.instQuasiIsoNatεToSingle₀, epi_homologyMap_shortComplexTruncLE_g, truncGE'Map_id, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_d_f, Homotopy.smul_hom, CochainComplex.triangleOfDegreewiseSplit_mor₃, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap_assoc, CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv_assoc, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_extMk, CochainComplex.HomComplex.Cochain.shiftAddHom_apply, groupCohomology.instAdditiveRepCochainComplexModuleCatNatCochainsFunctor, HomologicalComplex₂.total.mapAux.d₂_mapMap, CategoryTheory.InjectiveResolution.instQuasiIsoIntι', isZero_iff_isStrictlySupported_and_isStrictlySupportedOutside, CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₂, evalCompCoyonedaCorepresentableByDoubleId_homEquiv_symm_apply, CochainComplex.HomComplex.Cochain.δ_leftUnshift, HomotopyCategory.spectralObjectMappingCone_ω₁, HomologicalComplex₂.ιTotal_totalFlipIso_f_hom, CochainComplex.HomComplex.Cocycle.toSingleMk_neg, ChainComplex.fromSingle₀Equiv_apply, CategoryTheory.InjectiveResolution.desc_commutes_zero, Rep.FiniteCyclicGroup.resolution_quasiIso, cyclesMapIso_inv, singleObjCyclesSelfIso_hom_assoc, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, CochainComplex.shiftFunctorAdd'_hom_app_f', ComplexShape.Embedding.truncGE'Functor_map, CategoryTheory.Functor.mapHomotopyCategory_obj, AlgebraicTopology.DoldKan.P_zero, CochainComplex.HomComplex.Cochain.leftShift_add, ComplexShape.Embedding.homRestrict_precomp_assoc, CochainComplex.HomComplex.Cochain.leftShift_comp_zero_cochain, singleObjCyclesSelfIso_inv_naturality, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply, quasiIsoAt_iff_comp_left, opEquivalence_functor, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃_assoc, CochainComplex.augmentTruncate_hom_f_succ, CochainComplex.shiftEval_hom_app, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_counitIso_inv, singleCompEvalIsoSelf_hom_app, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃, homologicalComplexToDGO_obj_d, HomologicalComplex₂.flip_X_d, CochainComplex.instHasMapBifunctorObjIntShiftFunctor_1, CochainComplex.HomComplex.Cocycle.equivHomShift_comp, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality, instHasSeparator, CochainComplex.cm5b.i_f_comp_assoc, singleObjOpcyclesSelfIso_inv_naturality_assoc, instPreservesFiniteColimitsSingle, quasiIso_opFunctor_map_iff, AlgebraicTopology.alternatingCofaceMapComplex_map, Homotopy.comp_hom, CochainComplex.mappingCone.triangleRotateShortComplex_g, CategoryTheory.Idempotents.DoldKan.equivalence_functor, CochainComplex.shiftFunctor_obj_d', CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse_obj, biprod_inl_desc_f, CochainComplex.instHasMapBifunctorObjIntShiftFunctor, singleObjHomologySelfIso_inv_naturality, CochainComplex.ιTruncLE_naturality, AlgebraicTopology.DoldKan.N₂_obj_X_d, CochainComplex.HomComplex.Cocycle.equivHom_apply, CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_hom_app_f, restrictionToTruncGE'_naturality, instIsIsoιTruncLEOfIsStrictlySupported, CategoryTheory.Abelian.DoldKan.equivalence_functor, CochainComplex.mappingCone.inr_descShortComplex, DerivedCategory.instAdditiveCochainComplexIntQ, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom_assoc, CochainComplex.HomComplex.Cocycle.fromSingleMk_precomp, ComplexShape.Embedding.restrictionToTruncGE'NatTrans_app, CochainComplex.ι_mapBifunctorShift₁Iso_hom_f_assoc, groupCohomology.isoShortComplexH2_hom, CategoryTheory.ProjectiveResolution.exact₀, CochainComplex.triangleOfDegreewiseSplit_mor₁, CochainComplex.mappingCone.mapHomologicalComplexXIso'_hom, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_inv_f_f, CochainComplex.fromSingle₀Equiv_symm_apply_f_zero, evalCompCoyonedaCorepresentableBySingle_homEquiv_symm_apply, homologicalComplexToDGO_obj_obj, stupidTruncMap_comp_assoc, CochainComplex.HomComplex.Cochain.leftShift_units_smul, homotopyCofiber.desc_f, HomotopyCategory.homologyShiftIso_hom_app, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_X_p, ChainComplex.augmentTruncate_inv_f_zero, CochainComplex.shiftFunctorAdd_hom_app_f, ι_mapBifunctorFlipIso_hom, CochainComplex.truncateAugment_hom_f, AlgebraicTopology.DoldKan.homotopyPToId_eventually_constant, truncLE'Map_comp, biprod_inr_desc_f_assoc, CategoryTheory.Idempotents.DoldKan.Γ_map_app, evalCompCoyonedaCorepresentableBySingle_homEquiv_apply, CochainComplex.HomComplex.δ_map, CategoryTheory.Functor.map₂HomologicalComplex_obj_map, HomologicalComplex₂.totalShift₁Iso_hom_naturality_assoc, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso, shortComplexFunctor'_map_τ₃, unopInverse_obj, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_X, CochainComplex.mappingCone.inl_v_descShortComplex_f, opEquivalence_inverse, truncLE'Map_comp_assoc, CochainComplex.isIso_ιTruncLE_iff, HomologicalComplex₂.ι_D₁, opcyclesFunctor_obj, HomologicalComplex₂.flipEquivalenceCounitIso_inv_app_f_f, natTransHomologyι_app, homologyFunctorIso_hom_app, CochainComplex.HomComplex.Cochain.toSingleMk_postcomp, CochainComplex.HomComplex.Cochain.ofHom_add, ComplexShape.Embedding.restrictionFunctor_obj, HomologicalComplex₂.toGradedObjectFunctor_map, CategoryTheory.Functor.mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app, CochainComplex.mappingCone.triangleRotateShortComplexSplitting_s, CochainComplex.mappingCone.inr_f_descShortComplex_f, asFunctor_map_f, ChainComplex.alternatingConst_exactAt, CochainComplex.toSingle₀Equiv_apply, CochainComplex.HomComplex.Cochain.id_comp, singleObjCyclesSelfIso_hom_naturality_assoc, ComplexShape.Embedding.truncLE'ToRestrictionNatTrans_app, CategoryTheory.ProjectiveResolution.instQuasiIsoIntπ', groupHomology.chainsMap_zero, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comm_f, mkHomFromSingle_f, DerivedCategory.exists_iso_Q_obj_of_isLE, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, cyclesOpNatIso_hom_app, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₃, shortComplexFunctor_map_τ₂, instPreservesFiniteColimitsEvalOfHasFiniteColimits, CochainComplex.shiftFunctorAdd'_hom_app_f, CochainComplex.HomComplex.Cochain.ofHom_zero, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE_assoc, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_inv_app_f_f, CochainComplex.mappingCone.inr_f_triangle_mor₃_f_assoc, Homotopy.compLeft_hom, shortComplexFunctor_obj_g, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_add, groupHomology.isoShortComplexH2_inv, HomologicalComplex₂.ι_totalShift₂Iso_hom_f, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app, exactAt_single_obj, shortComplexTruncLE_X₁, HomologicalComplex₂.instHasTotalIntObjUpShiftFunctor₁, CategoryTheory.InjectiveResolution.Hom.ι_f_zero_comp_hom_f_zero_assoc, hasExactColimitsOfShape, CochainComplex.HomComplex.Cochain.map_ofHom, CochainComplex.HomComplex.CohomologyClass.toHom_mk_eq_zero_iff, extendMap_comp, quasiIso_unopFunctor_map_iff, CochainComplex.shiftFunctorComm_hom_app_f, ComplexShape.QFactorsThroughHomotopy.areEqualizedByLocalization, instPreservesBinaryBiproductEval, CategoryTheory.Abelian.DoldKan.comparisonN_hom_app_f, CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_counitIso, groupCohomology.map_cochainsFunctor_shortExact, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_f, HomologicalComplex₂.XXIsoOfEq_hom_ιTotal, CochainComplex.HomComplex.Cochain.leftShiftAddEquiv_symm_apply, Homotopy.nullHomotopy_hom, CochainComplex.HomComplex.Cochain.rightShift_neg, HomologySequence.composableArrows₃Functor_map, HomologicalComplex₂.totalShift₁Iso_hom_naturality, Hom.isoApp_inv, CochainComplex.mappingConeCompTriangle_mor₃_naturality_assoc, HomotopyCategory.quotient_obj_singleFunctors_obj, HomologicalComplex₂.total.mapAux.d₁_mapMap_assoc, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f, CategoryTheory.InjectiveResolution.instMonoFNatι, CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃, HomologicalComplex₂.d₂_eq', DerivedCategory.instEssSurjCochainComplexIntQ, CochainComplex.HomComplex.Cochain.fromSingleMk_v_eq_zero, dgoEquivHomologicalComplex_inverse, DerivedCategory.singleFunctorsPostcompQIso_hom_hom, ComplexShape.quotient_isLocalization, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₂, CochainComplex.HomComplex.Cocycle.equivHomShift_symm_precomp, quasiIso_iff_comp_right, CategoryTheory.Functor.mapCochainComplexShiftIso_hom_app_f, CochainComplex.shiftEval_inv_app, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles_assoc, unopEquivalence_inverse, CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁, CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι_assoc, AlgebraicTopology.DoldKan.Γ₂_obj_X_obj, HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic, homotopyCofiber.inlX_desc_f, AlgebraicTopology.DoldKan.QInfty_comp_PInfty_assoc, HomotopyCategory.instAdditiveHomologicalComplexQuotient, HomotopyCategory.quotient_map_out, CategoryTheory.InjectiveResolution.homotopyEquiv_hom_ι, HomologicalComplex₂.d₁_eq', CochainComplex.HomComplex.Cocycle.rightShiftAddEquiv_apply, truncLE'ToRestriction_naturality, AlgebraicTopology.DoldKan.Γ₂_map_f_app, CochainComplex.HomComplex.Cocycle.fromSingleMk_mem_coboundaries_iff, groupCohomology.cochainsFunctor_map, instPreservesFiniteLimitsSingle, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso_hom, extendMap_zero, quasiIsoAt_iff, CategoryTheory.InjectiveResolution.exact₀, quasiIsoAt_map_of_preservesHomology, instAdditiveSingle, shortComplexFunctor'_obj_f, CochainComplex.HomComplex.Cocycle.equivHomShift_comp_shift, HomotopyCategory.homologyFunctor_shiftMap, CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv_symm_apply, HomologySequence.composableArrows₃Functor_obj, HomologicalComplex₂.toGradedObjectMap_apply, CochainComplex.shiftShortComplexFunctor'_inv_app_τ₁, HomologicalComplex₂.ιTotalOrZero_eq_zero, CochainComplex.shiftShortComplexFunctorIso_zero_add_hom_app, CochainComplex.isKProjective_shift_iff, opFunctor_additive, instPreservesZeroMorphismsCyclesFunctor, instQuasiIsoShortComplexTruncLEX₃ToTruncGE, eval_additive, CochainComplex.instIsStrictlyLEObjIntSingleFunctor, CochainComplex.mappingCone.triangle_obj₂, CochainComplex.instIsStrictlyGEObjIntSingleFunctor, HomologicalComplex₂.flip_d_f, CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₃, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_counitIso_inv, CochainComplex.mappingConeCompTriangle_mor₂, AlgebraicTopology.DoldKan.Γ₂N₁_inv, HomologicalComplex₂.D₁_totalShift₂XIso_hom, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_d_f, CochainComplex.cm5b.degreewiseEpiWithInjectiveKernel_p, CochainComplex.HomComplex.Cochain.rightShift_v, CochainComplex.HomComplex.Cochain.rightUnshift_zero, AlgebraicTopology.DoldKan.instReflectsIsomorphismsKaroubiSimplicialObjectChainComplexNatN₂, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_X_X, CochainComplex.mappingConeCompTriangleh_comm₁, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_extMk, CochainComplex.HomComplex.Cocycle.toSingleMk_postcomp, AlgebraicTopology.DoldKan.Q_zero, CochainComplex.HomComplex.Cocycle.leftShift_coe, CategoryTheory.InjectiveResolution.homotopyEquiv_inv_ι_assoc, opcyclesMap_zero, HomologicalComplex₂.D₂_totalShift₂XIso_hom, instEpiπTruncGE, instHasBinaryBiproductObjEval, ChainComplex.truncate_obj_X, groupCohomology.isoShortComplexH1_inv, AlgebraicTopology.DoldKan.identity_N₂_objectwise, CochainComplex.single₀_obj_zero, shortExact_iff_degreewise_shortExact, shortComplexTruncLE_shortExact_δ_eq_zero, CochainComplex.HomComplex.Cochain.shift_v', CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_map_f_f, AlgebraicTopology.inclusionOfMooreComplexMap_f, CategoryTheory.Idempotents.DoldKan.hη, CochainComplex.cm5b.instInjectiveXIntMappingConeIdI, biprod_lift_snd_f_assoc, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_inv_app_f_f, biprod_inr_fst_f_assoc, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f, ComplexShape.Embedding.extendFunctor_obj, AlgebraicTopology.alternatingFaceMapComplex_obj_X, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, DerivedCategory.mem_distTriang_iff, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f, CategoryTheory.Functor.instCommShiftCochainComplexIntMapMap₂CochainComplex, CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_d_f, CochainComplex.isKInjective_iff_rightOrthogonal, AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex_assoc, CochainComplex.HomComplex.Cochain.rightShift_add, CochainComplex.ShiftSequence.shiftIso_inv_app, neg_f_apply, CategoryTheory.ProjectiveResolution.instEpiFNatπ, CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero_assoc, groupCohomology.cochainsMap_id_comp_assoc, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_X, truncGEMap_comp, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor_map, dgoEquivHomologicalComplexUnitIso_inv_app_f, unopFunctor_map_f, homologyOp_hom_naturality, locallySmall, DerivedCategory.instIsLEObjCochainComplexIntQOfIsLE, AlgebraicTopology.DoldKan.P_idem_assoc, AlgebraicTopology.DoldKan.PInfty_comp_QInfty_assoc, CategoryTheory.Functor.instCommShiftCochainComplexIntMapFlipMap₂CochainComplex, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_d, HomologicalComplex₂.flipEquivalenceCounitIso_hom_app_f_f, homologyFunctor_inverts_quasiIso, CochainComplex.HomComplex.Cochain.toSingleEquiv_toSingleMk, instHasColimitDiscreteWalkingPairCompPairEval, CochainComplex.isGE_shift, instPreservesZeroMorphismsSingle, AlgebraicTopology.DoldKan.N₂_map_f_f, CochainComplex.truncate_obj_d, CategoryTheory.InjectiveResolution.rightDerivedToHomotopyCategory_app_eq, DerivedCategory.Q_map_eq_of_homotopy, CategoryTheory.Functor.commShiftIso_map₂CochainComplex_hom_app, singleObjCyclesSelfIso_hom, CochainComplex.mappingCone.triangleRotateShortComplex_f, CochainComplex.HomComplex.Cocycle.fromSingleMk_postcomp, quasiIsoAt_opFunctor_map_iff, HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_exactAt, CochainComplex.HomComplex.Cocycle.rightUnshift_coe, HomologicalComplex₂.d_comm_assoc, CategoryTheory.Functor.mapHomotopyEquiv_hom, CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃, CategoryTheory.Equivalence.mapHomologicalComplex_inverse, ComplexShape.Embedding.truncGEFunctor_map, CochainComplex.HomComplex.Cochain.δ_leftShift, HomologicalComplex₂.totalAux.d₁_eq', DerivedCategory.isIso_Q_map_iff_quasiIso, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_hom_app_f_f, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_hom, cylinder.ι₁_desc, ι_mapBifunctorFlipIso_hom_assoc, CochainComplex.HomComplex.Cocycle.toSingleMk_precomp, extendSingleIso_hom_f, CochainComplex.HomComplex.CohomologyClass.toHom_mk, AlgebraicTopology.DoldKan.N₁Γ₀_app, HomologicalComplex₂.total.hom_ext_iff, groupCohomology.isoShortComplexH2_inv, CochainComplex.πTruncGE_naturality_assoc, instFullSingle, CochainComplex.HomComplex.Cocycle.leftShiftAddEquiv_apply, HomotopyCategory.quotient_map_mem_quasiIso_iff, CochainComplex.instIsMultiplicativeIntDegreewiseEpiWithInjectiveKernel, biprod_inl_snd_f, CochainComplex.toSingle₀Equiv_symm_apply_f_zero, DerivedCategory.left_fac_of_isStrictlyGE, CochainComplex.mappingConeHomOfDegreewiseSplitIso_hom_f, homologyFunctorIso_inv_app, CochainComplex.augmentTruncate_hom_f_zero, comp_f_assoc, unopFunctor_additive, ChainComplex.alternatingConst_map_f, instHasZeroObject, CategoryTheory.Idempotents.DoldKan.N_map, ChainComplex.single₀_obj_zero, instIsNormalMonoCategory, g_shortComplexTruncLEX₃ToTruncGE_assoc, CategoryTheory.InjectiveResolution.quasiIso, ChainComplex.fromSingle₀Equiv_symm_apply_f_succ, instFaithfulSingle, unopEquivalence_counitIso, ComplexShape.Embedding.homRestrict_comp_extendMap, truncGEMap_id, opInverse_map, CochainComplex.HomComplex.Cochain.leftShift_neg, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, HomologicalComplex₂.flipFunctor_map_f_f, singleObjHomologySelfIso_inv_homologyι, homologyFunctor_obj, AlgebraicTopology.DoldKan.HigherFacesVanish.induction, HomotopyCategory.isoOfHomotopyEquiv_inv, CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app, CochainComplex.HomComplex.Cochain.toSingleMk_sub, shortComplexTruncLE_X₃_isSupportedOutside, biprod_inl_desc_f_assoc, CategoryTheory.ProjectiveResolution.fromLeftDerivedZero_eq, CategoryTheory.InjectiveResolution.Hom.ι_comp_hom, extendMap_id, Hom.isoApp_hom, CategoryTheory.Abelian.DoldKan.comparisonN_inv_app_f, homologyFunctorSingleIso_hom_app, CochainComplex.HomComplex.Cocycle.equivHomShift_apply, ComplexShape.Embedding.AreComplementary.hom_ext', CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₁, singleObjOpcyclesSelfIso_hom_assoc, homologyMap_comp_assoc, ChainComplex.single₀_map_f_zero, ChainComplex.alternatingConst_obj, CochainComplex.HomComplex.Cochain.leftUnshift_neg, singleObjHomologySelfIso_hom_singleObjHomologySelfIso_inv, isZero_single_comp_eval, CategoryTheory.instPreservesZeroMorphismsHomologicalComplexMapHomologicalComplex, CochainComplex.isLE_shift, CochainComplex.mappingCone.triangle_obj₁, cylinder.ι₀_desc_assoc, dgoEquivHomologicalComplexCounitIso_inv_app_f, Homotopy.nullHomotopy'_hom, Hom.isIso_of_components, AlgebraicTopology.DoldKan.Γ₀'_map_f, singleObjOpcyclesSelfIso_hom_naturality, CochainComplex.mappingCone.mapHomologicalComplexXIso'_inv, HomologicalComplexUpToQuasiIso.isIso_Q_map_iff_mem_quasiIso, CochainComplex.cm5b, homologyMapIso_inv, Rep.FiniteCyclicGroup.resolution.π_f, natIsoSc'_inv_app_τ₁, instHasFiniteLimits, exact_iff_degreewise_exact, groupCohomology.cochainsFunctor_obj, CategoryTheory.InjectiveResolution.rightDerived_app_eq, instHasHomologyObjOppositeSymmUnopFunctorOp, CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom', CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_symm_apply, Hom.fAddMonoidHom_apply, epi_of_epi_f, CochainComplex.shiftFunctor_obj_d, HomologicalComplex₂.total.map_id, CochainComplex.HomComplex.Cochain.toSingleMk_precomp, HomotopyCategory.instLinearHomologicalComplexQuotient, CochainComplex.HomComplex.Cocycle.rightShift_coe, CochainComplex.single₀ObjXSelf, CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id_assoc, HomologicalComplex₂.total.forget_map, AlgebraicTopology.DoldKan.Γ₂N₂_inv, HomologicalComplex₂.totalFunctor_map, natIsoSc'_hom_app_τ₁, instPreservesZeroMorphismsOpcyclesFunctor, extendMap_id_f, CochainComplex.HomComplex.Cochain.leftUnshift_zero, ComplexShape.Embedding.stupidTruncFunctor_obj, DerivedCategory.left_fac, CategoryTheory.Idempotents.DoldKan.η_hom_app_f, AlgebraicTopology.normalizedMooreComplex_obj, CochainComplex.mappingCone.triangle_obj₃, cyclesMapIso_hom, AlgebraicTopology.DoldKan.natTransQ_app, CochainComplex.HomComplex.Cochain.map_neg, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_toGradedObject, HomologicalComplex₂.ιTotal_map_assoc, CochainComplex.instFaithfulIntSingleFunctor, AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app, ι_mapBifunctorFlipIso_inv, CochainComplex.HomComplex.CohomologyClass.homAddEquiv_apply, CochainComplex.mappingConeCompTriangle_obj₁, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_counitIso_hom, CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_apply, CategoryTheory.Idempotents.DoldKan.equivalence_unitIso, cylinder.πCompι₀Homotopy.inlX_nullHomotopy_f, ChainComplex.map_chain_complex_of, HomologicalComplex₂.totalFlipIso_hom_f_D₂_assoc, CochainComplex.instAdditiveHomologicalComplexIntUpShiftFunctor, HomologicalComplex₂.ι_totalShift₁Iso_hom_f, forgetEval_inv_app, CategoryTheory.instIsIsoFromLeftDerivedZero', ComplexShape.Embedding.instPreservesZeroMorphismsHomologicalComplexRestrictionFunctor, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, HomologicalComplex₂.instFaithfulGradedObjectProdToGradedObjectFunctor, ComplexShape.Embedding.truncGEFunctor_obj, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_d_f, CochainComplex.ι_mapBifunctorShift₁Iso_hom_f, shortComplexFunctor_obj_X₃, AlgebraicTopology.DoldKan.PInfty_add_QInfty, CochainComplex.ShiftSequence.shiftIso_hom_app, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_neg, groupCohomology.cochainsMap_id, HomotopyCategory.instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors, CochainComplex.mappingCone.map_δ, HomologicalComplex₂.ιTotal_totalFlipIso_f_inv, CochainComplex.HomComplex.Cochain.ofHom_comp, CochainComplex.ConnectData.restrictionGEIso_hom_f, quasiIsoAt_map_iff_of_preservesHomology, Hom.sqFrom_id
instHasZeroMorphisms 📖	CompOp	220 math math: CategoryTheory.ShortComplex.ShortExact.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoX₃CochainComplexMapSingleFunctorOfNatX₁, CochainComplex.triangleOfDegreewiseSplit_obj₁, CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_map_f_f, HomologicalComplex₂.totalShift₂Iso_hom_naturality_assoc, biprod_inr_desc_f, biprod_lift_fst_f_assoc, groupCohomology.instPreservesZeroMorphismsRepCochainComplexModuleCatNatCochainsFunctor, HomologicalComplex₂.shiftFunctor₂XXIso_refl, HomologicalComplex₂.comm_f, HomologicalComplex₂.total.mapIso_hom, inl_biprodXIso_inv_assoc, biprod_inr_snd_f_assoc, biprod_inl_snd_f_assoc, HomologicalComplex₂.totalAux.d₂_eq, instIsNormalEpiCategory, HomologicalComplex₂.D₂_totalShift₁XIso_hom_assoc, biprodXIso_hom_fst, HomologicalComplex₂.D₂_totalShift₂XIso_hom_assoc, HomologicalComplex₂.d_f_comp_d_f, HomologicalComplex₂.flipEquivalence_unitIso, HomologicalComplex₂.d₁_eq_zero', CochainComplex.cm5b.fac, biprod_lift_fst_f, HomologicalComplex₂.toGradedObjectFunctor_obj, HomologicalComplex₂.ιTotalOrZero_map_assoc, HomologicalComplex₂.ιTotal_map, HomologicalComplex₂.ι_totalShift₁Iso_hom_f_assoc, HomologicalComplex₂.ι_D₁_assoc, HomologicalComplex₂.ιTotal_totalFlipIso_f_inv_assoc, CochainComplex.mappingCone.inr_f_descShortComplex_f_assoc, HomologicalComplex₂.d₂_eq_zero, HomologicalComplex₂.ι_totalShift₁Iso_inv_f, HomologicalComplex₂.ι_totalDesc_assoc, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁, CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_X_d, CochainComplex.mappingCone.inr_descShortComplex_assoc, instEpiGShortComplexTruncLE, HomologicalComplex₂.flipEquivalenceUnitIso_hom_app_f_f, HomologicalComplex₂.ι_totalShift₂Iso_inv_f_assoc, HomologicalComplex₂.d_comm, CochainComplex.triangleOfDegreewiseSplit_obj₂, inr_biprodXIso_inv, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE, HomologicalComplex₂.d_f_comp_d_f_assoc, HomologicalComplex₂.ι_D₂, HomologicalComplex₂.total.mapAux.d₁_mapMap, HomologicalComplex₂.d₁_eq, HomologicalComplex₂.instHasTotalIntObjUpShiftFunctor₂, biprod_inr_snd_f, HomologicalComplex₂.XXIsoOfEq_hom_ιTotal_assoc, groupHomology.map_chainsFunctor_shortExact, instMonoFShortComplexTruncLE, CochainComplex.mappingCone.triangleRotateShortComplex_X₂, HomologicalComplex₂.instHasTotalIntObjUpCompShiftFunctor₁ShiftFunctor₂, HomologicalComplex₂.XXIsoOfEq_rfl, HomologicalComplex₂.ι_D₂_assoc, isIso_homologyMap_shortComplexTruncLE_g, CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv, CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_X_X, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂, CochainComplex.mappingCone.triangleRotateShortComplex_X₃, HomologicalComplex₂.totalFunctor_obj, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom, HomologicalComplex₂.flipFunctor_obj, HomologicalComplex₂.totalAux.d₂_eq', HomologicalComplex₂.totalAux.d₁_eq, instPreservesZeroMorphismsEval, HomologicalComplex₂.D₁_totalShift₂XIso_hom_assoc, HomologicalComplex₂.shiftFunctor₁XXIso_refl, CochainComplex.mappingCone.triangleRotateShortComplex_X₁, HomologicalComplex₂.ι_totalDesc, HomologicalComplex₂.total.mapAux.d₂_mapMap_assoc, HomologicalComplex₂.d₁_eq_zero, HomologicalComplex₂.flip_X_X, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃, biprod_lift_snd_f, biprod_inl_fst_f_assoc, g_shortComplexTruncLEX₃ToTruncGE, CategoryTheory.Functor.mapBifunctorHomologicalComplex_map_app_f_f, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_inv_f_f, inl_biprodXIso_inv, mono_homologyMap_shortComplexTruncLE_g, HomologicalComplex₂.D₁_totalShift₁XIso_hom_assoc, cylinder.inrX_π_assoc, biprod_inl_fst_f, HomologicalComplex₂.instHasTotalIntObjUpCompShiftFunctor₂ShiftFunctor₁, CochainComplex.cm5b.instIsStrictlyGEBiprodIntMappingConeIdIOfHAddOfNat, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_X_d, CochainComplex.triangleOfDegreewiseSplit_mor₂, biprod_inr_fst_f, CochainComplex.cm5b.fac_assoc, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_hom_f_f, biprodXIso_hom_fst_assoc, CochainComplex.triangleOfDegreewiseSplit_obj₃, HomologicalComplex₂.flipEquivalenceUnitIso_inv_app_f_f, quasiIsoAt_shortComplexTruncLE_g, HomologicalComplex₂.d₂_eq_zero', HomologicalComplex₂.ι_totalShift₁Iso_inv_f_assoc, HomologicalComplex₂.ιTotal_totalFlipIso_f_hom_assoc, HomologicalComplex₂.XXIsoOfEq_inv_ιTotal_assoc, HomologicalComplex₂.total.mapIso_inv, shortComplexTruncLE_f, biprodXIso_hom_snd, CochainComplex.homOfDegreewiseSplit_f, HomologicalComplex₂.flipEquivalence_counitIso, HomologicalComplex₂.ι_totalShift₂Iso_hom_f_assoc, biprodXIso_hom_snd_assoc, instPreservesZeroMorphismsHomologyFunctor, CochainComplex.cm5b.instQuasiIsoIntP, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃, HomologicalComplex₂.D₁_totalShift₁XIso_hom, HomologicalComplex₂.D₂_totalShift₁XIso_hom, HomologicalComplex₂.comm_f_assoc, cylinder.inrX_π, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁, HomologicalComplex₂.XXIsoOfEq_inv_ιTotal, cylinder.πCompι₀Homotopy.inrX_nullHomotopy_f, HomologicalComplex₂.total.map_comp, CochainComplex.cm5b.instMonoFIntI, HomologicalComplex₂.ofGradedObject_X_d, HomologicalComplex₂.flipEquivalence_functor, CochainComplex.mappingCone.cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v, inr_biprodXIso_inv_assoc, ComplexShape.Embedding.instPreservesZeroMorphismsHomologicalComplexExtendFunctor, HomologicalComplex₂.ofGradedObject_X_X, HomologicalComplex₂.flipEquivalence_inverse, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃_assoc, CochainComplex.mappingCone.triangleRotateShortComplexSplitting_r, CochainComplex.mappingCone.inl_v_descShortComplex_f_assoc, shortComplexTruncLE_shortExact, HomologicalComplex₂.ιTotalOrZero_map, HomologicalComplex₂.totalShift₁Iso_trans_totalShift₂Iso, CochainComplex.cm5b.instMonoIntI, shortComplexTruncLE_X₂, HomologicalComplex₂.d₂_eq, HomologicalComplex₂.total.map_comp_assoc, HomologicalComplex₂.shape_f, CochainComplex.shortComplexTruncLE_shortExact, CochainComplex.cm5b.i_f_comp, groupHomology.instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor, instHasBinaryBiproduct, HomologicalComplex₂.ofGradedObject_d_f, HomologicalComplex₂.ι_totalShift₂Iso_inv_f, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_X_X, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_hom_f_f, HomologicalComplex₂.totalShift₂Iso_hom_naturality, mapBifunctorMapHomotopy.comm₁_aux, epi_homologyMap_shortComplexTruncLE_g, CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv_assoc, HomologicalComplex₂.total.mapAux.d₂_mapMap, HomologicalComplex₂.ιTotal_totalFlipIso_f_hom, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃, HomologicalComplex₂.flip_X_d, CochainComplex.cm5b.i_f_comp_assoc, CochainComplex.mappingCone.triangleRotateShortComplex_g, biprod_inl_desc_f, CochainComplex.mappingCone.inr_descShortComplex, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom_assoc, CochainComplex.triangleOfDegreewiseSplit_mor₁, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_inv_f_f, biprod_inr_desc_f_assoc, HomologicalComplex₂.totalShift₁Iso_hom_naturality_assoc, CochainComplex.mappingCone.inl_v_descShortComplex_f, HomologicalComplex₂.ι_D₁, HomologicalComplex₂.flipEquivalenceCounitIso_inv_app_f_f, HomologicalComplex₂.toGradedObjectFunctor_map, CochainComplex.mappingCone.triangleRotateShortComplexSplitting_s, CochainComplex.mappingCone.inr_f_descShortComplex_f, CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂, CochainComplex.g_shortComplexTruncLEX₃ToTruncGE_assoc, HomologicalComplex₂.ι_totalShift₂Iso_hom_f, shortComplexTruncLE_X₁, HomologicalComplex₂.instHasTotalIntObjUpShiftFunctor₁, instPreservesBinaryBiproductEval, groupCohomology.map_cochainsFunctor_shortExact, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_f, HomologicalComplex₂.XXIsoOfEq_hom_ιTotal, HomologicalComplex₂.totalShift₁Iso_hom_naturality, HomologicalComplex₂.total.mapAux.d₁_mapMap_assoc, HomologicalComplex₂.d₂_eq', HomologicalComplex₂.d₁_eq', HomologicalComplex₂.toGradedObjectMap_apply, HomologicalComplex₂.ιTotalOrZero_eq_zero, instPreservesZeroMorphismsCyclesFunctor, instQuasiIsoShortComplexTruncLEX₃ToTruncGE, HomologicalComplex₂.flip_d_f, HomologicalComplex₂.D₁_totalShift₂XIso_hom, CochainComplex.cm5b.degreewiseEpiWithInjectiveKernel_p, HomologicalComplex₂.D₂_totalShift₂XIso_hom, shortExact_iff_degreewise_shortExact, shortComplexTruncLE_shortExact_δ_eq_zero, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_map_f_f, biprod_lift_snd_f_assoc, biprod_inr_fst_f_assoc, CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_d_f, HomologicalComplex₂.flipEquivalenceCounitIso_hom_app_f_f, instPreservesZeroMorphismsSingle, CochainComplex.mappingCone.triangleRotateShortComplex_f, HomologicalComplex₂.d_comm_assoc, HomologicalComplex₂.totalAux.d₁_eq', HomologicalComplex₂.total.hom_ext_iff, biprod_inl_snd_f, CochainComplex.mappingConeHomOfDegreewiseSplitIso_hom_f, instIsNormalMonoCategory, g_shortComplexTruncLEX₃ToTruncGE_assoc, HomologicalComplex₂.flipFunctor_map_f_f, shortComplexTruncLE_X₃_isSupportedOutside, biprod_inl_desc_f_assoc, CategoryTheory.instPreservesZeroMorphismsHomologicalComplexMapHomologicalComplex, exact_iff_degreewise_exact, HomologicalComplex₂.total.map_id, HomologicalComplex₂.totalFunctor_map, instPreservesZeroMorphismsOpcyclesFunctor, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_toGradedObject, HomologicalComplex₂.ιTotal_map_assoc, HomologicalComplex₂.ι_totalShift₁Iso_hom_f, ComplexShape.Embedding.instPreservesZeroMorphismsHomologicalComplexRestrictionFunctor, HomologicalComplex₂.instFaithfulGradedObjectProdToGradedObjectFunctor, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_d_f, HomologicalComplex₂.ιTotal_totalFlipIso_f_inv
instInhabitedHom 📖	CompOp	—
instInhabitedOfHasZeroObject 📖	CompOp	—
instZeroHom 📖	CompOp	8 math math: CategoryTheory.Abelian.LeftResolution.chainComplexMap_zero, ComplexShape.Embedding.AreComplementary.hom_ext, zero_f, cyclesMap_zero, homologyMap_zero, extendMap_zero, opcyclesMap_zero, ComplexShape.Embedding.AreComplementary.hom_ext'
xNext 📖	CompOp	23 math math: dFrom_comp_xNextIsoSelf, dFrom_eq_zero, Hom.comm_from_apply, Homotopy.mkInductiveAux₃, Hom.next_eq, Hom.sqFrom_comp, dTo_comp_dFrom, Homotopy.mkCoinductiveAux₂_add_one, Homotopy.mkCoinductiveAux₂_zero, kernel_from_eq_kernel, Homotopy.mkCoinductiveAux₃, dNext_eq_dFrom_fromNext, Hom.sqFrom_left, Hom.comm_from, Hom.sqFrom_right, Hom.comm_from_assoc, dFrom_comp_xNextIso_assoc, dFrom_eq, dFrom_comp_xNextIso, Homotopy.mkInductiveAux₂_zero, dFrom_comp_xNextIsoSelf_assoc, Homotopy.mkInductiveAux₂_add_one, Hom.sqFrom_id
xNextIso 📖	CompOp	9 math math: Homotopy.mkInductiveAux₃, Hom.next_eq, Homotopy.mkCoinductiveAux₂_add_one, Homotopy.mkCoinductiveAux₂_zero, Homotopy.mkCoinductiveAux₃, dFrom_comp_xNextIso_assoc, dFrom_eq, dFrom_comp_xNextIso, Homotopy.mkInductiveAux₂_add_one
xNextIsoSelf 📖	CompOp	2 math math: dFrom_comp_xNextIsoSelf, dFrom_comp_xNextIsoSelf_assoc
xPrev 📖	CompOp	21 math math: Homotopy.mkInductiveAux₃, dTo_eq_zero, Hom.comm_to_apply, xPrevIsoSelf_comp_dTo, dTo_eq, prevD_eq_toPrev_dTo, dTo_comp_dFrom, xPrevIso_comp_dTo, Hom.comm_to, Homotopy.mkCoinductiveAux₂_add_one, xPrevIso_comp_dTo_assoc, Homotopy.mkCoinductiveAux₂_zero, xPrevIsoSelf_comp_dTo_assoc, Homotopy.mkCoinductiveAux₃, image_to_eq_image, Hom.sqTo_right, Hom.sqTo_left, Hom.comm_to_assoc, Homotopy.mkInductiveAux₂_zero, Hom.prev_eq, Homotopy.mkInductiveAux₂_add_one
xPrevIso 📖	CompOp	9 math math: Homotopy.mkInductiveAux₃, dTo_eq, xPrevIso_comp_dTo, Homotopy.mkCoinductiveAux₂_add_one, xPrevIso_comp_dTo_assoc, Homotopy.mkCoinductiveAux₃, Homotopy.mkInductiveAux₂_zero, Hom.prev_eq, Homotopy.mkInductiveAux₂_add_one
xPrevIsoSelf 📖	CompOp	2 math math: xPrevIsoSelf_comp_dTo, xPrevIsoSelf_comp_dTo_assoc
zero 📖	CompOp	1 math math: isZero_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
XIsoOfEq_hom_comp_XIsoOfEq_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom XIsoOfEq	—	CategoryTheory.eqToHom_trans
XIsoOfEq_hom_comp_XIsoOfEq_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom XIsoOfEq	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' XIsoOfEq_hom_comp_XIsoOfEq_hom
XIsoOfEq_hom_comp_XIsoOfEq_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom XIsoOfEq CategoryTheory.Iso.inv	—	CategoryTheory.eqToHom_trans
XIsoOfEq_hom_comp_XIsoOfEq_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom XIsoOfEq CategoryTheory.Iso.inv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' XIsoOfEq_hom_comp_XIsoOfEq_inv
XIsoOfEq_hom_comp_d 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom XIsoOfEq d	—	CategoryTheory.Category.id_comp
XIsoOfEq_hom_comp_d_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.hom XIsoOfEq d	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' XIsoOfEq_hom_comp_d
XIsoOfEq_hom_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X Hom.f CategoryTheory.Iso.hom XIsoOfEq	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
XIsoOfEq_hom_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X Hom.f CategoryTheory.Iso.hom XIsoOfEq	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' XIsoOfEq_hom_naturality
XIsoOfEq_inv_comp_XIsoOfEq_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.inv XIsoOfEq CategoryTheory.Iso.hom	—	CategoryTheory.eqToHom_trans
XIsoOfEq_inv_comp_XIsoOfEq_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.inv XIsoOfEq CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' XIsoOfEq_inv_comp_XIsoOfEq_hom
XIsoOfEq_inv_comp_XIsoOfEq_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.inv XIsoOfEq CategoryTheory.Iso.hom	—	CategoryTheory.eqToHom_trans
XIsoOfEq_inv_comp_XIsoOfEq_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.inv XIsoOfEq CategoryTheory.Iso.hom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' XIsoOfEq_inv_comp_XIsoOfEq_inv
XIsoOfEq_inv_comp_d 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.inv XIsoOfEq d	—	CategoryTheory.Category.id_comp
XIsoOfEq_inv_comp_d_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.Iso.inv XIsoOfEq d	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' XIsoOfEq_inv_comp_d
XIsoOfEq_inv_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X Hom.f CategoryTheory.Iso.inv XIsoOfEq	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
XIsoOfEq_inv_naturality_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X Hom.f CategoryTheory.Iso.inv XIsoOfEq	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' XIsoOfEq_inv_naturality
XIsoOfEq_rfl 📖	mathematical	—	XIsoOfEq CategoryTheory.Iso.refl X	—	—
comp_f 📖	mathematical	—	Hom.f CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory X	—	—
comp_f_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X Hom.f HomologicalComplex instCategory	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_f
congr_hom 📖	mathematical	—	Hom.f	—	—
dFrom_comp_xNextIso 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X xNext dFrom CategoryTheory.Iso.hom xNextIso d	—	dFrom_eq CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
dFrom_comp_xNextIsoSelf 📖	mathematical	ComplexShape.Rel ComplexShape.next	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X xNext dFrom CategoryTheory.Iso.hom xNextIsoSelf Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	shape CategoryTheory.Limits.zero_comp
dFrom_comp_xNextIsoSelf_assoc 📖	mathematical	ComplexShape.Rel ComplexShape.next	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X xNext dFrom CategoryTheory.Iso.hom xNextIsoSelf Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' dFrom_comp_xNextIsoSelf
dFrom_comp_xNextIso_assoc 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X xNext dFrom CategoryTheory.Iso.hom xNextIso d	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' dFrom_comp_xNextIso
dFrom_eq 📖	mathematical	ComplexShape.Rel	dFrom CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X xNext d CategoryTheory.Iso.inv xNextIso	—	CategoryTheory.Category.comp_id ComplexShape.next_eq'
dFrom_eq_zero 📖	mathematical	ComplexShape.Rel ComplexShape.next	dFrom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X xNext CategoryTheory.Limits.HasZeroMorphisms.zero	—	shape
dTo_comp_dFrom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct xPrev X xNext dTo dFrom Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	d_comp_d
dTo_eq 📖	mathematical	ComplexShape.Rel	dTo CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct xPrev X CategoryTheory.Iso.hom xPrevIso d	—	CategoryTheory.Category.id_comp ComplexShape.prev_eq'
dTo_eq_zero 📖	mathematical	ComplexShape.Rel ComplexShape.prev	dTo Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct xPrev X CategoryTheory.Limits.HasZeroMorphisms.zero	—	shape
d_comp_XIsoOfEq_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X d CategoryTheory.Iso.hom XIsoOfEq	—	CategoryTheory.Category.comp_id
d_comp_XIsoOfEq_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X d CategoryTheory.Iso.hom XIsoOfEq	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d_comp_XIsoOfEq_hom
d_comp_XIsoOfEq_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X d CategoryTheory.Iso.inv XIsoOfEq	—	CategoryTheory.Category.comp_id
d_comp_XIsoOfEq_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X d CategoryTheory.Iso.inv XIsoOfEq	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d_comp_XIsoOfEq_inv
d_comp_d 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	d_comp_d' shape CategoryTheory.Limits.comp_zero CategoryTheory.Limits.zero_comp
d_comp_d' 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
d_comp_d_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d_comp_d
d_comp_eqToHom 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X d CategoryTheory.eqToHom ComplexShape.next_eq	—	ComplexShape.next_eq CategoryTheory.Category.comp_id
epi_of_epi_f 📖	mathematical	CategoryTheory.Epi X Hom.f	HomologicalComplex instCategory	—	hom_ext CategoryTheory.cancel_epi congr_hom
eqToHom_comp_d 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X CategoryTheory.eqToHom ComplexShape.prev_eq d	—	CategoryTheory.Category.id_comp ComplexShape.prev_eq
eqToHom_f 📖	mathematical	—	Hom.f CategoryTheory.eqToHom HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory X	—	—
eval_map 📖	mathematical	—	CategoryTheory.Functor.map HomologicalComplex instCategory eval Hom.f	—	—
eval_obj 📖	mathematical	—	CategoryTheory.Functor.obj HomologicalComplex instCategory eval X	—	—
ext 📖	—	X CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct d CategoryTheory.eqToHom	—	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
forgetEval_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app HomologicalComplex instCategory CategoryTheory.Functor.comp CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects forget CategoryTheory.GradedObject.eval eval CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category forgetEval CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct X	—	—
forgetEval_inv_app 📖	mathematical	—	CategoryTheory.NatTrans.app HomologicalComplex instCategory eval CategoryTheory.Functor.comp CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects forget CategoryTheory.GradedObject.eval CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category forgetEval CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct X	—	—
forget_map 📖	mathematical	—	CategoryTheory.Functor.map HomologicalComplex instCategory CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects forget Hom.f	—	—
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj HomologicalComplex instCategory CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects forget X	—	—
hom_ext 📖	—	Hom.f	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.f	—	hom_ext
hom_f_injective 📖	mathematical	—	Hom Hom.f	—	Hom.ext
id_f 📖	mathematical	—	Hom.f CategoryTheory.CategoryStruct.id HomologicalComplex CategoryTheory.Category.toCategoryStruct instCategory X	—	—
image_eq_image 📖	mathematical	ComplexShape.Rel	CategoryTheory.Limits.imageSubobject X d CategoryTheory.Limits.HasImages.has_image	—	CategoryTheory.Limits.HasImages.has_image ComplexShape.prev_eq eqToHom_comp_d CategoryTheory.Limits.imageSubobject_iso_comp CategoryTheory.instIsIsoEqToHom
image_to_eq_image 📖	mathematical	ComplexShape.Rel	CategoryTheory.Limits.imageSubobject xPrev X dTo CategoryTheory.Limits.HasImages.has_image d	—	CategoryTheory.Limits.HasImages.has_image dTo_eq CategoryTheory.Limits.imageSubobject_iso_comp CategoryTheory.Iso.isIso_hom
instFaithfulGradedObjectForget 📖	mathematical	—	CategoryTheory.Functor.Faithful HomologicalComplex instCategory CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects forget	—	hom_ext
instHasZeroObject 📖	mathematical	—	CategoryTheory.Limits.HasZeroObject HomologicalComplex instCategory	—	isZero_zero
instPreservesZeroMorphismsEval 📖	mathematical	—	CategoryTheory.Functor.PreservesZeroMorphisms HomologicalComplex instCategory instHasZeroMorphisms eval	—	—
isZero_zero 📖	mathematical	—	CategoryTheory.Limits.IsZero HomologicalComplex instCategory zero	—	hom_ext Unique.instSubsingleton
kernel_eq_kernel 📖	mathematical	ComplexShape.Rel	CategoryTheory.Limits.kernelSubobject X d CategoryTheory.Limits.HasKernels.has_limit	—	CategoryTheory.Limits.HasKernels.has_limit ComplexShape.next_eq d_comp_eqToHom CategoryTheory.Limits.kernelSubobject_comp_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.instIsIsoEqToHom
kernel_from_eq_kernel 📖	mathematical	ComplexShape.Rel	CategoryTheory.Limits.kernelSubobject X xNext dFrom CategoryTheory.Limits.HasKernels.has_limit d	—	CategoryTheory.Limits.HasKernels.has_limit dFrom_eq CategoryTheory.Limits.kernelSubobject_comp_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso CategoryTheory.Iso.isIso_inv
mono_of_mono_f 📖	mathematical	CategoryTheory.Mono X Hom.f	HomologicalComplex instCategory	—	hom_ext CategoryTheory.cancel_mono congr_hom
shape 📖	mathematical	ComplexShape.Rel	d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct X CategoryTheory.Limits.HasZeroMorphisms.zero	—	—
xPrevIsoSelf_comp_dTo 📖	mathematical	ComplexShape.Rel ComplexShape.prev	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X xPrev CategoryTheory.Iso.inv xPrevIsoSelf dTo Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	shape CategoryTheory.Limits.comp_zero
xPrevIsoSelf_comp_dTo_assoc 📖	mathematical	ComplexShape.Rel ComplexShape.prev	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X xPrev CategoryTheory.Iso.inv xPrevIsoSelf dTo Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' xPrevIsoSelf_comp_dTo
xPrevIso_comp_dTo 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X xPrev CategoryTheory.Iso.inv xPrevIso dTo d	—	dTo_eq CategoryTheory.Iso.inv_hom_id_assoc
xPrevIso_comp_dTo_assoc 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X xPrev CategoryTheory.Iso.inv xPrevIso dTo d	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' xPrevIso_comp_dTo
zero_f 📖	mathematical	—	Hom.f Quiver.Hom HomologicalComplex CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory instZeroHom X CategoryTheory.Limits.HasZeroMorphisms.zero	—	—

HomologicalComplex.Hom

Definitions

Name	Category	Theorems
f 📖	CompOp	591 math math: CategoryTheory.InjectiveResolution.Hom.hom'_f, HomologicalComplex.eqToHom_f, HomologicalComplex.extendSingleIso_inv_f, HomologicalComplex.opcyclesMap_comp_descOpcycles_assoc, HomologicalComplex.restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv, HomologicalComplex.evalCompCoyonedaCorepresentableByDoubleId_homEquiv_apply, AlgebraicTopology.DoldKan.P_f_0_eq, HomologicalComplex.singleMapHomologicalComplex_hom_app_ne, ChainComplex.truncate_map_f, AlgebraicTopology.DoldKan.PInfty_f_add_QInfty_f, CategoryTheory.NatIso.mapHomologicalComplex_inv_app_f, ComplexShape.Embedding.isIso_liftExtend_f_iff, CategoryTheory.Functor.mapHomologicalComplexIdIso_hom_app_f, CategoryTheory.InjectiveResolution.extMk_comp_mk₀, HomologicalComplex₂.totalFlipIso_hom_f_D₁, HomologicalComplex.singleMapHomologicalComplex_hom_app_self, AlgebraicTopology.DoldKan.σ_comp_PInfty_assoc, CochainComplex.mappingCone.inr_f_d_assoc, HomologicalComplex.liftCycles_comp_cyclesMap, CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_map_f_f, comm_from_apply, prevD_comp_left, AlgebraicTopology.DoldKan.HigherFacesVanish.inclusionOfMooreComplexMap, groupHomology.chainsMap_f_3_comp_chainsIso₃_apply, CategoryTheory.InjectiveResolution.ι'_f_zero, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_map_f_f, CochainComplex.augmentTruncate_inv_f_zero, CochainComplex.mappingCone.inr_f_fst_v, HomologicalComplex.biprod_inr_desc_f, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.map_f_f, ChainComplex.mkHom_f_0, HomologicalComplex.biprod_lift_fst_f_assoc, AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_inv_f, Homotopy.nullHomotopicMap_comp, CategoryTheory.ProjectiveResolution.lift_commutes_zero_assoc, HomologicalComplex.homotopyCofiber.inrCompHomotopy_hom_desc_hom_assoc, AlgebraicTopology.DoldKan.HigherFacesVanish.of_P, SimplicialObject.Splitting.PInfty_comp_πSummand_id, HomologicalComplex₂.comm_f, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso_inv_app_f_f, comm_to_apply, HomologicalComplex.inl_biprodXIso_inv_assoc, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_assoc, HomologicalComplex.biprod_inr_snd_f_assoc, CategoryTheory.Functor.mapHomologicalComplex_map_f, HomologicalComplex.biprod_inl_snd_f_assoc, Homotopy.nullHomotopicMap_f_eq_zero, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_succ, CochainComplex.mappingCone.d_snd_v, HomologicalComplex.eval_map, HomologicalComplex.to_single_hom_ext_iff, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_p_f, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂, HomologicalComplex.biprodXIso_hom_fst, HomologicalComplex₂.d_f_comp_d_f, HomologicalComplex.add_f_apply, HomologicalComplex.extend_op_d_assoc, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.comp_p_d, CochainComplex.HomComplex.Cochain.ofHom_v_comp_d, HomologicalComplex.unopInverse_map, next_eq, CategoryTheory.NatTrans.mapHomologicalComplex_app_f, HomologicalComplex.homotopyCofiber.desc_f', CategoryTheory.InjectiveResolution.desc_commutes_zero_assoc, HomologicalComplex.biprod_lift_fst_f, HomologicalComplex.forget_map, HomologicalComplex₂.ιTotalOrZero_map_assoc, CochainComplex.ι_mapBifunctorShift₂Iso_hom_f_assoc, HomologicalComplex₂.ιTotal_map, HomologicalComplex₂.ι_totalShift₁Iso_hom_f_assoc, CochainComplex.mappingCone.inr_f_d, groupHomology.chainsMap_id_f_map_mono, HomologicalComplex₂.ιTotal_totalFlipIso_f_inv_assoc, CochainComplex.fromSingle₀Equiv_apply_coe, HomologicalComplex.instEpiFπTruncGE, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_apply, CochainComplex.mappingCone.inr_f_descShortComplex_f_assoc, HomologicalComplex.shortComplexFunctor'_map_τ₂, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃_apply, HomologicalComplex.XIsoOfEq_inv_naturality_assoc, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_f, Homotopy.nullHomotopicMap'_f_eq_zero, CochainComplex.mappingCone.lift_f_fst_v, CochainComplex.mappingCone.inl_v_triangle_mor₃_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_p, AlgebraicTopology.DoldKan.PInfty_f_naturality_assoc, HomologicalComplex.mapBifunctorMapHomotopy.comm₁, HomologicalComplex₂.ι_totalShift₁Iso_inv_f, HomologicalComplex.extendSingleIso_inv_f_assoc, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comm_f_assoc, CategoryTheory.Limits.FormalCoproduct.cochainComplexFunctor_map_f, HomologicalComplex.XIsoOfEq_inv_naturality, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_p_f, AlgebraicTopology.DoldKan.comp_P_eq_self_iff, CochainComplex.mappingCone.id_X, groupHomology.chainsMap_f_3_comp_chainsIso₃, HomologicalComplex.instEpiFOfHasFiniteColimits, HomologicalComplex.instIsIsoFRestrictionToTruncGE'OfIsStrictlySupported, AlgebraicTopology.AlternatingFaceMapComplex.map_f, CochainComplex.HomComplex.Cochain.fromSingleMk_postcomp, HomologicalComplex.sub_f_apply, CochainComplex.mappingCone.d_snd_v'_assoc, AlgebraicTopology.DoldKan.QInfty_f, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁_assoc, HomologicalComplex₂.flipEquivalenceUnitIso_hom_app_f_f, CochainComplex.shiftFunctorZero_inv_app_f, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comp_d_assoc, AlgebraicTopology.DoldKan.PInfty_f_comp_QInfty_f_assoc, ChainComplex.toSingle₀Equiv_apply_coe, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self_assoc, HomologicalComplex.extendMap_f, HomologicalComplex₂.ι_totalShift₂Iso_inv_f_assoc, AlgebraicTopology.alternatingFaceMapComplex_map_f, AlgebraicTopology.DoldKan.P_f_idem_assoc, HomologicalComplex₂.d_comm, HomologicalComplex.extend.mapX_some, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroZero_assoc, ChainComplex.mkHom_f_1, HomologicalComplex.inr_biprodXIso_inv, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.comp_p_d_assoc, HomologicalComplex.homotopyCofiber.inrCompHomotopy_hom_desc_hom, HomologicalComplex₂.d_f_comp_d_f_assoc, isoOfComponents_inv_f, ChainComplex.truncateAugment_inv_f, AlgebraicTopology.DoldKan.QInfty_f_0, CategoryTheory.InjectiveResolution.ι_f_succ, HomologicalComplex.from_single_hom_ext_iff, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, HomologicalComplex.mkHomFromDouble_f₀, Homotopy.nullHomotopicMap'_comp, HomologicalComplex.instMonoFιTruncLE, HomologicalComplex₂.total.mapAux.d₁_mapMap, CochainComplex.mappingCone.lift_f_fst_v_assoc, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_hom_app_f_f, CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d_assoc, groupHomology.chainsMap_f_single, HomologicalComplex₂.d₁_eq, groupCohomology.cochainsMap_f_map_epi, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_map_f_f, AlgebraicTopology.DoldKan.map_Hσ, HomologicalComplex.instMonoFTruncLE'ToRestriction, HomologicalComplex.biprod_inr_snd_f, HomologicalComplex.id_f, HomologicalComplex.singleMapHomologicalComplex_inv_app_self, HomologicalComplex.restrictionMap_f'_assoc, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_1, HomologicalComplex.extendSingleIso_hom_f_assoc, AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_hom_f, AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_f, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app_f_f, CategoryTheory.ProjectiveResolution.mk₀_comp_extMk, CochainComplex.single₀_map_f_zero, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq_zero, CategoryTheory.ProjectiveResolution.Hom.hom'_f_assoc, CochainComplex.mappingCone.ext_from_iff, ChainComplex.augmentTruncate_inv_f_succ, HomologicalComplex.units_smul_f_apply, HomologicalComplex.p_opcyclesMap, AlgebraicTopology.DoldKan.PInfty_comp_map_mono_eq_zero, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero'_assoc, CategoryTheory.NatIso.mapHomologicalComplex_hom_app_f, SimplicialObject.Splitting.cofan_inj_comp_PInfty_eq_zero, groupHomology.chainsMap_f_map_epi, Homotopy.nullHomotopicMap_f, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_zero, CochainComplex.HomComplex.Cochain.ofHom_v, HomologicalComplex.opFunctor_map_f, CochainComplex.mappingCone.inr_f_snd_v, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map_f_f, CategoryTheory.ProjectiveResolution.π'_f_zero_assoc, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_p_f, HomologicalComplex.truncLE'Map_f_eq_cyclesMap, CategoryTheory.ProjectiveResolution.π_f_succ, HomologicalComplex₂.totalAux.d₁_eq, ComplexShape.Embedding.epi_liftExtend_f_iff, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_inv_f_f, AlgebraicTopology.DoldKan.P_f_idem, CochainComplex.shiftFunctor_map_f', HomologicalComplex₂.total.mapAux.d₂_mapMap_assoc, CochainComplex.ConnectData.restrictionLEIso_inv_f, HomologicalComplex.ι_mapBifunctorFlipIso_inv_assoc, CochainComplex.mappingCone.inr_f_desc_f, HomologicalComplex.zsmul_f_apply, HomologicalComplex.cyclesMap_i_assoc, CategoryTheory.ProjectiveResolution.Hom.hom'_f, HomologicalComplex.biprod_lift_snd_f, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero', AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, isoOfComponents_hom_f, HomologicalComplex.biprod_inl_fst_f_assoc, CategoryTheory.ProjectiveResolution.Hom.hom_f_zero_comp_π_f_zero_assoc, CochainComplex.mappingCone.inl_v_desc_f_assoc, HomologicalComplex.nsmul_f_apply, CochainComplex.shiftFunctorAdd'_inv_app_f', Rep.FiniteCyclicGroup.chainComplexFunctor_map_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_d_f, CategoryTheory.Functor.mapBifunctorHomologicalComplex_map_app_f_f, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_0, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_inv_f_f, HomologicalComplex.inl_biprodXIso_inv, AlgebraicTopology.DoldKan.QInfty_f_naturality_assoc, CategoryTheory.Functor.mapCochainComplexShiftIso_inv_app_f, CochainComplex.shiftFunctorAdd'_inv_app_f, CategoryTheory.InjectiveResolution.ι_f_zero_comp_complex_d, HomologicalComplex.cylinder.inrX_π_assoc, groupHomology.chainsMap_id_f_map_epi, CochainComplex.truncateAugment_inv_f, HomologicalComplex.homotopyCofiber.inlX_desc_f_assoc, HomologicalComplex.biprod_inl_fst_f, SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty, CochainComplex.mappingCone.inl_v_triangle_mor₃_f_assoc, AlgebraicTopology.DoldKan.map_PInfty_f, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, groupCohomology.cochainsMap_id_f_map_mono, HomologicalComplex.shortComplexFunctor_map_τ₁, HomologicalComplex.comp_f, HomologicalComplex.cylinder.inlX_π, SimplicialObject.Split.nondegComplexFunctor_map_f, HomologicalComplex.biprod_inr_fst_f, CochainComplex.mappingCone.inr_f_triangle_mor₃_f, CategoryTheory.Functor.mapHomologicalComplexIdIso_inv_app_f, HomologicalComplex.homotopyCofiber.inrX_desc_f, Homotopy.compRight_hom, AlgebraicTopology.DoldKan.Hσ_eq_zero, CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_hom_f_f, HomologicalComplex.biprodXIso_hom_fst_assoc, CochainComplex.shiftFunctorZero'_hom_app_f, HomologicalComplex₂.flipEquivalenceUnitIso_inv_app_f_f, CategoryTheory.ProjectiveResolution.lift_commutes_zero, HomologicalComplex.cylinder.inlX_π_assoc, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_apply, HomologicalComplex.shortComplexFunctor_map_τ₃, CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero_comp, HomologicalComplex₂.ι_totalShift₁Iso_inv_f_assoc, HomologicalComplex₂.ιTotal_totalFlipIso_f_hom_assoc, HomologicalComplex.zero_f, CochainComplex.mkHom_f_succ_succ, CochainComplex.mappingCone.d_snd_v_assoc, AlgebraicTopology.DoldKan.PInfty_f, CochainComplex.shiftFunctor_map_f, HomologicalComplex.isIso_truncLE'ToRestriction, CochainComplex.mappingCone.d_snd_v', HomologicalComplex.extend_op_d, ComplexShape.Embedding.mono_liftExtend_f_iff, AlgebraicTopology.DoldKan.Γ₀_map_app, comm_to, AlgebraicTopology.DoldKan.Q_f_0_eq, HomologicalComplex.complexOfFunctorsToFunctorToComplex_map_app_f, CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero, HomologicalComplex.mkHomToSingle_f, HomologicalComplex.biprodXIso_hom_snd, HomologicalComplex.stupidTruncMap_stupidTruncXIso_hom_assoc, Homotopy.nullHomotopicMap_f_of_not_rel_right, CochainComplex.mappingCone.inr_f_descCochain_v_assoc, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_apply, AlgebraicTopology.DoldKan.QInfty_f_naturality, CochainComplex.HomComplex.Cocycle.homOf_f, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_idem, CochainComplex.homOfDegreewiseSplit_f, CochainComplex.shiftFunctorAdd_inv_app_f, CochainComplex.truncate_map_f, HomologicalComplex₂.ι_totalShift₂Iso_hom_f_assoc, ChainComplex.augmentTruncate_hom_f_succ, groupHomology.chainsMap_id_f_hom_eq_mapRange, HomologicalComplex.XIsoOfEq_hom_naturality_assoc, HomologicalComplex.biprodXIso_hom_snd_assoc, CategoryTheory.ProjectiveResolution.π'_f_zero, HomologicalComplex₂.totalFlipIso_hom_f_D₂, HomologicalComplex.opcyclesMap_comp_descOpcycles, dNext_comp_left, AlgebraicTopology.DoldKan.P_f_naturality_assoc, AlgebraicTopology.DoldKan.map_P, HomologicalComplex.homotopyCofiber.inlX_d, CategoryTheory.Idempotents.DoldKan.η_inv_app_f, Homotopy.comp_nullHomotopicMap, groupHomology.chainsMap_f_map_mono, HomologicalComplex.single_map_f_self_assoc, HomologicalComplex.ι_mapBifunctorMap_assoc, HomologicalComplex.homologicalComplexToDGO_map_f, CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_inv_app_f, AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self, AlgebraicTopology.DoldKan.degeneracy_comp_PInfty_assoc, CochainComplex.ConnectData.restrictionLEIso_hom_f, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comp_d, groupHomology.chainsMap_f_1_comp_chainsIso₁_assoc, CochainComplex.mappingCone.inr_f_descCochain_v, CochainComplex.ι_mapBifunctorShift₂Iso_hom_f, groupHomology.lsingle_comp_chainsMap_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_p, HomologicalComplex₂.comm_f_assoc, HomologicalComplex.cylinder.inrX_π, HomologicalComplex₂.totalFlipIso_hom_f_D₁_assoc, Homotopy.comp_nullHomotopicMap', groupCohomology.cochainsMap_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_map_f_f, AlgebraicTopology.DoldKan.Γ₀.map_app, CategoryTheory.InjectiveResolution.Hom.ι_f_zero_comp_hom_f_zero, HomologicalComplex.cylinder.πCompι₀Homotopy.inrX_nullHomotopy_f, CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne_comp_assoc, groupHomology.chainsMap_f_3_comp_chainsIso₃_assoc, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_map_f_f, HomologicalComplex.smul_f_apply, CochainComplex.cm5b.instMonoFIntI, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₂, groupHomology.chainsMap_f_0_comp_chainsIso₀_assoc, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self_assoc, AlgebraicTopology.DoldKan.Q_is_eventually_constant, AlgebraicTopology.DoldKan.Q_f_naturality_assoc, Homotopy.compLeftId_hom, HomologicalComplex.zero_f_apply, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_P_eq_self, HomologicalComplex.homotopyCofiber.inlX_d'_assoc, CochainComplex.mappingCone.inr_f_fst_v_assoc, CategoryTheory.InjectiveResolution.ι'_f_zero_assoc, CochainComplex.mappingCone.inl_v_d_assoc, CochainComplex.shiftFunctorZero'_inv_app_f, CochainComplex.mappingCone.inl_v_desc_f, CochainComplex.mappingCone.cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v, SimplicialObject.Splitting.PInfty_comp_πSummand_id_assoc, HomologicalComplex.inr_biprodXIso_inv_assoc, HomologicalComplex.singleMapHomologicalComplex_inv_app_ne, HomologicalComplex.dgoToHomologicalComplex_map_f, ChainComplex.truncateAugment_hom_f, HomologicalComplex.shortComplexFunctor'_map_τ₁, HomologicalComplex.mkHomFromDouble_f₁, HomologicalComplex.liftCycles_comp_cyclesMap_assoc, ext_iff, HomologicalComplex.instMonoFOfHasFiniteLimits, AlgebraicTopology.DoldKan.natTransPInfty_f_app, HomologicalComplex.single_map_f_self, ChainComplex.fromSingle₀Equiv_symm_apply_f_zero, AlgebraicTopology.NormalizedMooreComplex.map_f, Homotopy.compRightId_hom, HomologicalComplex.homotopyCofiber.d_sndX, CategoryTheory.InjectiveResolution.Hom.hom'_f_assoc, CochainComplex.toSingle₀Equiv_symm_apply_f_succ, CochainComplex.mappingCone.inl_v_descShortComplex_f_assoc, ChainComplex.augmentTruncate_hom_f_zero, HomologicalComplex₂.ιTotalOrZero_map, HomologicalComplex.truncGE'Map_f_eq_opcyclesMap, groupHomology.chainsMap_f_1_comp_chainsIso₁, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_naturality, ChainComplex.toSingle₀Equiv_symm_apply_f_zero, groupHomology.chainsMap_f_2_comp_chainsIso₂, AlgebraicTopology.DoldKan.MorphComponents.id_a, Homotopy.nullHomotopicMap'_f_of_not_rel_left, HomologicalComplex.coconeOfHasColimitEval_ι_app_f, HomologicalComplex.homotopyCofiber.inlX_d', AlgebraicTopology.DoldKan.PInfty_f_0, Homotopy.nullHomotopicMap_f_of_not_rel_left, ChainComplex.ofHom_f, groupCohomology.cochainsMap_f_map_mono, AlgebraicTopology.DoldKan.PInfty_f_naturality, HomologicalComplex₂.shape_f, AlgebraicTopology.DoldKan.PInfty_f_idem_assoc, ComplexShape.Embedding.liftExtend_f, CochainComplex.cm5b.i_f_comp, CochainComplex.mappingCone.decomp_to, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroOne_assoc, ComplexShape.Embedding.liftExtend.f_eq, groupCohomology.cochainsMap_id_f_map_epi, HomologicalComplex.dgoEquivHomologicalComplexCounitIso_hom_app_f, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_idem_assoc, CochainComplex.mappingCone.lift_desc_f, groupHomology.chainsMap_f_hom, CochainComplex.ConnectData.restrictionGEIso_inv_f, AlgebraicTopology.DoldKan.P_is_eventually_constant, AlgebraicTopology.DoldKan.map_Q, HomologicalComplex₂.ofGradedObject_d_f, HomologicalComplex₂.ι_totalShift₂Iso_inv_f, AlgebraicTopology.DoldKan.PInfty_f_idem, AlgebraicTopology.DoldKan.N₂_obj_p_f, HomologicalComplex.hom_f_injective, sqTo_right, CochainComplex.mappingCone.desc_f, CategoryTheory.ProjectiveResolution.liftHomotopyZeroZero_comp_assoc, HomologicalComplex.to_double_hom_ext_iff, AlgebraicTopology.DoldKan.σ_comp_PInfty, CochainComplex.mkHom_f_1, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_hom_f_f, CochainComplex.augmentTruncate_inv_f_succ, CochainComplex.mappingCone.inl_v_d, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso_hom_app_f_f, sqFrom_left, CochainComplex.shiftFunctorZero_hom_app_f, CategoryTheory.ProjectiveResolution.Hom.hom_f_zero_comp_π_f_zero, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀, CochainComplex.mappingCone.inr_f_snd_v_assoc, HomologicalComplex.mapBifunctorMapHomotopy.comm₁_aux, comm_assoc, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_d_f, CochainComplex.mkHom_f_0, HomologicalComplex.instIsIsoFTruncLE'ToRestrictionOfIsStrictlySupported, HomologicalComplex₂.total.mapAux.d₂_mapMap, groupCohomology.cochainsMap_f_3_comp_cochainsIso₃, HomologicalComplex.restrictionMap_f', SimplicialObject.Splitting.πSummand_comp_cofan_inj_id_comp_PInfty_eq_PInfty_assoc, HomologicalComplex₂.ιTotal_totalFlipIso_f_hom, ChainComplex.fromSingle₀Equiv_apply, CategoryTheory.InjectiveResolution.desc_commutes_zero, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, CochainComplex.shiftFunctorAdd'_hom_app_f', Homotopy.comm, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply, comm_from, CochainComplex.augmentTruncate_hom_f_succ, groupCohomology.cochainsMap_f_hom, HomologicalComplex.congr_hom, HomologicalComplex₂.flip_X_d, CochainComplex.cm5b.i_f_comp_assoc, Homotopy.comp_hom, HomologicalComplex.biprod_inl_desc_f, CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_hom_app_f, HomologicalComplex.coneOfHasLimitEval_π_app_f, HomologicalComplex.restrictionMap_f, CochainComplex.ι_mapBifunctorShift₁Iso_hom_f_assoc, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroOne, CategoryTheory.ProjectiveResolution.exact₀, CochainComplex.mappingCone.mapHomologicalComplexXIso'_hom, HomologicalComplex.homotopyCofiber.inlX_d_assoc, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_inv_f_f, CochainComplex.HomComplex.Cochain.d_comp_ofHom_v, AlgebraicTopology.DoldKan.karoubi_PInfty_f, CochainComplex.fromSingle₀Equiv_symm_apply_f_zero, HomologicalComplex.homotopyCofiber.desc_f, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_X_p, ChainComplex.augmentTruncate_inv_f_zero, CochainComplex.shiftFunctorAdd_hom_app_f, HomologicalComplex.ι_mapBifunctorFlipIso_hom, CochainComplex.truncateAugment_hom_f, HomologicalComplex.mkHomFromDouble_f₀_assoc, SimplicialObject.Splitting.comp_PInfty_eq_zero_iff, HomologicalComplex.biprod_inr_desc_f_assoc, CategoryTheory.Idempotents.DoldKan.Γ_map_app, HomologicalComplex.evalCompCoyonedaCorepresentableBySingle_homEquiv_apply, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, CochainComplex.ofHom_f, HomologicalComplex.shortComplexFunctor'_map_τ₃, CochainComplex.mappingCone.inl_v_descShortComplex_f, HomologicalComplex₂.flipEquivalenceCounitIso_inv_app_f_f, AlgebraicTopology.DoldKan.degeneracy_comp_PInfty, CochainComplex.mappingCone.inr_f_descShortComplex_f, HomologicalComplex.asFunctor_map_f, comm_from_assoc, CochainComplex.toSingle₀Equiv_apply, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁_assoc, CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne_comp, ComplexShape.Embedding.homRestrict_f, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comm_f, HomologicalComplex.mkHomFromSingle_f, HomologicalComplex.shortComplexFunctor_map_τ₂, CochainComplex.shiftFunctorAdd'_hom_app_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_inv_app_f_f, CochainComplex.mappingCone.inr_f_triangle_mor₃_f_assoc, Homotopy.compLeft_hom, HomologicalComplex.isIso_restrictionToTruncGE', HomologicalComplex.truncLE'Map_f_eq, prevD_comp_right, comm', HomologicalComplex₂.ι_totalShift₂Iso_hom_f, AlgebraicTopology.DoldKan.HigherFacesVanish.comp_Hσ_eq, CategoryTheory.InjectiveResolution.Hom.ι_f_zero_comp_hom_f_zero_assoc, groupHomology.chainsMap_f_2_comp_chainsIso₂_assoc, AlgebraicTopology.DoldKan.QInfty_f_idem_assoc, CochainComplex.shiftFunctorComm_hom_app_f, ComplexShape.Embedding.homRestrict.f_eq, AlgebraicTopology.DoldKan.QInfty_f_idem, CategoryTheory.Abelian.DoldKan.comparisonN_hom_app_f, CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_f, isoApp_inv, HomologicalComplex₂.total.mapAux.d₁_mapMap_assoc, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f, AlgebraicTopology.DoldKan.PInfty_f_comp_QInfty_f, CategoryTheory.InjectiveResolution.instMonoFNatι, CategoryTheory.InjectiveResolution.comp_descHomotopyZeroZero, Homotopy.nullHomotopicMap'_f, CategoryTheory.Functor.mapCochainComplexShiftIso_hom_app_f, groupCohomology.cochainsMap_f_2_comp_cochainsIso₂_assoc, CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles_assoc, Homotopy.nullHomotopicMap'_f_of_not_rel_right, dNext_comp_right, HomologicalComplex.homotopyCofiber.inlX_desc_f, HomologicalComplex₂.d₁_eq', HomologicalComplex.cyclesMap_i, AlgebraicTopology.DoldKan.Γ₂_map_f_app, AlgebraicTopology.DoldKan.decomposition_Q, HomologicalComplex.extendMap_f_eq_zero, CategoryTheory.InjectiveResolution.exact₀, CategoryTheory.Abelian.LeftResolution.chainComplexMap_f_succ_succ, AlgebraicTopology.DoldKan.σ_comp_P_eq_zero, HomologicalComplex₂.toGradedObjectMap_apply, groupHomology.chainsMap_f_0_comp_chainsIso₀_apply, CochainComplex.mappingCone.lift_f_snd_v, HomologicalComplex₂.flip_d_f, HomologicalComplex.truncGE'Map_f_eq, HomologicalComplex.hom_ext_iff, AlgebraicTopology.DoldKan.Q_f_idem_assoc, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_d_f, AlgebraicTopology.DoldKan.Q_f_naturality, groupHomology.lsingle_comp_chainsMap_f_assoc, ChainComplex.mkHom_f_succ_succ, AlgebraicTopology.DoldKan.QInfty_f_comp_PInfty_f_assoc, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_map_f_f, HomologicalComplex.restrictionToTruncGE'_f_eq_iso_hom_iso_inv, AlgebraicTopology.inclusionOfMooreComplexMap_f, HomologicalComplex.stupidTruncMap_stupidTruncXIso_hom, groupCohomology.cochainsMap_id_f_hom_eq_compLeft, HomologicalComplex.biprod_lift_snd_f_assoc, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_inv_app_f_f, HomologicalComplex.biprod_inr_fst_f_assoc, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f, HomologicalComplex.homotopyCofiber.d_sndX_assoc, CategoryTheory.Functor.mapBifunctorHomologicalComplexObj_obj_d_f, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁, groupCohomology.cochainsMap_f_1_comp_cochainsIso₁, HomologicalComplex.neg_f_apply, CategoryTheory.ProjectiveResolution.instEpiFNatπ, CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero_assoc, HomologicalComplex.unopFunctor_map_f, comm, groupCohomology.cochainsMap_f_0_comp_cochainsIso₀_assoc, HomologicalComplex₂.flipEquivalenceCounitIso_hom_app_f_f, AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty_assoc, AlgebraicTopology.DoldKan.N₂_map_f_f, CochainComplex.HomComplex.Cocycle.fromSingleMk_postcomp, HomologicalComplex₂.d_comm_assoc, AlgebraicTopology.DoldKan.P_f_naturality, CochainComplex.mappingCone.lift_f, HomologicalComplex.XIsoOfEq_hom_naturality, AlgebraicTopology.DoldKan.factors_normalizedMooreComplex_PInfty, HomologicalComplex₂.totalAux.d₁_eq', CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_hom_app_f_f, comm_to_assoc, HomologicalComplex.ι_mapBifunctorFlipIso_hom_assoc, CochainComplex.HomComplex.Cocycle.toSingleMk_precomp, HomologicalComplex.extendSingleIso_hom_f, HomologicalComplex.biprod_inl_snd_f, CochainComplex.toSingle₀Equiv_symm_apply_f_zero, CochainComplex.mappingConeHomOfDegreewiseSplitIso_hom_f, CochainComplex.augmentTruncate_hom_f_zero, HomologicalComplex.comp_f_assoc, ChainComplex.alternatingConst_map_f, ChainComplex.fromSingle₀Equiv_symm_apply_f_succ, AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_naturality_assoc, AlgebraicTopology.DoldKan.P_add_Q_f, HomologicalComplex.opInverse_map, HomologicalComplex₂.flipFunctor_map_f_f, AlgebraicTopology.DoldKan.HigherFacesVanish.induction, AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty, groupHomology.chainsMap_f_1_comp_chainsIso₁_apply, HomologicalComplex.biprod_inl_desc_f_assoc, isoApp_hom, CategoryTheory.Abelian.DoldKan.comparisonN_inv_app_f, ChainComplex.single₀_map_f_zero, HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₂_assoc, HomologicalComplex.dgoEquivHomologicalComplexCounitIso_inv_app_f, AlgebraicTopology.DoldKan.Γ₀'_map_f, CochainComplex.mappingCone.lift_f_snd_v_assoc, CochainComplex.mappingCone.mapHomologicalComplexXIso'_inv, HomologicalComplex.mkHomFromDouble_f₁_assoc, Rep.FiniteCyclicGroup.resolution.π_f, HomologicalComplex.from_double_hom_ext_iff, CochainComplex.mappingCone.inr_f_desc_f_assoc, fAddMonoidHom_apply, CochainComplex.HomComplex.Cochain.toSingleMk_precomp, HomologicalComplex.ι_mapBifunctorMap, HomologicalComplex.homotopyCofiber.inr_f, HomologicalComplex.homotopyCofiber.inrX_desc_f_assoc, HomologicalComplex.extendMap_id_f, HomologicalComplex.p_opcyclesMap_assoc, CategoryTheory.Idempotents.DoldKan.η_hom_app_f, groupHomology.chainsMap_f_0_comp_chainsIso₀, HomologicalComplex₂.ιTotal_map_assoc, HomologicalComplex.ι_mapBifunctorFlipIso_inv, HomologicalComplex.cylinder.πCompι₀Homotopy.inlX_nullHomotopy_f, HomologicalComplex₂.totalFlipIso_hom_f_D₂_assoc, HomologicalComplex₂.ι_totalShift₁Iso_hom_f, HomologicalComplex.instEpiFRestrictionToTruncGE', Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, CategoryTheory.Functor.mapBifunctorHomologicalComplex_obj_obj_d_f, CochainComplex.ι_mapBifunctorShift₁Iso_hom_f, groupHomology.chainsMap_f, groupHomology.chainsMap_f_2_comp_chainsIso₂_apply, AlgebraicTopology.DoldKan.Q_f_idem, prev_eq, HomologicalComplex₂.ιTotal_totalFlipIso_f_inv, CochainComplex.ConnectData.restrictionGEIso_hom_f
isoApp 📖	CompOp	3 math math: isoOfComponents_app, isoApp_inv, isoApp_hom
isoOfComponents 📖	CompOp	3 math math: isoOfComponents_inv_f, isoOfComponents_app, isoOfComponents_hom_f
next 📖	CompOp	5 math math: comm_from_apply, next_eq, comm_from, sqFrom_right, comm_from_assoc
prev 📖	CompOp	5 math math: comm_to_apply, comm_to, sqTo_left, comm_to_assoc, prev_eq
sqFrom 📖	CompOp	4 math math: sqFrom_comp, sqFrom_left, sqFrom_right, sqFrom_id
sqTo 📖	CompOp	2 math math: sqTo_right, sqTo_left

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X f HomologicalComplex.d	—	comm' HomologicalComplex.shape CategoryTheory.Limits.comp_zero CategoryTheory.Limits.zero_comp
comm' 📖	mathematical	ComplexShape.Rel	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X f HomologicalComplex.d	—	—
comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X f HomologicalComplex.d	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm
comm_from 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X HomologicalComplex.xNext f HomologicalComplex.dFrom next	—	comm
comm_from_apply 📖	mathematical	—	DFunLike.coe HomologicalComplex.X HomologicalComplex.xNext CategoryTheory.ConcreteCategory.hom HomologicalComplex.dFrom f next	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise comm_from
comm_from_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X f HomologicalComplex.xNext HomologicalComplex.dFrom next	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm_from
comm_to 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.xPrev HomologicalComplex.X prev HomologicalComplex.dTo f	—	comm
comm_to_apply 📖	mathematical	—	DFunLike.coe HomologicalComplex.xPrev HomologicalComplex.X CategoryTheory.ConcreteCategory.hom HomologicalComplex.dTo prev f	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise comm_to
comm_to_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.xPrev prev HomologicalComplex.X HomologicalComplex.dTo f	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comm_to
ext 📖	—	f	—	—	—
ext_iff 📖	mathematical	—	f	—	ext
isIso_of_components 📖	mathematical	CategoryTheory.IsIso HomologicalComplex.X f	HomologicalComplex HomologicalComplex.instCategory	—	CategoryTheory.Iso.isIso_hom comm
isoApp_hom 📖	mathematical	—	CategoryTheory.Iso.hom HomologicalComplex.X isoApp f HomologicalComplex HomologicalComplex.instCategory	—	—
isoApp_inv 📖	mathematical	—	CategoryTheory.Iso.inv HomologicalComplex.X isoApp f HomologicalComplex HomologicalComplex.instCategory	—	—
isoOfComponents_app 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Iso.hom HomologicalComplex.d	isoApp isoOfComponents	—	CategoryTheory.Iso.ext
isoOfComponents_hom_f 📖	mathematical	—	f CategoryTheory.Iso.hom HomologicalComplex HomologicalComplex.instCategory isoOfComponents HomologicalComplex.X	—	—
isoOfComponents_inv_f 📖	mathematical	—	f CategoryTheory.Iso.inv HomologicalComplex HomologicalComplex.instCategory isoOfComponents HomologicalComplex.X	—	—
next_eq 📖	mathematical	ComplexShape.Rel	next CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.xNext HomologicalComplex.X CategoryTheory.Iso.hom HomologicalComplex.xNextIso f CategoryTheory.Iso.inv	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp ComplexShape.next_eq'
prev_eq 📖	mathematical	ComplexShape.Rel	prev CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.xPrev HomologicalComplex.X CategoryTheory.Iso.hom HomologicalComplex.xPrevIso f CategoryTheory.Iso.inv	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp ComplexShape.prev_eq'
sqFrom_comp 📖	mathematical	—	sqFrom CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory CategoryTheory.Arrow CategoryTheory.instCategoryArrow HomologicalComplex.X HomologicalComplex.xNext HomologicalComplex.dFrom	—	—
sqFrom_id 📖	mathematical	—	sqFrom CategoryTheory.CategoryStruct.id HomologicalComplex CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory CategoryTheory.Arrow CategoryTheory.instCategoryArrow HomologicalComplex.X HomologicalComplex.xNext HomologicalComplex.dFrom	—	—
sqFrom_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id HomologicalComplex.X HomologicalComplex.xNext HomologicalComplex.dFrom sqFrom f	—	—
sqFrom_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id HomologicalComplex.X HomologicalComplex.xNext HomologicalComplex.dFrom sqFrom next	—	—
sqTo_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left CategoryTheory.Functor.id HomologicalComplex.xPrev HomologicalComplex.X HomologicalComplex.dTo sqTo prev	—	—
sqTo_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right CategoryTheory.Functor.id HomologicalComplex.xPrev HomologicalComplex.X HomologicalComplex.dTo sqTo f	—	—

(root)

Definitions

Name	Category	Theorems
ChainComplex 📖	CompOp	207 math math: AlgebraicTopology.DoldKan.natTransPInfty_app, AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex, ChainComplex.truncate_map_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_d, AlgebraicTopology.DoldKan.N₁_map_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_X, AlgebraicTopology.DoldKan.HigherFacesVanish.inclusionOfMooreComplexMap, CategoryTheory.ProjectiveResolution.quasiIso, AlgebraicTopology.singularChainComplexFunctor_exactAt_of_totallyDisconnectedSpace, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_inv_app, AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_inv_f, CategoryTheory.ProjectiveResolution.lift_commutes_zero_assoc, AlgebraicTopology.DoldKan.identity_N₂, AlgebraicTopology.DoldKan.PInfty_comp_QInfty, CategoryTheory.Abelian.LeftResolution.chainComplexMap_zero, groupHomology.chainsMap_id, CategoryTheory.Abelian.LeftResolution.chainComplexMap_comp, CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π_assoc, CategoryTheory.Abelian.LeftResolution.chainComplexMap_id, AlgebraicTopology.DoldKan.PInfty_idem, CategoryTheory.Preadditive.DoldKan.equivalence_unitIso, AlgebraicTopology.DoldKan.instIsIsoFunctorSimplicialObjectKaroubiNatTrans, CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_succ, AlgebraicTopology.DoldKan.QInfty_idem, CochainComplex.ConnectData.map_comp_map, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_inv, CategoryTheory.Preadditive.DoldKan.equivalence_functor, CategoryTheory.ProjectiveResolution.self_π, AlgebraicTopology.alternatingFaceMapComplex_obj_d, CategoryTheory.Functor.mapProjectiveResolution_π, Rep.FiniteCyclicGroup.chainComplexFunctor_obj, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_p, AlgebraicTopology.DoldKan.instIsIsoFunctorKaroubiSimplicialObjectNatTrans, AlgebraicTopology.DoldKan.N₁_obj_p, CategoryTheory.Preadditive.DoldKan.equivalence_counitIso, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_p_f, AlgebraicTopology.DoldKan.QInfty_idem_assoc, ChainComplex.toSingle₀Equiv_apply_coe, AlgebraicTopology.alternatingFaceMapComplex_map_f, Rep.standardComplex.εToSingle₀_comp_eq, AlgebraicTopology.DoldKan.Γ₀'_obj, ChainComplex.exactAt_succ_single_obj, CategoryTheory.Idempotents.DoldKan.hε, ChainComplex.truncateAugment_inv_f, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyHomInvId, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, CategoryTheory.Idempotents.DoldKan.N₂_map_isoΓ₀_hom_app_f, CategoryTheory.ProjectiveResolution.Hom.hom_comp_π_assoc, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_map_f_f, AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans, AlgebraicTopology.DoldKan.Γ₀NondegComplexIso_hom_f, AlgebraicTopology.DoldKan.Γ₀_obj_map, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app_f_f, groupHomology.map_chainsFunctor_shortExact, AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty_assoc, CategoryTheory.Idempotents.DoldKan.equivalence_counitIso, AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_hom_app, CategoryTheory.Abelian.LeftResolution.chainComplexMap_comp_assoc, ChainComplex.augmentTruncate_inv_f_succ, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero'_assoc, AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_zero, CategoryTheory.ProjectiveResolution.homotopyEquiv_inv_π, CategoryTheory.ProjectiveResolution.of_def, CategoryTheory.ProjectiveResolution.π'_f_zero_assoc, CategoryTheory.ProjectiveResolution.π_f_succ, AlgebraicTopology.inclusionOfMooreComplex_app, AlgebraicTopology.DoldKan.Γ₂_obj_X_map, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_inv_f_f, AlgebraicTopology.DoldKan.PInfty_idem_assoc, groupHomology.chainsFunctor_obj, CategoryTheory.Idempotents.DoldKan.equivalence_inverse, CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero', AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, AlgebraicTopology.DoldKan.inclusionOfMooreComplexMap_comp_PInfty, CategoryTheory.ProjectiveResolution.Hom.hom_f_zero_comp_π_f_zero_assoc, Rep.FiniteCyclicGroup.chainComplexFunctor_map_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_d_f, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_hom_app, AlgebraicTopology.DoldKan.compatibility_N₂_N₁_karoubi, AlgebraicTopology.DoldKan.P_succ, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, groupHomology.chainsMap_id_comp, AlgebraicTopology.DoldKan.N₂Γ₂_compatible_with_N₁Γ₀, SimplicialObject.Split.nondegComplexFunctor_map_f, AlgebraicTopology.DoldKan.Γ₀'_map_F, AlgebraicTopology.normalizedMooreComplex_objD, CategoryTheory.ProjectiveResolution.lift_commutes_zero, AlgebraicTopology.DoldKan.QInfty_comp_PInfty, AlgebraicTopology.DoldKan.Q_idem, AlgebraicTopology.DoldKan.whiskerLeft_toKaroubi_N₂Γ₂_hom, AlgebraicTopology.normalizedMooreComplex_map, CategoryTheory.ProjectiveResolution.lift_commutes, AlgebraicTopology.DoldKan.Q_idem_assoc, AlgebraicTopology.DoldKan.Γ₀_map_app, CategoryTheory.ProjectiveResolution.homotopyEquiv_hom_π_assoc, CategoryTheory.Idempotents.DoldKan.N_obj, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_hom_app, CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero, CategoryTheory.ProjectiveResolution.Hom.hom_comp_π, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_X, ChainComplex.augmentTruncate_hom_f_succ, CategoryTheory.ProjectiveResolution.π'_f_zero, CategoryTheory.Idempotents.DoldKan.η_inv_app_f, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_inv_app, AlgebraicTopology.DoldKan.P_idem, groupHomology.chainsMap_comp, AlgebraicTopology.DoldKan.natTransP_app, SimplicialObject.Split.nondegComplexFunctor_obj, AlgebraicTopology.DoldKan.N₁_obj_X, AlgebraicTopology.map_alternatingFaceMapComplex, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_map_f_f, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap, AlgebraicTopology.DoldKan.Γ₀_obj_obj, CategoryTheory.Idempotents.DoldKan.Γ_obj_map, Rep.standardComplex.quasiIso_forget₂_εToSingle₀, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality_assoc, CategoryTheory.ProjectiveResolution.self_complex, ChainComplex.truncateAugment_hom_f, AlgebraicTopology.DoldKan.Q_succ, AlgebraicTopology.DoldKan.natTransPInfty_f_app, CategoryTheory.Idempotents.DoldKan.Γ_obj_obj, ChainComplex.fromSingle₀Equiv_symm_apply_f_zero, AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_inv_app, AlgebraicTopology.DoldKan.instMonoChainComplexNatInclusionOfMooreComplexMap, CategoryTheory.Abelian.DoldKan.equivalence_inverse, ChainComplex.augmentTruncate_hom_f_zero, CategoryTheory.ProjectiveResolution.lift_commutes_assoc, AlgebraicTopology.DoldKan.P_add_Q, AlgebraicTopology.DoldKan.instReflectsIsomorphismsSimplicialObjectKaroubiChainComplexNatN₁, ChainComplex.toSingle₀Equiv_symm_apply_f_zero, ChainComplex.instHasHomologyNatObjAlternatingConst, ChainComplex.truncate_obj_d, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_homotopyInvHomId, Rep.FiniteCyclicGroup.resolution_complex, groupHomology.chainsFunctor_map, CategoryTheory.Preadditive.DoldKan.equivalence_inverse, groupHomology.instPreservesZeroMorphismsRepChainComplexModuleCatNatChainsFunctor, CochainComplex.ConnectData.map_id, AlgebraicTopology.DoldKan.N₂_obj_p_f, CategoryTheory.ProjectiveResolution.Hom.hom_f_zero_comp_π_f_zero, AlgebraicTopology.DoldKan.N₂_obj_X_X, CategoryTheory.Idempotents.DoldKan.isoN₁_hom_app_f, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app, Rep.standardComplex.instQuasiIsoNatεToSingle₀, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_comp_inclusionOfMooreComplexMap_assoc, ChainComplex.fromSingle₀Equiv_apply, Rep.FiniteCyclicGroup.resolution_quasiIso, AlgebraicTopology.DoldKan.P_zero, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_counitIso_inv, AlgebraicTopology.DoldKan.PInftyToNormalizedMooreComplex_naturality, CategoryTheory.Idempotents.DoldKan.equivalence_functor, AlgebraicTopology.DoldKan.N₂_obj_X_d, CategoryTheory.Abelian.DoldKan.equivalence_functor, CategoryTheory.ProjectiveResolution.exact₀, Rep.standardComplex.forget₂ToModuleCatHomotopyEquiv_f_0_eq, ChainComplex.augmentTruncate_inv_f_zero, CategoryTheory.Idempotents.DoldKan.Γ_map_app, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, ChainComplex.alternatingConst_exactAt, groupHomology.chainsMap_zero, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_inv_app_f_f, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app, CategoryTheory.Abelian.DoldKan.comparisonN_hom_app_f, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f, AlgebraicTopology.DoldKan.Γ₂_obj_X_obj, AlgebraicTopology.DoldKan.QInfty_comp_PInfty_assoc, AlgebraicTopology.DoldKan.Γ₂_map_f_app, AlgebraicTopology.DoldKan.Γ₂N₁_inv, AlgebraicTopology.DoldKan.instReflectsIsomorphismsKaroubiSimplicialObjectChainComplexNatN₂, AlgebraicTopology.DoldKan.Q_zero, ChainComplex.truncate_obj_X, AlgebraicTopology.DoldKan.identity_N₂_objectwise, AlgebraicTopology.inclusionOfMooreComplexMap_f, CategoryTheory.Idempotents.DoldKan.hη, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f, AlgebraicTopology.alternatingFaceMapComplex_obj_X, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f, AlgebraicTopology.DoldKan.PInfty_comp_PInftyToNormalizedMooreComplex_assoc, CategoryTheory.ProjectiveResolution.instEpiFNatπ, CategoryTheory.ProjectiveResolution.complex_d_comp_π_f_zero_assoc, AlgebraicTopology.DoldKan.P_idem_assoc, AlgebraicTopology.DoldKan.PInfty_comp_QInfty_assoc, AlgebraicTopology.DoldKan.N₂_map_f_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_hom_app_f_f, AlgebraicTopology.DoldKan.homotopyEquivNormalizedMooreComplexAlternatingFaceMapComplex_hom, AlgebraicTopology.DoldKan.N₁Γ₀_app, ChainComplex.alternatingConst_map_f, CategoryTheory.Idempotents.DoldKan.N_map, ChainComplex.single₀_obj_zero, ChainComplex.fromSingle₀Equiv_symm_apply_f_succ, AlgebraicTopology.DoldKan.HigherFacesVanish.induction, CategoryTheory.Abelian.DoldKan.comparisonN_inv_app_f, ChainComplex.single₀_map_f_zero, ChainComplex.alternatingConst_obj, AlgebraicTopology.DoldKan.Γ₀'_map_f, Rep.FiniteCyclicGroup.resolution.π_f, AlgebraicTopology.DoldKan.Γ₂N₂_inv, CategoryTheory.Idempotents.DoldKan.η_hom_app_f, AlgebraicTopology.normalizedMooreComplex_obj, AlgebraicTopology.DoldKan.natTransQ_app, AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_counitIso_hom, CategoryTheory.Idempotents.DoldKan.equivalence_unitIso, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, AlgebraicTopology.DoldKan.PInfty_add_QInfty

---

← Back to Index