MappingCone

📁 Source: Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean

Statistics

Metric	Count
Definitions mappingCone, desc, descCochain, descCocycle, descHomotopy, fst, inl, inr, liftCochain, liftCocycle, liftHomotopy, mapHomologicalComplexIso, mapHomologicalComplexXIso, mapHomologicalComplexXIso', snd	15
Theorems instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat, d_fst_v, d_fst_v', d_fst_v'_assoc, d_fst_v_assoc, d_snd_v, d_snd_v', d_snd_v'_assoc, d_snd_v_assoc, decomp_from, decomp_to, descCocycle_coe, desc_f, ext_cochain_from_iff, ext_cochain_to_iff, ext_from, ext_from_iff, ext_to, ext_to_iff, id, id_X, inl_desc, inl_descCochain, inl_fst, inl_fst_assoc, inl_snd, inl_snd_assoc, inl_v_d, inl_v_d_assoc, inl_v_descCochain_v, inl_v_descCochain_v_assoc, inl_v_desc_f, inl_v_desc_f_assoc, inl_v_fst_v, inl_v_fst_v_assoc, inl_v_snd_v, inl_v_snd_v_assoc, inr_desc, inr_descCochain, inr_desc_assoc, inr_f_d, inr_f_d_assoc, inr_f_descCochain_v, inr_f_descCochain_v_assoc, inr_f_desc_f, inr_f_desc_f_assoc, inr_f_fst_v, inr_f_fst_v_assoc, inr_f_snd_v, inr_f_snd_v_assoc, inr_fst, inr_fst_assoc, inr_snd, inr_snd_assoc, isZero_X_iff, liftCochain_descCochain, liftCochain_fst, liftCochain_snd, liftCochain_v_descCochain_v, liftCochain_v_fst_v, liftCochain_v_fst_v_assoc, liftCochain_v_snd_v, liftCochain_v_snd_v_assoc, liftCocycle_coe, lift_desc_f, lift_f, lift_f_fst_v, lift_f_fst_v_assoc, lift_f_snd_v, lift_f_snd_v_assoc, lift_fst, lift_snd, mapHomologicalComplexXIso'_hom, mapHomologicalComplexXIso'_inv, mapHomologicalComplexXIso_eq, map_inr, ofHom_desc, ofHom_lift, δ_descCochain, δ_inl, δ_liftCochain, δ_snd	82
Total	97

CochainComplex

Definitions

Name	Category	Theorems
mappingCone 📖	CompOp	140 math math: mappingConeCompTriangleh_comm₁_assoc, mappingCone.δ_inl, mappingCone.inl_v_descCochain_v_assoc, mappingCone.ofHom_desc, mappingCone.inr_f_d_assoc, mappingConeCompTriangle_obj₂, mappingCone.id, mappingCone.liftCochain_v_snd_v_assoc, mappingCone.inr_f_fst_v, mappingCone.inr_desc_assoc, mappingCone.liftCochain_v_snd_v, mappingCone.homologySequenceδ_triangleh, mappingCone.d_snd_v, mappingCone.inl_snd_assoc, mappingConeCompTriangle_mor₃, mappingCone.rotateHomotopyEquiv_comm₂_assoc, mappingCone.liftCochain_descCochain, cm5b.fac, mappingCone.liftCocycle_coe, mappingCone.inr_f_d, mappingCone.inr_f_descShortComplex_f_assoc, mappingCone.liftCochain_v_descCochain_v, mappingCone.lift_f_fst_v, mappingCone.inl_v_triangle_mor₃_f, mappingCone.inr_triangleδ, mappingCone.id_X, mappingCone.inr_descShortComplex_assoc, mappingConeCompHomotopyEquiv_comm₂_assoc, mappingConeCompHomotopyEquiv_hom_inv_id, mappingCone.d_snd_v'_assoc, mappingCone.inr_snd_assoc, MappingConeCompHomotopyEquiv.hom_inv_id_assoc, mappingCone.lift_f_fst_v_assoc, mappingConeCompHomotopyEquiv_comm₁, mappingCone.rotateHomotopyEquiv_comm₂, mappingCone.triangleMapOfHomotopy_comm₂, mappingCone.ext_from_iff, shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv, mappingConeCompHomotopyEquiv_comm₁_assoc, mappingCone.inl_snd, mappingCone.inl_desc, mappingCone.inr_f_snd_v, mappingConeCompTriangle_mor₃_naturality, mappingCone.ofHom_lift, mappingCone.ext_to_iff, mappingCone.inr_f_desc_f, mappingCone.lift_fst, HomotopyCategory.composableArrowsFunctor_obj, mappingCone.ext_cochain_to_iff, mappingCone.inl_v_desc_f_assoc, mappingCone.map_inr, mappingCone.liftCochain_v_fst_v, mappingCone.decomp_from, mappingCone.inl_v_triangle_mor₃_f_assoc, mappingCone.inr_triangleδ_assoc, cm5b.instIsStrictlyGEBiprodIntMappingConeIdIOfHAddOfNat, mappingCone.inl_v_snd_v_assoc, mappingCone.inr_f_triangle_mor₃_f, cm5b.fac_assoc, mappingCone.descCocycle_coe, MappingConeCompHomotopyEquiv.hom_inv_id, mappingCone.d_snd_v_assoc, mappingCone.d_snd_v', mappingCone.liftCochain_fst, mappingCone.inr_f_descCochain_v_assoc, mappingCone.d_fst_v_assoc, mappingCone.map_id, mappingCone.δ_snd, mappingConeCompTriangle_obj₃, mappingCone.inl_v_fst_v, mappingCone.ext_cochain_from_iff, mappingCone.inr_desc, mappingCone.inr_f_descCochain_v, cm5b.instQuasiIsoIntP, mappingCone.liftCochain_snd, mappingCone.triangleMapOfHomotopy_comm₂_assoc, mappingCone.isZero_X_iff, mappingCone.quasiIso_descShortComplex, mappingConeCompHomotopyEquiv_comm₂, cm5b.instMonoFIntI, mappingCone.rotateHomotopyEquiv_comm₃_assoc, mappingCone.inr_f_fst_v_assoc, mappingCone.inl_v_d_assoc, mappingCone.inl_v_desc_f, mappingCone.map_comp_assoc, mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃_assoc, mappingCone.triangleRotateShortComplexSplitting_r, mappingCone.inl_v_descShortComplex_f_assoc, cm5b.instMonoIntI, mappingCone.lift_snd, mappingCone.map_comp, cm5b.i_f_comp, mappingCone.inr_snd, mappingCone.decomp_to, mappingCone.inl_fst, mappingCone.liftCochain_v_fst_v_assoc, mappingCone.lift_desc_f, mappingCone.δ_liftCochain, mappingCone.desc_f, mappingCone.d_fst_v'_assoc, mappingCone.inl_v_d, mappingCone.inr_f_snd_v_assoc, shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv_assoc, mappingCone.d_fst_v', mappingCone.inl_v_descCochain_v, mappingCone.triangleMapOfHomotopy_comm₃_assoc, mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃, cm5b.i_f_comp_assoc, mappingCone.inl_fst_assoc, mappingCone.inl_descCochain, mappingCone.inr_descShortComplex, mappingCone.mapHomologicalComplexXIso'_hom, mappingCone.inl_v_descShortComplex_f, mappingCone.triangleRotateShortComplexSplitting_s, mappingCone.inr_f_descShortComplex_f, mappingCone.inr_f_triangle_mor₃_f_assoc, mappingCone.δ_descCochain, mappingCone.inl_v_snd_v, mappingConeHomOfDegreewiseSplitIso_inv_f, mappingConeCompTriangle_mor₃_naturality_assoc, mappingCone.triangleMapOfHomotopy_comm₃, mappingCone.lift_f_snd_v, mappingCone.inr_descCochain, cm5b.degreewiseEpiWithInjectiveKernel_p, mappingConeCompTriangleh_comm₁, cm5b.instInjectiveXIntMappingConeIdI, mappingCone.rotateHomotopyEquiv_comm₃, mappingCone.lift_f, mappingConeHomOfDegreewiseSplitIso_hom_f, mappingCone.inl_v_fst_v_assoc, mappingCone.inr_fst, mappingCone.lift_f_snd_v_assoc, mappingCone.mapHomologicalComplexXIso'_inv, mappingCone.inr_f_desc_f_assoc, mappingCone.d_fst_v, mappingConeCompHomotopyEquiv_hom_inv_id_assoc, mappingCone.triangle_obj₃, mappingCone.inr_fst_assoc, mappingConeCompTriangle_obj₁, mappingCone.map_δ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat 📖	mathematical	CategoryTheory.Limits.HasBinaryBiproduct CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd	HomologicalComplex.HasHomotopyCofiber	—	AddRightCancelSemigroup.toIsRightCancelAdd

CochainComplex.mappingCone

Definitions

Name	Category	Theorems
desc 📖	CompOp	10 math math: ofHom_desc, inr_desc_assoc, inl_desc, inr_f_desc_f, inl_v_desc_f_assoc, inr_desc, inl_v_desc_f, lift_desc_f, desc_f, inr_f_desc_f_assoc
descCochain 📖	CompOp	11 math math: inl_v_descCochain_v_assoc, ofHom_desc, liftCochain_descCochain, liftCochain_v_descCochain_v, descCocycle_coe, inr_f_descCochain_v_assoc, inr_f_descCochain_v, inl_v_descCochain_v, inl_descCochain, δ_descCochain, inr_descCochain
descCocycle 📖	CompOp	1 math math: descCocycle_coe
descHomotopy 📖	CompOp	—
fst 📖	CompOp	32 math math: id, inr_f_fst_v, d_snd_v, lift_f_fst_v, id_X, d_snd_v'_assoc, lift_f_fst_v_assoc, ext_to_iff, lift_fst, ext_cochain_to_iff, liftCochain_v_fst_v, decomp_from, d_snd_v_assoc, d_snd_v', liftCochain_fst, d_fst_v_assoc, δ_snd, inl_v_fst_v, inr_f_fst_v_assoc, inl_fst, liftCochain_v_fst_v_assoc, desc_f, d_fst_v'_assoc, d_fst_v', inl_fst_assoc, mapHomologicalComplexXIso'_hom, δ_descCochain, inl_v_fst_v_assoc, inr_fst, mapHomologicalComplexXIso'_inv, d_fst_v, inr_fst_assoc
inl 📖	CompOp	31 math math: δ_inl, inl_v_descCochain_v_assoc, id, inl_snd_assoc, inl_v_triangle_mor₃_f, id_X, ext_from_iff, inl_snd, inl_desc, inl_v_desc_f_assoc, inl_v_triangle_mor₃_f_assoc, inl_v_snd_v_assoc, inl_v_fst_v, ext_cochain_from_iff, inl_v_d_assoc, inl_v_desc_f, inl_v_descShortComplex_f_assoc, decomp_to, inl_fst, δ_liftCochain, inl_v_d, inl_v_descCochain_v, inl_fst_assoc, inl_descCochain, mapHomologicalComplexXIso'_hom, inl_v_descShortComplex_f, triangleRotateShortComplexSplitting_s, inl_v_snd_v, lift_f, inl_v_fst_v_assoc, mapHomologicalComplexXIso'_inv
inr 📖	CompOp	52 math math: CochainComplex.mappingConeCompTriangleh_comm₁_assoc, δ_inl, inr_f_d_assoc, id, inr_f_fst_v, inr_desc_assoc, CochainComplex.mappingConeCompTriangle_mor₃, rotateHomotopyEquiv_comm₂_assoc, inr_f_d, inr_f_descShortComplex_f_assoc, inr_triangleδ, id_X, inr_descShortComplex_assoc, inr_snd_assoc, CochainComplex.mappingConeCompHomotopyEquiv_comm₁, rotateHomotopyEquiv_comm₂, triangleMapOfHomotopy_comm₂, ext_from_iff, CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv, CochainComplex.mappingConeCompHomotopyEquiv_comm₁_assoc, inr_f_snd_v, inr_f_desc_f, map_inr, inr_triangleδ_assoc, inr_f_triangle_mor₃_f, triangle_mor₂, inr_f_descCochain_v_assoc, ext_cochain_from_iff, inr_desc, inr_f_descCochain_v, triangleMapOfHomotopy_comm₂_assoc, rotateHomotopyEquiv_comm₃_assoc, inr_f_fst_v_assoc, inl_v_d_assoc, inr_snd, decomp_to, δ_liftCochain, inl_v_d, inr_f_snd_v_assoc, CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv_assoc, inr_descShortComplex, mapHomologicalComplexXIso'_hom, inr_f_descShortComplex_f, inr_f_triangle_mor₃_f_assoc, inr_descCochain, CochainComplex.mappingConeCompTriangleh_comm₁, rotateHomotopyEquiv_comm₃, lift_f, inr_fst, mapHomologicalComplexXIso'_inv, inr_f_desc_f_assoc, inr_fst_assoc
liftCochain 📖	CompOp	11 math math: liftCochain_v_snd_v_assoc, liftCochain_v_snd_v, liftCochain_descCochain, liftCocycle_coe, liftCochain_v_descCochain_v, ofHom_lift, liftCochain_v_fst_v, liftCochain_fst, liftCochain_snd, liftCochain_v_fst_v_assoc, δ_liftCochain
liftCocycle 📖	CompOp	1 math math: liftCocycle_coe
liftHomotopy 📖	CompOp	—
mapHomologicalComplexIso 📖	CompOp	2 math math: map_inr, map_δ
mapHomologicalComplexXIso 📖	CompOp	1 math math: mapHomologicalComplexXIso_eq
mapHomologicalComplexXIso' 📖	CompOp	3 math math: mapHomologicalComplexXIso_eq, mapHomologicalComplexXIso'_hom, mapHomologicalComplexXIso'_inv
snd 📖	CompOp	31 math math: id, liftCochain_v_snd_v_assoc, liftCochain_v_snd_v, d_snd_v, inl_snd_assoc, id_X, d_snd_v'_assoc, inr_snd_assoc, inl_snd, inr_f_snd_v, ext_to_iff, ext_cochain_to_iff, decomp_from, inl_v_snd_v_assoc, d_snd_v_assoc, d_snd_v', δ_snd, liftCochain_snd, triangleRotateShortComplexSplitting_r, lift_snd, CochainComplex.cm5b.i_f_comp, inr_snd, desc_f, inr_f_snd_v_assoc, CochainComplex.cm5b.i_f_comp_assoc, mapHomologicalComplexXIso'_hom, δ_descCochain, inl_v_snd_v, lift_f_snd_v, lift_f_snd_v_assoc, mapHomologicalComplexXIso'_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
d_fst_v 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone HomologicalComplex.d CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst Quiver.Hom CategoryTheory.CategoryStruct.toQuiver NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.homotopyCofiber.d_fstX
d_fst_v' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone HomologicalComplex.d CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst Quiver.Hom CategoryTheory.CategoryStruct.toQuiver NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	AddRightCancelSemigroup.toIsRightCancelAdd d_fst_v
d_fst_v'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone HomologicalComplex.d CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst Quiver.Hom CategoryTheory.CategoryStruct.toQuiver NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d_fst_v'
d_fst_v_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone HomologicalComplex.d CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst Quiver.Hom CategoryTheory.CategoryStruct.toQuiver NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d_fst_v
d_snd_v 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone HomologicalComplex.d CochainComplex.HomComplex.Cochain.v snd add_zero AddMonoid.toAddZeroClass Int.instAddMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst HomologicalComplex.Hom.f	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CochainComplex.HomComplex.Cochain.ofHoms_v HomologicalComplex.homotopyCofiber.d_sndX
d_snd_v' 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone HomologicalComplex.d CochainComplex.HomComplex.Cochain.v snd add_zero AddMonoid.toAddZeroClass Int.instAddMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst HomologicalComplex.Hom.f	—	AddRightCancelSemigroup.toIsRightCancelAdd d_snd_v
d_snd_v'_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone HomologicalComplex.d CochainComplex.HomComplex.Cochain.v snd add_zero AddMonoid.toAddZeroClass Int.instAddMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst HomologicalComplex.Hom.f	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d_snd_v'
d_snd_v_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone HomologicalComplex.d CochainComplex.HomComplex.Cochain.v snd add_zero AddMonoid.toAddZeroClass Int.instAddMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst HomologicalComplex.Hom.f	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d_snd_v
decomp_from 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.comp CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst snd add_zero AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero ext_from CategoryTheory.Preadditive.comp_add inl_v_fst_v_assoc inl_v_snd_v_assoc CategoryTheory.Limits.zero_comp inr_f_fst_v_assoc inr_f_snd_v_assoc zero_add
decomp_to 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.comp CochainComplex.HomComplex.Cochain.v inl HomologicalComplex.Hom.f inr	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero ext_to CategoryTheory.Category.assoc CategoryTheory.Preadditive.add_comp inl_v_fst_v CategoryTheory.Category.comp_id inr_f_fst_v CategoryTheory.Limits.comp_zero inl_v_snd_v inr_f_snd_v zero_add
descCocycle_coe 📖	mathematical	CochainComplex.HomComplex.δ Units Int.instMonoid CochainComplex.HomComplex.Cochain Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain Int.negOnePow CochainComplex.HomComplex.Cochain.comp CochainComplex.HomComplex.Cochain.ofHom AddSubgroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle zero_add AddMonoid.toAddZeroClass Int.instAddMonoid	CochainComplex.mappingCone descCocycle descCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd zero_add
desc_f 📖	mathematical	CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.ofHom CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd	HomologicalComplex.Hom.f CochainComplex.mappingCone desc Quiver.Hom CategoryTheory.CategoryStruct.toQuiver HomologicalComplex.X AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst snd add_zero AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero ext_from_iff inl_v_desc_f CategoryTheory.Preadditive.comp_add inl_v_fst_v_assoc inl_v_snd_v_assoc CategoryTheory.Limits.zero_comp inr_f_desc_f inr_f_fst_v_assoc inr_f_snd_v_assoc zero_add
ext_cochain_from_iff 📖	mathematical	—	CochainComplex.HomComplex.Cochain.comp CochainComplex.mappingCone inl CochainComplex.HomComplex.Cochain.ofHom inr zero_add AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd zero_add CochainComplex.HomComplex.Cochain.ext ext_from_iff CochainComplex.HomComplex.Cochain.congr_v CochainComplex.HomComplex.Cochain.comp_v add_zero CochainComplex.HomComplex.Cochain.zero_cochain_comp_v CochainComplex.HomComplex.Cochain.ofHom_v
ext_cochain_to_iff 📖	mathematical	—	CochainComplex.HomComplex.Cochain.comp CochainComplex.mappingCone CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst snd add_zero AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CochainComplex.HomComplex.Cochain.ext ext_to_iff CochainComplex.HomComplex.Cochain.congr_v CochainComplex.HomComplex.Cochain.comp_v CochainComplex.HomComplex.Cochain.comp_zero_cochain_v
ext_from 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.v inl HomologicalComplex.Hom.f inr	—	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.homotopyCofiber.ext_from_X
ext_from_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.v inl HomologicalComplex.Hom.f inr	—	AddRightCancelSemigroup.toIsRightCancelAdd ext_from
ext_to 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst snd add_zero AddMonoid.toAddZeroClass Int.instAddMonoid	—	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero HomologicalComplex.homotopyCofiber.ext_to_X CochainComplex.HomComplex.Cochain.ofHoms_v
ext_to_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst snd add_zero AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero ext_to
id 📖	mathematical	—	CochainComplex.HomComplex.Cochain CochainComplex.mappingCone AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Int.instAddGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.Cochain.comp AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst inl add_neg_cancel snd CochainComplex.HomComplex.Cochain.ofHom inr add_zero Int.instAddMonoid CategoryTheory.CategoryStruct.id CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd	—	AddRightCancelSemigroup.toIsRightCancelAdd add_neg_cancel add_zero neg_add_cancel zero_add ext_cochain_from_iff CochainComplex.HomComplex.Cochain.comp_add inl_fst_assoc inl_snd_assoc CochainComplex.HomComplex.Cochain.comp_id inr_fst_assoc inr_snd_assoc
id_X 📖	mathematical	—	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.comp CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst inl snd add_zero AddMonoid.toAddZeroClass Int.instAddMonoid HomologicalComplex.Hom.f inr CategoryTheory.CategoryStruct.id	—	AddRightCancelSemigroup.toIsRightCancelAdd add_neg_cancel add_zero CochainComplex.HomComplex.Cochain.comp_v CochainComplex.HomComplex.Cochain.comp_zero_cochain_v CochainComplex.HomComplex.Cochain.ofHom_v CochainComplex.HomComplex.Cochain.congr_v id
inl_desc 📖	mathematical	CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.ofHom CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd	CochainComplex.HomComplex.Cochain.comp CochainComplex.mappingCone inl desc add_zero AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero neg_add_cancel ofHom_desc inl_descCochain
inl_descCochain 📖	mathematical	—	CochainComplex.HomComplex.Cochain.comp CochainComplex.mappingCone inl descCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.HomComplex.Cochain.comp_add inl_fst_assoc inl_snd_assoc add_zero
inl_fst 📖	mathematical	—	CochainComplex.HomComplex.Cochain.comp CochainComplex.mappingCone AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Int.instAddGroup inl CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst neg_add_cancel CochainComplex.HomComplex.Cochain.ofHom CategoryTheory.CategoryStruct.id CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.HomComplex.Cochain.ext₀ neg_add_cancel add_zero CochainComplex.HomComplex.Cochain.comp_v inl_v_fst_v CochainComplex.HomComplex.Cochain.ofHom_v
inl_fst_assoc 📖	mathematical	—	CochainComplex.HomComplex.Cochain.comp CochainComplex.mappingCone inl CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst	—	AddRightCancelSemigroup.toIsRightCancelAdd neg_add_cancel CochainComplex.HomComplex.Cochain.comp_assoc inl_fst zero_add CochainComplex.HomComplex.Cochain.id_comp
inl_snd 📖	mathematical	—	CochainComplex.HomComplex.Cochain.comp CochainComplex.mappingCone inl snd add_zero AddMonoid.toAddZeroClass Int.instAddMonoid CochainComplex.HomComplex.Cochain NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.HomComplex.Cochain.ext add_zero CochainComplex.HomComplex.Cochain.comp_zero_cochain_v inl_v_snd_v
inl_snd_assoc 📖	mathematical	—	CochainComplex.HomComplex.Cochain.comp CochainComplex.mappingCone inl snd CochainComplex.HomComplex.Cochain NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero zero_add CochainComplex.HomComplex.Cochain.comp_assoc_of_second_is_zero_cochain inl_snd CochainComplex.HomComplex.Cochain.zero_comp
inl_v_d 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.v inl HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup HomologicalComplex.Hom.f inr	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.homotopyCofiber.inlX_d Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.const_add_termg add_zero
inl_v_d_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.v inl HomologicalComplex.d Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup HomologicalComplex.Hom.f inr	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_v_d
inl_v_descCochain_v 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.v inl descCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.HomComplex.Cochain.comp_v CochainComplex.HomComplex.Cochain.congr_v inl_descCochain
inl_v_descCochain_v_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.v inl descCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_v_descCochain_v
inl_v_desc_f 📖	mathematical	CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.ofHom CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd	HomologicalComplex.X CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.v inl HomologicalComplex.Hom.f desc	—	AddRightCancelSemigroup.toIsRightCancelAdd inl_v_descCochain_v
inl_v_desc_f_assoc 📖	mathematical	CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.ofHom CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd	HomologicalComplex.X CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.v inl HomologicalComplex.Hom.f desc	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_v_desc_f
inl_v_fst_v 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.v inl CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst CategoryTheory.CategoryStruct.id	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.homotopyCofiber.inlX_fstX
inl_v_fst_v_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.v inl CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inl_v_fst_v
inl_v_snd_v 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.v inl snd add_zero AddMonoid.toAddZeroClass Int.instAddMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CochainComplex.HomComplex.Cochain.ofHoms_v HomologicalComplex.homotopyCofiber.inlX_sndX
inl_v_snd_v_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.v inl snd add_zero AddMonoid.toAddZeroClass Int.instAddMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_v_snd_v
inr_desc 📖	mathematical	CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.ofHom CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd	CochainComplex.mappingCone inr desc	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.hom_ext inr_f_desc_f
inr_descCochain 📖	mathematical	—	CochainComplex.HomComplex.Cochain.comp CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.ofHom inr descCochain zero_add AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd zero_add CochainComplex.HomComplex.Cochain.comp_add inr_fst_assoc inr_snd_assoc
inr_desc_assoc 📖	mathematical	CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.ofHom CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd	CochainComplex.mappingCone inr desc	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_desc
inr_f_d 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone HomologicalComplex.Hom.f inr HomologicalComplex.d	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.Hom.comm
inr_f_d_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone HomologicalComplex.Hom.f inr HomologicalComplex.d	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_f_d
inr_f_descCochain_v 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone HomologicalComplex.Hom.f inr CochainComplex.HomComplex.Cochain.v descCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd zero_add add_zero CochainComplex.HomComplex.Cochain.comp_v CochainComplex.HomComplex.Cochain.ofHom_v CochainComplex.HomComplex.Cochain.congr_v inr_descCochain
inr_f_descCochain_v_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone HomologicalComplex.Hom.f inr CochainComplex.HomComplex.Cochain.v descCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_f_descCochain_v
inr_f_desc_f 📖	mathematical	CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.ofHom CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd	HomologicalComplex.X CochainComplex.mappingCone HomologicalComplex.Hom.f inr desc	—	AddRightCancelSemigroup.toIsRightCancelAdd inr_f_descCochain_v CochainComplex.HomComplex.Cochain.ofHom_v
inr_f_desc_f_assoc 📖	mathematical	CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.ofHom CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd	HomologicalComplex.X CochainComplex.mappingCone HomologicalComplex.Hom.f inr desc	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_f_desc_f
inr_f_fst_v 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone HomologicalComplex.Hom.f inr CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.homotopyCofiber.inrX_fstX
inr_f_fst_v_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone HomologicalComplex.Hom.f inr CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_f_fst_v
inr_f_snd_v 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone HomologicalComplex.Hom.f inr CochainComplex.HomComplex.Cochain.v snd add_zero AddMonoid.toAddZeroClass Int.instAddMonoid CategoryTheory.CategoryStruct.id	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CochainComplex.HomComplex.Cochain.ofHoms_v HomologicalComplex.homotopyCofiber.inrX_sndX
inr_f_snd_v_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone HomologicalComplex.Hom.f inr CochainComplex.HomComplex.Cochain.v snd add_zero AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inr_f_snd_v
inr_fst 📖	mathematical	—	CochainComplex.HomComplex.Cochain.comp CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.ofHom inr CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst zero_add AddMonoid.toAddZeroClass Int.instAddMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.HomComplex.Cochain.ext zero_add add_zero CochainComplex.HomComplex.Cochain.zero_cochain_comp_v CochainComplex.HomComplex.Cochain.ofHom_v inr_f_fst_v
inr_fst_assoc 📖	mathematical	—	CochainComplex.HomComplex.Cochain.comp CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.ofHom inr CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd zero_add CochainComplex.HomComplex.Cochain.comp_assoc_of_first_is_zero_cochain inr_fst CochainComplex.HomComplex.Cochain.zero_comp
inr_snd 📖	mathematical	—	CochainComplex.HomComplex.Cochain.comp CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.ofHom inr snd zero_add AddMonoid.toAddZeroClass Int.instAddMonoid CategoryTheory.CategoryStruct.id CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.HomComplex.Cochain.ext₀ zero_add add_zero CochainComplex.HomComplex.Cochain.comp_zero_cochain_v CochainComplex.HomComplex.Cochain.ofHom_v inr_f_snd_v
inr_snd_assoc 📖	mathematical	—	CochainComplex.HomComplex.Cochain.comp CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.ofHom inr snd	—	AddRightCancelSemigroup.toIsRightCancelAdd zero_add CochainComplex.HomComplex.Cochain.comp_assoc_of_first_is_zero_cochain inr_snd CochainComplex.HomComplex.Cochain.id_comp
isZero_X_iff 📖	mathematical	—	CategoryTheory.Limits.IsZero HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.HasHomotopyCofiber.hasBinaryBiproduct CategoryTheory.Limits.biprod_isZero_iff CategoryTheory.Iso.isZero_iff
liftCochain_descCochain 📖	mathematical	—	CochainComplex.HomComplex.Cochain.comp CochainComplex.mappingCone liftCochain descCochain CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Int.instIsStrictOrderedRing Mathlib.Tactic.Linarith.lt_of_lt_of_eq neg_neg_of_pos Int.instIsOrderedAddMonoid Mathlib.Tactic.Linarith.zero_lt_one sub_eq_zero_of_eq neg_eq_zero Mathlib.Tactic.Linarith.sub_nonpos_of_le IsStrictOrderedRing.toIsOrderedRing Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isNat_add CochainComplex.HomComplex.Cochain.comp_add CochainComplex.HomComplex.Cochain.add_comp CochainComplex.HomComplex.Cochain.comp_assoc inl_fst_assoc add_zero zero_add CochainComplex.HomComplex.Cochain.comp_assoc_of_second_is_zero_cochain inr_fst_assoc CochainComplex.HomComplex.Cochain.comp_zero inl_snd_assoc inr_snd_assoc
liftCochain_fst 📖	mathematical	—	CochainComplex.HomComplex.Cochain.comp CochainComplex.mappingCone liftCochain CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.HomComplex.Cochain.add_comp neg_add_cancel add_zero CochainComplex.HomComplex.Cochain.comp_assoc_of_second_degree_eq_neg_third_degree inl_fst CochainComplex.HomComplex.Cochain.comp_id zero_add CochainComplex.HomComplex.Cochain.comp_assoc_of_second_is_zero_cochain inr_fst CochainComplex.HomComplex.Cochain.comp_zero
liftCochain_snd 📖	mathematical	—	CochainComplex.HomComplex.Cochain.comp CochainComplex.mappingCone liftCochain snd add_zero AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CochainComplex.HomComplex.Cochain.add_comp CochainComplex.HomComplex.Cochain.comp_assoc_of_third_is_zero_cochain inl_snd CochainComplex.HomComplex.Cochain.comp_zero zero_add CochainComplex.HomComplex.Cochain.comp_assoc_of_second_is_zero_cochain inr_snd CochainComplex.HomComplex.Cochain.comp_id
liftCochain_v_descCochain_v 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.v liftCochain descCochain Quiver.Hom CategoryTheory.CategoryStruct.toQuiver AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.HomComplex.Cochain.congr_v liftCochain_descCochain CochainComplex.HomComplex.Cochain.comp_v
liftCochain_v_fst_v 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.v liftCochain CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.HomComplex.Cochain.comp_v CochainComplex.HomComplex.Cochain.congr_v liftCochain_fst
liftCochain_v_fst_v_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.v liftCochain CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' liftCochain_v_fst_v
liftCochain_v_snd_v 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.v liftCochain snd add_zero AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CochainComplex.HomComplex.Cochain.comp_v CochainComplex.HomComplex.Cochain.congr_v liftCochain_snd
liftCochain_v_snd_v_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone CochainComplex.HomComplex.Cochain.v liftCochain snd add_zero AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' liftCochain_v_snd_v
liftCocycle_coe 📖	mathematical	CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.comp AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle CochainComplex.HomComplex.Cochain.ofHom add_zero AddMonoid.toAddZeroClass Int.instAddMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	CochainComplex.mappingCone liftCocycle liftCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero
lift_desc_f 📖	mathematical	CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.comp AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle CochainComplex.HomComplex.Cochain.ofHom add_zero AddMonoid.toAddZeroClass Int.instAddMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd	HomologicalComplex.X CochainComplex.mappingCone HomologicalComplex.Hom.f lift desc Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Preadditive.homGroup CochainComplex.HomComplex.Cochain.v	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero zero_add neg_add_cancel liftCochain_v_descCochain_v CochainComplex.HomComplex.Cochain.ofHom_v
lift_f 📖	mathematical	CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.comp AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle CochainComplex.HomComplex.Cochain.ofHom add_zero AddMonoid.toAddZeroClass Int.instAddMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	HomologicalComplex.Hom.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone lift Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.comp CochainComplex.HomComplex.Cochain.v inl inr	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero ext_to_iff lift_f_fst_v CategoryTheory.Preadditive.add_comp CategoryTheory.Category.assoc inl_v_fst_v CategoryTheory.Category.comp_id inr_f_fst_v CategoryTheory.Limits.comp_zero lift_f_snd_v inl_v_snd_v inr_f_snd_v zero_add
lift_f_fst_v 📖	mathematical	CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.comp AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle CochainComplex.HomComplex.Cochain.ofHom add_zero AddMonoid.toAddZeroClass Int.instAddMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone HomologicalComplex.Hom.f lift CochainComplex.HomComplex.Cochain.v fst	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero liftCochain_v_fst_v
lift_f_fst_v_assoc 📖	mathematical	CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.comp AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle CochainComplex.HomComplex.Cochain.ofHom add_zero AddMonoid.toAddZeroClass Int.instAddMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone HomologicalComplex.Hom.f lift CochainComplex.HomComplex.Cochain.v fst	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_f_fst_v
lift_f_snd_v 📖	mathematical	CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.comp AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle CochainComplex.HomComplex.Cochain.ofHom add_zero AddMonoid.toAddZeroClass Int.instAddMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone HomologicalComplex.Hom.f lift CochainComplex.HomComplex.Cochain.v snd	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero liftCochain_v_snd_v
lift_f_snd_v_assoc 📖	mathematical	CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.comp AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle CochainComplex.HomComplex.Cochain.ofHom add_zero AddMonoid.toAddZeroClass Int.instAddMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex.mappingCone HomologicalComplex.Hom.f lift CochainComplex.HomComplex.Cochain.v snd	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_f_snd_v
lift_fst 📖	mathematical	CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.comp AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle CochainComplex.HomComplex.Cochain.ofHom add_zero AddMonoid.toAddZeroClass Int.instAddMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	CochainComplex.mappingCone lift fst zero_add	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero zero_add ofHom_lift liftCochain_fst
lift_snd 📖	mathematical	CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.comp AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle CochainComplex.HomComplex.Cochain.ofHom add_zero AddMonoid.toAddZeroClass Int.instAddMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	CochainComplex.mappingCone lift snd zero_add	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero zero_add ofHom_lift liftCochain_snd
mapHomologicalComplexXIso'_hom 📖	mathematical	—	CategoryTheory.Iso.hom HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CochainComplex.mappingCone AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.Functor.map mapHomologicalComplexXIso' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.comp CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst inl snd HomologicalComplex.Hom.f inr	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive
mapHomologicalComplexXIso'_inv 📖	mathematical	—	CategoryTheory.Iso.inv HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Functor.obj HomologicalComplex HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CochainComplex.mappingCone AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.Functor.map mapHomologicalComplexXIso' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.comp CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst inl snd HomologicalComplex.Hom.f inr	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive
mapHomologicalComplexXIso_eq 📖	mathematical	—	mapHomologicalComplexXIso mapHomologicalComplexXIso'	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive
map_inr 📖	mathematical	—	CategoryTheory.CategoryStruct.comp HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CochainComplex.mappingCone AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.Functor.map inr CategoryTheory.Iso.hom mapHomologicalComplexIso	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive HomologicalComplex.hom_ext add_zero mapHomologicalComplexXIso_eq CategoryTheory.Preadditive.comp_add ext_to_iff CategoryTheory.Preadditive.add_comp CategoryTheory.Category.assoc inl_v_fst_v CategoryTheory.Category.comp_id CategoryTheory.Functor.map_comp inr_f_fst_v CategoryTheory.Functor.map_zero CategoryTheory.Limits.comp_zero inl_v_snd_v inr_f_snd_v CategoryTheory.Functor.map_id zero_add
ofHom_desc 📖	mathematical	CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.ofHom CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd	CochainComplex.mappingCone desc descCochain neg_add_cancel	—	AddRightCancelSemigroup.toIsRightCancelAdd neg_add_cancel CochainComplex.HomComplex.Cocycle.cochain_ofHom_homOf_eq_coe
ofHom_lift 📖	mathematical	CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.comp AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle CochainComplex.HomComplex.Cochain.ofHom add_zero AddMonoid.toAddZeroClass Int.instAddMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	CochainComplex.mappingCone lift liftCochain zero_add	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero zero_add CochainComplex.HomComplex.Cocycle.cochain_ofHom_homOf_eq_coe
δ_descCochain 📖	mathematical	—	CochainComplex.HomComplex.δ CochainComplex.mappingCone descCochain CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.Cochain.comp AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid Int.negOnePow CochainComplex.HomComplex.Cochain.ofHom zero_add AddMonoid.toAddZeroClass Int.instAddMonoid snd	—	AddRightCancelSemigroup.toIsRightCancelAdd zero_add CochainComplex.HomComplex.δ_add CochainComplex.HomComplex.δ_comp CochainComplex.HomComplex.Cocycle.δ_eq_zero CochainComplex.HomComplex.Cochain.zero_comp smul_zero add_zero δ_snd CochainComplex.HomComplex.Cochain.neg_comp CochainComplex.HomComplex.Cochain.comp_assoc_of_second_is_zero_cochain smul_neg Int.negOnePow_succ Units.neg_smul CochainComplex.HomComplex.Cochain.comp_add CochainComplex.HomComplex.Cochain.comp_neg CochainComplex.HomComplex.Cochain.comp_units_smul Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg Mathlib.Tactic.Abel.const_add_termg
δ_inl 📖	mathematical	—	CochainComplex.HomComplex.δ CochainComplex.mappingCone inl CochainComplex.HomComplex.Cochain.ofHom CategoryTheory.CategoryStruct.comp CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd inr	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.HomComplex.Cochain.ext₀ add_zero neg_add_cancel CochainComplex.HomComplex.δ_v inl_v_d one_smul sub_add_cancel zero_add CochainComplex.HomComplex.Cochain.v.congr_simp CochainComplex.HomComplex.Cochain.ofHom_comp CochainComplex.HomComplex.Cochain.comp_zero_cochain_v CochainComplex.HomComplex.Cochain.ofHom_v
δ_liftCochain 📖	mathematical	—	CochainComplex.HomComplex.δ CochainComplex.mappingCone liftCochain CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.Cochain.comp inl CochainComplex.HomComplex.Cochain.ofHom add_zero AddMonoid.toAddZeroClass Int.instAddMonoid inr	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero zero_add neg_add_cancel CochainComplex.HomComplex.δ_add CochainComplex.HomComplex.δ_comp δ_inl CochainComplex.HomComplex.Cochain.ofHom_comp Int.negOnePow_neg Units.neg_smul one_smul CochainComplex.HomComplex.δ_comp_zero_cochain CochainComplex.HomComplex.δ_ofHom CochainComplex.HomComplex.Cochain.comp_zero CochainComplex.HomComplex.Cochain.add_comp CochainComplex.HomComplex.Cochain.comp_assoc_of_second_is_zero_cochain Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_constg Mathlib.Tactic.Abel.const_add_termg
δ_snd 📖	mathematical	—	CochainComplex.HomComplex.δ CochainComplex.mappingCone snd CochainComplex.HomComplex.Cochain NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.Cochain.comp AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle fst CochainComplex.HomComplex.Cochain.ofHom add_zero AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.HomComplex.Cochain.ext add_zero CochainComplex.HomComplex.δ_zero_cochain_v d_snd_v sub_add_cancel_right CochainComplex.HomComplex.Cochain.comp_zero_cochain_v CochainComplex.HomComplex.Cochain.ofHom_v

---

← Back to Index