Skip to content

feat(GroupExtension/Abelian): define conjClassesEquivH1#21837

Closed
yu-yama wants to merge 3 commits intomasterfrom
yu-yama/GroupExtension-Abelian-H1
Closed

feat(GroupExtension/Abelian): define conjClassesEquivH1#21837
yu-yama wants to merge 3 commits intomasterfrom
yu-yama/GroupExtension-Abelian-H1

Conversation

@yu-yama
Copy link
Copy Markdown
Collaborator

@yu-yama yu-yama commented Feb 13, 2025

As the third part of #19582, this PR adds the first part of the Abelian file.

It mainly:

  • defines SemidirectProduct.conjClassesEquivH1, a bijection between the conjugacy classes of splittings of a group extension associated to a semidirect product and $H^1 (G, N)$.

Open in Gitpod

@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 13, 2025 •
edited
Loading

PR summary e6886de347

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.GroupTheory.GroupExtension.Abelian (new file) 1920

Declarations diff

+ isConj_iff_sub_mem_oneCoboundaries
+ splittingEquivOneCocycles
+ splittingOfOneCocycle
+ splittingToOneCocycle
+ toRep
+ toRep_ρ_apply_apply

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 Feb 13, 2025
@yu-yama yu-yama mentioned this pull request Feb 13, 2025
Open
3 tasks
erdOne
erdOne reviewed Apr 1, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@erdOne erdOne left a comment

Choose a reason for hiding this comment

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

Sorry I did not notice this PR in my inbox. Feel free to ping/dm me for reviews if I forget your PRs again.

Mathlib/GroupTheory/GroupExtension/Abelian.lean
theorem toRep_ρ_apply_apply (g : G) (n : Additive N) :
((toRep φ).ρ g) n = Additive.ofMul (φ g (Additive.toMul n)) := rfl

/-- Returns the 1-cocycle corresponding to a splitting. -/
Copy link
Copy Markdown
Member

@erdOne erdOne Apr 1, 2025

Choose a reason for hiding this comment

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

Suggested change
/-- Returns the 1-cocycle corresponding to a splitting. -/
/-- The 1-cocycle corresponding to a splitting. -/

And perhaps call it Splitting.oneCocycle so that one could write s.oneCocycle directly.

Mathlib/GroupTheory/GroupExtension/Abelian.lean
Comment on lines +42 to +67
def splittingToOneCocycle (s : (toGroupExtension φ).Splitting) :
groupCohomology.oneCocycles (toRep φ) where
val g := Additive.ofMul (α := N) (s g).left
property := by
rw [groupCohomology.mem_oneCocycles_iff]
intro g₁ g₂
rw [toRep_ρ_apply_apply, toMul_ofMul, map_mul, mul_left, mul_comm, ← ofMul_mul, right_splitting]

/-- Returns the splitting corresponding to a 1-cocycle. -/
def splittingOfOneCocycle (f : groupCohomology.oneCocycles (toRep φ)) :
(toGroupExtension φ).Splitting where
toFun g := ⟨Additive.toMul (f g), g⟩
map_one' := by
ext
· simp only [one_left, groupCohomology.oneCocycles_map_one, toMul_zero]
· simp only [one_right]
map_mul' g₁ g₂ := by
ext
· simp only [mul_left]
rw [(groupCohomology.mem_oneCocycles_iff f).mp f.property g₁ g₂, toMul_add, mul_comm,
toRep_ρ_apply_apply, toMul_ofMul]
· simp only [mul_right]
rightInverse_rightHom g := by simp only [toGroupExtension_rightHom, rightHom_eq_right]
Copy link
Copy Markdown
Member

@erdOne erdOne Apr 1, 2025

Choose a reason for hiding this comment

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

These defs are missing some API (e.g. (splittingOfOneCocycle φ f g).1 = Additive.toMul (f g)). Maybe simps can generate them?

Mathlib/GroupTheory/GroupExtension/Abelian.lean
rw [toRep_ρ_apply_apply, toMul_ofMul, map_mul, mul_left, mul_comm, ← ofMul_mul, right_splitting]

/-- Returns the splitting corresponding to a 1-cocycle. -/
def splittingOfOneCocycle (f : groupCohomology.oneCocycles (toRep φ)) :
Copy link
Copy Markdown
Member

@erdOne erdOne Apr 1, 2025

Choose a reason for hiding this comment

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

Similarly this could be Splitting.ofOneCocycle for the anonymous dot notation.

@erdOne erdOne added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 1, 2025
@erdOne
Copy link
Copy Markdown
Member

erdOne commented Jun 26, 2025

@yu-yama Hi! Are you still planning to work on getting this into mathlib? The results here (along with the correspondence for H2) would be really valuable for Class field theory and related areas. Your work already looks great, and it seems only a few minor adjustments are needed to align it with mathlib’s style. @YaelDillies mentioned they’d be happy to help take over if you’re unable to continue, but of course, it would be wonderful if you could complete it yourself.

@YaelDillies YaelDillies force-pushed the yu-yama/GroupExtension-Abelian-H1 branch from c2d9541 to 8b463ae Compare June 27, 2025 10:45
@erdOne
Copy link
Copy Markdown
Member

erdOne commented Jun 27, 2025

@YaelDillies Could you please not touch other people's branch without their permission? Thanks a lot. As I said, I would strongly prefer if @yu-yama could push this PR through the review process themselves, both because this is their work and they might have better ideas about how to fix certain things, and that the review process would be useful to them to learn about mathlib styles as well.

@YaelDillies
Copy link
Copy Markdown
Contributor

YaelDillies commented Jun 27, 2025

Apologies, I got interrupted before I could explain what I was doing.

Yesterday, Edison spent an hour updating this file to v4.19.0. I didn't want his work to be lost, so I rebased this branch and moved over his changes (as well as the ones necessary to go from v4.19.0 to v4.21.0-rc3).

That's all. I didn't intend to act on your review, and haven't done so.

@yu-yama yu-yama mentioned this pull request Jul 3, 2025
Open
@yu-yama
Copy link
Copy Markdown
Collaborator Author

yu-yama commented Jul 3, 2025

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

@yu-yama yu-yama closed this Jul 3, 2025
@yu-yama
Copy link
Copy Markdown
Collaborator Author

yu-yama commented Jul 3, 2025

@erdOne @YaelDillies
Actually, I had already updated most of the file to the then-latest Lean version on my local machine but did not push it right away because I could not adapt conjClassesEquivH1 to the new definition quite right.
I have now finished updating (and resolving review comments) and am reopening this PR from a personal fork.

@YaelDillies YaelDillies deleted the yu-yama/GroupExtension-Abelian-H1 branch July 3, 2025 15:35
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@erdOne erdOne erdOne left review comments

Assignees

@erdOne erdOne

Labels

awaiting-author A reviewer has asked the author a question or requested changes. migrated-to-fork t-algebra Algebra (groups, rings, fields, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@yu-yama @erdOne @YaelDillies