feat(GroupExtension/Abelian): define `OfMulDistribMulAction.equivH2` by yu-yama · Pull Request #19582 · leanprover-community/mathlib4

yu-yama · 2024-11-28T21:08:37Z

Mainly defines:

structure GroupExtension.OfMulDistribMulAction N G [MulDistribMulAction G N]: group extensions of G by N where the multiplicative action of G on N is the conjugation
structure GroupExtension.OfMulDistribMulActionWithSection N G [MulDistribMulAction G N]: group extensions with specific choices of sections
def GroupExtension.OfMulDistribMulAction.equivH2: a bijection between the equivalence classes of group extensions and $H^2 (G, N)$

depends on: [Merged by Bors] - chore(GroupExtension/Defs): define Section and redefine Splitting #20802 (split PR: contains changes to the Defs file)
depends on: [Merged by Bors] - chore(GroupExtension/Basic): add lemmas about extensions by (non-abelian) groups #20998 (split PR: mainly adds the Basic file)
depends on: feat(GroupExtension/Abelian): define conjClassesEquivH1 #26670 (split PR: adds the first part of the Abelian file)

Here is a relevant TODO in Mathlib:

mathlib4/Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean

Lines 46 to 48 in 4e9fa40

    
           ## TODO 
        
           * The relationship between `H2` and group extensions

I would appreciate your comments.

github-actions · 2024-11-28T21:09:32Z

PR summary 18d4bf634f

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

+ conjAct
+ conjAct_eq
+ conjAct_inl
+ conjClassesEquivH1
+ conj_eq_of_rightHom_eq_one
+ equivH2
+ equivTwoCocycles
+ exists_cochain_of_sub_mem_twoCoboundaries
+ extensionOfTwoCocycle
+ extensionOfTwoCocycle_inl
+ extensionOfTwoCocycle_rightHom
+ inl
+ inl_conjAct_comm
+ inl_injective
+ inl_smul_eq_conj_inl
+ inl_toTwoCocycle
+ instance : Group (middleOfTwoCocycle f)
+ instance : Inv (middleOfTwoCocycle f)
+ instance : Mul (middleOfTwoCocycle f)
+ instance : One (middleOfTwoCocycle f)
+ inv_def
+ inv_left
+ inv_right
+ isConj_iff_sub_mem_oneCoboundaries
+ left_inl
+ map_one_snd
+ mem_range_inl
+ middleOfTwoCocycle
+ mul_def
+ mul_left
+ mul_right
+ ofH2
+ ofMulDistribMulAction
+ ofMulDistribMulActionWithSection
+ ofTwoCocycle
+ ofTwoCocycleToTwoCocycleEquiv
+ one_def
+ one_left
+ one_right
+ range_inl_eq_ker_rightHom
+ rightHom
+ rightHom_eq_right
+ rightHom_surjective
+ right_inl
+ sectionOfTwoCocycle
+ smul_map_inv_eq
+ splittingEquivOneCocycles
+ splittingOfOneCocycle
+ splittingToOneCocycle
+ sub_mem_twoCoboundaries_of_equiv
+ sub_mem_twoCoboundaries_of_toOfMulDistribMulAction_equiv
+ toH2
+ toRep
+ toRep_ρ_apply_apply
+ toTwoCocycle
+ toTwoCocycle_apply
+ toTwoCocycle_eq_of_equiv
+ toTwoCocycle_ofTwoCocycle
+ toofMulDistribMulActionEquivOfCochain
++ Equiv
++ EquivClasses
++ instance : Group S'.E := S'.GroupE
++ instance : Group S.E := S.GroupE
++ setoid

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

erdOne · 2024-12-20T10:52:44Z

Thanks for the contribution!
This PR is quite large. Is it possible to split up the PR into smaller chunks? (e.g. the changes to three files could be three sequential PRs)
And maybe also the file too. 700+ lines for a file is already a bit long.

Feel free to ping me on the split off PRs.

…#20802) This PR: - defines `structure (Add)?GroupExtension.Section` as a right inverse to `rightHom` - redefines `structure (Add)?GroupExtension.Splitting` using `Section` - rewrites the definition of `structure (Add)?GroupExtension.Equiv` with `extends` As the first part of #19582, this PR contains only the changes to the `Defs` file. Moves: - GroupExtension.Splitting.sectionHom -> GroupExtension.Splitting.toMonoidHom - GroupExtension.Splitting.rightHom_comp_sectionHom -> GroupExtension.Splitting.rightInverse_rightHom

…ian) groups (#20998) As the second part of #19582, this PR mostly contains the changes to the `Basic` file. It mainly: - redefines `GroupExtension.Equiv` with `MulEquiv` rather than `MonoidHom`; - adds lemmas that do not require a commutative group, as a preparation for the main PR; - defines `GroupExtension.Splitting.semidirectProductMulEquiv`, an isomorphism between the group associated to a split extension and a semidirect product; and - defines `GroupExtension.ConjClasses`, the conjugacy classes of splittings. It also contains some definitions and lemmas unused in the main PR, such as: - `GroupExtension.quotientRangeInlEquivRight`, provided as a shorthand for end-users; and - `GroupExtension.Section.section_inv_mul_mem_range`, provided as a symmetric counterpart of a required lemma. They may be dropped if this PR would introduce a too large diff. Moves: - GroupExtension.Equiv.mk -> GroupExtension.Equiv.ofMonoidHom

…uivH1`

…ction.equivH2`

The former code no longer compiles after updating to v4.16.0-rc1.

style: use `where` and `__` instead of braces and `with` … besides one-line definitions chore: move variables to the top of each namespace

style: move braces to the same lines as fields

chore: drop `conjActSurjInvRightHom`

YaelDillies · 2025-06-28T09:01:01Z

I've rebased. Sadly a lot of things broke because mem_twoCoboundaries_iff was deleted in #22047 and because H1 and H2 are defined as homology groups rather than quotients. I couldn't locate a replacement for mem_twoCoboundaries_iff nor an iso between H1/H2 and the corresponding quotient, but maybe @101damnations knows.

mathlib4-dependent-issues-bot · 2025-07-03T15:38:43Z

This PR/issue depends on:

~~[Merged by Bors] - chore(GroupExtension/Defs): define Section and redefine Splitting #20802~~
~~[Merged by Bors] - chore(GroupExtension/Basic): add lemmas about extensions by (non-abelian) groups #20998~~
feat(GroupExtension/Abelian): define conjClassesEquivH1 #26670
By Dependent Issues (🤖). Happy coding!

mathlib4-merge-conflict-bot · 2025-08-21T19:24:19Z

This pull request has conflicts, please merge master and resolve them.

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Nov 28, 2024

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Nov 28, 2024

kim-em added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 11, 2025

yu-yama mentioned this pull request Jan 16, 2025

[Merged by Bors] - chore(GroupExtension/Defs): define Section and redefine Splitting #20802

Closed

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 Jan 16, 2025

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 Jan 17, 2025

yu-yama mentioned this pull request Jan 23, 2025

[Merged by Bors] - chore(GroupExtension/Basic): add lemmas about extensions by (non-abelian) groups #20998

Closed

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 Jan 23, 2025

leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 31, 2025

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 Feb 7, 2025

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 Feb 11, 2025

yu-yama mentioned this pull request Feb 13, 2025

feat(GroupExtension/Abelian): define conjClassesEquivH1 #21837

Closed

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 Feb 13, 2025

yu-yama removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 13, 2025

yu-yama changed the title ~~feat(GroupExtension/Abelian): define ofMulDistribMulAction.equivH2~~ feat(GroupExtension/Abelian): define OfMulDistribMulAction.equivH2 Feb 13, 2025

yu-yama and others added 9 commits June 27, 2025 13:38

feat(GroupExtension/Abelian): define `SemidirectProduct.conjClassesEq…

939a5a5

…uivH1`

docs: remove a resolved TODO

ae9f444

fix

9b0d308

feat(GroupExtension/Abelian): define `GroupExtension.ofMulDistribMulA…

5d4cd3c

…ction.equivH2`

docs: populate missing docstrings

e42d563

fix: use rw tactic instead of ▸

ee159bf

The former code no longer compiles after updating to v4.16.0-rc1.

docs: improve docstrings

b2dce99

style: use `where` and `__` instead of braces and `with` … besides one-line definitions chore: move variables to the top of each namespace

chore: patch lemmas and defs affected by redefinition of Equiv

d14accf

style: move braces to the same lines as fields

refactor: require smul_eq_conjAct as a field rather than a lemma

4791390

chore: drop `conjActSurjInvRightHom`

fix

11a3622

YaelDillies force-pushed the yu-yama/GroupExtension-Abelian branch from 457ed67 to 11a3622 Compare June 28, 2025 08:55

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 Jul 3, 2025

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 Jul 3, 2025

mathlib4-merge-conflict-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 Aug 21, 2025

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(GroupExtension/Abelian): define `OfMulDistribMulAction.equivH2`#19582

feat(GroupExtension/Abelian): define `OfMulDistribMulAction.equivH2`#19582
yu-yama wants to merge 10 commits intomasterfrom
yu-yama/GroupExtension-Abelian

yu-yama commented Nov 28, 2024 •

edited

Loading

Uh oh!

github-actions bot commented Nov 28, 2024 •

edited

Loading

Declarations diff

Uh oh!

erdOne commented Dec 20, 2024

Uh oh!

YaelDillies commented Jun 28, 2025

Uh oh!

mathlib4-dependent-issues-bot commented Jul 3, 2025 •

edited

Loading

Uh oh!

mathlib4-merge-conflict-bot commented Aug 21, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

Conversation

yu-yama commented Nov 28, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Nov 28, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 18d4bf634f

Import changes for modified files

Declarations diff

Uh oh!

erdOne commented Dec 20, 2024

Uh oh!

YaelDillies commented Jun 28, 2025

Uh oh!

mathlib4-dependent-issues-bot commented Jul 3, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

mathlib4-merge-conflict-bot commented Aug 21, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

yu-yama commented Nov 28, 2024 •

edited

Loading

github-actions bot commented Nov 28, 2024 •

edited

Loading

mathlib4-dependent-issues-bot commented Jul 3, 2025 •

edited

Loading