[Merged by Bors] - feat(RingTheory/ClassGroup): prove mulEquiv by mariainesdff · Pull Request #35535 · leanprover-community/mathlib4

mariainesdff · 2026-02-19T11:55:13Z

We prove that isomorphic rings have isomorphic class groups.

Co-authored by: @xgenereux.

github-actions · 2026-02-19T11:56:22Z

PR summary cc9c9b7838

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ ClassGroup.mulEquiv
+ FractionalIdeal.map_ringEquivOfRingEquiv_toPrincipalIdeal
+ _root_.IsFractional.mapEquiv
+ ringEquivOfRingEquiv
+ ringEquivOfRingEquiv_apply
+ ringEquivOfRingEquiv_apply_val
+ ringEquivOfRingEquiv_comp
+ ringEquivOfRingEquiv_refl
+ ringEquivOfRingEquiv_spanSingleton
+ ringEquivOfRingEquiv_symm_eq
+ ringEquivOfRingEquiv_trans
+ ringEquivOfRingEquiv_trans_apply
+ semilinearEquivOfRingEquiv
+ semilinearEquivOfRingEquiv_algebraMap
+ semilinearEquivOfRingEquiv_apply
+ semilinearEquivOfRingEquiv_comp
+ semilinearEquivOfRingEquiv_symm_apply

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).

eric-wieser · 2026-02-19T21:36:03Z

+      rfl
+
+/-- A ring isomorphism `P ≃+* P'` induces an isomorphism on their class groups. -/
+noncomputable def RingEquiv.classGroupEquiv {P P' : Type*} [CommRing P] [IsDomain P] [CommRing P']


To match QuotientGroup.congr this should perhaps be ClassGroup.congr

I could change it, but why not rename QuotientGroup.congr to QuotientGroup.mulEquiv instead (and this to ClassGroup.mulEquiv? That seems more discoverable to me than congr.

eric-wieser · 2026-02-19T21:37:11Z

+        ← FractionalIdeal.ringEquivOfRingEquiv_symm_eq, hu]
+      rfl
+
+/-- A ring isomorphism `P ≃+* P'` induces an isomorphism on their class groups. -/


Can you characterize via a lemma what this isomorphism does to ClassGroup.mk?

I don't think there is a nice formula for this.

mathlib-merge-conflicts · 2026-02-25T08:33:42Z

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

erdOne · 2026-02-28T17:04:09Z

+  have : RingHomCompTriple f (g : S →+* T) (f.trans g : R →+* T) := ⟨rfl⟩
+  apply RingHom.ext
+  intro I
+  rw [Subtype.ext_iff]
+  simp only [ringHomOfRingEquiv, RingEquiv.coe_ringHom_trans, val_eq_coe, RingHom.coe_mk,
+    MonoidHom.coe_mk, OneHom.coe_mk, coe_mk, RingHom.coe_comp, Function.comp_apply]
+  rw [← Submodule.map_comp, IsFractionRing.semilinearEquivOfRingEquiv_comp K L f M]
+  rfl


Suggested change

have : RingHomCompTriple f (g : S →+* T) (f.trans g : R →+* T) := ⟨rfl⟩

apply RingHom.ext

intro I

rw [Subtype.ext_iff]

simp only [ringHomOfRingEquiv, RingEquiv.coe_ringHom_trans, val_eq_coe, RingHom.coe_mk,

MonoidHom.coe_mk, OneHom.coe_mk, coe_mk, RingHom.coe_comp, Function.comp_apply]

rw [← Submodule.map_comp, IsFractionRing.semilinearEquivOfRingEquiv_comp K L f M]

rfl

ext1 I

simp [FractionalIdeal.coe_ext_iff, LinearEquiv.coe_trans,

IsFractionRing.semilinearEquivOfRingEquiv_comp (K := K) (L := L), Submodule.map_comp]

This did not work.

erdOne · 2026-02-28T17:06:18Z

+  rw [Subtype.ext_iff]
+  simp only [ringHomOfRingEquiv_apply, RingEquiv.coe_ringHom_refl, RingEquiv.symm_refl, val_eq_coe,
+    coe_mk, RingHom.id_apply]
+  convert Submodule.map_id _
+  ext x
+  simp [IsFractionRing.semilinearEquivOfRingEquiv]


Can you add a ringHomOfRingEquiv_refl lemma to make this proof simp [FractionalIdeal.coe_ext_iff]? Thanks.

What do you mean?

jcommelin

bors d+

mathlib-bors · 2026-04-29T13:21:40Z

✌️ mariainesdff can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

mariainesdff · 2026-04-29T14:12:52Z

bors r+

@xgenereux

We prove that isomorphic rings have isomorphic class groups. Co-authored by: @xgenereux. Co-authored-by: mariainesdff <mariaines.dff@gmail.com>

mathlib-bors · 2026-04-29T15:43:34Z

Pull request successfully merged into master.

Build succeeded:

@xgenereux

We prove that isomorphic rings have isomorphic class groups. Co-authored by: @xgenereux. Co-authored-by: mariainesdff <mariaines.dff@gmail.com>

feat(RingTheory/ClassGroup): prove mulEquiv

d33499d

mariainesdff added the t-ring-theory Ring theory label Feb 19, 2026

eric-wieser reviewed Feb 19, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/FractionalIdeal/Operations.lean Outdated

eric-wieser reviewed Feb 19, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/Localization/FractionRing.lean Outdated

eric-wieser reviewed Feb 19, 2026

View reviewed changes

tb65536 reviewed Feb 20, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/FractionalIdeal/Operations.lean Outdated

mariainesdff added 3 commits February 23, 2026 15:30

some suggested changes

6a6138c

suggested change

3b717ee

fix build

cbb0ffe

mariainesdff added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Feb 23, 2026

mathlib-merge-conflicts 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 Feb 25, 2026

mariainesdff added 2 commits February 25, 2026 10:13

lint

1620702

Merge branch 'master' into class_group_equiv

5226493

github-actions Bot removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels Feb 25, 2026

mariainesdff commented Feb 25, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Ring/CompTypeclasses.lean Outdated

erdOne reviewed Feb 28, 2026

View reviewed changes

Comment thread Mathlib/Algebra/Ring/CompTypeclasses.lean

erdOne reviewed Feb 28, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/FractionalIdeal/Operations.lean Outdated

erdOne reviewed Feb 28, 2026

View reviewed changes

erdOne added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 28, 2026

mariainesdff added 2 commits March 4, 2026 11:21

suggested changes

3033593

remove instance

656ca84

mariainesdff removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 4, 2026

mariainesdff added 4 commits March 4, 2026 13:07

fix

689b7e1

Merge branch 'master' into class_group_equiv

7f33d1b

fix

8fdb591

fix

dc8a439

mathlib-triage Bot assigned mattrobball Mar 14, 2026

mathlib-triage Bot assigned jcommelin and unassigned mattrobball Apr 5, 2026

jcommelin reviewed Apr 8, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/FractionalIdeal/Operations.lean Outdated

jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 8, 2026

mariainesdff added 2 commits April 8, 2026 18:09

suggested change

13afa3a

Merge branch 'master' into class_group_equiv

101f5dc

mariainesdff removed awaiting-author A reviewer has asked the author a question or requested changes. labels Apr 8, 2026

jcommelin reviewed Apr 14, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/FractionalIdeal/Operations.lean Outdated

Comment thread Mathlib/RingTheory/FractionalIdeal/Operations.lean Outdated

jcommelin reviewed Apr 14, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/FractionalIdeal/Operations.lean Outdated

Comment thread Mathlib/RingTheory/FractionalIdeal/Operations.lean Outdated

Comment thread Mathlib/RingTheory/FractionalIdeal/Operations.lean Outdated

jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 14, 2026

jcommelin reviewed Apr 14, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/FractionalIdeal/Operations.lean Outdated

mariainesdff added 3 commits April 21, 2026 10:30

Merge branch 'master' into class_group_equiv

a66f1d6

test change

2d0b331

suggested changes

7d620cc

mariainesdff removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 28, 2026

jcommelin reviewed Apr 29, 2026

View reviewed changes

Comment thread Mathlib/RingTheory/ClassGroup.lean Outdated

mathlib-triage Bot added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Apr 29, 2026

suggested change

0854ea2

mariainesdff added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 29, 2026

github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 29, 2026

mathlib-bors Bot pushed a commit that referenced this pull request Apr 29, 2026

feat(RingTheory/ClassGroup): prove mulEquiv (#35535)

ddecc33

We prove that isomorphic rings have isomorphic class groups. Co-authored by: @xgenereux. Co-authored-by: mariainesdff <mariaines.dff@gmail.com>

mathlib-bors Bot changed the title ~~feat(RingTheory/ClassGroup): prove mulEquiv~~ [Merged by Bors] - feat(RingTheory/ClassGroup): prove mulEquiv Apr 29, 2026

mathlib-bors Bot closed this Apr 29, 2026

mathlib-bors Bot deleted the class_group_equiv branch April 29, 2026 15:43

Conversation

mariainesdff commented Feb 19, 2026

Uh oh!

github-actions Bot commented Feb 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary cc9c9b7838

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mathlib-merge-conflicts Bot commented Feb 25, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

mathlib-bors Bot commented Apr 29, 2026

Uh oh!

mariainesdff commented Apr 29, 2026

Uh oh!

mathlib-bors Bot commented Apr 29, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

github-actions Bot commented Feb 19, 2026 •

edited

Loading