Skip to content

[Merged by Bors] - refactor: denote low degree group cohomology API indices with subscripts#26546

Closed
101damnations wants to merge 14 commits intoleanprover-community:masterfrom
101damnations:gpcohlowdegrenaming
Closed

[Merged by Bors] - refactor: denote low degree group cohomology API indices with subscripts#26546
101damnations wants to merge 14 commits intoleanprover-community:masterfrom
101damnations:gpcohlowdegrenaming

Conversation

@101damnations
Copy link
Copy Markdown
Collaborator

@101damnations 101damnations commented Jun 30, 2025

This PR replaces names like groupCohomology.oneCocycles with groupCohomology.cocycles₁, to bring this API in line with the group homology naming scheme suggested by @jcommelin in #25873.

Open in Gitpod

@github-actions github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Jun 30, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 30, 2025 •
edited
Loading

PR summary ff1ed4822d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ IsCoboundary₁
+ IsCoboundary₂
+ IsCocycle₁
+ IsCocycle₂
+ IsMulCoboundary₁
+ IsMulCoboundary₂
+ IsMulCocycle₁
+ IsMulCocycle₂
+ coboundariesOfIsCoboundary₁
+ coboundariesOfIsCoboundary₂
+ coboundariesOfIsMulCoboundary₁
+ coboundariesOfIsMulCoboundary₂
+ coboundariesToCocycles₁
+ coboundariesToCocycles₁_apply
+ coboundariesToCocycles₂
+ coboundariesToCocycles₂_apply
+ coboundaries₁
+ coboundaries₁.coe_mk
+ coboundaries₁.val_eq_coe
+ coboundaries₁_eq_bot_of_isTrivial
+ coboundaries₁_ext
+ coboundaries₁_le_cocycles₁
+ coboundaries₂
+ coboundaries₂.coe_mk
+ coboundaries₂.val_eq_coe
+ coboundaries₂_ext
+ coboundaries₂_le_cocycles₂
+ cochainsIso₀
+ cochainsIso₁
+ cochainsIso₂
+ cochainsIso₃
+ cochainsMap_f_0_comp_cochainsIso₀
+ cochainsMap_f_1_comp_cochainsIso₁
+ cochainsMap_f_2_comp_cochainsIso₂
+ cochainsMap_f_3_comp_cochainsIso₃
+ cocyclesIso₀
+ cocyclesIso₀_hom_comp_f
+ cocyclesIso₀_inv_comp_iCocycles
+ cocyclesMap_cocyclesIso₀_hom_f
+ cocyclesMap_comp_isoCocycles₁_hom
+ cocyclesMap_comp_isoCocycles₂_hom
+ cocyclesMk₀_eq
+ cocyclesMk₁_eq
+ cocyclesMk₂_eq
+ cocyclesOfIsCocycle₁
+ cocyclesOfIsCocycle₂
+ cocyclesOfIsMulCocycle₁
+ cocyclesOfIsMulCocycle₂
+ cocycles₁
+ cocycles₁.coe_mk
+ cocycles₁.d₁₂_apply
+ cocycles₁.val_eq_coe
+ cocycles₁IsoOfIsTrivial
+ cocycles₁_ext
+ cocycles₁_map_inv
+ cocycles₁_map_mul_of_isTrivial
+ cocycles₁_map_one
+ cocycles₂
+ cocycles₂.coe_mk
+ cocycles₂.d₂₃_apply
+ cocycles₂.val_eq_coe
+ cocycles₂_ext
+ cocycles₂_map_one_fst
+ cocycles₂_map_one_snd
+ cocycles₂_ρ_map_inv_sub_map_inv
+ coe_mapCocycles₁
+ coe_mapCocycles₂
+ comp_d₀₁_eq
+ comp_d₁₂_eq
+ comp_d₂₃_eq
+ dArrowIso₀₁
+ d₀₁
+ d₀₁_apply_mem_cocycles₁
+ d₀₁_comp_d₁₂
+ d₀₁_eq_zero
+ d₀₁_ker_eq_invariants
+ d₁₂
+ d₁₂_apply_mem_cocycles₂
+ d₁₂_comp_d₂₃
+ d₂₃
+ eq_d₀₁_comp_inv
+ eq_d₁₂_comp_inv
+ eq_d₂₃_comp_inv
+ f₁
+ f₂
+ f₃
+ instance : FunLike (coboundaries₁ A) G A := ⟨Subtype.val, Subtype.val_injective⟩
+ instance : FunLike (coboundaries₂ A) (G × G) A := ⟨Subtype.val, Subtype.val_injective⟩
+ instance : FunLike (cocycles₁ A) G A := ⟨Subtype.val, Subtype.val_injective⟩
+ instance : FunLike (cocycles₂ A) (G × G) A := ⟨Subtype.val, Subtype.val_injective⟩
+ isCoboundary₁_of_mem_coboundaries₁
+ isCoboundary₂_of_mem_coboundaries₂
+ isCocycle₁_of_mem_cocycles₁
+ isCocycle₂_of_mem_cocycles₂
+ isMulCoboundary₁_of_isMulCocycle₁_of_aut_to_units
+ isMulCoboundary₁_of_mem_coboundaries₁
+ isMulCoboundary₂_of_mem_coboundaries₂
+ isMulCocycle₁_of_mem_cocycles₁
+ isMulCocycle₂_of_mem_cocycles₂
+ isoCocycles₁
+ isoCocycles₁_hom_comp_i
+ isoCocycles₁_inv_comp_iCocycles
+ isoCocycles₂
+ isoCocycles₂_hom_comp_i
+ isoCocycles₂_inv_comp_iCocycles
+ mapCocycles₁
+ mapCocycles₁_comp_i
+ mapCocycles₁_one
+ mapCocycles₂
+ mapCocycles₂_comp_i
+ 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₁_of_comp_eq_d₀₁
+ mem_cocycles₂_def
+ mem_cocycles₂_iff
+ mem_cocycles₂_of_comp_eq_d₁₂
+ smul_map_inv_div_map_inv_of_isMulCocycle₂
+ smul_map_inv_sub_map_inv_of_isCocycle₂
+ subtype_comp_d₀₁
+ toCocycles_comp_isoCocycles₁_hom
+ toCocycles_comp_isoCocycles₂_hom
- instance : FunLike (oneCoboundaries A) G A := ⟨Subtype.val, Subtype.val_injective⟩
- instance : FunLike (oneCocycles A) G A := ⟨Subtype.val, Subtype.val_injective⟩
- instance : FunLike (twoCoboundaries A) (G × G) A := ⟨Subtype.val, Subtype.val_injective⟩
- instance : FunLike (twoCocycles A) (G × G) A := ⟨Subtype.val, Subtype.val_injective⟩

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).

kbuzzard
kbuzzard approved these changes Jul 1, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@kbuzzard kbuzzard left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Having looked through the entire thing manually, I realised that the missing deprecations can just be read off by the few - lines at the end of the declarations diff part of the post by github-actions in the PR.

@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 Jul 2, 2025
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 2, 2025
@kbuzzard
Copy link
Copy Markdown
Member

kbuzzard commented Jul 2, 2025

This looks great now!

To maintainers: this is a largeish PR but it's just a change in naming convention plus many deprecations. It brings the naming convention for group cohomology in line with the naming convention for group homology introduced in #25873 . I've read through all of it but am reluctant to merge myself because the author is my PhD student.

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jul 2, 2025

🚀 Pull request has been placed on the maintainer queue by kbuzzard.

@ghost ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 2, 2025
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Jul 3, 2025

Thanks!

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jul 3, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jul 3, 2025
@101damnations
refactor: denote low degree group cohomology API indices with subscri…
7e9586b 
…pts (#26546)

This PR replaces names like `groupCohomology.oneCocycles` with `groupCohomology.cocycles₁`, to bring this API in line with the group homology naming scheme suggested by @jcommelin in #25873.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 3, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title refactor: denote low degree group cohomology API indices with subscripts [Merged by Bors] - refactor: denote low degree group cohomology API indices with subscripts Jul 3, 2025
@mathlib-bors mathlib-bors bot closed this Jul 3, 2025
joelriou pushed a commit to joelriou/mathlib4 that referenced this pull request Jul 7, 2025
@101damnations @joelriou
refactor: denote low degree group cohomology API indices with subscri…
1fa4bdc 
…pts (leanprover-community#26546)

This PR replaces names like `groupCohomology.oneCocycles` with `groupCohomology.cocycles₁`, to bring this API in line with the group homology naming scheme suggested by @jcommelin in leanprover-community#25873.
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
@101damnations @callesonne
refactor: denote low degree group cohomology API indices with subscri…
c6ef337 
…pts (leanprover-community#26546)

This PR replaces names like `groupCohomology.oneCocycles` with `groupCohomology.cocycles₁`, to bring this API in line with the group homology naming scheme suggested by @jcommelin in leanprover-community#25873.
hrmacbeth pushed a commit to szqzs/mathlib4 that referenced this pull request Jul 28, 2025
@101damnations @hrmacbeth
refactor: denote low degree group cohomology API indices with subscri…
bba344b 
…pts (leanprover-community#26546)

This PR replaces names like `groupCohomology.oneCocycles` with `groupCohomology.cocycles₁`, to bring this API in line with the group homology naming scheme suggested by @jcommelin in leanprover-community#25873.
@YaelDillies
Copy link
Copy Markdown
Contributor

YaelDillies commented Sep 7, 2025 •
edited
Loading

I found IsCocycle₁/IsCocycle₂ really hard to type in search tools like the docs or grep. I considered renaming them to IsOneCocycle/IsTwoCocycle before realising this would precisely revert this PR! In other parts of the library, we have banished hard to type characters in definition names (eg Memℒp became MemLp), why are we sailing against the wind here?

EDIT: Posted on Zulip

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kbuzzard kbuzzard kbuzzard approved these changes

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@101damnations @kbuzzard @riccardobrasca @YaelDillies