LowDegree

📁 Source: Mathlib/RepresentationTheory/Homological/GroupCohomology/LowDegree.lean

Statistics

Metric	Count
Definitions H0, H0Iso, H0IsoOfIsTrivial, H1Iso, H1IsoOfIsTrivial, H1π, H2, H2Iso, H2π, IsCoboundary₁, IsCoboundary₂, IsCocycle₁, IsCocycle₂, IsMulCoboundary₁, IsMulCoboundary₂, IsMulCocycle₁, IsMulCocycle₂, coboundariesOfIsCoboundary₁, coboundariesOfIsCoboundary₂, coboundariesOfIsMulCoboundary₁, coboundariesOfIsMulCoboundary₂, coboundariesToCocycles₁, coboundariesToCocycles₂, coboundaries₁, coboundaries₂, cochainsIso₀, cochainsIso₁, cochainsIso₂, cochainsIso₃, cocyclesIso₀, cocyclesOfIsCocycle₁, cocyclesOfIsCocycle₂, cocyclesOfIsMulCocycle₁, cocyclesOfIsMulCocycle₂, cocycles₁, cocycles₁IsoOfIsTrivial, cocycles₂, dArrowIso₀₁, d₀₁, d₁₂, d₂₃, instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCoboundaries₁, instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCocycles₁, instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCoboundaries₂, instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCocycles₂, isoCocycles₁, isoCocycles₂, isoShortComplexH1, isoShortComplexH2, shortComplexH0, shortComplexH1, shortComplexH2	52
Theorems H0IsoOfIsTrivial_hom, H0IsoOfIsTrivial_inv_apply, H0_induction_on, H1IsoOfIsTrivial_H1π_apply_apply, H1IsoOfIsTrivial_inv_apply, H1_induction_on, H1π_comp_H1IsoOfIsTrivial_hom, H1π_comp_H1IsoOfIsTrivial_hom_apply, H1π_comp_H1IsoOfIsTrivial_hom_assoc, H1π_eq_iff, H1π_eq_zero_iff, H2_induction_on, H2π_eq_iff, H2π_eq_zero_iff, coboundariesOfIsCoboundary₁_coe, coboundariesOfIsCoboundary₂_coe, coboundariesOfIsMulCoboundary₁_coe, coboundariesToCocycles₁_apply, coboundariesToCocycles₂_apply, coe_mk, val_eq_coe, coboundaries₁_eq_bot_of_isTrivial, coboundaries₁_ext, coboundaries₁_ext_iff, coboundaries₁_le_cocycles₁, coe_mk, val_eq_coe, coboundaries₂_ext, coboundaries₂_ext_iff, coboundaries₂_le_cocycles₂, cocyclesIso₀_hom_comp_f, cocyclesIso₀_hom_comp_f_apply, cocyclesIso₀_hom_comp_f_assoc, cocyclesIso₀_inv_comp_iCocycles, cocyclesIso₀_inv_comp_iCocycles_apply, cocyclesIso₀_inv_comp_iCocycles_assoc, cocyclesMk₀_eq, cocyclesMk₁_eq, cocyclesMk₂_eq, cocyclesOfIsCocycle₁_coe, cocyclesOfIsCocycle₂_coe, cocyclesOfIsMulCocycle₁_coe, cocyclesOfIsMulCocycle₂_coe, coe_mk, d₁₂_apply, val_eq_coe, cocycles₁IsoOfIsTrivial_hom_hom_apply_apply, cocycles₁IsoOfIsTrivial_inv_hom_apply_coe, cocycles₁_ext, cocycles₁_ext_iff, cocycles₁_map_inv, cocycles₁_map_mul_of_isTrivial, cocycles₁_map_one, coe_mk, d₂₃_apply, val_eq_coe, cocycles₂_ext, cocycles₂_ext_iff, cocycles₂_map_one_fst, cocycles₂_map_one_snd, cocycles₂_ρ_map_inv_sub_map_inv, comp_d₀₁_eq, comp_d₁₂_eq, comp_d₂₃_eq, dArrowIso₀₁_hom_left, dArrowIso₀₁_hom_right, dArrowIso₀₁_inv_left, dArrowIso₀₁_inv_right, d₀₁_apply_mem_cocycles₁, d₀₁_comp_d₁₂, d₀₁_comp_d₁₂_apply, d₀₁_comp_d₁₂_assoc, d₀₁_eq_zero, d₀₁_hom_apply, d₀₁_ker_eq_invariants, d₁₂_apply_mem_cocycles₂, d₁₂_comp_d₂₃, d₁₂_comp_d₂₃_apply, d₁₂_comp_d₂₃_assoc, d₁₂_hom_apply, d₂₃_hom_apply, eq_d₀₁_comp_inv, eq_d₀₁_comp_inv_apply, eq_d₀₁_comp_inv_assoc, eq_d₁₂_comp_inv, eq_d₁₂_comp_inv_apply, eq_d₁₂_comp_inv_assoc, eq_d₂₃_comp_inv, eq_d₂₃_comp_inv_apply, eq_d₂₃_comp_inv_assoc, instEpiModuleCatH1π, instEpiModuleCatH2π, instMonoModuleCatFShortComplexH0, isCoboundary₁_of_mem_coboundaries₁, isCoboundary₂_of_mem_coboundaries₂, isCocycle₁_of_mem_cocycles₁, isCocycle₂_of_mem_cocycles₂, isMulCoboundary₁_of_mem_coboundaries₁, isMulCoboundary₂_of_mem_coboundaries₂, isMulCocycle₁_of_mem_cocycles₁, isMulCocycle₂_of_mem_cocycles₂, isoCocycles₁_hom_comp_i, isoCocycles₁_hom_comp_i_apply, isoCocycles₁_hom_comp_i_assoc, isoCocycles₁_inv_comp_iCocycles, isoCocycles₁_inv_comp_iCocycles_apply, isoCocycles₁_inv_comp_iCocycles_assoc, isoCocycles₂_hom_comp_i, isoCocycles₂_hom_comp_i_apply, isoCocycles₂_hom_comp_i_assoc, isoCocycles₂_inv_comp_iCocycles, isoCocycles₂_inv_comp_iCocycles_apply, isoCocycles₂_inv_comp_iCocycles_assoc, isoShortComplexH1_hom, isoShortComplexH1_inv, isoShortComplexH2_hom, isoShortComplexH2_inv, map_inv_of_isCocycle₁, map_inv_of_isMulCocycle₁, map_one_fst_of_isCocycle₂, map_one_fst_of_isMulCocycle₂, map_one_of_isCocycle₁, map_one_of_isMulCocycle₁, map_one_snd_of_isCocycle₂, map_one_snd_of_isMulCocycle₂, mem_cocycles₁_def, mem_cocycles₁_iff, mem_cocycles₁_of_addMonoidHom, mem_cocycles₂_def, mem_cocycles₂_iff, shortComplexH0_exact, shortComplexH0_f, shortComplexH0_g, shortComplexH1_f, shortComplexH1_g, shortComplexH2_f, shortComplexH2_g, smul_map_inv_div_map_inv_of_isMulCocycle₂, smul_map_inv_sub_map_inv_of_isCocycle₂, subtype_comp_d₀₁, subtype_comp_d₀₁_apply, subtype_comp_d₀₁_assoc, toCocycles_comp_isoCocycles₁_hom, toCocycles_comp_isoCocycles₁_hom_apply, toCocycles_comp_isoCocycles₁_hom_assoc, toCocycles_comp_isoCocycles₂_hom, toCocycles_comp_isoCocycles₂_hom_apply, toCocycles_comp_isoCocycles₂_hom_assoc, π_comp_H0IsoOfIsTrivial_hom, π_comp_H0IsoOfIsTrivial_hom_apply, π_comp_H0IsoOfIsTrivial_hom_assoc, π_comp_H0Iso_hom, π_comp_H0Iso_hom_apply, π_comp_H0Iso_hom_assoc, π_comp_H1Iso_hom, π_comp_H1Iso_hom_apply, π_comp_H1Iso_hom_assoc, π_comp_H2Iso_hom, π_comp_H2Iso_hom_apply, π_comp_H2Iso_hom_assoc	160
Total	212

groupCohomology

Definitions

Name	Category	Theorems
H0 📖	CompOp	14 math math: π_comp_H0IsoOfIsTrivial_hom_assoc, π_comp_H0Iso_hom, H0IsoOfIsTrivial_hom, map_H0Iso_hom_f_apply, H0IsoOfIsTrivial_inv_apply, π_comp_H0IsoOfIsTrivial_hom, map_H0Iso_hom_f, π_comp_H0Iso_hom_apply, π_comp_H0Iso_hom_assoc, map_id_comp_H0Iso_hom_apply, map_id_comp_H0Iso_hom, δ₀_apply, map_H0Iso_hom_f_assoc, map_id_comp_H0Iso_hom_assoc
H0Iso 📖	CompOp	12 math math: π_comp_H0Iso_hom, H0IsoOfIsTrivial_hom, map_H0Iso_hom_f_apply, H0IsoOfIsTrivial_inv_apply, map_H0Iso_hom_f, π_comp_H0Iso_hom_apply, π_comp_H0Iso_hom_assoc, map_id_comp_H0Iso_hom_apply, map_id_comp_H0Iso_hom, δ₀_apply, map_H0Iso_hom_f_assoc, map_id_comp_H0Iso_hom_assoc
H0IsoOfIsTrivial 📖	CompOp	4 math math: π_comp_H0IsoOfIsTrivial_hom_assoc, H0IsoOfIsTrivial_hom, H0IsoOfIsTrivial_inv_apply, π_comp_H0IsoOfIsTrivial_hom
H1Iso 📖	CompOp	3 math math: π_comp_H1Iso_hom_assoc, π_comp_H1Iso_hom, π_comp_H1Iso_hom_apply
H1IsoOfIsTrivial 📖	CompOp	5 math math: H1IsoOfIsTrivial_inv_apply, H1IsoOfIsTrivial_H1π_apply_apply, H1π_comp_H1IsoOfIsTrivial_hom_apply, H1π_comp_H1IsoOfIsTrivial_hom, H1π_comp_H1IsoOfIsTrivial_hom_assoc
H1π 📖	CompOp	13 math math: H1π_comp_map_assoc, H1IsoOfIsTrivial_inv_apply, H1IsoOfIsTrivial_H1π_apply_apply, δ₁_apply, instEpiModuleCatH1π, H1π_eq_zero_iff, H1π_comp_H1IsoOfIsTrivial_hom_apply, H1π_comp_map_apply, δ₀_apply, H1π_comp_H1IsoOfIsTrivial_hom, H1π_comp_map, H1π_comp_H1IsoOfIsTrivial_hom_assoc, H1π_eq_iff
H2 📖	CompOp	10 math math: instEpiModuleCatH2π, H2π_comp_map_apply, H2π_eq_iff, δ₁_apply, H2π_comp_map, H2π_comp_map_assoc, H2π_eq_zero_iff, π_comp_H2Iso_hom_assoc, π_comp_H2Iso_hom_apply, π_comp_H2Iso_hom
H2Iso 📖	CompOp	3 math math: π_comp_H2Iso_hom_assoc, π_comp_H2Iso_hom_apply, π_comp_H2Iso_hom
H2π 📖	CompOp	7 math math: instEpiModuleCatH2π, H2π_comp_map_apply, H2π_eq_iff, δ₁_apply, H2π_comp_map, H2π_comp_map_assoc, H2π_eq_zero_iff
IsCoboundary₁ 📖	MathDef	1 math math: isCoboundary₁_of_mem_coboundaries₁
IsCoboundary₂ 📖	MathDef	1 math math: isCoboundary₂_of_mem_coboundaries₂
IsCocycle₁ 📖	MathDef	1 math math: isCocycle₁_of_mem_cocycles₁
IsCocycle₂ 📖	MathDef	1 math math: isCocycle₂_of_mem_cocycles₂
IsMulCoboundary₁ 📖	MathDef	2 math math: isMulCoboundary₁_of_mem_coboundaries₁, isMulCoboundary₁_of_isMulCocycle₁_of_aut_to_units
IsMulCoboundary₂ 📖	MathDef	1 math math: isMulCoboundary₂_of_mem_coboundaries₂
IsMulCocycle₁ 📖	MathDef	1 math math: isMulCocycle₁_of_mem_cocycles₁
IsMulCocycle₂ 📖	MathDef	1 math math: isMulCocycle₂_of_mem_cocycles₂
coboundariesOfIsCoboundary₁ 📖	CompOp	1 math math: coboundariesOfIsCoboundary₁_coe
coboundariesOfIsCoboundary₂ 📖	CompOp	1 math math: coboundariesOfIsCoboundary₂_coe
coboundariesOfIsMulCoboundary₁ 📖	CompOp	1 math math: coboundariesOfIsMulCoboundary₁_coe
coboundariesOfIsMulCoboundary₂ 📖	CompOp	—
coboundariesToCocycles₁ 📖	CompOp	1 math math: coboundariesToCocycles₁_apply
coboundariesToCocycles₂ 📖	CompOp	1 math math: coboundariesToCocycles₂_apply
coboundaries₁ 📖	CompOp	9 math math: coboundariesToCocycles₁_apply, coboundaries₁_eq_bot_of_isTrivial, coboundariesOfIsCoboundary₁_coe, coboundariesOfIsMulCoboundary₁_coe, H1π_eq_zero_iff, coboundaries₁.val_eq_coe, coboundaries₁_ext_iff, coboundaries₁_le_cocycles₁, H1π_eq_iff
coboundaries₂ 📖	CompOp	7 math math: coboundaries₂_le_cocycles₂, coboundaries₂.val_eq_coe, H2π_eq_iff, coboundariesToCocycles₂_apply, H2π_eq_zero_iff, coboundaries₂_ext_iff, coboundariesOfIsCoboundary₂_coe
cochainsIso₀ 📖	CompOp	25 math math: toCocycles_comp_isoCocycles₁_hom, π_comp_H0IsoOfIsTrivial_hom_assoc, cocyclesIso₀_hom_comp_f, eq_d₀₁_comp_inv, cocyclesMap_cocyclesIso₀_hom_f_apply, cocyclesIso₀_inv_comp_iCocycles, π_comp_H0IsoOfIsTrivial_hom, comp_d₀₁_eq, dArrowIso₀₁_inv_left, dArrowIso₀₁_hom_left, eq_d₀₁_comp_inv_apply, cocyclesIso₀_inv_comp_iCocycles_assoc, π_comp_H0IsoOfIsTrivial_hom_apply, toCocycles_comp_isoCocycles₁_hom_assoc, cochainsMap_f_0_comp_cochainsIso₀_apply, cocyclesIso₀_hom_comp_f_assoc, isoShortComplexH1_hom, toCocycles_comp_isoCocycles₁_hom_apply, cochainsMap_f_0_comp_cochainsIso₀, cocyclesIso₀_hom_comp_f_apply, cocyclesIso₀_inv_comp_iCocycles_apply, cocyclesMk₀_eq, isoShortComplexH1_inv, cochainsMap_f_0_comp_cochainsIso₀_assoc, eq_d₀₁_comp_inv_assoc
cochainsIso₁ 📖	CompOp	27 math math: isoCocycles₁_hom_comp_i_apply, toCocycles_comp_isoCocycles₂_hom_apply, eq_d₀₁_comp_inv, eq_d₁₂_comp_inv, comp_d₁₂_eq, dArrowIso₀₁_inv_right, eq_d₁₂_comp_inv_apply, cochainsMap_f_1_comp_cochainsIso₁_apply, dArrowIso₀₁_hom_right, toCocycles_comp_isoCocycles₂_hom, cochainsMap_f_1_comp_cochainsIso₁_assoc, comp_d₀₁_eq, isoCocycles₁_inv_comp_iCocycles_apply, eq_d₀₁_comp_inv_apply, isoCocycles₁_inv_comp_iCocycles, cocyclesMk₁_eq, toCocycles_comp_isoCocycles₂_hom_assoc, isoShortComplexH1_hom, isoCocycles₁_hom_comp_i, isoShortComplexH2_hom, isoCocycles₁_inv_comp_iCocycles_assoc, isoShortComplexH1_inv, cochainsMap_f_1_comp_cochainsIso₁, eq_d₁₂_comp_inv_assoc, isoShortComplexH2_inv, eq_d₀₁_comp_inv_assoc, isoCocycles₁_hom_comp_i_assoc
cochainsIso₂ 📖	CompOp	22 math math: eq_d₁₂_comp_inv, cochainsMap_f_2_comp_cochainsIso₂, comp_d₁₂_eq, eq_d₂₃_comp_inv_assoc, eq_d₂₃_comp_inv_apply, eq_d₁₂_comp_inv_apply, comp_d₂₃_eq, isoCocycles₂_hom_comp_i, isoCocycles₂_inv_comp_iCocycles_apply, cochainsMap_f_2_comp_cochainsIso₂_apply, eq_d₂₃_comp_inv, isoShortComplexH1_hom, isoCocycles₂_inv_comp_iCocycles, cocyclesMk₂_eq, isoShortComplexH2_hom, cochainsMap_f_2_comp_cochainsIso₂_assoc, isoCocycles₂_hom_comp_i_apply, isoShortComplexH1_inv, eq_d₁₂_comp_inv_assoc, isoShortComplexH2_inv, isoCocycles₂_hom_comp_i_assoc, isoCocycles₂_inv_comp_iCocycles_assoc
cochainsIso₃ 📖	CompOp	9 math math: cochainsMap_f_3_comp_cochainsIso₃_assoc, eq_d₂₃_comp_inv_assoc, eq_d₂₃_comp_inv_apply, cochainsMap_f_3_comp_cochainsIso₃_apply, comp_d₂₃_eq, eq_d₂₃_comp_inv, cochainsMap_f_3_comp_cochainsIso₃, isoShortComplexH2_hom, isoShortComplexH2_inv
cocyclesIso₀ 📖	CompOp	13 math math: cocyclesIso₀_hom_comp_f, π_comp_H0Iso_hom, cocyclesIso₀_inv_comp_iCocycles, π_comp_H0Iso_hom_apply, cocyclesIso₀_inv_comp_iCocycles_assoc, π_comp_H0Iso_hom_assoc, π_comp_H0IsoOfIsTrivial_hom_apply, cocyclesMap_cocyclesIso₀_hom_f_assoc, cocyclesIso₀_hom_comp_f_assoc, cocyclesMap_cocyclesIso₀_hom_f, cocyclesIso₀_hom_comp_f_apply, cocyclesIso₀_inv_comp_iCocycles_apply, cocyclesMk₀_eq
cocyclesOfIsCocycle₁ 📖	CompOp	1 math math: cocyclesOfIsCocycle₁_coe
cocyclesOfIsCocycle₂ 📖	CompOp	1 math math: cocyclesOfIsCocycle₂_coe
cocyclesOfIsMulCocycle₁ 📖	CompOp	1 math math: cocyclesOfIsMulCocycle₁_coe
cocyclesOfIsMulCocycle₂ 📖	CompOp	1 math math: cocyclesOfIsMulCocycle₂_coe
cocycles₁ 📖	CompOp	50 math math: toCocycles_comp_isoCocycles₁_hom, isoCocycles₁_hom_comp_i_apply, H1π_comp_map_assoc, π_comp_H1Iso_hom_assoc, coe_mapCocycles₁, coboundariesToCocycles₁_apply, mem_cocycles₁_of_addMonoidHom, mem_cocycles₁_def, H1IsoOfIsTrivial_inv_apply, mem_cocycles₁_of_comp_eq_d₀₁, cocycles₁IsoOfIsTrivial_hom_hom_apply_apply, cocyclesOfIsCocycle₁_coe, H1IsoOfIsTrivial_H1π_apply_apply, d₀₁_apply_mem_cocycles₁, π_comp_H1Iso_hom, cocyclesMap_comp_isoCocycles₁_hom_assoc, instEpiModuleCatH1π, isoCocycles₁_inv_comp_iCocycles_apply, cocyclesMap_comp_isoCocycles₁_hom, cocycles₁_map_inv, mapCocycles₁_one, mem_cocycles₁_iff, toCocycles_comp_isoCocycles₁_hom_assoc, isoCocycles₁_inv_comp_iCocycles, cocycles₁_map_mul_of_isTrivial, cocycles₁IsoOfIsTrivial_inv_hom_apply_coe, H1π_eq_zero_iff, cocyclesMap_comp_isoCocycles₁_hom_apply, cocyclesMk₁_eq, H1π_comp_H1IsoOfIsTrivial_hom_apply, cocyclesOfIsMulCocycle₁_coe, mapCocycles₁_comp_i_assoc, cocycles₁.val_eq_coe, H1π_comp_map_apply, cocycles₁_map_one, δ₀_apply, toCocycles_comp_isoCocycles₁_hom_apply, isoCocycles₁_hom_comp_i, mapCocycles₁_comp_i_apply, π_comp_H1Iso_hom_apply, isoCocycles₁_inv_comp_iCocycles_assoc, H1π_comp_H1IsoOfIsTrivial_hom, coboundaries₁_le_cocycles₁, H1π_comp_map, cocycles₁_ext_iff, H1π_comp_H1IsoOfIsTrivial_hom_assoc, H1π_eq_iff, isoCocycles₁_hom_comp_i_assoc, mapCocycles₁_comp_i, cocycles₁.d₁₂_apply
cocycles₁IsoOfIsTrivial 📖	CompOp	6 math math: H1IsoOfIsTrivial_inv_apply, cocycles₁IsoOfIsTrivial_hom_hom_apply_apply, cocycles₁IsoOfIsTrivial_inv_hom_apply_coe, H1π_comp_H1IsoOfIsTrivial_hom_apply, H1π_comp_H1IsoOfIsTrivial_hom, H1π_comp_H1IsoOfIsTrivial_hom_assoc
cocycles₂ 📖	CompOp	41 math math: instEpiModuleCatH2π, mem_cocycles₂_def, toCocycles_comp_isoCocycles₂_hom_apply, mapCocycles₂_comp_i, cocycles₂.d₂₃_apply, mapCocycles₂_comp_i_apply, cocyclesMap_comp_isoCocycles₂_hom_apply, cocycles₂_map_one_fst, mapCocycles₂_comp_i_assoc, H2π_comp_map_apply, toCocycles_comp_isoCocycles₂_hom, coboundaries₂_le_cocycles₂, d₁₂_apply_mem_cocycles₂, H2π_eq_iff, cocycles₂_map_one_snd, δ₁_apply, cocycles₂_ρ_map_inv_sub_map_inv, H2π_comp_map, isoCocycles₂_hom_comp_i, mem_cocycles₂_iff, H2π_comp_map_assoc, mem_cocycles₂_of_comp_eq_d₁₂, isoCocycles₂_inv_comp_iCocycles_apply, cocyclesMap_comp_isoCocycles₂_hom, cocyclesOfIsMulCocycle₂_coe, coboundariesToCocycles₂_apply, H2π_eq_zero_iff, π_comp_H2Iso_hom_assoc, toCocycles_comp_isoCocycles₂_hom_assoc, cocyclesMap_comp_isoCocycles₂_hom_assoc, cocycles₂.val_eq_coe, isoCocycles₂_inv_comp_iCocycles, cocyclesMk₂_eq, cocycles₂_ext_iff, π_comp_H2Iso_hom_apply, isoCocycles₂_hom_comp_i_apply, cocyclesOfIsCocycle₂_coe, isoCocycles₂_hom_comp_i_assoc, coe_mapCocycles₂, π_comp_H2Iso_hom, isoCocycles₂_inv_comp_iCocycles_assoc
dArrowIso₀₁ 📖	CompOp	4 math math: dArrowIso₀₁_inv_right, dArrowIso₀₁_hom_right, dArrowIso₀₁_inv_left, dArrowIso₀₁_hom_left
d₀₁ 📖	CompOp	20 math math: d₀₁_comp_d₁₂, eq_d₀₁_comp_inv, d₀₁_hom_apply, dArrowIso₀₁_inv_right, dArrowIso₀₁_hom_right, shortComplexH0_g, shortComplexH1_f, d₀₁_apply_mem_cocycles₁, subtype_comp_d₀₁_apply, comp_d₀₁_eq, dArrowIso₀₁_inv_left, dArrowIso₀₁_hom_left, eq_d₀₁_comp_inv_apply, d₀₁_ker_eq_invariants, subtype_comp_d₀₁_assoc, d₀₁_comp_d₁₂_assoc, d₀₁_comp_d₁₂_apply, subtype_comp_d₀₁, eq_d₀₁_comp_inv_assoc, d₀₁_eq_zero
d₁₂ 📖	CompOp	15 math math: d₀₁_comp_d₁₂, eq_d₁₂_comp_inv, d₁₂_hom_apply, comp_d₁₂_eq, d₁₂_comp_d₂₃_apply, eq_d₁₂_comp_inv_apply, d₁₂_apply_mem_cocycles₂, shortComplexH2_f, d₁₂_comp_d₂₃_assoc, d₁₂_comp_d₂₃, d₀₁_comp_d₁₂_assoc, d₀₁_comp_d₁₂_apply, eq_d₁₂_comp_inv_assoc, cocycles₁.d₁₂_apply, shortComplexH1_g
d₂₃ 📖	CompOp	10 math math: d₂₃_hom_apply, cocycles₂.d₂₃_apply, d₁₂_comp_d₂₃_apply, eq_d₂₃_comp_inv_assoc, eq_d₂₃_comp_inv_apply, comp_d₂₃_eq, d₁₂_comp_d₂₃_assoc, d₁₂_comp_d₂₃, eq_d₂₃_comp_inv, shortComplexH2_g
instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCoboundaries₁ 📖	CompOp	3 math math: coboundaries₁.val_eq_coe, coboundaries₁_ext_iff, coboundaries₁.coe_mk
instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCocycles₁ 📖	CompOp	14 math math: coe_mapCocycles₁, coboundariesToCocycles₁_apply, cocycles₁IsoOfIsTrivial_hom_hom_apply_apply, H1IsoOfIsTrivial_H1π_apply_apply, cocycles₁_map_inv, cocycles₁_map_mul_of_isTrivial, H1π_eq_zero_iff, cocyclesMk₁_eq, cocycles₁.val_eq_coe, cocycles₁_map_one, cocycles₁_ext_iff, cocycles₁.coe_mk, H1π_eq_iff, cocycles₁.d₁₂_apply
instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCoboundaries₂ 📖	CompOp	3 math math: coboundaries₂.val_eq_coe, coboundaries₂.coe_mk, coboundaries₂_ext_iff
instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCocycles₂ 📖	CompOp	12 math math: cocycles₂.d₂₃_apply, cocycles₂_map_one_fst, H2π_eq_iff, cocycles₂_map_one_snd, cocycles₂_ρ_map_inv_sub_map_inv, cocycles₂.coe_mk, coboundariesToCocycles₂_apply, H2π_eq_zero_iff, cocycles₂.val_eq_coe, cocyclesMk₂_eq, cocycles₂_ext_iff, coe_mapCocycles₂
isoCocycles₁ 📖	CompOp	16 math math: toCocycles_comp_isoCocycles₁_hom, isoCocycles₁_hom_comp_i_apply, π_comp_H1Iso_hom_assoc, π_comp_H1Iso_hom, cocyclesMap_comp_isoCocycles₁_hom_assoc, isoCocycles₁_inv_comp_iCocycles_apply, cocyclesMap_comp_isoCocycles₁_hom, toCocycles_comp_isoCocycles₁_hom_assoc, isoCocycles₁_inv_comp_iCocycles, cocyclesMap_comp_isoCocycles₁_hom_apply, cocyclesMk₁_eq, toCocycles_comp_isoCocycles₁_hom_apply, isoCocycles₁_hom_comp_i, π_comp_H1Iso_hom_apply, isoCocycles₁_inv_comp_iCocycles_assoc, isoCocycles₁_hom_comp_i_assoc
isoCocycles₂ 📖	CompOp	16 math math: toCocycles_comp_isoCocycles₂_hom_apply, cocyclesMap_comp_isoCocycles₂_hom_apply, toCocycles_comp_isoCocycles₂_hom, isoCocycles₂_hom_comp_i, isoCocycles₂_inv_comp_iCocycles_apply, cocyclesMap_comp_isoCocycles₂_hom, π_comp_H2Iso_hom_assoc, toCocycles_comp_isoCocycles₂_hom_assoc, cocyclesMap_comp_isoCocycles₂_hom_assoc, isoCocycles₂_inv_comp_iCocycles, cocyclesMk₂_eq, π_comp_H2Iso_hom_apply, isoCocycles₂_hom_comp_i_apply, isoCocycles₂_hom_comp_i_assoc, π_comp_H2Iso_hom, isoCocycles₂_inv_comp_iCocycles_assoc
isoShortComplexH1 📖	CompOp	2 math math: isoShortComplexH1_hom, isoShortComplexH1_inv
isoShortComplexH2 📖	CompOp	2 math math: isoShortComplexH2_hom, isoShortComplexH2_inv
shortComplexH0 📖	CompOp	18 math math: cocyclesIso₀_hom_comp_f, H0IsoOfIsTrivial_hom, map_H0Iso_hom_f_apply, cocyclesMap_cocyclesIso₀_hom_f_apply, cocyclesIso₀_inv_comp_iCocycles, shortComplexH0_f, shortComplexH0_g, map_H0Iso_hom_f, cocyclesIso₀_inv_comp_iCocycles_assoc, instMonoModuleCatFShortComplexH0, π_comp_H0IsoOfIsTrivial_hom_apply, cocyclesMap_cocyclesIso₀_hom_f_assoc, cocyclesIso₀_hom_comp_f_assoc, cocyclesMap_cocyclesIso₀_hom_f, cocyclesIso₀_hom_comp_f_apply, shortComplexH0_exact, cocyclesIso₀_inv_comp_iCocycles_apply, map_H0Iso_hom_f_assoc
shortComplexH1 📖	CompOp	28 math math: mapShortComplexH1_τ₂, toCocycles_comp_isoCocycles₁_hom, isoCocycles₁_hom_comp_i_apply, π_comp_H1Iso_hom_assoc, mapShortComplexH1_τ₃, shortComplexH1_f, π_comp_H1Iso_hom, isoCocycles₁_inv_comp_iCocycles_apply, mapShortComplexH1_id, toCocycles_comp_isoCocycles₁_hom_assoc, isoCocycles₁_inv_comp_iCocycles, mapCocycles₁_comp_i_assoc, mapShortComplexH1_id_comp, mapShortComplexH1_comp, isoShortComplexH1_hom, toCocycles_comp_isoCocycles₁_hom_apply, isoCocycles₁_hom_comp_i, mapCocycles₁_comp_i_apply, mapShortComplexH1_id_comp_assoc, mapShortComplexH1_zero, mapShortComplexH1_comp_assoc, π_comp_H1Iso_hom_apply, isoCocycles₁_inv_comp_iCocycles_assoc, isoShortComplexH1_inv, isoCocycles₁_hom_comp_i_assoc, mapShortComplexH1_τ₁, mapCocycles₁_comp_i, shortComplexH1_g
shortComplexH2 📖	CompOp	28 math math: toCocycles_comp_isoCocycles₂_hom_apply, mapCocycles₂_comp_i, mapShortComplexH2_comp_assoc, mapCocycles₂_comp_i_apply, mapCocycles₂_comp_i_assoc, toCocycles_comp_isoCocycles₂_hom, mapShortComplexH2_comp, shortComplexH2_f, isoCocycles₂_hom_comp_i, mapShortComplexH2_zero, isoCocycles₂_inv_comp_iCocycles_apply, mapShortComplexH2_τ₁, mapShortComplexH2_id_comp_assoc, π_comp_H2Iso_hom_assoc, toCocycles_comp_isoCocycles₂_hom_assoc, isoCocycles₂_inv_comp_iCocycles, mapShortComplexH2_τ₂, π_comp_H2Iso_hom_apply, isoShortComplexH2_hom, mapShortComplexH2_id_comp, mapShortComplexH2_id, isoCocycles₂_hom_comp_i_apply, shortComplexH2_g, mapShortComplexH2_τ₃, isoShortComplexH2_inv, isoCocycles₂_hom_comp_i_assoc, π_comp_H2Iso_hom, isoCocycles₂_inv_comp_iCocycles_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
H0IsoOfIsTrivial_hom 📖	mathematical	—	CategoryTheory.Iso.hom ModuleCat CommRing.toRing ModuleCat.moduleCategory H0 Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid H0IsoOfIsTrivial CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ModuleCat.of ModuleCat.carrier Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH0 H0Iso CategoryTheory.ShortComplex.f	—	—
H0IsoOfIsTrivial_inv_apply 📖	mathematical	—	DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid H0 ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.inv H0IsoOfIsTrivial ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Rep.instAddCommGroupCarrierVModuleCat SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ Submodule.addCommGroup Submodule.module H0Iso	—	—
H0_induction_on 📖	—	DFunLike.coe ModuleCat.of CommRing.toRing ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module H0 CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.inv H0Iso	—	—	CategoryTheory.Iso.hom_inv_id_apply
H1IsoOfIsTrivial_H1π_apply_apply 📖	mathematical	—	DFunLike.coe ModuleCat.carrier CommRing.toRing ModuleCat.of AddMonoidHom Additive Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddZeroClass.toAddZero Additive.addZeroClass Monoid.toMulOneClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Rep.instAddCommGroupCarrierVModuleCat AddMonoidHom.instAddCommGroup AddMonoidHom.instModule Ring.toSemiring Additive.addMonoid AddCommGroup.toAddCommMonoid ModuleCat.isModule AddMonoidHom.instFunLike H1 CategoryTheory.ConcreteCategory.hom LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.hom H1IsoOfIsTrivial Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid Pi.Function.module SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module H1π instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCocycles₁ Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.toMul	—	H1π_comp_H1IsoOfIsTrivial_hom_apply
H1IsoOfIsTrivial_inv_apply 📖	mathematical	—	DFunLike.coe ModuleCat.of CommRing.toRing AddMonoidHom Additive ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddZeroClass.toAddZero Additive.addZeroClass Monoid.toMulOneClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Rep.instAddCommGroupCarrierVModuleCat AddMonoidHom.instAddCommGroup AddMonoidHom.instModule Ring.toSemiring Additive.addMonoid AddCommGroup.toAddCommMonoid ModuleCat.isModule H1 CategoryTheory.ConcreteCategory.hom LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.inv H1IsoOfIsTrivial Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid Pi.Function.module SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module H1π cocycles₁IsoOfIsTrivial	—	—
H1_induction_on 📖	—	DFunLike.coe ModuleCat.of CommRing.toRing Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module H1 CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier H1π	—	—	groupCohomology_induction_on CategoryTheory.Iso.hom_inv_id_apply
H1π_comp_H1IsoOfIsTrivial_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module H1 AddMonoidHom Additive AddZeroClass.toAddZero Additive.addZeroClass Monoid.toMulOneClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddMonoidHom.instAddCommGroup AddMonoidHom.instModule Ring.toSemiring Additive.addMonoid H1π CategoryTheory.Iso.hom H1IsoOfIsTrivial cocycles₁IsoOfIsTrivial	—	CategoryTheory.Category.assoc HomologicalComplex.isoHomologyπ_hom_inv_id_assoc CategoryTheory.Iso.inv_hom_id_assoc
H1π_comp_H1IsoOfIsTrivial_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier H1 AddMonoidHom Additive Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddZeroClass.toAddZero Additive.addZeroClass Monoid.toMulOneClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Rep.instAddCommGroupCarrierVModuleCat AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup AddMonoidHom.instAddCommGroup ModuleCat.isModule AddMonoidHom.instModule Additive.addMonoid LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom H1IsoOfIsTrivial Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid Pi.Function.module SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module H1π cocycles₁IsoOfIsTrivial	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise H1π_comp_H1IsoOfIsTrivial_hom
H1π_comp_H1IsoOfIsTrivial_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module H1 H1π AddMonoidHom Additive AddZeroClass.toAddZero Additive.addZeroClass Monoid.toMulOneClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddMonoidHom.instAddCommGroup AddMonoidHom.instModule Ring.toSemiring Additive.addMonoid CategoryTheory.Iso.hom H1IsoOfIsTrivial cocycles₁IsoOfIsTrivial	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' H1π_comp_H1IsoOfIsTrivial_hom
H1π_eq_iff 📖	mathematical	—	DFunLike.coe ModuleCat.of CommRing.toRing Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module H1 CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier H1π coboundaries₁ Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCocycles₁	—	sub_eq_zero map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass H1π_eq_zero_iff
H1π_eq_zero_iff 📖	mathematical	—	DFunLike.coe ModuleCat.of CommRing.toRing Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module H1 CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier H1π NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid coboundaries₁ instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCocycles₁	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.ShortComplex.leftHomologyπ_naturality'_assoc RingHomCompTriple.ids map_eq_zero_iff ModuleCat.mono_iff_injective AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.isIso_inv d₀₁_comp_d₁₂ LinearMap.range_codRestrict CategoryTheory.ShortComplex.moduleCat_zero_apply
H2_induction_on 📖	—	DFunLike.coe ModuleCat.of CommRing.toRing Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ Submodule.addCommGroup Pi.addCommGroup Submodule.module H2 CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier H2π	—	—	groupCohomology_induction_on CategoryTheory.Iso.hom_inv_id_apply
H2π_eq_iff 📖	mathematical	—	DFunLike.coe ModuleCat.of CommRing.toRing Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ Submodule.addCommGroup Pi.addCommGroup Submodule.module H2 CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier H2π coboundaries₂ Pi.instSub SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCocycles₂	—	sub_eq_zero map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass H2π_eq_zero_iff
H2π_eq_zero_iff 📖	mathematical	—	DFunLike.coe ModuleCat.of CommRing.toRing Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ Submodule.addCommGroup Pi.addCommGroup Submodule.module H2 CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier H2π NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid coboundaries₂ instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCocycles₂	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.ShortComplex.leftHomologyπ_naturality'_assoc RingHomCompTriple.ids map_eq_zero_iff ModuleCat.mono_iff_injective AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Iso.isIso_inv d₁₂_comp_d₂₃ LinearMap.range_codRestrict CategoryTheory.ShortComplex.moduleCat_zero_apply
coboundariesOfIsCoboundary₁_coe 📖	mathematical	IsCoboundary₁ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid Group.toDivInvMonoid	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory Rep.ofDistribMulAction AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike coboundaries₁ coboundariesOfIsCoboundary₁	—	—
coboundariesOfIsCoboundary₂_coe 📖	mathematical	IsCoboundary₂ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory Rep.ofDistribMulAction AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike coboundaries₂ coboundariesOfIsCoboundary₂	—	—
coboundariesOfIsMulCoboundary₁_coe 📖	mathematical	IsMulCoboundary₁ SemigroupAction.toSMul Monoid.toSemigroup DivInvMonoid.toMonoid Group.toDivInvMonoid MulAction.toSemigroupAction MulDistribMulAction.toMulAction CommGroup.toGroup	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory Rep.ofMulDistribMulAction AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike coboundaries₁ coboundariesOfIsMulCoboundary₁ DFunLike.coe Equiv Additive EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul	—	—
coboundariesToCocycles₁_apply 📖	mathematical	—	DFunLike.coe Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCocycles₁ LinearMap RingHom.id Semiring.toNonAssocSemiring coboundaries₁ Submodule.addCommMonoid Submodule.module LinearMap.instFunLike coboundariesToCocycles₁	—	—
coboundariesToCocycles₂_apply 📖	mathematical	—	DFunLike.coe Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCocycles₂ LinearMap RingHom.id Semiring.toNonAssocSemiring coboundaries₂ Submodule.addCommMonoid Submodule.module LinearMap.instFunLike coboundariesToCocycles₂	—	—
coboundaries₁_eq_bot_of_isTrivial 📖	mathematical	—	coboundaries₁ Bot.bot Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule Submodule.instBot	—	LinearMap.range.congr_simp d₀₁_eq_zero LinearMap.range_eq_bot
coboundaries₁_ext 📖	—	DFunLike.coe Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike coboundaries₁ instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCoboundaries₁	—	—	DFunLike.ext
coboundaries₁_ext_iff 📖	mathematical	—	DFunLike.coe Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike coboundaries₁ instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCoboundaries₁	—	coboundaries₁_ext
coboundaries₁_le_cocycles₁ 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder coboundaries₁ cocycles₁	—	d₀₁_apply_mem_cocycles₁
coboundaries₂_ext 📖	—	DFunLike.coe Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike coboundaries₂ instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCoboundaries₂	—	—	DFunLike.ext
coboundaries₂_ext_iff 📖	mathematical	—	DFunLike.coe Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike coboundaries₂ instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCoboundaries₂	—	coboundaries₂_ext
coboundaries₂_le_cocycles₂ 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder coboundaries₂ cocycles₂	—	d₁₂_apply_mem_cocycles₂
cocyclesIso₀_hom_comp_f 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles ModuleCat.of ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH0 CategoryTheory.Iso.hom cocyclesIso₀ CategoryTheory.ShortComplex.f HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains iCocycles cochainsIso₀	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Limits.KernelFork.mapOfIsLimit_ι shortComplexH0_exact instMonoModuleCatFShortComplexH0
cocyclesIso₀_hom_comp_f_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH0 Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.ShortComplex.f cocycles CategoryTheory.Iso.hom cocyclesIso₀ Pi.addCommGroup Pi.Function.module cochainsIso₀ iCocycles	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise cocyclesIso₀_hom_comp_f
cocyclesIso₀_hom_comp_f_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles ModuleCat.of ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module CategoryTheory.Iso.hom cocyclesIso₀ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH0 CategoryTheory.ShortComplex.f HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains iCocycles cochainsIso₀	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cocyclesIso₀_hom_comp_f
cocyclesIso₀_inv_comp_iCocycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module cocycles HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains CategoryTheory.Iso.inv cocyclesIso₀ iCocycles CategoryTheory.ShortComplex.X₁ shortComplexH0 CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f cochainsIso₀	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Iso.inv_comp_eq CategoryTheory.Category.assoc CategoryTheory.Iso.eq_comp_inv cocyclesIso₀_hom_comp_f
cocyclesIso₀_inv_comp_iCocycles_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier cocycles AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup Pi.addCommGroup Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule Pi.Function.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of iCocycles Submodule CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ Submodule.addCommGroup Submodule.module CategoryTheory.Iso.inv cocyclesIso₀ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH0 cochainsIso₀ CategoryTheory.ShortComplex.f	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise cocyclesIso₀_inv_comp_iCocycles
cocyclesIso₀_inv_comp_iCocycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module cocycles CategoryTheory.Iso.inv cocyclesIso₀ HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains iCocycles CategoryTheory.ShortComplex.X₂ shortComplexH0 CategoryTheory.ShortComplex.f cochainsIso₀	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' cocyclesIso₀_inv_comp_iCocycles
cocyclesMk₀_eq 📖	mathematical	—	cocyclesMk DFunLike.coe Action.V ModuleCat CommRing.toRing ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.inv cochainsIso₀ Submodule CommSemiring.toSemiring CommRing.toCommSemiring Rep.instAddCommGroupCarrierVModuleCat SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ ModuleCat.of Submodule.addCommGroup Submodule.module cocycles cocyclesIso₀	—	AddRightCancelSemigroup.toIsRightCancelAdd ModuleCat.mono_iff_injective HomologicalComplex.instMonoICycles cocyclesIso₀_inv_comp_iCocycles_apply
cocyclesMk₁_eq 📖	mathematical	—	cocyclesMk DFunLike.coe ModuleCat.of CommRing.toRing Pi.addCommGroup ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains CategoryTheory.ConcreteCategory.hom LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.inv cochainsIso₁ Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid SetLike.instMembership Submodule.setLike cocycles₁ instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCocycles₁ Submodule.addCommGroup Submodule.module cocycles isoCocycles₁	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian AddCommGrpCat.mono_iff_injective CategoryTheory.Functor.map_mono CategoryTheory.ConcreteCategory.forget₂_preservesMonomorphisms ModuleCat.forget_preservesMonomorphisms HomologicalComplex.instMonoICycles HomologicalComplex.i_cyclesMk isoCocycles₁_inv_comp_iCocycles_apply
cocyclesMk₂_eq 📖	mathematical	—	cocyclesMk DFunLike.coe ModuleCat.of CommRing.toRing Pi.addCommGroup ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains CategoryTheory.ConcreteCategory.hom LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.inv cochainsIso₂ Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid SetLike.instMembership Submodule.setLike cocycles₂ instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCocycles₂ Submodule.addCommGroup Submodule.module cocycles isoCocycles₂	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian AddCommGrpCat.mono_iff_injective CategoryTheory.Functor.map_mono CategoryTheory.ConcreteCategory.forget₂_preservesMonomorphisms ModuleCat.forget_preservesMonomorphisms HomologicalComplex.instMonoICycles HomologicalComplex.i_cyclesMk isoCocycles₂_inv_comp_iCocycles_apply
cocyclesOfIsCocycle₁_coe 📖	mathematical	IsCocycle₁ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory Rep.ofDistribMulAction AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ cocyclesOfIsCocycle₁	—	—
cocyclesOfIsCocycle₂_coe 📖	mathematical	IsCocycle₂ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory Rep.ofDistribMulAction AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ cocyclesOfIsCocycle₂	—	—
cocyclesOfIsMulCocycle₁_coe 📖	mathematical	IsMulCocycle₁ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction MulDistribMulAction.toMulAction CommGroup.toGroup	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory Rep.ofMulDistribMulAction AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ cocyclesOfIsMulCocycle₁ DFunLike.coe Equiv Additive EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul	—	—
cocyclesOfIsMulCocycle₂_coe 📖	mathematical	IsMulCocycle₂ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction MulDistribMulAction.toMulAction CommGroup.toGroup	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory Rep.ofMulDistribMulAction AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ cocyclesOfIsMulCocycle₂ DFunLike.coe Equiv Additive EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul	—	—
cocycles₁IsoOfIsTrivial_hom_hom_apply_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom Additive ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddZeroClass.toAddZero Additive.addZeroClass Monoid.toMulOneClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Rep.instAddCommGroupCarrierVModuleCat AddMonoidHom.instFunLike LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid AddCommGroup.toAddCommMonoid Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup AddMonoidHom.instAddCommGroup Submodule.module AddMonoidHom.instModule Additive.addMonoid LinearMap.instFunLike ModuleCat.Hom.hom ModuleCat.of CategoryTheory.Iso.hom cocycles₁IsoOfIsTrivial instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCocycles₁ Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.toMul	—	—
cocycles₁IsoOfIsTrivial_inv_hom_apply_coe 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddMonoidHom Additive AddZeroClass.toAddZero Additive.addZeroClass Monoid.toMulOneClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddMonoidHom.instAddCommGroup Submodule.addCommGroup Pi.addCommGroup AddMonoidHom.instModule Additive.addMonoid Submodule.module LinearMap.instFunLike ModuleCat.Hom.hom ModuleCat.of CategoryTheory.Iso.inv cocycles₁IsoOfIsTrivial AddMonoidHom.instFunLike	—	—
cocycles₁_ext 📖	—	DFunLike.coe Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCocycles₁	—	—	DFunLike.ext
cocycles₁_ext_iff 📖	mathematical	—	DFunLike.coe Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCocycles₁	—	cocycles₁_ext
cocycles₁_map_inv 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ Submodule Pi.addCommMonoid Pi.Function.module SetLike.instMembership Submodule.setLike cocycles₁ instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCocycles₁ InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	add_eq_zero_iff_eq_neg cocycles₁_map_one mul_inv_cancel mem_cocycles₁_iff
cocycles₁_map_mul_of_isTrivial 📖	mathematical	—	DFunLike.coe Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCocycles₁ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	mem_cocycles₁_iff Representation.isTrivial_apply add_comm
cocycles₁_map_one 📖	mathematical	—	DFunLike.coe Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCocycles₁ InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	mem_cocycles₁_def map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass mul_one sub_self zero_add
cocycles₂_ext 📖	—	DFunLike.coe Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCocycles₂	—	—	DFunLike.ext
cocycles₂_ext_iff 📖	mathematical	—	DFunLike.coe Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCocycles₂	—	cocycles₂_ext
cocycles₂_map_one_fst 📖	mathematical	—	DFunLike.coe Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCocycles₂ InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	mem_cocycles₂_iff map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass one_mul AddLeftCancelSemigroup.toIsLeftCancelAdd
cocycles₂_map_one_snd 📖	mathematical	—	DFunLike.coe Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCocycles₂ InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ	—	mem_cocycles₂_iff mul_one AddRightCancelSemigroup.toIsRightCancelAdd
cocycles₂_ρ_map_inv_sub_map_inv 📖	mathematical	—	ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Rep.instAddCommGroupCarrierVModuleCat DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ Submodule Pi.addCommMonoid Pi.Function.module SetLike.instMembership Submodule.setLike cocycles₂ instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCocycles₂ InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid InvOneClass.toOne	—	mem_cocycles₂_iff sub_eq_sub_iff_add_eq_add mul_inv_cancel cocycles₂_map_one_fst inv_mul_cancel
comp_d₀₁_eq 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid ModuleCat.of Pi.addCommGroup ModuleCat.carrier Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule CategoryTheory.Iso.hom cochainsIso₀ d₀₁ HomologicalComplex.d cochainsIso₁	—	ModuleCat.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd LinearMap.ext Fin.isEmpty' Finset.sum_congr zero_add pow_one neg_smul one_smul Finset.sum_singleton sub_eq_add_neg
comp_d₁₂_eq 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains ModuleCat.of Pi.addCommGroup ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule CategoryTheory.Iso.hom cochainsIso₁ d₁₂ HomologicalComplex.d cochainsIso₂	—	ModuleCat.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd LinearMap.ext Fin.sum_univ_two sub_eq_add_neg add_assoc zero_add pow_one neg_smul one_smul neg_one_sq
comp_d₂₃_eq 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains ModuleCat.of Pi.addCommGroup ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule CategoryTheory.Iso.hom cochainsIso₂ d₂₃ HomologicalComplex.d cochainsIso₃	—	ModuleCat.hom_ext AddRightCancelSemigroup.toIsRightCancelAdd LinearMap.ext Fin.sum_univ_three sub_eq_add_neg add_assoc zero_add pow_one neg_smul one_smul neg_sq one_pow pow_succ' mul_one Fintype.complete
dArrowIso₀₁_hom_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.id HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne inhomogeneousCochains HomologicalComplex.d Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid ModuleCat.of Pi.addCommGroup ModuleCat.carrier Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule d₀₁ CategoryTheory.Iso.hom CategoryTheory.Arrow CategoryTheory.instCategoryArrow AddRightCancelSemigroup.toIsRightCancelAdd dArrowIso₀₁ cochainsIso₀	—	AddRightCancelSemigroup.toIsRightCancelAdd
dArrowIso₀₁_hom_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.id HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne inhomogeneousCochains HomologicalComplex.d Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid ModuleCat.of Pi.addCommGroup ModuleCat.carrier Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule d₀₁ CategoryTheory.Iso.hom CategoryTheory.Arrow CategoryTheory.instCategoryArrow AddRightCancelSemigroup.toIsRightCancelAdd dArrowIso₀₁ cochainsIso₁	—	AddRightCancelSemigroup.toIsRightCancelAdd
dArrowIso₀₁_inv_left 📖	mathematical	—	CategoryTheory.CommaMorphism.left ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.id Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid ModuleCat.of Pi.addCommGroup ModuleCat.carrier Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule d₀₁ HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne inhomogeneousCochains HomologicalComplex.d CategoryTheory.Iso.inv CategoryTheory.Arrow CategoryTheory.instCategoryArrow AddRightCancelSemigroup.toIsRightCancelAdd dArrowIso₀₁ cochainsIso₀	—	AddRightCancelSemigroup.toIsRightCancelAdd
dArrowIso₀₁_inv_right 📖	mathematical	—	CategoryTheory.CommaMorphism.right ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Functor.id Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid ModuleCat.of Pi.addCommGroup ModuleCat.carrier Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule d₀₁ HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid Nat.instOne inhomogeneousCochains HomologicalComplex.d CategoryTheory.Iso.inv CategoryTheory.Arrow CategoryTheory.instCategoryArrow AddRightCancelSemigroup.toIsRightCancelAdd dArrowIso₀₁ cochainsIso₁	—	AddRightCancelSemigroup.toIsRightCancelAdd
d₀₁_apply_mem_cocycles₁ 📖	mathematical	—	ModuleCat.carrier CommRing.toRing ModuleCat.of Pi.addCommGroup Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid SetLike.instMembership Submodule.setLike cocycles₁ DFunLike.coe CategoryTheory.ConcreteCategory.hom LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier d₀₁	—	d₀₁_comp_d₁₂_apply
d₀₁_comp_d₁₂ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid ModuleCat.of Pi.addCommGroup ModuleCat.carrier Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule d₀₁ d₁₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver ModuleCat.instZeroHom	—	ModuleCat.hom_ext LinearMap.ext map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass sub_sub_sub_cancel_left sub_add_sub_cancel sub_self Pi.zero_apply
d₀₁_comp_d₁₂_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Pi.addCommGroup ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.isAddCommGroup ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of d₁₂ d₀₁ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise d₀₁_comp_d₁₂
d₀₁_comp_d₁₂_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid ModuleCat.of Pi.addCommGroup ModuleCat.carrier Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule d₀₁ d₁₂ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver ModuleCat.instZeroHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d₀₁_comp_d₁₂
d₀₁_eq_zero 📖	mathematical	—	d₀₁ Quiver.Hom ModuleCat CommRing.toRing CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid ModuleCat.of Pi.addCommGroup ModuleCat.carrier Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule ModuleCat.instZeroHom	—	ModuleCat.hom_ext LinearMap.ext d₀₁_hom_apply Representation.isTrivial_apply sub_self
d₀₁_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup Pi.addCommGroup Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule Pi.Function.module LinearMap.instFunLike ModuleCat.Hom.hom ModuleCat.of d₀₁ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CommSemiring.toSemiring CommRing.toCommSemiring Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ	—	—
d₀₁_ker_eq_invariants 📖	mathematical	—	LinearMap.ker ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid ModuleCat.of Pi.addCommGroup Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule ModuleCat.isAddCommGroup RingHom.id Semiring.toNonAssocSemiring ModuleCat.Hom.hom d₀₁ Representation.invariants CommRing.toCommSemiring Rep.ρ	—	Submodule.ext sub_eq_zero
d₁₂_apply_mem_cocycles₂ 📖	mathematical	—	ModuleCat.carrier CommRing.toRing ModuleCat.of Pi.addCommGroup Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid SetLike.instMembership Submodule.setLike cocycles₂ DFunLike.coe CategoryTheory.ConcreteCategory.hom LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier d₁₂	—	d₁₂_comp_d₂₃_apply
d₁₂_comp_d₂₃ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Pi.addCommGroup ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule d₁₂ d₂₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver ModuleCat.instZeroHom	—	ModuleCat.hom_ext LinearMap.ext d₂₃_hom_apply map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass mul_assoc Pi.zero_apply Mathlib.Tactic.Abel.unfold_sub 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.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Abel.zero_termg
d₁₂_comp_d₂₃_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Pi.addCommGroup ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.isAddCommGroup ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of d₂₃ d₁₂ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise d₁₂_comp_d₂₃
d₁₂_comp_d₂₃_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Pi.addCommGroup ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule d₁₂ d₂₃ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver ModuleCat.instZeroHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' d₁₂_comp_d₂₃
d₁₂_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Pi.addCommGroup ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule LinearMap.instFunLike ModuleCat.Hom.hom ModuleCat.of d₁₂ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CommSemiring.toSemiring CommRing.toCommSemiring Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ MulOne.toMul	—	—
d₂₃_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Pi.addCommGroup ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule LinearMap.instFunLike ModuleCat.Hom.hom ModuleCat.of d₂₃ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup CommSemiring.toSemiring CommRing.toCommSemiring Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ MulOne.toMul	—	—
eq_d₀₁_comp_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains CategoryTheory.Iso.inv cochainsIso₀ HomologicalComplex.d ModuleCat.of Pi.addCommGroup ModuleCat.carrier Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule d₀₁ cochainsIso₁	—	CategoryTheory.CommSq.w AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CommSq.horiz_inv comp_d₀₁_eq
eq_d₀₁_comp_inv_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Pi.addCommGroup ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.isAddCommGroup ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of HomologicalComplex.d CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains CategoryTheory.Iso.inv cochainsIso₀ cochainsIso₁ d₀₁	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise eq_d₀₁_comp_inv
eq_d₀₁_comp_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains CategoryTheory.Iso.inv cochainsIso₀ HomologicalComplex.d ModuleCat.of Pi.addCommGroup ModuleCat.carrier Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule d₀₁ cochainsIso₁	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eq_d₀₁_comp_inv
eq_d₁₂_comp_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Pi.addCommGroup ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains CategoryTheory.Iso.inv cochainsIso₁ HomologicalComplex.d d₁₂ cochainsIso₂	—	CategoryTheory.CommSq.w AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CommSq.horiz_inv comp_d₁₂_eq
eq_d₁₂_comp_inv_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Pi.addCommGroup ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.isAddCommGroup ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of HomologicalComplex.d CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains CategoryTheory.Iso.inv cochainsIso₁ cochainsIso₂ d₁₂	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise eq_d₁₂_comp_inv
eq_d₁₂_comp_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Pi.addCommGroup ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains CategoryTheory.Iso.inv cochainsIso₁ HomologicalComplex.d d₁₂ cochainsIso₂	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eq_d₁₂_comp_inv
eq_d₂₃_comp_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Pi.addCommGroup ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains CategoryTheory.Iso.inv cochainsIso₂ HomologicalComplex.d d₂₃ cochainsIso₃	—	CategoryTheory.CommSq.w AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CommSq.horiz_inv comp_d₂₃_eq
eq_d₂₃_comp_inv_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid Pi.addCommGroup ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.isAddCommGroup ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of HomologicalComplex.d CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains CategoryTheory.Iso.inv cochainsIso₂ cochainsIso₃ d₂₃	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise eq_d₂₃_comp_inv
eq_d₂₃_comp_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Pi.addCommGroup ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains CategoryTheory.Iso.inv cochainsIso₂ HomologicalComplex.d d₂₃ cochainsIso₃	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' eq_d₂₃_comp_inv
instEpiModuleCatH1π 📖	mathematical	—	CategoryTheory.Epi ModuleCat CommRing.toRing ModuleCat.moduleCategory ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module H1 H1π	—	CategoryTheory.epi_comp CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv HomologicalComplex.instEpiHomologyπ
instEpiModuleCatH2π 📖	mathematical	—	CategoryTheory.Epi ModuleCat CommRing.toRing ModuleCat.moduleCategory ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ Submodule.addCommGroup Pi.addCommGroup Submodule.module H2 H2π	—	CategoryTheory.epi_comp CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.Iso.isIso_inv HomologicalComplex.instEpiHomologyπ
instMonoModuleCatFShortComplexH0 📖	mathematical	—	CategoryTheory.Mono ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.ShortComplex.X₁ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH0 CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.f	—	ModuleCat.mono_iff_injective Submodule.injective_subtype
isCoboundary₁_of_mem_coboundaries₁ 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.ofDistribMulAction AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike coboundaries₁	IsCoboundary₁ SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	—
isCoboundary₂_of_mem_coboundaries₂ 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.ofDistribMulAction AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike coboundaries₂	IsCoboundary₂ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	—
isCocycle₁_of_mem_cocycles₁ 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.ofDistribMulAction AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁	IsCocycle₁ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	mem_cocycles₁_iff
isCocycle₂_of_mem_cocycles₂ 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.ofDistribMulAction AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂	IsCocycle₂ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	mem_cocycles₂_iff
isMulCoboundary₁_of_mem_coboundaries₁ 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.ofMulDistribMulAction AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike coboundaries₁	IsMulCoboundary₁ SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction MulDistribMulAction.toMulAction CommGroup.toGroup DFunLike.coe Equiv Additive EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul	—	—
isMulCoboundary₂_of_mem_coboundaries₂ 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.ofMulDistribMulAction AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike coboundaries₂	IsMulCoboundary₂ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction MulDistribMulAction.toMulAction CommGroup.toGroup Additive DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.toMul	—	—
isMulCocycle₁_of_mem_cocycles₁ 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.ofMulDistribMulAction AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁	IsMulCocycle₁ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction MulDistribMulAction.toMulAction CommGroup.toGroup Additive DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.toMul	—	mem_cocycles₁_iff
isMulCocycle₂_of_mem_cocycles₂ 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Int.instCommRing Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.ofMulDistribMulAction AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂	IsMulCocycle₂ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction MulDistribMulAction.toMulAction CommGroup.toGroup Additive DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.toMul	—	mem_cocycles₂_iff
isoCocycles₁_hom_comp_i 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 CategoryTheory.Iso.hom isoCocycles₁ CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.moduleCatLeftHomologyData HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains Ring.toSemiring iCocycles cochainsIso₁	—	comp_d₀₁_eq comp_d₁₂_eq CategoryTheory.ShortComplex.cyclesMap'_i CategoryTheory.Category.id_comp
isoCocycles₁_hom_comp_i_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 Submodule.addCommGroup Pi.addCommGroup ModuleCat.isAddCommGroup Submodule.module LinearMap.instFunLike Submodule.subtype LinearMap.ker CategoryTheory.ShortComplex.X₃ ModuleCat.Hom.hom CategoryTheory.ShortComplex.g cocycles CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom isoCocycles₁ cochainsIso₁ iCocycles	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise isoCocycles₁_hom_comp_i
isoCocycles₁_hom_comp_i_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module CategoryTheory.Iso.hom isoCocycles₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.moduleCatLeftHomologyData HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains iCocycles Ring.toSemiring cochainsIso₁	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoCocycles₁_hom_comp_i
isoCocycles₁_inv_comp_iCocycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module cocycles HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains CategoryTheory.Iso.inv isoCocycles₁ iCocycles CategoryTheory.ShortComplex.LeftHomologyData.K shortComplexH1 CategoryTheory.ShortComplex.moduleCatLeftHomologyData CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.LeftHomologyData.i Ring.toSemiring cochainsIso₁	—	CategoryTheory.CommSq.w AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CommSq.horiz_inv isoCocycles₁_hom_comp_i
isoCocycles₁_inv_comp_iCocycles_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier cocycles AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup Pi.addCommGroup Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule Pi.Function.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of iCocycles Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Submodule.module CategoryTheory.Iso.inv isoCocycles₁ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 cochainsIso₁ Submodule.subtype LinearMap.ker CategoryTheory.ShortComplex.X₃ ModuleCat.Hom.hom CategoryTheory.ShortComplex.g	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise isoCocycles₁_inv_comp_iCocycles
isoCocycles₁_inv_comp_iCocycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module cocycles CategoryTheory.Iso.inv isoCocycles₁ HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains iCocycles CategoryTheory.ShortComplex.X₂ shortComplexH1 CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.moduleCatLeftHomologyData Ring.toSemiring cochainsIso₁	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoCocycles₁_inv_comp_iCocycles
isoCocycles₂_hom_comp_i 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ Submodule.addCommGroup Pi.addCommGroup Submodule.module CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 CategoryTheory.Iso.hom isoCocycles₂ CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.moduleCatLeftHomologyData HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains Ring.toSemiring iCocycles cochainsIso₂	—	comp_d₁₂_eq comp_d₂₃_eq CategoryTheory.ShortComplex.cyclesMap'_i CategoryTheory.Category.id_comp
isoCocycles₂_hom_comp_i_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 Submodule.addCommGroup Pi.addCommGroup ModuleCat.isAddCommGroup Submodule.module LinearMap.instFunLike Submodule.subtype LinearMap.ker CategoryTheory.ShortComplex.X₃ ModuleCat.Hom.hom CategoryTheory.ShortComplex.g cocycles CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom isoCocycles₂ cochainsIso₂ iCocycles	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise isoCocycles₂_hom_comp_i
isoCocycles₂_hom_comp_i_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ Submodule.addCommGroup Pi.addCommGroup Submodule.module CategoryTheory.Iso.hom isoCocycles₂ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.moduleCatLeftHomologyData HomologicalComplex.X ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains iCocycles Ring.toSemiring cochainsIso₂	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoCocycles₂_hom_comp_i
isoCocycles₂_inv_comp_iCocycles 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ Submodule.addCommGroup Pi.addCommGroup Submodule.module cocycles HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains CategoryTheory.Iso.inv isoCocycles₂ iCocycles CategoryTheory.ShortComplex.LeftHomologyData.K shortComplexH2 CategoryTheory.ShortComplex.moduleCatLeftHomologyData CategoryTheory.ShortComplex.X₂ CategoryTheory.ShortComplex.LeftHomologyData.i Ring.toSemiring cochainsIso₂	—	CategoryTheory.CommSq.w AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CommSq.horiz_inv isoCocycles₂_hom_comp_i
isoCocycles₂_inv_comp_iCocycles_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier cocycles AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup Pi.addCommGroup Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule Pi.Function.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of iCocycles Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid SetLike.instMembership Submodule.setLike cocycles₂ Submodule.addCommGroup Submodule.module CategoryTheory.Iso.inv isoCocycles₂ CategoryTheory.ShortComplex.X₂ CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 cochainsIso₂ Submodule.subtype LinearMap.ker CategoryTheory.ShortComplex.X₃ ModuleCat.Hom.hom CategoryTheory.ShortComplex.g	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise isoCocycles₂_inv_comp_iCocycles
isoCocycles₂_inv_comp_iCocycles_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ Submodule.addCommGroup Pi.addCommGroup Submodule.module cocycles CategoryTheory.Iso.inv isoCocycles₂ HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains iCocycles CategoryTheory.ShortComplex.X₂ shortComplexH2 CategoryTheory.ShortComplex.LeftHomologyData.i CategoryTheory.ShortComplex.moduleCatLeftHomologyData Ring.toSemiring cochainsIso₂	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoCocycles₂_inv_comp_iCocycles
isoShortComplexH1_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.ShortComplex ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.instCategory HomologicalComplex.sc ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains shortComplexH1 isoShortComplexH1 CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.sc' CategoryTheory.NatTrans.app HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.shortComplexFunctor HomologicalComplex.shortComplexFunctor' CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.natIsoSc' CategoryTheory.ShortComplex.isoMk cochainsIso₀ cochainsIso₁ cochainsIso₂ comp_d₀₁_eq comp_d₁₂_eq	—	AddRightCancelSemigroup.toIsRightCancelAdd
isoShortComplexH1_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.ShortComplex ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.instCategory HomologicalComplex.sc ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains shortComplexH1 isoShortComplexH1 CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.sc' CategoryTheory.ShortComplex.homMk ModuleCat.of Pi.addCommGroup ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule CategoryTheory.ShortComplex.X₁ cochainsIso₀ CategoryTheory.ShortComplex.X₂ cochainsIso₁ CategoryTheory.ShortComplex.X₃ cochainsIso₂ comp_d₀₁_eq comp_d₁₂_eq CategoryTheory.NatTrans.app HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.shortComplexFunctor' HomologicalComplex.shortComplexFunctor CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.natIsoSc'	—	AddRightCancelSemigroup.toIsRightCancelAdd
isoShortComplexH2_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.ShortComplex ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.instCategory HomologicalComplex.sc ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains shortComplexH2 isoShortComplexH2 CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.sc' CategoryTheory.NatTrans.app HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.shortComplexFunctor HomologicalComplex.shortComplexFunctor' CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.natIsoSc' CategoryTheory.ShortComplex.isoMk cochainsIso₁ cochainsIso₂ cochainsIso₃ comp_d₁₂_eq comp_d₂₃_eq	—	AddRightCancelSemigroup.toIsRightCancelAdd
isoShortComplexH2_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.ShortComplex ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive CategoryTheory.ShortComplex.instCategory HomologicalComplex.sc ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains shortComplexH2 isoShortComplexH2 CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct HomologicalComplex.sc' CategoryTheory.ShortComplex.homMk ModuleCat.of Pi.addCommGroup ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule CategoryTheory.ShortComplex.X₁ cochainsIso₁ CategoryTheory.ShortComplex.X₂ cochainsIso₂ CategoryTheory.ShortComplex.X₃ cochainsIso₃ comp_d₁₂_eq comp_d₂₃_eq CategoryTheory.NatTrans.app HomologicalComplex HomologicalComplex.instCategory HomologicalComplex.shortComplexFunctor' HomologicalComplex.shortComplexFunctor CategoryTheory.Functor CategoryTheory.Functor.category HomologicalComplex.natIsoSc'	—	AddRightCancelSemigroup.toIsRightCancelAdd
map_inv_of_isCocycle₁ 📖	mathematical	IsCocycle₁ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	add_eq_zero_iff_eq_neg map_one_of_isCocycle₁ mul_inv_cancel
map_inv_of_isMulCocycle₁ 📖	mathematical	IsMulCocycle₁ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	mul_eq_one_iff_eq_inv map_one_of_isMulCocycle₁ mul_inv_cancel
map_one_fst_of_isCocycle₂ 📖	mathematical	IsCocycle₂ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	MulOne.toOne	—	one_smul one_mul mul_one AddLeftCancelSemigroup.toIsLeftCancelAdd
map_one_fst_of_isMulCocycle₂ 📖	mathematical	IsMulCocycle₂ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	MulOne.toOne	—	one_smul one_mul mul_one LeftCancelSemigroup.toIsLeftCancelMul
map_one_of_isCocycle₁ 📖	mathematical	IsCocycle₁ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	MulOne.toOne NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	mul_one one_smul AddLeftCancelSemigroup.toIsLeftCancelAdd
map_one_of_isMulCocycle₁ 📖	mathematical	IsMulCocycle₁ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	MulOne.toOne InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroup.toDivisionCommMonoid	—	mul_one one_smul LeftCancelSemigroup.toIsLeftCancelMul
map_one_snd_of_isCocycle₂ 📖	mathematical	IsCocycle₂ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	MulOne.toOne	—	mul_one AddRightCancelSemigroup.toIsRightCancelAdd
map_one_snd_of_isMulCocycle₂ 📖	mathematical	IsMulCocycle₂ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	MulOne.toOne	—	mul_one RightCancelSemigroup.toIsRightCancelMul
mem_cocycles₁_def 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ MulOne.toMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	LinearMap.mem_ker
mem_cocycles₁_iff 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ	—	sub_add_eq_add_sub
mem_cocycles₁_of_addMonoidHom 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Additive DFunLike.coe AddMonoidHom AddZeroClass.toAddZero Additive.addZeroClass Monoid.toMulOneClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddMonoidHom.instFunLike Equiv EquivLike.toFunLike Equiv.instEquivLike Additive.ofMul	—	mem_cocycles₁_iff map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass add_comm Representation.isTrivial_apply
mem_cocycles₂_def 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ MulOne.toMul NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	LinearMap.mem_ker d₂₃_hom_apply
mem_cocycles₂_iff 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring Rep.ρ	—	sub_add_eq_add_sub add_comm
shortComplexH0_exact 📖	mathematical	—	CategoryTheory.ShortComplex.Exact ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH0	—	CategoryTheory.ShortComplex.moduleCat_exact_iff sub_eq_zero
shortComplexH0_f 📖	mathematical	—	CategoryTheory.ShortComplex.f ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH0 ModuleCat.ofHom ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module Submodule.subtype	—	—
shortComplexH0_g 📖	mathematical	—	CategoryTheory.ShortComplex.g ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH0 d₀₁	—	—
shortComplexH1_f 📖	mathematical	—	CategoryTheory.ShortComplex.f ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 d₀₁	—	—
shortComplexH1_g 📖	mathematical	—	CategoryTheory.ShortComplex.g ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 d₁₂	—	—
shortComplexH2_f 📖	mathematical	—	CategoryTheory.ShortComplex.f ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 d₁₂	—	—
shortComplexH2_g 📖	mathematical	—	CategoryTheory.ShortComplex.g ModuleCat CommRing.toRing ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 d₂₃	—	—
smul_map_inv_div_map_inv_of_isMulCocycle₂ 📖	mathematical	IsMulCocycle₂ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	DivInvMonoid.toDiv CommGroup.toGroup InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid InvOneClass.toOne	—	div_eq_div_iff_mul_eq_mul mul_inv_cancel map_one_fst_of_isMulCocycle₂ inv_mul_cancel
smul_map_inv_sub_map_inv_of_isCocycle₂ 📖	mathematical	IsCocycle₂ MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid InvOneClass.toOne	—	sub_eq_sub_iff_add_eq_add mul_inv_cancel map_one_fst_of_isCocycle₂ inv_mul_cancel
subtype_comp_d₀₁ 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module Pi.addCommGroup Pi.Function.module Ring.toSemiring ModuleCat.ofHom Submodule.subtype d₀₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver ModuleCat.instZeroHom	—	ModuleCat.hom_ext LinearMap.ext sub_eq_zero
subtype_comp_d₀₁_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup Pi.addCommGroup Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule Pi.Function.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of d₀₁ Submodule CommSemiring.toSemiring CommRing.toCommSemiring SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise subtype_comp_d₀₁
subtype_comp_d₀₁_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory ModuleCat.of ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module ModuleCat.ofHom Submodule.subtype Pi.addCommGroup Pi.Function.module Ring.toSemiring d₀₁ Quiver.Hom CategoryTheory.CategoryStruct.toQuiver ModuleCat.instZeroHom	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' subtype_comp_d₀₁
toCocycles_comp_isoCocycles₁_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains cocycles ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module toCocycles CategoryTheory.Iso.hom isoCocycles₁ CategoryTheory.ShortComplex.LeftHomologyData.K shortComplexH1 CategoryTheory.ShortComplex.moduleCatLeftHomologyData cochainsIso₀ CategoryTheory.ShortComplex.LeftHomologyData.f'	—	CategoryTheory.cancel_mono CategoryTheory.ShortComplex.LeftHomologyData.instMonoI AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc isoCocycles₁_hom_comp_i HomologicalComplex.toCycles_i_assoc CategoryTheory.ShortComplex.LeftHomologyData.f'_i comp_d₀₁_eq
toCocycles_comp_isoCocycles₁_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier cocycles Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ ModuleCat.isAddCommGroup Submodule.addCommGroup Pi.addCommGroup Submodule.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom isoCocycles₁ toCocycles CategoryTheory.ShortComplex.moduleCatToCycles shortComplexH1 cochainsIso₀	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise toCocycles_comp_isoCocycles₁_hom
toCocycles_comp_isoCocycles₁_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains cocycles toCocycles ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module CategoryTheory.Iso.hom isoCocycles₁ cochainsIso₀ CategoryTheory.ShortComplex.LeftHomologyData.f' shortComplexH1 CategoryTheory.ShortComplex.moduleCatLeftHomologyData	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toCocycles_comp_isoCocycles₁_hom
toCocycles_comp_isoCocycles₂_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains cocycles ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ Submodule.addCommGroup Pi.addCommGroup Submodule.module toCocycles CategoryTheory.Iso.hom isoCocycles₂ Ring.toSemiring CategoryTheory.ShortComplex.LeftHomologyData.K shortComplexH2 CategoryTheory.ShortComplex.moduleCatLeftHomologyData cochainsIso₁ CategoryTheory.ShortComplex.LeftHomologyData.f'	—	CategoryTheory.cancel_mono CategoryTheory.ShortComplex.LeftHomologyData.instMonoI AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc isoCocycles₂_hom_comp_i HomologicalComplex.toCycles_i_assoc CategoryTheory.ShortComplex.LeftHomologyData.f'_i comp_d₁₂_eq
toCocycles_comp_isoCocycles₂_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier cocycles Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ ModuleCat.isAddCommGroup Submodule.addCommGroup Pi.addCommGroup Submodule.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom isoCocycles₂ toCocycles CategoryTheory.ShortComplex.moduleCatToCycles shortComplexH2 cochainsIso₁	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise toCocycles_comp_isoCocycles₂_hom
toCocycles_comp_isoCocycles₂_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains cocycles toCocycles ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ Submodule.addCommGroup Pi.addCommGroup Submodule.module CategoryTheory.Iso.hom isoCocycles₂ Ring.toSemiring cochainsIso₁ CategoryTheory.ShortComplex.LeftHomologyData.f' shortComplexH2 CategoryTheory.ShortComplex.moduleCatLeftHomologyData	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toCocycles_comp_isoCocycles₂_hom
π_comp_H0IsoOfIsTrivial_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles groupCohomology Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid π CategoryTheory.Iso.hom H0 H0IsoOfIsTrivial HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains iCocycles cochainsIso₀	—	AddRightCancelSemigroup.toIsRightCancelAdd π_comp_H0Iso_hom_assoc cocyclesIso₀_hom_comp_f
π_comp_H0IsoOfIsTrivial_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module LinearMap.instFunLike ModuleCat.Hom.hom ModuleCat.of CategoryTheory.ShortComplex.f CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH0 cocycles CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Iso.hom cocyclesIso₀ Pi.addCommGroup Pi.Function.module cochainsIso₀ iCocycles	—	AddRightCancelSemigroup.toIsRightCancelAdd π_comp_H0Iso_hom_apply CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise π_comp_H0IsoOfIsTrivial_hom
π_comp_H0IsoOfIsTrivial_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles groupCohomology π Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid CategoryTheory.Iso.hom H0 H0IsoOfIsTrivial HomologicalComplex.X CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddCancelCommMonoid.toAddCancelMonoid Nat.instAddCancelCommMonoid AddRightCancelSemigroup.toIsRightCancelAdd Nat.instOne inhomogeneousCochains iCocycles cochainsIso₀	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_comp_H0IsoOfIsTrivial_hom
π_comp_H0Iso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles groupCohomology ModuleCat.of ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module π CategoryTheory.Iso.hom H0 H0Iso cocyclesIso₀	—	HomologicalComplex.isoHomologyπ_hom_inv_id_assoc
π_comp_H0Iso_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier groupCohomology Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ ModuleCat.isAddCommGroup Submodule.addCommGroup Submodule.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom H0 H0Iso cocycles π cocyclesIso₀	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise π_comp_H0Iso_hom
π_comp_H0Iso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles groupCohomology π ModuleCat.of ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat ModuleCat.isModule SetLike.instMembership Submodule.setLike Representation.invariants Rep.ρ Submodule.addCommGroup ModuleCat.isAddCommGroup Submodule.module CategoryTheory.Iso.hom H0 H0Iso cocyclesIso₀	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_comp_H0Iso_hom
π_comp_H1Iso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles groupCohomology CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 CategoryTheory.ShortComplex.moduleCatLeftHomologyData π CategoryTheory.Iso.hom H1 H1Iso ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module isoCocycles₁ CategoryTheory.ShortComplex.LeftHomologyData.π	—	comp_d₀₁_eq comp_d₁₂_eq CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.ShortComplex.homologyπ_comp_leftHomologyIso_inv_assoc CategoryTheory.ShortComplex.leftHomologyπ_naturality'
π_comp_H1Iso_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier groupCohomology HasQuotient.Quotient CategoryTheory.ShortComplex.X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 Submodule AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule SetLike.instMembership Submodule.setLike LinearMap.ker CategoryTheory.ShortComplex.X₃ ModuleCat.Hom.hom CategoryTheory.ShortComplex.g Submodule.addCommMonoid Submodule.module Submodule.hasQuotient Submodule.addCommGroup LinearMap.range CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.moduleCatToCycles Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom H1 H1Iso cocycles π CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module cocycles₁ Pi.addCommGroup Submodule.mkQ isoCocycles₁	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise π_comp_H1Iso_hom
π_comp_H1Iso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles groupCohomology π CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH1 CategoryTheory.ShortComplex.moduleCatLeftHomologyData CategoryTheory.Iso.hom H1 H1Iso ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₁ Submodule.addCommGroup Pi.addCommGroup Submodule.module isoCocycles₁ CategoryTheory.ShortComplex.LeftHomologyData.π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_comp_H1Iso_hom
π_comp_H2Iso_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles groupCohomology CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 CategoryTheory.ShortComplex.moduleCatLeftHomologyData π CategoryTheory.Iso.hom H2 H2Iso ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ Submodule.addCommGroup Pi.addCommGroup Submodule.module isoCocycles₂ CategoryTheory.ShortComplex.LeftHomologyData.π	—	comp_d₁₂_eq comp_d₂₃_eq CategoryTheory.ShortComplex.hasLeftHomology_of_hasHomology CategoryTheory.ShortComplex.homologyπ_comp_leftHomologyIso_inv_assoc CategoryTheory.ShortComplex.leftHomologyπ_naturality'
π_comp_H2Iso_hom_apply 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring CommRing.toRing RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier groupCohomology HasQuotient.Quotient CategoryTheory.ShortComplex.X₂ ModuleCat ModuleCat.moduleCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 Submodule AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule SetLike.instMembership Submodule.setLike LinearMap.ker CategoryTheory.ShortComplex.X₃ ModuleCat.Hom.hom CategoryTheory.ShortComplex.g Submodule.addCommMonoid Submodule.module Submodule.hasQuotient Submodule.addCommGroup LinearMap.range CategoryTheory.ShortComplex.X₁ CategoryTheory.ShortComplex.moduleCatToCycles Submodule.Quotient.addCommGroup Submodule.Quotient.module LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier ModuleCat.of CategoryTheory.Iso.hom H2 H2Iso cocycles π CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module cocycles₂ Pi.addCommGroup Submodule.mkQ isoCocycles₂	—	CategoryTheory.comp_apply Mathlib.Tactic.Elementwise.hom_elementwise π_comp_H2Iso_hom
π_comp_H2Iso_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp ModuleCat CommRing.toRing CategoryTheory.Category.toCategoryStruct ModuleCat.moduleCategory cocycles groupCohomology π CategoryTheory.ShortComplex.LeftHomologyData.H CategoryTheory.Preadditive.preadditiveHasZeroMorphisms ModuleCat.instPreadditive shortComplexH2 CategoryTheory.ShortComplex.moduleCatLeftHomologyData CategoryTheory.Iso.hom H2 H2Iso ModuleCat.of Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier Action.V DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike cocycles₂ Submodule.addCommGroup Pi.addCommGroup Submodule.module isoCocycles₂ CategoryTheory.ShortComplex.LeftHomologyData.π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_comp_H2Iso_hom

groupCohomology.coboundaries₁

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_mk 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike groupCohomology.coboundaries₁	DFunLike.coe groupCohomology.instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCoboundaries₁	—	—
val_eq_coe 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike groupCohomology.coboundaries₁ DFunLike.coe groupCohomology.instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCoboundaries₁	—	—

groupCohomology.coboundaries₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_mk 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike groupCohomology.coboundaries₂	DFunLike.coe groupCohomology.instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCoboundaries₂	—	—
val_eq_coe 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike groupCohomology.coboundaries₂ DFunLike.coe groupCohomology.instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCoboundaries₂	—	—

groupCohomology.cocycles₁

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_mk 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike groupCohomology.cocycles₁	DFunLike.coe groupCohomology.instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCocycles₁	—	—
d₁₂_apply 📖	mathematical	—	DFunLike.coe ModuleCat.of CommRing.toRing Pi.addCommGroup ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule CategoryTheory.ConcreteCategory.hom LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier groupCohomology.d₁₂ Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid SetLike.instMembership Submodule.setLike groupCohomology.cocycles₁ groupCohomology.instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCocycles₁ Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
val_eq_coe 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike groupCohomology.cocycles₁ DFunLike.coe groupCohomology.instFunLikeSubtypeForallCarrierVModuleCatMemSubmoduleCocycles₁	—	—

groupCohomology.cocycles₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_mk 📖	mathematical	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike groupCohomology.cocycles₂	DFunLike.coe groupCohomology.instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCocycles₂	—	—
d₂₃_apply 📖	mathematical	—	DFunLike.coe ModuleCat.of CommRing.toRing Pi.addCommGroup ModuleCat.carrier Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule CategoryTheory.ConcreteCategory.hom LinearMap RingHom.id Semiring.toNonAssocSemiring ModuleCat.isAddCommGroup LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier groupCohomology.d₂₃ Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid SetLike.instMembership Submodule.setLike groupCohomology.cocycles₂ groupCohomology.instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCocycles₂ Pi.instZero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
val_eq_coe 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring Pi.addCommMonoid ModuleCat.carrier CommRing.toRing Action.V ModuleCat ModuleCat.moduleCategory DivInvMonoid.toMonoid Group.toDivInvMonoid AddCommGroup.toAddCommMonoid Rep.instAddCommGroupCarrierVModuleCat Pi.Function.module ModuleCat.isModule SetLike.instMembership Submodule.setLike groupCohomology.cocycles₂ DFunLike.coe groupCohomology.instFunLikeSubtypeForallProdCarrierVModuleCatMemSubmoduleCocycles₂	—	—

---

← Back to Index