Skip to content

refactor(RepresentationTheory/GroupCohomology): refactor low degree group cohomology#25310

Closed
101damnations wants to merge 45 commits intomasterfrom
arlcohlowdegrefactor
Closed

refactor(RepresentationTheory/GroupCohomology): refactor low degree group cohomology#25310
101damnations wants to merge 45 commits intomasterfrom
arlcohlowdegrefactor

Conversation

@101damnations
Copy link
Copy Markdown
Collaborator

@101damnations 101damnations commented May 30, 2025

groupCohomology A n is defined as the abstract homology of the complex of inhomogeneous cochains in RepresentationTheory.GroupCohomology.Basic, whose objects are (Fin n → G) → A, whilst in RepresentationTheory.GroupCohomology.LowDegree we provide alternative definitions of H0, H1, H2 which are more concrete. But these extra definitions are not worth the extra API they necessitate, as long as we define the (one/two)-co(cycles/boundaries) as submodules of G → A and G × G → A respectively and relate these (and Aᴳ) to the original groupCohomology A n for n = 0, 1, 2. This PR implements that.


Open in Gitpod

@101damnations 101damnations added the WIP Work in progress label May 30, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented May 30, 2025

PR summary 8e87a39073

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ H0Iso
+ H0IsoOfIsTrivial_hom
+ H0_induction_on
+ H1Iso
+ H1π_comp_H1IsoOfIsTrivial_hom:
+ H1π_comp_map
+ H1π_eq_iff
+ H2Iso
+ H2π_comp_map
+ H2π_eq_iff
+ cocyclesMap_zeroIsoCocycles_hom_f
+ instance : Epi (H1π A) := by unfold H1π; infer_instance
+ instance : Epi (H2π A) := by unfold H2π; infer_instance
+ map_1_one
+ map_H0Iso_hom_f
+ map_id_comp_H0Iso_hom
+ mono_map_0_of_mono
+ zeroCocyclesIso
+ zeroCocyclesIso_hom_comp_f
+ zeroCocyclesIso_inv_comp_iCocycles
+ π_comp_H0IsoOfIsTrivial_hom
+ π_comp_H0Iso_hom
+ π_comp_H1Iso_hom
+ π_comp_H2Iso_hom
- H0IsoOfIsTrivial_hom_apply
- H0IsoOfIsTrivial_hom_hom
- H1π_comp_H1IsoOfIsTrivial_hom
- isoZeroCocycles_hom_comp_f
- map_comp_isoH0_hom
- map_comp_isoH1_hom
- map_comp_isoH2_hom
- π_comp_isoH0_hom
- π_comp_isoH1_hom
- π_comp_isoH2_hom

You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.


No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label May 30, 2025
@101damnations 101damnations changed the title feat(RepresentationTheory): refactor low degree group cohomology refactor(RepresentationTheory): refactor low degree group cohomology May 30, 2025
@101damnations 101damnations changed the title refactor(RepresentationTheory): refactor low degree group cohomology refactor(RepresentationTheory/GroupCohomology): refactor low degree group cohomology May 30, 2025
@github-actions github-actions bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 2, 2025
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 2, 2025
@github-actions github-actions bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 6, 2025
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 6, 2025
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 12, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jun 13, 2025
Extra lemmas about group cohomology in preparation for #25310.
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 13, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

This PR/issue depends on:

@101damnations
Copy link
Copy Markdown
Collaborator Author

This PR has been migrated to a fork-based workflow: #25870

pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Jun 15, 2025
pfaffelh pushed a commit to pfaffelh/mathlib4 that referenced this pull request Jun 15, 2025
Rida-Hamadani pushed a commit to Rida-Hamadani/mathlib4 that referenced this pull request Jun 24, 2025
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
@YaelDillies YaelDillies deleted the arlcohlowdegrefactor branch August 18, 2025 07:32
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants