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 f318334181

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.map'
+ 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

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

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

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

Increase in tech debt: (relative, absolute) = (4.00, 0.00)

Current number	Change	Type
10036	4	backward.isDefEq

Current commit dc8a439359
Reference commit f318334181

You can run this locally as

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

Mathlib/RingTheory/FractionalIdeal/Operations.lean

Mathlib/RingTheory/Localization/FractionRing.lean

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

Mathlib/RingTheory/ClassGroup.lean

+      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

Mathlib/RingTheory/ClassGroup.lean

+        ← 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/RingTheory/FractionalIdeal/Operations.lean

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

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

Mathlib/Algebra/Ring/CompTypeclasses.lean

Mathlib/RingTheory/FractionalIdeal/Operations.lean

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

Mathlib/RingTheory/FractionalIdeal/Operations.lean

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

Mathlib/RingTheory/FractionalIdeal/Operations.lean

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

Mathlib/RingTheory/FractionalIdeal/Operations.lean

+  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?

Mathlib/RingTheory/FractionalIdeal/Operations.lean

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

Mathlib/RingTheory/FractionalIdeal/Operations.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Feb 19, 2026

View reviewed changes

Mathlib/RingTheory/Localization/FractionRing.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Feb 19, 2026

View reviewed changes

tb65536 reviewed Feb 20, 2026

View reviewed changes

Mathlib/RingTheory/FractionalIdeal/Operations.lean Outdated Show resolved Hide resolved

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

Mathlib/Algebra/Ring/CompTypeclasses.lean Outdated Show resolved Hide resolved

erdOne reviewed Feb 28, 2026

View reviewed changes

Mathlib/Algebra/Ring/CompTypeclasses.lean Show resolved Hide resolved

erdOne reviewed Feb 28, 2026

View reviewed changes

Mathlib/RingTheory/FractionalIdeal/Operations.lean Outdated Show resolved Hide resolved

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 unassigned mattrobball Apr 5, 2026

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 f318334181

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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

github-actions bot commented Feb 19, 2026 •

edited

Loading