Commit 2025-07-07 22:18 7fbffbbe

View on Github →

feat(RepresentationTheory/Homological/GroupHomology/LowDegree): API for n-cycles & n-boundaries for n = 1, 2 (#25882) This PR is more API for low degree group homology, adding cyclesₙ, boundariesₙ for n = 1, 2, following the structure of RepresentationTheory.Homological.GroupCohomology.LowDegree.

Estimated changes

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

added theorem groupHomology.boundariesToCycles₁_apply

added theorem groupHomology.boundariesToCycles₂_apply

added def groupHomology.boundaries₁

added theorem groupHomology.boundaries₁_le_cycles₁

added def groupHomology.boundaries₂

added theorem groupHomology.boundaries₂_le_cycles₂

added def groupHomology.cycles₁

added theorem groupHomology.cycles₁_eq_top_of_isTrivial

added def groupHomology.cycles₂

added theorem groupHomology.d₂₁_apply_mem_cycles₁

added theorem groupHomology.d₃₂_apply_mem_cycles₂

added theorem groupHomology.mem_cycles₁_iff

added theorem groupHomology.mem_cycles₁_of_mem_boundaries₁

added theorem groupHomology.mem_cycles₂_iff

added theorem groupHomology.mem_cycles₂_of_mem_boundaries₂

added theorem groupHomology.single_inv_ρ_self_add_single_mem_boundaries₁

added theorem groupHomology.single_mem_cycles₁_iff

added theorem groupHomology.single_mem_cycles₁_of_mem_invariants

added theorem groupHomology.single_mem_cycles₂_iff

added theorem groupHomology.single_mem_cycles₂_iff_inv

added theorem groupHomology.single_one_fst_sub_single_one_fst_mem_boundaries₂

added theorem groupHomology.single_one_fst_sub_single_one_snd_mem_boundaries₂

added theorem groupHomology.single_one_mem_boundaries₁

added theorem groupHomology.single_one_snd_sub_single_one_fst_mem_boundaries₂

added theorem groupHomology.single_one_snd_sub_single_one_snd_mem_boundaries₂

added theorem groupHomology.single_ρ_self_add_single_inv_mem_boundaries₁