Commit 2025-06-30 14:03 df074b28

View on Github →

feat(RepresentationTheory/Homological/GroupHomology/LowDegree): simpler expressions for differentials (#25873) The first part of a file giving simpler expressions for group homology in low degree, following the structure of RepresentationTheory/Homological/GroupCohomology/LowDegree.lean.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/RepresentationTheory/Homological/GroupHomology/Basic.lean

Created Mathlib/RepresentationTheory/Homological/GroupHomology/LowDegree.lean

added def groupHomology.chainsIso₀

added def groupHomology.chainsIso₁

added def groupHomology.chainsIso₂

added def groupHomology.chainsIso₃

added def groupHomology.chains₁ToCoinvariantsKer

added theorem groupHomology.comp_d₁₀_eq

added theorem groupHomology.comp_d₂₁_eq

added theorem groupHomology.comp_d₃₂_eq

added def groupHomology.d₁₀

added theorem groupHomology.d₁₀_comp_coinvariantsMk

added theorem groupHomology.d₁₀_eq_zero_of_isTrivial

added theorem groupHomology.d₁₀_single

added theorem groupHomology.d₁₀_single_inv

added theorem groupHomology.d₁₀_single_one

added def groupHomology.d₂₁

added theorem groupHomology.d₂₁_comp_d₁₀

added theorem groupHomology.d₂₁_single

added theorem groupHomology.d₂₁_single_inv_mul_ρ_add_single

added theorem groupHomology.d₂₁_single_inv_self_ρ_sub_self_inv

added theorem groupHomology.d₂₁_single_one_fst

added theorem groupHomology.d₂₁_single_one_snd

added theorem groupHomology.d₂₁_single_self_inv_ρ_sub_inv_self

added theorem groupHomology.d₂₁_single_ρ_add_single_inv_mul

added def groupHomology.d₃₂

added theorem groupHomology.d₃₂_comp_d₂₁

added theorem groupHomology.d₃₂_single

added theorem groupHomology.d₃₂_single_one_fst

added theorem groupHomology.d₃₂_single_one_snd

added theorem groupHomology.d₃₂_single_one_thd

added theorem groupHomology.eq_d₁₀_comp_inv

added theorem groupHomology.eq_d₂₁_comp_inv

added theorem groupHomology.eq_d₃₂_comp_inv

added theorem groupHomology.range_d₁₀_eq_coinvariantsKer