MappingCocone

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

Statistics

Metric	Count
Definitions mappingCocone, desc, descCochain, descCocycle, fst, inl, inr, liftCochain, liftCocycle, rotateTriangleIso, snd, triangle	12
Theorems descCocycle_coe, id_X, inl_comp_descCochain, inl_v_descCochain_v, inl_v_descCochain_v_assoc, inl_v_desc_f, inl_v_desc_f_assoc, inl_v_fst_f, inl_v_fst_f_assoc, inl_v_snd_v, inl_v_snd_v_assoc, inr_comp_descCochain, inr_v_descCochain_v, inr_v_descCochain_v_assoc, inr_v_desc_f, inr_v_desc_f_assoc, inr_v_fst_f, inr_v_fst_f_assoc, inr_v_snd_v, inr_v_snd_v_assoc, liftCochain_comp_fst, liftCochain_comp_snd, liftCochain_v_fst_f, liftCochain_v_fst_f_assoc, liftCochain_v_snd_v, liftCochain_v_snd_v_assoc, liftCocycle_coe, lift_f_fst_f, lift_f_fst_f_assoc, lift_f_snd_v, lift_f_snd_v_assoc, lift_fst, lift_fst_assoc, ofHom_desc, ofHom_lift, triangle_mor₁, triangle_mor₂, triangle_obj₁, triangle_obj₂, triangle_obj₃, δ_descCochain, δ_liftCochain	42
Total	54

CochainComplex

Definitions

Name	Category	Theorems
mappingCocone 📖	CompOp	38 math math: mappingCocone.inr_v_snd_v_assoc, mappingCocone.inl_v_descCochain_v, mappingCocone.inr_v_snd_v, mappingCocone.lift_fst, mappingCocone.liftCochain_v_snd_v_assoc, mappingCocone.inr_v_desc_f_assoc, mappingCocone.id_X, mappingCocone.descCocycle_coe, mappingCocone.ofHom_lift, mappingCocone.inr_comp_descCochain, mappingCocone.liftCochain_v_fst_f, mappingCocone.liftCochain_comp_fst, mappingCocone.ofHom_desc, mappingCocone.inl_v_snd_v, mappingCocone.lift_f_snd_v_assoc, mappingCocone.liftCochain_v_fst_f_assoc, mappingCocone.liftCochain_comp_snd, mappingCocone.lift_f_fst_f, mappingCocone.inr_v_fst_f_assoc, mappingCocone.lift_f_snd_v, mappingCocone.lift_fst_assoc, mappingCocone.liftCochain_v_snd_v, mappingCocone.inl_v_fst_f_assoc, mappingCocone.inr_v_fst_f, mappingCocone.δ_descCochain, mappingCocone.inl_comp_descCochain, mappingCocone.triangle_obj₁, mappingCocone.inl_v_desc_f, mappingCocone.inl_v_fst_f, mappingCocone.inr_v_descCochain_v_assoc, mappingCocone.δ_liftCochain, mappingCocone.inl_v_descCochain_v_assoc, mappingCocone.inl_v_desc_f_assoc, mappingCocone.inl_v_snd_v_assoc, mappingCocone.inr_v_descCochain_v, mappingCocone.liftCocycle_coe, mappingCocone.lift_f_fst_f_assoc, mappingCocone.inr_v_desc_f

CochainComplex.mappingCocone

Definitions

Name	Category	Theorems
desc 📖	CompOp	5 math math: inr_v_desc_f_assoc, ofHom_desc, inl_v_desc_f, inl_v_desc_f_assoc, inr_v_desc_f
descCochain 📖	CompOp	9 math math: inl_v_descCochain_v, descCocycle_coe, inr_comp_descCochain, ofHom_desc, δ_descCochain, inl_comp_descCochain, inr_v_descCochain_v_assoc, inl_v_descCochain_v_assoc, inr_v_descCochain_v
descCocycle 📖	CompOp	1 math math: descCocycle_coe
fst 📖	CompOp	14 math math: lift_fst, id_X, liftCochain_v_fst_f, triangle_mor₁, liftCochain_comp_fst, liftCochain_v_fst_f_assoc, lift_f_fst_f, inr_v_fst_f_assoc, lift_fst_assoc, inl_v_fst_f_assoc, inr_v_fst_f, δ_descCochain, inl_v_fst_f, lift_f_fst_f_assoc
inl 📖	CompOp	11 math math: inl_v_descCochain_v, id_X, inl_v_snd_v, inl_v_fst_f_assoc, inl_comp_descCochain, inl_v_desc_f, inl_v_fst_f, δ_liftCochain, inl_v_descCochain_v_assoc, inl_v_desc_f_assoc, inl_v_snd_v_assoc
inr 📖	CompOp	11 math math: inr_v_snd_v_assoc, inr_v_snd_v, inr_v_desc_f_assoc, id_X, inr_comp_descCochain, inr_v_fst_f_assoc, inr_v_fst_f, inr_v_descCochain_v_assoc, δ_liftCochain, inr_v_descCochain_v, inr_v_desc_f
liftCochain 📖	CompOp	9 math math: liftCochain_v_snd_v_assoc, ofHom_lift, liftCochain_v_fst_f, liftCochain_comp_fst, liftCochain_v_fst_f_assoc, liftCochain_comp_snd, liftCochain_v_snd_v, δ_liftCochain, liftCocycle_coe
liftCocycle 📖	CompOp	1 math math: liftCocycle_coe
rotateTriangleIso 📖	CompOp	—
snd 📖	CompOp	11 math math: inr_v_snd_v_assoc, inr_v_snd_v, liftCochain_v_snd_v_assoc, id_X, inl_v_snd_v, lift_f_snd_v_assoc, liftCochain_comp_snd, lift_f_snd_v, liftCochain_v_snd_v, δ_descCochain, inl_v_snd_v_assoc
triangle 📖	CompOp	6 math math: triangle_obj₂, triangle_obj₃, triangle_mor₁, triangle_mor₂, triangle_obj₁, DerivedCategory.mappingCocone_triangle_distinguished

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
descCocycle_coe 📖	mathematical	CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.δ Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Int.negOnePow CochainComplex.HomComplex.Cochain.comp CochainComplex.HomComplex.Cochain.ofHom AddSubgroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle zero_add AddMonoid.toAddZeroClass Int.instAddMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	CochainComplex.HomComplex.Cochain CochainComplex.mappingCocone AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle descCocycle descCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd zero_add
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.mappingCocone AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.comp HomologicalComplex.Hom.f fst CochainComplex.HomComplex.Cochain.v inl add_zero AddMonoid.toAddZeroClass Int.instAddMonoid snd CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle inr CategoryTheory.CategoryStruct.id	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CochainComplex.HomComplex.Cochain.leftShift_v MulZeroClass.mul_zero mul_neg neg_mul one_mul neg_neg Int.instCharZero Nat.instAtLeastTwoHAddOfNat zero_add CategoryTheory.Category.id_comp Units.neg_smul one_smul CochainComplex.HomComplex.Cochain.rightShift_v CategoryTheory.Category.comp_id mul_one Int.negOnePow_even CochainComplex.HomComplex.Cochain.ofHom_v CochainComplex.mappingCone.id_X
inl_comp_descCochain 📖	mathematical	—	CochainComplex.HomComplex.Cochain.comp CochainComplex.mappingCocone inl descCochain zero_add AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd zero_add CochainComplex.HomComplex.Cochain.ext add_zero CochainComplex.HomComplex.Cochain.zero_cochain_comp_v inl_v_descCochain_v
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.mappingCocone CochainComplex.HomComplex.Cochain.v inl add_zero AddMonoid.toAddZeroClass Int.instAddMonoid descCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CochainComplex.HomComplex.Cochain.rightShift_v CategoryTheory.Category.comp_id CochainComplex.HomComplex.Cochain.leftShift_v neg_mul one_mul mul_neg neg_neg Int.instCharZero Nat.instAtLeastTwoHAddOfNat CategoryTheory.Category.id_comp smul_smul Int.units_mul_self one_smul CochainComplex.mappingCone.inl_v_descCochain_v
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.mappingCocone CochainComplex.HomComplex.Cochain.v inl add_zero AddMonoid.toAddZeroClass Int.instAddMonoid descCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_v_descCochain_v
inl_v_desc_f 📖	mathematical	CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.comp CochainComplex.HomComplex.Cochain.ofHom AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle zero_add 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.mappingCocone CochainComplex.HomComplex.Cochain.v inl add_zero AddMonoid.toAddZeroClass Int.instAddMonoid HomologicalComplex.Hom.f desc	—	AddRightCancelSemigroup.toIsRightCancelAdd zero_add add_zero inl_v_descCochain_v
inl_v_desc_f_assoc 📖	mathematical	CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.comp CochainComplex.HomComplex.Cochain.ofHom AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle zero_add 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.mappingCocone CochainComplex.HomComplex.Cochain.v inl add_zero AddMonoid.toAddZeroClass Int.instAddMonoid HomologicalComplex.Hom.f desc	—	AddRightCancelSemigroup.toIsRightCancelAdd zero_add add_zero CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inl_v_desc_f
inl_v_fst_f 📖	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.mappingCocone CochainComplex.HomComplex.Cochain.v inl add_zero AddMonoid.toAddZeroClass Int.instAddMonoid HomologicalComplex.Hom.f fst CategoryTheory.CategoryStruct.id	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CochainComplex.HomComplex.Cochain.rightShift_v CategoryTheory.Category.comp_id CochainComplex.HomComplex.Cochain.leftShift_v MulZeroClass.mul_zero mul_neg neg_mul one_mul neg_neg Int.instCharZero Nat.instAtLeastTwoHAddOfNat zero_add CategoryTheory.Category.id_comp Units.neg_smul one_smul CochainComplex.mappingCone.inl_v_fst_v
inl_v_fst_f_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.mappingCocone CochainComplex.HomComplex.Cochain.v inl add_zero AddMonoid.toAddZeroClass Int.instAddMonoid HomologicalComplex.Hom.f fst	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inl_v_fst_f
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.mappingCocone CochainComplex.HomComplex.Cochain.v inl add_zero AddMonoid.toAddZeroClass Int.instAddMonoid snd Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CochainComplex.HomComplex.Cochain.rightShift_v CategoryTheory.Category.comp_id CochainComplex.HomComplex.Cochain.leftShift_v mul_neg mul_one neg_neg neg_mul one_mul Int.instCharZero Nat.instAtLeastTwoHAddOfNat CategoryTheory.Category.id_comp CategoryTheory.Linear.comp_units_smul CochainComplex.mappingCone.inl_v_snd_v smul_zero
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.mappingCocone CochainComplex.HomComplex.Cochain.v inl add_zero AddMonoid.toAddZeroClass Int.instAddMonoid snd 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_comp_descCochain 📖	mathematical	—	CochainComplex.HomComplex.Cochain.comp CochainComplex.mappingCocone CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle inr descCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.HomComplex.Cochain.ext CochainComplex.HomComplex.Cochain.comp_v inr_v_descCochain_v
inr_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.mappingCocone CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle inr descCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CochainComplex.HomComplex.Cochain.rightShift_v CochainComplex.HomComplex.Cochain.ofHom_v CategoryTheory.Category.comp_id CochainComplex.HomComplex.Cochain.leftShift_v neg_mul one_mul mul_neg neg_neg Int.instCharZero Nat.instAtLeastTwoHAddOfNat CategoryTheory.Category.id_comp smul_smul Int.units_mul_self one_smul CochainComplex.mappingCone.inr_f_descCochain_v
inr_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.mappingCocone CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle inr descCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_v_descCochain_v
inr_v_desc_f 📖	mathematical	CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.comp CochainComplex.HomComplex.Cochain.ofHom AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle zero_add 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.mappingCocone CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle inr HomologicalComplex.Hom.f desc	—	AddRightCancelSemigroup.toIsRightCancelAdd zero_add inr_v_descCochain_v
inr_v_desc_f_assoc 📖	mathematical	CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.comp CochainComplex.HomComplex.Cochain.ofHom AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle zero_add 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.mappingCocone CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle inr HomologicalComplex.Hom.f desc	—	AddRightCancelSemigroup.toIsRightCancelAdd zero_add CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_v_desc_f
inr_v_fst_f 📖	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.mappingCocone CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle inr HomologicalComplex.Hom.f fst Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CochainComplex.HomComplex.Cochain.rightShift_v CochainComplex.HomComplex.Cochain.ofHom_v CochainComplex.HomComplex.Cochain.leftShift_v MulZeroClass.mul_zero mul_neg neg_mul one_mul neg_neg Int.instCharZero Nat.instAtLeastTwoHAddOfNat zero_add Units.neg_smul one_smul CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc CochainComplex.mappingCone.inr_f_fst_v
inr_v_fst_f_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.mappingCocone CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle inr HomologicalComplex.Hom.f fst Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' inr_v_fst_f
inr_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.mappingCocone CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle inr snd CategoryTheory.CategoryStruct.id	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CochainComplex.HomComplex.Cochain.rightShift_v CochainComplex.HomComplex.Cochain.ofHom_v CochainComplex.HomComplex.Cochain.leftShift_v mul_neg mul_one neg_neg neg_mul one_mul Int.instCharZero Nat.instAtLeastTwoHAddOfNat Int.negOnePow_even one_smul CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc CochainComplex.mappingCone.inr_f_snd_v
inr_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.mappingCocone CochainComplex.HomComplex.Cochain.v CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle inr snd	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc CategoryTheory.Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' inr_v_snd_v
liftCochain_comp_fst 📖	mathematical	—	CochainComplex.HomComplex.Cochain.comp CochainComplex.mappingCocone liftCochain CochainComplex.HomComplex.Cochain.ofHom fst add_zero AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CochainComplex.HomComplex.Cochain.ext CochainComplex.HomComplex.Cochain.comp_zero_cochain_v CochainComplex.HomComplex.Cochain.ofHom_v liftCochain_v_fst_f
liftCochain_comp_snd 📖	mathematical	—	CochainComplex.HomComplex.Cochain.comp CochainComplex.mappingCocone liftCochain snd	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.HomComplex.Cochain.ext CochainComplex.HomComplex.Cochain.comp_v liftCochain_v_snd_v
liftCochain_v_fst_f 📖	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.mappingCocone CochainComplex.HomComplex.Cochain.v liftCochain HomologicalComplex.Hom.f fst	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.HomComplex.Cochain.rightShift_v CategoryTheory.Category.comp_id CochainComplex.HomComplex.Cochain.leftShift_v MulZeroClass.mul_zero mul_neg neg_mul one_mul neg_neg Int.instCharZero Nat.instAtLeastTwoHAddOfNat zero_add CategoryTheory.Category.id_comp Units.neg_smul one_smul CochainComplex.mappingCone.liftCochain_v_fst_v
liftCochain_v_fst_f_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.mappingCocone CochainComplex.HomComplex.Cochain.v liftCochain HomologicalComplex.Hom.f fst	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' liftCochain_v_fst_f
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.mappingCocone CochainComplex.HomComplex.Cochain.v liftCochain snd	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CochainComplex.HomComplex.Cochain.rightShift_v CategoryTheory.Category.comp_id CochainComplex.HomComplex.Cochain.leftShift_v mul_neg mul_one neg_neg neg_mul one_mul Int.instCharZero Nat.instAtLeastTwoHAddOfNat Int.negOnePow_even CategoryTheory.Category.id_comp one_smul CochainComplex.mappingCone.liftCochain_v_snd_v
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.mappingCocone CochainComplex.HomComplex.Cochain.v liftCochain snd	—	AddRightCancelSemigroup.toIsRightCancelAdd 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.HomComplex.Cochain CochainComplex.mappingCocone AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle liftCocycle liftCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero
lift_f_fst_f 📖	mathematical	CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain 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 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.mappingCocone HomologicalComplex.Hom.f lift fst	—	AddRightCancelSemigroup.toIsRightCancelAdd liftCochain_v_fst_f CochainComplex.HomComplex.Cochain.ofHom_v
lift_f_fst_f_assoc 📖	mathematical	CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain 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 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.mappingCocone HomologicalComplex.Hom.f lift fst	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_f_fst_f
lift_f_snd_v 📖	mathematical	CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain 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 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.mappingCocone HomologicalComplex.Hom.f lift CochainComplex.HomComplex.Cochain.v snd	—	AddRightCancelSemigroup.toIsRightCancelAdd 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.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 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.mappingCocone HomologicalComplex.Hom.f lift CochainComplex.HomComplex.Cochain.v snd	—	AddRightCancelSemigroup.toIsRightCancelAdd 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.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 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 CochainComplex.mappingCocone lift fst	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.hom_ext lift_f_fst_f
lift_fst_assoc 📖	mathematical	CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain 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 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 CochainComplex.mappingCocone lift fst	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' lift_fst
ofHom_desc 📖	mathematical	CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain.comp CochainComplex.HomComplex.Cochain.ofHom AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle zero_add AddMonoid.toAddZeroClass Int.instAddMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	CochainComplex.HomComplex.Cochain.ofHom CochainComplex.mappingCocone desc descCochain CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle	—	AddRightCancelSemigroup.toIsRightCancelAdd zero_add 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.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 NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	CochainComplex.HomComplex.Cochain.ofHom CochainComplex.mappingCocone lift liftCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.HomComplex.Cocycle.cochain_ofHom_homOf_eq_coe
triangle_mor₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.Triangle.mor₁ CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasShiftInt triangle fst	—	AddRightCancelSemigroup.toIsRightCancelAdd
triangle_mor₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.Triangle.mor₂ CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasShiftInt triangle	—	AddRightCancelSemigroup.toIsRightCancelAdd
triangle_obj₁ 📖	mathematical	—	CategoryTheory.Pretriangulated.Triangle.obj₁ CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasShiftInt triangle CochainComplex.mappingCocone	—	AddRightCancelSemigroup.toIsRightCancelAdd
triangle_obj₂ 📖	mathematical	—	CategoryTheory.Pretriangulated.Triangle.obj₂ CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasShiftInt triangle	—	AddRightCancelSemigroup.toIsRightCancelAdd
triangle_obj₃ 📖	mathematical	—	CategoryTheory.Pretriangulated.Triangle.obj₃ CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasShiftInt triangle	—	AddRightCancelSemigroup.toIsRightCancelAdd
δ_descCochain 📖	mathematical	—	CochainComplex.HomComplex.δ CochainComplex.mappingCocone descCochain CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.Cochain.comp CochainComplex.HomComplex.Cochain.ofHom fst Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Int.negOnePow zero_add AddMonoid.toAddZeroClass Int.instAddMonoid snd	—	AddRightCancelSemigroup.toIsRightCancelAdd zero_add CochainComplex.HomComplex.Cochain.ext add_zero CochainComplex.HomComplex.Cochain.v.congr_simp Int.negOnePow_add Int.negOnePow_neg mul_neg mul_one Units.neg_smul CochainComplex.HomComplex.δ_neg CochainComplex.HomComplex.δ_units_smul CochainComplex.HomComplex.Cochain.δ_leftShift CochainComplex.mappingCone.δ_descCochain Int.negOnePow_even CochainComplex.HomComplex.Cochain.comp_add CochainComplex.HomComplex.Cochain.comp_units_smul CochainComplex.HomComplex.Cochain.leftShift_add CochainComplex.HomComplex.Cochain.leftShift_units_smul smul_add one_smul smul_smul neg_mul one_mul smul_neg Int.units_mul_self neg_add_rev neg_neg CochainComplex.HomComplex.Cochain.leftShift_v Int.instCharZero Nat.instAtLeastTwoHAddOfNat neg_add_cancel_comm CochainComplex.HomComplex.Cochain.zero_cochain_comp_v CategoryTheory.Category.id_comp CochainComplex.HomComplex.Cochain.comp_v CochainComplex.HomComplex.Cochain.ofHom_v CochainComplex.HomComplex.Cochain.ofHom_neg CochainComplex.HomComplex.Cocycle.cochain_ofHom_homOf_eq_coe CochainComplex.HomComplex.Cochain.neg_comp MulZeroClass.mul_zero CategoryTheory.Preadditive.neg_comp
δ_liftCochain 📖	mathematical	—	CochainComplex.HomComplex.δ CochainComplex.mappingCocone liftCochain CochainComplex.HomComplex.Cochain SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.Cochain.comp inl add_zero AddMonoid.toAddZeroClass Int.instAddMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.Cochain.ofHom AddSubgroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle inr	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CochainComplex.HomComplex.Cochain.ext zero_add CochainComplex.HomComplex.Cochain.v.congr_simp CochainComplex.HomComplex.Cochain.δ_rightShift Int.negOnePow_neg CochainComplex.mappingCone.δ_liftCochain CochainComplex.HomComplex.Cochain.add_comp CochainComplex.HomComplex.Cochain.comp_assoc_of_second_is_zero_cochain CochainComplex.HomComplex.Cochain.rightShift_add CochainComplex.HomComplex.Cochain.rightShift_neg smul_add smul_neg Units.neg_smul one_smul neg_neg CochainComplex.HomComplex.Cochain.rightShift_v CochainComplex.HomComplex.Cochain.comp_v CategoryTheory.Category.comp_id CochainComplex.HomComplex.Cochain.comp_zero_cochain_v CochainComplex.HomComplex.Cochain.ofHom_v CochainComplex.HomComplex.Cochain.zero_cochain_comp_v

---

← Back to Index