HomComplex

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

Statistics

Metric	Count
Definitions HomComplex, comp, diff, equivHomotopy, map, mk, ofHom, ofHomotopy, ofHoms, single, v, Cocycle, diff, equivHom, homOf, instCoeCochain, instModule, instSMul, isKernel, mk, ofHom, postcomp, precomp, toCochainAddMonoidHom, Triplet, p, q, cocycle, instAddCommGroupCochain, instAddCommGroupCocycle, instModuleCochain, δ, δ_hom	33
Theorems add_comp, add_v, comp_add, comp_assoc, comp_assoc_of_first_is_zero_cochain, comp_assoc_of_second_degree_eq_neg_third_degree, comp_assoc_of_second_is_zero_cochain, comp_assoc_of_third_is_zero_cochain, comp_id, comp_neg, comp_smul, comp_sub, comp_units_smul, comp_v, comp_zero, comp_zero_cochain_v, congr_v, d_comp_ofHom_v, d_comp_ofHoms_v, diff_v, equivHomotopy_apply_coe, equivHomotopy_apply_of_eq, equivHomotopy_symm_apply_hom, ext, ext_iff, ext₀, ext₀_iff, id_comp, map_add, map_comp, map_neg, map_ofHom, map_sub, map_v, map_zero, mk_v, neg_comp, neg_v, ofHom_add, ofHom_comp, ofHom_injective, ofHom_neg, ofHom_sub, ofHom_v, ofHom_v_comp_d, ofHom_zero, ofHomotopy_ofEq, ofHomotopy_refl, ofHoms_comp, ofHoms_v, ofHoms_v_comp_d, ofHoms_zero, single_v, single_v_eq_zero, single_v_eq_zero', single_zero, smul_comp, smul_v, sub_comp, sub_v, units_smul_comp, units_smul_v, v_comp_XIsoOfEq_hom, v_comp_XIsoOfEq_hom_assoc, v_comp_XIsoOfEq_inv, v_comp_XIsoOfEq_inv_assoc, zero_cochain_comp_v, zero_comp, zero_v, δ_single, cochain_ofHom_homOf_eq_coe, coe_add, coe_neg, coe_smul, coe_sub, coe_units_smul, coe_zero, diff_coe, equivHom_apply, equivHom_symm_apply, ext, ext_iff, homOf_f, homOf_ofHom_eq_self, mem_iff, mk_coe, ofHom_coe, ofHom_homOf_eq_self, postcomp_coe, precomp_coe, toCochainAddMonoidHom_apply, δ_eq_zero, hpq, δ_add, δ_comp, δ_comp_ofHom, δ_comp_zero_cochain, δ_comp_zero_cocycle, δ_hom_apply, δ_map, δ_neg, δ_neg_one_cochain, δ_ofHom, δ_ofHom_comp, δ_ofHomotopy, δ_shape, δ_smul, δ_sub, δ_units_smul, δ_v, δ_zero, δ_zero_cochain_comp, δ_zero_cochain_v, δ_zero_cocycle_comp, δ_δ, HomComplex_X, HomComplex_d_hom_apply	117
Total	150

CochainComplex

Definitions

Name	Category	Theorems
HomComplex 📖	CompOp	10 math math: HomComplex.leftHomologyData_K_coe, HomComplex.leftHomologyData'_i, HomComplex.leftHomologyData_π_hom_apply, HomComplex.leftHomologyData_i_hom_apply, HomComplex.leftHomologyData_H_coe, HomComplex.leftHomologyData'_K_coe, HomComplex_X, HomComplex.leftHomologyData'_H_coe, HomComplex.leftHomologyData'_π, HomComplex_d_hom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
HomComplex_X 📖	mathematical	—	HomologicalComplex.X AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomComplex AddCommGrpCat.of HomComplex.Cochain HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd
HomComplex_d_hom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom HomComplex.Cochain AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup HomComplex.instAddCommGroupCochain AddMonoidHom.instFunLike AddCommGrpCat.Hom.hom AddCommGrpCat.of HomologicalComplex.d AddCommGrpCat AddCommGrpCat.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddCommGrpCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomComplex HomComplex.δ	—	AddRightCancelSemigroup.toIsRightCancelAdd

CochainComplex.HomComplex

Definitions

Name	Category	Theorems
Cocycle 📖	CompOp	53 math math: Cocycle.fromSingleMk_add, Cocycle.leftShiftAddEquiv_symm_apply, Cocycle.equivHom_symm_apply, Cocycle.coe_smul, Cocycle.coe_sub, Cocycle.toCochainAddMonoidHom_apply, Cocycle.equivHomShift_symm_postcomp, Cocycle.coe_units_smul, leftHomologyData_K_coe, CohomologyClass.mk_surjective, leftHomologyData'_i, CohomologyClass.mk_eq_zero_iff, Cocycle.equivHomShift'_symm_apply, leftHomologyData_π_hom_apply, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, leftHomologyData_i_hom_apply, CohomologyClass.toSmallShiftedHom_mk, Cocycle.toSingleMk_add, Cocycle.toSingleMk_mem_coboundaries_iff, CategoryTheory.ProjectiveResolution.extMk_hom, Cocycle.toSingleMk_zero, Cocycle.coe_neg, CohomologyClass.equiv_toSmallShiftedHom_mk, mem_coboundaries_iff, CohomologyClass.mk_zero, Cocycle.equivHomShift_symm_apply, Cocycle.fromSingleMk_neg, Cocycle.rightShiftAddEquiv_symm_apply, Cocycle.fromSingleMk_zero, CohomologyClass.mkAddMonoidHom_apply, Cocycle.equivHomShift'_apply, Cocycle.toSingleMk_sub, CategoryTheory.InjectiveResolution.extMk_hom, Cocycle.fromSingleMk_sub, leftHomologyData'_K_coe, Cocycle.toSingleMk_neg, Cocycle.equivHomShift_comp, Cocycle.equivHom_apply, Cocycle.coe_zero, leftHomologyData'_π, CohomologyClass.mk_add, CohomologyClass.toHom_mk_eq_zero_iff, Cocycle.equivHomShift_symm_precomp, Cocycle.rightShiftAddEquiv_apply, Cocycle.fromSingleMk_mem_coboundaries_iff, Cocycle.equivHomShift_comp_shift, CohomologyClass.mk_sub, Cocycle.coe_add, CohomologyClass.mk_neg, CohomologyClass.toHom_mk, Cocycle.leftShiftAddEquiv_apply, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, Cocycle.equivHomShift_apply
Triplet 📖	CompData	—
cocycle 📖	CompOp	59 math math: Cocycle.precomp_coe, Cocycle.coe_smul, CochainComplex.mappingCone.id, CochainComplex.mappingCone.inr_f_fst_v, Cocycle.coe_sub, Cocycle.toCochainAddMonoidHom_apply, CochainComplex.mappingCone.d_snd_v, Cocycle.postcomp_coe, Cocycle.coe_units_smul, CochainComplex.mappingCone.id_X, leftHomologyData_i_hom_apply, CochainComplex.mappingCone.d_snd_v'_assoc, Cocycle.cochain_ofHom_homOf_eq_coe, Cocycle.coe_neg, Cocycle.toSingleMk_coe, CochainComplex.mappingCone.ext_to_iff, CochainComplex.mappingCone.ext_cochain_to_iff, CochainComplex.mappingCone.liftCochain_v_fst_v, CochainComplex.mappingCone.decomp_from, mem_coboundaries_iff, Cocycle.fromSingleMk_coe, Cocycle.leftUnshift_coe, CochainComplex.mappingCone.d_snd_v_assoc, CochainComplex.mappingCone.d_snd_v', CochainComplex.mappingCone.liftCochain_fst, Cocycle.homOf_f, CochainComplex.mappingCone.d_fst_v_assoc, CochainComplex.homOfDegreewiseSplit_f, Cocycle.δ_eq_zero, CochainComplex.mappingCone.δ_snd, CochainComplex.mappingCone.inl_v_fst_v, CochainComplex.mappingCone.inr_f_fst_v_assoc, CochainComplex.mappingCone.cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v, CochainComplex.mappingCone.inl_fst, Cocycle.shift_coe, CochainComplex.mappingCone.liftCochain_v_fst_v_assoc, CochainComplex.mappingCone.desc_f, CochainComplex.mappingCone.d_fst_v'_assoc, CochainComplex.mappingCone.d_fst_v', CochainComplex.mappingCone.inl_fst_assoc, Cocycle.ext_iff, Cocycle.ofHom_coe, CochainComplex.mappingCone.mapHomologicalComplexXIso'_hom, δ_comp_zero_cocycle, Cocycle.coe_zero, CochainComplex.mappingCone.δ_descCochain, Cocycle.leftShift_coe, Cocycle.coe_add, Cocycle.diff_coe, Cocycle.rightUnshift_coe, CochainComplex.mappingCone.inl_v_fst_v_assoc, Cocycle.mk_coe, CochainComplex.mappingCone.inr_fst, CochainComplex.mappingCone.mapHomologicalComplexXIso'_inv, Cocycle.mem_iff, Cocycle.rightShift_coe, CochainComplex.mappingCone.d_fst_v, CochainComplex.mappingCone.inr_fst_assoc, δ_zero_cocycle_comp
instAddCommGroupCochain 📖	CompOp	169 math math: δ_units_smul, Cochain.rightShiftAddEquiv_symm_apply, Cochain.fromSingleMk_neg, Cocycle.precomp_coe, Cochain.δ_single, Cocycle.coe_smul, CochainComplex.mappingCone.id, CochainComplex.mappingCone.inr_f_fst_v, Cochain.leftShift_smul, Cochain.fromSingleEquiv_fromSingleMk, Cocycle.coe_sub, Cocycle.toCochainAddMonoidHom_apply, δ_neg, CochainComplex.mappingCone.d_snd_v, Cochain.rightUnshift_neg, CochainComplex.mappingCone.inl_snd_assoc, Cocycle.postcomp_coe, Cocycle.coe_units_smul, Cochain.units_smul_comp, Cochain.shift_add, Cochain.toSingleMk_neg, CochainComplex.mappingCone.liftCochain_descCochain, Cochain.comp_neg, Cochain.map_zero, leftHomologyData'_i, Cochain.leftShiftLinearEquiv_apply, Cochain.shift_neg, Cochain.toSingleMk_add, Cochain.neg_v, Cochain.sub_v, Cochain.rightUnshift_units_smul, CochainComplex.mappingCone.id_X, Cochain.single_zero, Cochain.comp_add, Cochain.neg_comp, leftHomologyData_i_hom_apply, CochainComplex.mappingCone.d_snd_v'_assoc, Cochain.shift_zero, Cochain.leftShift_comp, δ_zero, Cochain.add_comp, Cochain.leftShift_rightShift_eq_negOnePow_rightShift_leftShift, Cochain.leftShift_rightShift, Cochain.ofHom_neg, Cochain.zero_v, δ_ofHom, Cochain.map_add, Cocycle.cochain_ofHom_homOf_eq_coe, Cochain.fromSingleMk_add, Cochain.shift_smul, Cochain.leftShiftAddEquiv_apply, Cochain.ofHomotopy_refl, Cochain.rightShiftAddEquiv_apply, Cocycle.coe_neg, CochainComplex.mappingCone.inl_snd, Cochain.rightShift_leftShift, Cochain.ofHom_sub, Cochain.leftUnshift_smul, Cochain.shiftLinearMap_apply, Cocycle.toSingleMk_coe, CochainComplex.mappingCone.ext_to_iff, Cochain.rightShift_zero, CochainComplex.mappingCone.ext_cochain_to_iff, δ_smul, CochainComplex.mappingCone.liftCochain_v_fst_v, Cochain.fromSingleMk_zero, CochainComplex.mappingCone.decomp_from, δ_comp, Cochain.leftShift_zero, mem_coboundaries_iff, Cocycle.fromSingleMk_coe, Cochain.smul_comp, Cocycle.leftUnshift_coe, Cochain.equivHomotopy_apply_of_eq, CochainComplex.mappingCone.d_snd_v_assoc, δ_add, CochainComplex.mappingCone.d_snd_v', Cochain.rightShift_smul, CochainComplex.mappingCone.liftCochain_fst, Cochain.map_sub, Cocycle.homOf_f, CochainComplex.mappingCone.d_fst_v_assoc, CochainComplex.homOfDegreewiseSplit_f, Cocycle.δ_eq_zero, CochainComplex.mappingCone.δ_snd, CochainComplex.mappingCone.inl_v_fst_v, Cochain.shift_units_smul, δ_hom_apply, Cochain.leftShiftLinearEquiv_symm_apply, Cochain.units_smul_v, Cochain.δ_toSingleMk, Cochain.leftUnshift_add, CochainComplex.mappingCone.inr_f_fst_v_assoc, CochainComplex.mappingCone.cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v, Cochain.rightShift_units_smul, Cochain.rightUnshift_smul, Cochain.smul_v, Cochain.δ_shift, Cochain.fromSingleMk_sub, Cochain.comp_units_smul, Cochain.δ_rightUnshift, Cochain.comp_sub, δ_δ, Cochain.leftUnshift_units_smul, CochainComplex.mappingCone.inl_fst, Cochain.rightShiftLinearEquiv_apply, Cocycle.shift_coe, CochainComplex.mappingCone.liftCochain_v_fst_v_assoc, CochainComplex.mappingCone.δ_liftCochain, Cochain.δ_rightShift, CochainComplex.mappingCone.desc_f, CochainComplex.mappingCone.d_fst_v'_assoc, Cochain.rightUnshift_add, Cochain.toSingleMk_zero, Cochain.shiftAddHom_apply, Cochain.δ_leftUnshift, CochainComplex.mappingCone.d_fst_v', Cochain.leftShift_add, CochainComplex.HomComplex_X, CochainComplex.mappingCone.inl_fst_assoc, Cocycle.ext_iff, Cocycle.ofHom_coe, δ_shape, CochainComplex.mappingCone.mapHomologicalComplexXIso'_hom, Cochain.leftShift_units_smul, Cochain.equivHomotopy_apply_coe, δ_comp_zero_cocycle, Cocycle.coe_zero, Cochain.ofHom_add, Cochain.zero_comp, Cochain.ofHom_zero, CochainComplex.mappingCone.δ_descCochain, Cochain.comp_zero, Cochain.leftShiftAddEquiv_symm_apply, Cochain.rightShift_neg, δ_comp_zero_cochain, Cochain.comp_smul, CochainComplex.isKInjective_of_injective_aux, Cochain.equivHomotopy_symm_apply_hom, δ_sub, Cochain.rightShiftLinearEquiv_symm_apply, Cochain.rightUnshift_zero, Cocycle.leftShift_coe, Cocycle.coe_add, Cochain.sub_comp, Cochain.rightShift_add, Cocycle.diff_coe, Cochain.toSingleEquiv_toSingleMk, Cochain.ofHoms_zero, Cocycle.rightUnshift_coe, Cochain.δ_leftShift, Cochain.add_v, CochainComplex.mappingCone.inl_v_fst_v_assoc, δ_zero_cochain_comp, Cochain.leftShift_neg, Cochain.toSingleMk_sub, Cochain.leftUnshift_neg, CochainComplex.mappingCone.inr_fst, CochainComplex.mappingCone.mapHomologicalComplexXIso'_inv, δ_ofHomotopy, Cocycle.mem_iff, Cocycle.rightShift_coe, CochainComplex.mappingCone.d_fst_v, Cochain.leftUnshift_zero, Cochain.map_neg, CochainComplex.HomComplex_d_hom_apply, CochainComplex.mappingCone.inr_fst_assoc, δ_zero_cocycle_comp, Cochain.ofHomotopy_ofEq
instAddCommGroupCocycle 📖	CompOp	48 math math: Cocycle.fromSingleMk_add, Cocycle.leftShiftAddEquiv_symm_apply, Cocycle.equivHom_symm_apply, Cocycle.coe_sub, Cocycle.toCochainAddMonoidHom_apply, Cocycle.equivHomShift_symm_postcomp, leftHomologyData'_i, CohomologyClass.mk_eq_zero_iff, Cocycle.equivHomShift'_symm_apply, leftHomologyData_π_hom_apply, CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom, leftHomologyData_i_hom_apply, CohomologyClass.toSmallShiftedHom_mk, Cocycle.toSingleMk_add, Cocycle.toSingleMk_mem_coboundaries_iff, CategoryTheory.ProjectiveResolution.extMk_hom, Cocycle.toSingleMk_zero, Cocycle.coe_neg, CohomologyClass.equiv_toSmallShiftedHom_mk, mem_coboundaries_iff, CohomologyClass.mk_zero, Cocycle.equivHomShift_symm_apply, Cocycle.fromSingleMk_neg, Cocycle.rightShiftAddEquiv_symm_apply, Cocycle.fromSingleMk_zero, CohomologyClass.mkAddMonoidHom_apply, Cocycle.equivHomShift'_apply, Cocycle.toSingleMk_sub, CategoryTheory.InjectiveResolution.extMk_hom, Cocycle.fromSingleMk_sub, Cocycle.toSingleMk_neg, Cocycle.equivHomShift_comp, Cocycle.equivHom_apply, Cocycle.coe_zero, leftHomologyData'_π, CohomologyClass.mk_add, CohomologyClass.toHom_mk_eq_zero_iff, Cocycle.equivHomShift_symm_precomp, Cocycle.rightShiftAddEquiv_apply, Cocycle.fromSingleMk_mem_coboundaries_iff, Cocycle.equivHomShift_comp_shift, CohomologyClass.mk_sub, Cocycle.coe_add, CohomologyClass.mk_neg, CohomologyClass.toHom_mk, Cocycle.leftShiftAddEquiv_apply, CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom, Cocycle.equivHomShift_apply
instModuleCochain 📖	CompOp	26 math math: δ_units_smul, Cocycle.coe_smul, Cochain.leftShift_smul, Cocycle.coe_units_smul, Cochain.units_smul_comp, Cochain.leftShiftLinearEquiv_apply, Cochain.rightUnshift_units_smul, Cochain.shift_smul, Cochain.leftUnshift_smul, Cochain.shiftLinearMap_apply, δ_smul, Cochain.smul_comp, Cochain.rightShift_smul, Cochain.shift_units_smul, δ_hom_apply, Cochain.leftShiftLinearEquiv_symm_apply, Cochain.units_smul_v, Cochain.rightShift_units_smul, Cochain.rightUnshift_smul, Cochain.smul_v, Cochain.comp_units_smul, Cochain.leftUnshift_units_smul, Cochain.rightShiftLinearEquiv_apply, Cochain.leftShift_units_smul, Cochain.comp_smul, Cochain.rightShiftLinearEquiv_symm_apply
δ 📖	CompOp	41 math math: δ_units_smul, CochainComplex.mappingCone.δ_inl, Cochain.δ_single, δ_neg, Cochain.δ_fromSingleMk, δ_v, δ_zero, δ_ofHom, δ_comp_ofHom, δ_smul, δ_comp, mem_coboundaries_iff, δ_ofHom_comp, Cochain.equivHomotopy_apply_of_eq, δ_add, Cocycle.δ_eq_zero, CochainComplex.mappingCone.δ_snd, δ_hom_apply, δ_zero_cochain_v, Cochain.δ_toSingleMk, Cochain.δ_shift, Cochain.δ_rightUnshift, δ_δ, CochainComplex.mappingCone.δ_liftCochain, Cochain.δ_rightShift, Cochain.δ_leftUnshift, δ_shape, Cochain.equivHomotopy_apply_coe, δ_comp_zero_cocycle, δ_map, CochainComplex.mappingCone.δ_descCochain, δ_comp_zero_cochain, Cochain.equivHomotopy_symm_apply_hom, δ_sub, δ_neg_one_cochain, Cochain.δ_leftShift, δ_zero_cochain_comp, δ_ofHomotopy, Cocycle.mem_iff, CochainComplex.HomComplex_d_hom_apply, δ_zero_cocycle_comp
δ_hom 📖	CompOp	1 math math: δ_hom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
δ_add 📖	mathematical	—	δ Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroupCochain	—	LinearMap.map_add
δ_comp 📖	mathematical	—	δ Cochain.comp Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroupCochain Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Int.negOnePow	—	Cochain.ext AddRightCancelSemigroup.toIsRightCancelAdd add_assoc Cochain.comp_v δ_v CategoryTheory.Category.assoc Int.negOnePow_succ Int.negOnePow_add mul_comm Units.neg_smul CategoryTheory.Preadditive.comp_add CategoryTheory.Preadditive.comp_neg CategoryTheory.Linear.comp_units_smul CategoryTheory.Preadditive.add_comp CategoryTheory.Preadditive.neg_comp CategoryTheory.Linear.units_smul_comp smul_add smul_neg smul_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 zero_add Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.zero_termg
δ_comp_ofHom 📖	mathematical	—	δ Cochain.comp Cochain.ofHom add_zero AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero Cocycle.ofHom_coe δ_comp_zero_cocycle
δ_comp_zero_cochain 📖	mathematical	—	δ Cochain.comp add_zero AddMonoid.toAddZeroClass Int.instAddMonoid Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroupCochain	—	add_zero zero_add δ_comp one_smul
δ_comp_zero_cocycle 📖	mathematical	—	δ Cochain.comp Cochain AddSubgroup AddCommGroup.toAddGroup instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike cocycle add_zero AddMonoid.toAddZeroClass Int.instAddMonoid	—	add_zero δ_comp_zero_cochain Cocycle.δ_eq_zero Cochain.comp_zero zero_add δ_shape Cochain.zero_comp
δ_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Cochain AddCommGroup.toAddCommMonoid instAddCommGroupCochain instModuleCochain LinearMap.instFunLike δ_hom δ	—	—
δ_map 📖	mathematical	—	δ CategoryTheory.Functor.obj HomologicalComplex 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 HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive Cochain.map	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive Cochain.ext δ_v CategoryTheory.Functor.map_add CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_units_smul CategoryTheory.Functor.intLinear δ_shape Cochain.map_zero
δ_neg 📖	mathematical	—	δ Cochain NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupCochain	—	LinearMap.map_neg
δ_neg_one_cochain 📖	mathematical	—	δ Cochain.ofHom Homotopy.nullHomotopicMap' ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing Cochain.v	—	Cochain.ext₀ AddRightCancelSemigroup.toIsRightCancelAdd add_zero neg_add_cancel δ_v one_smul Cochain.ofHom_v sub_add_cancel Homotopy.nullHomotopicMap'_f Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.const_add_termg
δ_ofHom 📖	mathematical	—	δ Cochain.ofHom Cochain NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd Cochain.ext add_zero δ_zero_cochain_v Cochain.ofHom_v HomologicalComplex.Hom.comm sub_self δ_shape
δ_ofHom_comp 📖	mathematical	—	δ Cochain.comp Cochain.ofHom zero_add AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd zero_add Cocycle.ofHom_coe δ_zero_cocycle_comp
δ_ofHomotopy 📖	mathematical	—	δ Cochain.ofHomotopy Cochain SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupCochain Cochain.ofHom	—	AddRightCancelSemigroup.toIsRightCancelAdd Cochain.ext₀ Homotopy.comm add_zero Cochain.ofHomotopy.eq_1 neg_add_cancel δ_v one_smul Cochain.ofHom_v prevD_eq sub_add_cancel dNext_eq Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.const_add_termg Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Tactic.Abel.zero_termg
δ_shape 📖	mathematical	—	δ Cochain NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupCochain	—	Cochain.ext AddRightCancelSemigroup.toIsRightCancelAdd Cochain.mk_v Cochain.zero_v HomologicalComplex.shape CategoryTheory.Limits.comp_zero zero_add CategoryTheory.Limits.zero_comp smul_zero
δ_smul 📖	mathematical	—	δ Cochain SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupCochain DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModuleCochain	—	LinearMap.map_smul
δ_sub 📖	mathematical	—	δ Cochain SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupCochain	—	LinearMap.map_sub
δ_units_smul 📖	mathematical	—	δ Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Cochain Units.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupCochain DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModuleCochain	—	δ_smul
δ_v 📖	mathematical	—	Cochain.v δ 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 AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.comp HomologicalComplex.d Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Int.negOnePow	—	AddRightCancelSemigroup.toIsRightCancelAdd
δ_zero 📖	mathematical	—	δ Cochain NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupCochain	—	LinearMap.map_zero
δ_zero_cochain_comp 📖	mathematical	—	δ Cochain.comp zero_add AddMonoid.toAddZeroClass Int.instAddMonoid Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroupCochain Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Int.negOnePow	—	δ_comp zero_add
δ_zero_cochain_v 📖	mathematical	—	Cochain.v δ 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 SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.comp add_zero AddMonoid.toAddZeroClass Int.instAddMonoid HomologicalComplex.d	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero zero_add δ_v Units.neg_smul one_smul sub_eq_add_neg
δ_zero_cocycle_comp 📖	mathematical	—	δ Cochain.comp Cochain AddSubgroup AddCommGroup.toAddGroup instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike cocycle zero_add AddMonoid.toAddZeroClass Int.instAddMonoid	—	zero_add δ_zero_cochain_comp Cocycle.δ_eq_zero Cochain.zero_comp smul_zero add_zero δ_shape Cochain.comp_zero
δ_δ 📖	mathematical	—	δ Cochain NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupCochain	—	Cochain.ext AddRightCancelSemigroup.toIsRightCancelAdd δ_v CategoryTheory.Preadditive.add_comp CategoryTheory.Category.assoc HomologicalComplex.d_comp_d CategoryTheory.Limits.comp_zero CategoryTheory.Linear.units_smul_comp zero_add Int.negOnePow_succ CategoryTheory.Preadditive.comp_add CategoryTheory.Linear.comp_units_smul HomologicalComplex.d_comp_d_assoc CategoryTheory.Limits.zero_comp smul_zero add_zero Units.neg_smul add_neg_cancel δ_shape δ_zero

CochainComplex.HomComplex.Cochain

Definitions

Name	Category	Theorems
comp 📖	CompOp	61 math math: CochainComplex.HomComplex.Cocycle.precomp_coe, comp_assoc, CochainComplex.mappingCone.id, CochainComplex.mappingCone.inl_snd_assoc, CochainComplex.HomComplex.Cocycle.postcomp_coe, units_smul_comp, comp_id, CochainComplex.mappingCone.liftCochain_descCochain, comp_neg, comp_v, comp_zero_cochain_v, rightUnshift_comp, ofHoms_comp, comp_add, neg_comp, fromSingleMk_postcomp, leftShift_comp, CochainComplex.mappingCone.inr_snd_assoc, zero_cochain_comp_v, add_comp, CochainComplex.mappingCone.inl_snd, CochainComplex.mappingCone.inl_desc, CochainComplex.HomComplex.δ_comp_ofHom, comp_assoc_of_first_is_zero_cochain, CochainComplex.mappingCone.ext_cochain_to_iff, CochainComplex.HomComplex.δ_comp, CochainComplex.HomComplex.δ_ofHom_comp, smul_comp, map_comp, CochainComplex.mappingCone.liftCochain_fst, CochainComplex.mappingCone.δ_snd, CochainComplex.mappingCone.ext_cochain_from_iff, CochainComplex.mappingCone.liftCochain_snd, fromSingleMk_precomp, comp_units_smul, comp_sub, CochainComplex.mappingCone.inr_snd, CochainComplex.mappingCone.inl_fst, CochainComplex.mappingCone.δ_liftCochain, leftShift_comp_zero_cochain, CochainComplex.mappingCone.inl_fst_assoc, CochainComplex.mappingCone.inl_descCochain, CochainComplex.HomComplex.δ_comp_zero_cocycle, toSingleMk_postcomp, zero_comp, id_comp, comp_assoc_of_third_is_zero_cochain, CochainComplex.mappingCone.δ_descCochain, comp_zero, CochainComplex.HomComplex.δ_comp_zero_cochain, comp_smul, CochainComplex.mappingCone.inr_descCochain, sub_comp, CochainComplex.HomComplex.δ_zero_cochain_comp, comp_assoc_of_second_is_zero_cochain, CochainComplex.mappingCone.inr_fst, toSingleMk_precomp, comp_assoc_of_second_degree_eq_neg_third_degree, CochainComplex.mappingCone.inr_fst_assoc, CochainComplex.HomComplex.δ_zero_cocycle_comp, ofHom_comp
diff 📖	CompOp	2 math math: diff_v, CochainComplex.HomComplex.Cocycle.diff_coe
equivHomotopy 📖	CompOp	3 math math: equivHomotopy_apply_of_eq, equivHomotopy_apply_coe, equivHomotopy_symm_apply_hom
map 📖	CompOp	8 math math: map_v, map_zero, map_add, map_comp, map_sub, CochainComplex.HomComplex.δ_map, map_ofHom, map_neg
mk 📖	CompOp	—
ofHom 📖	CompOp	39 math math: CochainComplex.mappingCone.δ_inl, CochainComplex.HomComplex.Cocycle.precomp_coe, CochainComplex.mappingCone.id, CochainComplex.HomComplex.Cocycle.postcomp_coe, comp_id, ofHom_v_comp_d, fromSingleMk_postcomp, CochainComplex.mappingCone.inr_snd_assoc, ofHom_neg, CochainComplex.HomComplex.δ_ofHom, CochainComplex.HomComplex.Cocycle.cochain_ofHom_homOf_eq_coe, ofHom_v, ofHom_sub, CochainComplex.HomComplex.δ_comp_ofHom, CochainComplex.HomComplex.δ_ofHom_comp, equivHomotopy_apply_of_eq, CochainComplex.mappingCone.δ_snd, CochainComplex.mappingCone.ext_cochain_from_iff, fromSingleMk_precomp, CochainComplex.mappingCone.inr_snd, CochainComplex.mappingCone.inl_fst, CochainComplex.mappingCone.δ_liftCochain, CochainComplex.HomComplex.Cocycle.ofHom_coe, d_comp_ofHom_v, equivHomotopy_apply_coe, toSingleMk_postcomp, ofHom_add, id_comp, ofHom_zero, map_ofHom, CochainComplex.mappingCone.δ_descCochain, equivHomotopy_symm_apply_hom, CochainComplex.mappingCone.inr_descCochain, CochainComplex.HomComplex.δ_neg_one_cochain, CochainComplex.mappingCone.inr_fst, CochainComplex.HomComplex.δ_ofHomotopy, toSingleMk_precomp, CochainComplex.mappingCone.inr_fst_assoc, ofHom_comp
ofHomotopy 📖	CompOp	4 math math: ofHomotopy_refl, equivHomotopy_apply_coe, CochainComplex.HomComplex.δ_ofHomotopy, ofHomotopy_ofEq
ofHoms 📖	CompOp	5 math math: ofHoms_comp, ofHoms_v, ofHoms_v_comp_d, d_comp_ofHoms_v, ofHoms_zero
single 📖	CompOp	6 math math: δ_single, single_zero, single_v_eq_zero', CochainComplex.isKInjective_of_injective_aux, single_v, single_v_eq_zero
v 📖	CompOp	96 math math: CochainComplex.mappingCone.inl_v_descCochain_v_assoc, CochainComplex.mappingCone.liftCochain_v_snd_v_assoc, CochainComplex.mappingCone.inr_f_fst_v, CochainComplex.mappingCone.liftCochain_v_snd_v, CochainComplex.mappingCone.d_snd_v, map_v, ofHom_v_comp_d, toSingleMk_v, CochainComplex.HomComplex.δ_v, comp_v, comp_zero_cochain_v, neg_v, sub_v, CochainComplex.mappingCone.liftCochain_v_descCochain_v, CochainComplex.mappingCone.lift_f_fst_v, CochainComplex.mappingCone.inl_v_triangle_mor₃_f, ext_iff, ext₀_iff, CochainComplex.mappingCone.id_X, CochainComplex.mappingCone.d_snd_v'_assoc, zero_cochain_comp_v, toSingleMk_v_eq_zero, CochainComplex.mappingCone.lift_f_fst_v_assoc, zero_v, fromSingleMk_v, CochainComplex.mappingCone.ext_from_iff, leftUnshift_v, congr_v, ofHom_v, CochainComplex.mappingCone.inr_f_snd_v, CochainComplex.mappingCone.ext_to_iff, rightUnshift_v, CochainComplex.mappingCone.inl_v_desc_f_assoc, ofHoms_v, CochainComplex.mappingCone.liftCochain_v_fst_v, CochainComplex.mappingCone.decomp_from, CochainComplex.mappingCone.inl_v_triangle_mor₃_f_assoc, CochainComplex.mappingCone.inl_v_snd_v_assoc, ofHoms_v_comp_d, v_comp_XIsoOfEq_inv, CochainComplex.mappingCone.d_snd_v_assoc, CochainComplex.mappingCone.d_snd_v', CochainComplex.mappingCone.inr_f_descCochain_v_assoc, CochainComplex.HomComplex.Cocycle.homOf_f, CochainComplex.mappingCone.d_fst_v_assoc, CochainComplex.homOfDegreewiseSplit_f, CochainComplex.mappingCone.inl_v_fst_v, CochainComplex.mappingCone.inr_f_descCochain_v, v_comp_XIsoOfEq_hom_assoc, CochainComplex.HomComplex.δ_zero_cochain_v, units_smul_v, v_comp_XIsoOfEq_hom, CochainComplex.mappingCone.inr_f_fst_v_assoc, CochainComplex.mappingCone.inl_v_d_assoc, CochainComplex.mappingCone.inl_v_desc_f, CochainComplex.mappingCone.cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v, smul_v, CochainComplex.mappingCone.triangleRotateShortComplexSplitting_r, CochainComplex.mappingCone.inl_v_descShortComplex_f_assoc, CochainComplex.cm5b.i_f_comp, CochainComplex.mappingCone.decomp_to, CochainComplex.mappingCone.liftCochain_v_fst_v_assoc, CochainComplex.mappingCone.lift_desc_f, leftShift_v, CochainComplex.mappingCone.desc_f, CochainComplex.mappingCone.d_fst_v'_assoc, CochainComplex.mappingCone.inl_v_d, shift_v, CochainComplex.mappingCone.inr_f_snd_v_assoc, CochainComplex.mappingCone.d_fst_v', CochainComplex.mappingCone.inl_v_descCochain_v, CochainComplex.cm5b.i_f_comp_assoc, CochainComplex.mappingCone.mapHomologicalComplexXIso'_hom, d_comp_ofHom_v, CochainComplex.mappingCone.inl_v_descShortComplex_f, d_comp_ofHoms_v, CochainComplex.mappingCone.triangleRotateShortComplexSplitting_s, single_v_eq_zero', CochainComplex.mappingCone.inl_v_snd_v, fromSingleMk_v_eq_zero, equivHomotopy_symm_apply_hom, CochainComplex.mappingCone.lift_f_snd_v, single_v, rightShift_v, mk_v, shift_v', v_comp_XIsoOfEq_inv_assoc, diff_v, CochainComplex.HomComplex.δ_neg_one_cochain, CochainComplex.mappingCone.lift_f, add_v, CochainComplex.mappingCone.inl_v_fst_v_assoc, CochainComplex.mappingCone.lift_f_snd_v_assoc, CochainComplex.mappingCone.mapHomologicalComplexXIso'_inv, CochainComplex.mappingCone.d_fst_v, single_v_eq_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_comp 📖	mathematical	—	comp CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	ext AddRightCancelSemigroup.toIsRightCancelAdd comp_v CategoryTheory.Preadditive.add_comp
add_v 📖	mathematical	—	v CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain 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 CategoryTheory.Preadditive.homGroup	—	AddRightCancelSemigroup.toIsRightCancelAdd
comp_add 📖	mathematical	—	comp CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	ext AddRightCancelSemigroup.toIsRightCancelAdd comp_v CategoryTheory.Preadditive.comp_add
comp_assoc 📖	mathematical	—	comp	—	ext AddRightCancelSemigroup.toIsRightCancelAdd add_assoc comp_v CategoryTheory.Category.assoc
comp_assoc_of_first_is_zero_cochain 📖	mathematical	—	comp zero_add AddMonoid.toAddZeroClass Int.instAddMonoid	—	comp_assoc zero_add
comp_assoc_of_second_degree_eq_neg_third_degree 📖	mathematical	—	comp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Int.instAddGroup neg_add_cancel add_zero Int.instAddMonoid	—	comp_assoc neg_add_cancel
comp_assoc_of_second_is_zero_cochain 📖	mathematical	—	comp add_zero AddMonoid.toAddZeroClass Int.instAddMonoid zero_add	—	comp_assoc add_zero zero_add
comp_assoc_of_third_is_zero_cochain 📖	mathematical	—	comp add_zero AddMonoid.toAddZeroClass Int.instAddMonoid	—	comp_assoc add_zero
comp_id 📖	mathematical	—	comp ofHom 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 add_zero AddMonoid.toAddZeroClass Int.instAddMonoid	—	ext AddRightCancelSemigroup.toIsRightCancelAdd add_zero comp_zero_cochain_v ofHom_v CategoryTheory.Category.comp_id
comp_neg 📖	mathematical	—	comp CochainComplex.HomComplex.Cochain NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	ext AddRightCancelSemigroup.toIsRightCancelAdd comp_v CategoryTheory.Preadditive.comp_neg
comp_smul 📖	mathematical	—	comp CochainComplex.HomComplex.Cochain SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instModuleCochain	—	ext AddRightCancelSemigroup.toIsRightCancelAdd comp_v CategoryTheory.Linear.comp_smul
comp_sub 📖	mathematical	—	comp CochainComplex.HomComplex.Cochain SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain	—	ext AddRightCancelSemigroup.toIsRightCancelAdd comp_v CategoryTheory.Preadditive.comp_sub
comp_units_smul 📖	mathematical	—	comp Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring CochainComplex.HomComplex.Cochain Units.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instModuleCochain	—	comp_smul
comp_v 📖	mathematical	—	v comp 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	—	AddRightCancelSemigroup.toIsRightCancelAdd
comp_zero 📖	mathematical	—	comp CochainComplex.HomComplex.Cochain NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	ext AddRightCancelSemigroup.toIsRightCancelAdd comp_v CategoryTheory.Limits.comp_zero
comp_zero_cochain_v 📖	mathematical	—	v comp add_zero AddMonoid.toAddZeroClass Int.instAddMonoid 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	—	comp_v add_zero
congr_v 📖	mathematical	—	v	—	AddRightCancelSemigroup.toIsRightCancelAdd
d_comp_ofHom_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 HomologicalComplex.d v ofHom HomologicalComplex.Hom.f	—	AddRightCancelSemigroup.toIsRightCancelAdd d_comp_ofHoms_v
d_comp_ofHoms_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 HomologicalComplex.d v ofHoms	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero ofHoms_v
diff_v 📖	mathematical	—	v diff HomologicalComplex.d 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	—	AddRightCancelSemigroup.toIsRightCancelAdd
equivHomotopy_apply_coe 📖	mathematical	—	CochainComplex.HomComplex.Cochain ofHom AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.δ DFunLike.coe Equiv Homotopy ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing EquivLike.toFunLike Equiv.instEquivLike equivHomotopy ofHomotopy	—	AddRightCancelSemigroup.toIsRightCancelAdd
equivHomotopy_apply_of_eq 📖	mathematical	—	CochainComplex.HomComplex.Cochain ofHom AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.δ DFunLike.coe Equiv Homotopy ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddRightCancelSemigroup.toIsRightCancelAdd AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing EquivLike.toFunLike Equiv.instEquivLike equivHomotopy Homotopy.ofEq NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd
equivHomotopy_symm_apply_hom 📖	mathematical	—	Homotopy.hom ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing DFunLike.coe Equiv CochainComplex.HomComplex.Cochain ofHom AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CochainComplex.HomComplex.δ Homotopy AddRightCancelSemigroup.toIsRightCancelAdd EquivLike.toFunLike Equiv.instEquivLike Equiv.symm equivHomotopy Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms v CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd
ext 📖	—	v	—	—	AddRightCancelSemigroup.toIsRightCancelAdd
ext_iff 📖	mathematical	—	v	—	AddRightCancelSemigroup.toIsRightCancelAdd ext
ext₀ 📖	—	v add_zero AddMonoid.toAddZeroClass Int.instAddMonoid	—	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero ext
ext₀_iff 📖	mathematical	—	v add_zero AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero ext₀
id_comp 📖	mathematical	—	comp ofHom 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 zero_add AddMonoid.toAddZeroClass Int.instAddMonoid	—	ext AddRightCancelSemigroup.toIsRightCancelAdd zero_add add_zero zero_cochain_comp_v ofHom_v CategoryTheory.Category.id_comp
map_add 📖	mathematical	—	map CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CategoryTheory.Functor.obj HomologicalComplex 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 HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive	—	ext AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.map_add
map_comp 📖	mathematical	—	map comp CategoryTheory.Functor.obj HomologicalComplex 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 HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive	—	ext AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive comp_v CategoryTheory.Functor.map_comp
map_neg 📖	mathematical	—	map CochainComplex.HomComplex.Cochain NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CategoryTheory.Functor.obj HomologicalComplex 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 HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive	—	ext AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.map_neg
map_ofHom 📖	mathematical	—	map ofHom CategoryTheory.Functor.obj HomologicalComplex 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 HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.map	—	AddRightCancelSemigroup.toIsRightCancelAdd ext₀ CategoryTheory.Functor.preservesZeroMorphisms_of_additive add_zero ofHom_v
map_sub 📖	mathematical	—	map CochainComplex.HomComplex.Cochain SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain CategoryTheory.Functor.obj HomologicalComplex 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 HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive	—	ext AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.map_sub
map_v 📖	mathematical	—	v CategoryTheory.Functor.obj HomologicalComplex 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 HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive map CategoryTheory.Functor.map HomologicalComplex.X	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive
map_zero 📖	mathematical	—	map CochainComplex.HomComplex.Cochain NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain CategoryTheory.Functor.obj HomologicalComplex 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 HomologicalComplex.instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.Functor.preservesZeroMorphisms_of_additive	—	ext AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Functor.map_zero
mk_v 📖	mathematical	—	v	—	AddRightCancelSemigroup.toIsRightCancelAdd
neg_comp 📖	mathematical	—	comp CochainComplex.HomComplex.Cochain NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	ext AddRightCancelSemigroup.toIsRightCancelAdd comp_v CategoryTheory.Preadditive.neg_comp
neg_v 📖	mathematical	—	v CochainComplex.HomComplex.Cochain NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain 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 CategoryTheory.Preadditive.homGroup	—	AddRightCancelSemigroup.toIsRightCancelAdd
ofHom_add 📖	mathematical	—	ofHom Quiver.Hom CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.instAddHom CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd ext₀ add_zero ofHom_v
ofHom_comp 📖	mathematical	—	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 comp zero_add AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd zero_add ofHoms_comp
ofHom_injective 📖	—	ofHom	—	—	AddRightCancelSemigroup.toIsRightCancelAdd AddEquiv.injective CochainComplex.HomComplex.Cocycle.ext
ofHom_neg 📖	mathematical	—	ofHom Quiver.Hom CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.instNegHom CochainComplex.HomComplex.Cochain NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd ext₀ add_zero ofHom_v
ofHom_sub 📖	mathematical	—	ofHom Quiver.Hom CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.instSubHom CochainComplex.HomComplex.Cochain SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd ext₀ add_zero ofHom_v
ofHom_v 📖	mathematical	—	v ofHom add_zero AddMonoid.toAddZeroClass Int.instAddMonoid 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	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero ofHoms_v
ofHom_v_comp_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 v ofHom HomologicalComplex.d HomologicalComplex.Hom.f	—	AddRightCancelSemigroup.toIsRightCancelAdd ofHoms_v_comp_d
ofHom_zero 📖	mathematical	—	ofHom Quiver.Hom CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.instZeroHom_1 CochainComplex.HomComplex.Cochain NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd ofHoms_zero
ofHomotopy_ofEq 📖	mathematical	—	ofHomotopy Homotopy.ofEq 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.HomComplex.Cochain NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd
ofHomotopy_refl 📖	mathematical	—	ofHomotopy Homotopy.refl 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.HomComplex.Cochain NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	AddRightCancelSemigroup.toIsRightCancelAdd
ofHoms_comp 📖	mathematical	—	comp ofHoms zero_add AddMonoid.toAddZeroClass Int.instAddMonoid 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	—	AddRightCancelSemigroup.toIsRightCancelAdd ext₀ zero_add add_zero comp_zero_cochain_v ofHoms_v
ofHoms_v 📖	mathematical	—	v ofHoms add_zero AddMonoid.toAddZeroClass Int.instAddMonoid	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero CategoryTheory.Category.comp_id
ofHoms_v_comp_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 v ofHoms HomologicalComplex.d	—	AddRightCancelSemigroup.toIsRightCancelAdd add_zero ofHoms_v
ofHoms_zero 📖	mathematical	—	ofHoms 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 CategoryTheory.Limits.HasZeroMorphisms.zero CochainComplex.HomComplex.Cochain NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	ext₀ AddRightCancelSemigroup.toIsRightCancelAdd add_zero ofHoms_v
single_v 📖	mathematical	—	v single	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
single_v_eq_zero 📖	mathematical	—	v single 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 CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd
single_v_eq_zero' 📖	mathematical	—	v single 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 CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd
single_zero 📖	mathematical	—	single 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 CategoryTheory.Limits.HasZeroMorphisms.zero CochainComplex.HomComplex.Cochain NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	ext AddRightCancelSemigroup.toIsRightCancelAdd single_v single_v_eq_zero' single_v_eq_zero
smul_comp 📖	mathematical	—	comp CochainComplex.HomComplex.Cochain SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instModuleCochain	—	ext AddRightCancelSemigroup.toIsRightCancelAdd comp_v CategoryTheory.Linear.smul_comp
smul_v 📖	mathematical	—	v CochainComplex.HomComplex.Cochain SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instModuleCochain 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 CategoryTheory.Preadditive.homGroup CategoryTheory.Linear.homModule	—	AddRightCancelSemigroup.toIsRightCancelAdd
sub_comp 📖	mathematical	—	comp CochainComplex.HomComplex.Cochain SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain	—	ext AddRightCancelSemigroup.toIsRightCancelAdd comp_v CategoryTheory.Preadditive.sub_comp
sub_v 📖	mathematical	—	v CochainComplex.HomComplex.Cochain SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain 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 CategoryTheory.Preadditive.homGroup	—	AddRightCancelSemigroup.toIsRightCancelAdd
units_smul_comp 📖	mathematical	—	comp Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring CochainComplex.HomComplex.Cochain Units.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instModuleCochain	—	smul_comp
units_smul_v 📖	mathematical	—	v Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring CochainComplex.HomComplex.Cochain Units.instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instModuleCochain 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 CategoryTheory.Preadditive.homGroup CategoryTheory.Linear.homModule	—	AddRightCancelSemigroup.toIsRightCancelAdd
v_comp_XIsoOfEq_hom 📖	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 v CategoryTheory.Iso.hom HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.comp_id
v_comp_XIsoOfEq_hom_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 v CategoryTheory.Iso.hom HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' v_comp_XIsoOfEq_hom
v_comp_XIsoOfEq_inv 📖	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 v CategoryTheory.Iso.inv HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.comp_id
v_comp_XIsoOfEq_inv_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 v CategoryTheory.Iso.inv HomologicalComplex.XIsoOfEq	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' v_comp_XIsoOfEq_inv
zero_cochain_comp_v 📖	mathematical	—	v comp zero_add AddMonoid.toAddZeroClass Int.instAddMonoid 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 add_zero	—	comp_v zero_add add_zero
zero_comp 📖	mathematical	—	comp CochainComplex.HomComplex.Cochain NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	—	ext AddRightCancelSemigroup.toIsRightCancelAdd comp_v CategoryTheory.Limits.zero_comp
zero_v 📖	mathematical	—	v CochainComplex.HomComplex.Cochain NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain 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 CategoryTheory.Limits.HasZeroMorphisms.zero	—	AddRightCancelSemigroup.toIsRightCancelAdd
δ_single 📖	mathematical	—	CochainComplex.HomComplex.δ single CochainComplex.HomComplex.Cochain AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain 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 HomologicalComplex.d Units Int.instMonoid Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Int.negOnePow	—	AddRightCancelSemigroup.toIsRightCancelAdd ext CochainComplex.HomComplex.δ_v add_v units_smul_v single_v single_v_eq_zero' CategoryTheory.Limits.zero_comp single_v_eq_zero CategoryTheory.Limits.comp_zero smul_zero

CochainComplex.HomComplex.Cocycle

Definitions

Name	Category	Theorems
diff 📖	CompOp	1 math math: diff_coe
equivHom 📖	CompOp	2 math math: equivHom_symm_apply, equivHom_apply
homOf 📖	CompOp	7 math math: equivHom_symm_apply, equivHomShift'_symm_apply, ofHom_homOf_eq_self, cochain_ofHom_homOf_eq_coe, equivHomShift_symm_apply, homOf_f, homOf_ofHom_eq_self
instCoeCochain 📖	CompOp	—
instModule 📖	CompOp	—
instSMul 📖	CompOp	2 math math: coe_smul, coe_units_smul
isKernel 📖	CompOp	—
mk 📖	CompOp	—
ofHom 📖	CompOp	6 math math: ofHom_homOf_eq_self, equivHomShift'_apply, homOf_ofHom_eq_self, equivHom_apply, ofHom_coe, equivHomShift_apply
postcomp 📖	CompOp	5 math math: equivHomShift_symm_postcomp, postcomp_coe, equivHomShift_comp_shift, toSingleMk_postcomp, fromSingleMk_postcomp
precomp 📖	CompOp	5 math math: precomp_coe, equivHomShift_comp, fromSingleMk_precomp, equivHomShift_symm_precomp, toSingleMk_precomp
toCochainAddMonoidHom 📖	CompOp	2 math math: toCochainAddMonoidHom_apply, CochainComplex.HomComplex.leftHomologyData'_i

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cochain_ofHom_homOf_eq_coe 📖	mathematical	—	CochainComplex.HomComplex.Cochain.ofHom homOf CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle	—	ofHom_homOf_eq_self
coe_add 📖	mathematical	—	CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle CochainComplex.HomComplex.Cocycle AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle	—	—
coe_neg 📖	mathematical	—	CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle CochainComplex.HomComplex.Cocycle NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle	—	—
coe_smul 📖	mathematical	—	CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle CochainComplex.HomComplex.Cocycle instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instModuleCochain	—	—
coe_sub 📖	mathematical	—	CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle CochainComplex.HomComplex.Cocycle SubNegMonoid.toSub AddGroup.toSubNegMonoid CochainComplex.HomComplex.instAddCommGroupCocycle	—	—
coe_units_smul 📖	mathematical	—	CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring CochainComplex.HomComplex.Cocycle Units.instSMul instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instModuleCochain	—	—
coe_zero 📖	mathematical	—	CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle CochainComplex.HomComplex.Cocycle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle	—	—
diff_coe 📖	mathematical	—	CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle diff CochainComplex.HomComplex.Cochain.diff	—	—
equivHom_apply 📖	mathematical	—	DFunLike.coe AddEquiv Quiver.Hom CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.HomComplex.Cocycle HomologicalComplex.instAddHom AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle EquivLike.toFunLike AddEquiv.instEquivLike equivHom ofHom	—	AddRightCancelSemigroup.toIsRightCancelAdd
equivHom_symm_apply 📖	mathematical	—	DFunLike.coe AddEquiv CochainComplex.HomComplex.Cocycle Quiver.Hom CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCocycle HomologicalComplex.instAddHom EquivLike.toFunLike AddEquiv.instEquivLike AddEquiv.symm equivHom homOf	—	AddRightCancelSemigroup.toIsRightCancelAdd
ext 📖	—	CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle	—	—	—
ext_iff 📖	mathematical	—	CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle	—	ext
homOf_f 📖	mathematical	—	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 homOf CochainComplex.HomComplex.Cochain.v AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass Int.instAddMonoid CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle	—	AddRightCancelSemigroup.toIsRightCancelAdd
homOf_ofHom_eq_self 📖	mathematical	—	homOf ofHom	—	AddRightCancelSemigroup.toIsRightCancelAdd HomologicalComplex.hom_ext CochainComplex.HomComplex.Cochain.ofHom_v
mem_iff 📖	mathematical	—	CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle CochainComplex.HomComplex.δ NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
mk_coe 📖	mathematical	CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CochainComplex.HomComplex.instAddCommGroupCochain	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle	—	—
ofHom_coe 📖	mathematical	—	CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle ofHom CochainComplex.HomComplex.Cochain.ofHom	—	AddRightCancelSemigroup.toIsRightCancelAdd
ofHom_homOf_eq_self 📖	mathematical	—	ofHom homOf	—	ext CochainComplex.HomComplex.Cochain.ext₀ AddRightCancelSemigroup.toIsRightCancelAdd add_zero CochainComplex.HomComplex.Cochain.ofHom_v
postcomp_coe 📖	mathematical	—	CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle postcomp CochainComplex.HomComplex.Cochain.comp CochainComplex.HomComplex.Cochain.ofHom	—	AddRightCancelSemigroup.toIsRightCancelAdd
precomp_coe 📖	mathematical	—	CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle precomp CochainComplex.HomComplex.Cochain.comp CochainComplex.HomComplex.Cochain.ofHom	—	AddRightCancelSemigroup.toIsRightCancelAdd
toCochainAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom CochainComplex.HomComplex.Cocycle CochainComplex.HomComplex.Cochain AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCocycle CochainComplex.HomComplex.instAddCommGroupCochain AddMonoidHom.instFunLike toCochainAddMonoidHom AddSubgroup SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle	—	—
δ_eq_zero 📖	mathematical	—	CochainComplex.HomComplex.δ CochainComplex.HomComplex.Cochain AddSubgroup AddCommGroup.toAddGroup CochainComplex.HomComplex.instAddCommGroupCochain SetLike.instMembership AddSubgroup.instSetLike CochainComplex.HomComplex.cocycle NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	mem_iff CochainComplex.HomComplex.δ_shape

CochainComplex.HomComplex.Triplet

Definitions

Name	Category	Theorems
p 📖	CompOp	1 math math: hpq
q 📖	CompOp	1 math math: hpq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hpq 📖	mathematical	—	p q	—	—

---

← Back to Index