[Merged by Bors] - feat(RingTheory): invertible modules and Picard group by alreadydone · Pull Request #25337 · leanprover-community/mathlib4

alreadydone · 2025-05-31T20:57:27Z

github-actions · 2025-05-31T20:58:42Z

PR summary 595c2c615b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.RingTheory.PicardGroup` (new file)	1995

Declarations diff

+ AsModule
+ CommRing.Pic
+ Invertible
+ _root_.Units.submodule_invertible
+ bijective_curry
+ bijective_of_surjective
+ congr
+ embAlgebra
+ embAlgebra_injective
+ ext_iff
+ finrank_eq_one
+ free_iff_linearEquiv
+ instance (L) [AddCommMonoid L] [Module R L] [Module A L] [IsScalarTower R A L]
+ instance (M : (Skeleton <| ModuleCat.{u} R)ˣ) : Module.Invertible R M
+ instance : CoeSort (Pic R) (Type u) := ⟨AsModule⟩
+ instance : CommGroup (Pic R) := (equivShrink _).symm.commGroup
+ instance : FaithfulSMul R M
+ instance : Module.Finite R M := (finite_projective R M).1
+ instance : Module.Invertible A (A ⊗[R] M)
+ instance : Module.Invertible R (Dual R M) := .left (linearEquiv R M)
+ instance : Module.Invertible R (Finite.repr R M) := .congr (Finite.reprEquiv R M).symm
+ instance : Module.Invertible R R := .left (TensorProduct.lid R R)
+ instance : Projective R M := (finite_projective R M).2
+ instance : Small.{u} (Skeleton <| ModuleCat.{u} R)ˣ
+ instance [IsLocalRing R] : Subsingleton (Pic R)
+ instance [Module.Invertible R N] : Module.Invertible R (M ⊗[R] N)
+ instance [Subsingleton (Pic R)] : Free R M
+ inv_eq_dual
+ kerRepr
+ lTensor_bijective_iff
+ lTensor_injective_iff
+ lTensor_surjective_iff
+ left
+ leftCancelEquiv
+ leftCancelEquiv_comp_lTensor_comp_symm
+ linearEquiv
+ linearEquivDual
+ mk
+ mk.linearEquiv
+ mk_dual
+ mk_eq_iff
+ mk_eq_mk_iff
+ mk_eq_one
+ mk_eq_one_iff
+ mk_eq_self
+ mk_self
+ mk_tensor
+ mul_eq_tensor
+ projective_of_isUnit
+ projective_unit
+ rTensorEquiv
+ rTensorInv
+ rTensorInv_injective
+ rTensorInv_leftInverse
+ rTensor_bijective_iff
+ rTensor_injective_iff
+ rTensor_surjective_iff
+ rank_eq_one
+ repr
+ reprEquiv
+ right
+ rightCancelEquiv
+ rightCancelEquiv_comp_rTensor_comp_symm
+ subsingleton_iff
+ tensorEquivMul
+ tensorInvEquiv
+ toModuleEnd_bijective
+ toSubmodule
+ unitsToPic

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

Mathlib/RingTheory/PicardGroup.lean

kckennylau

Thanks for the great work! 🎉

Mathlib/RingTheory/PicardGroup.lean

kckennylau · 2025-06-01T08:34:17Z

Mathlib/RingTheory/PicardGroup.lean

+      rw [LinearEquiv.coe_trans, LinearEquiv.eq_comp_toLinearMap_symm]; ext; rfl
+    rw [this]; apply LinearEquiv.bijective
+
+protected theorem left : Module.Invertible R M := .right (TensorProduct.comm R N M ≪≫ₗ e)


Should left be called right? I don't know if the mathlib convention might clash with the math convention

Why should it be called right? This theorem states the left factor in M ⊗[R] N ≃ₗ[R] R is invertible.

Because I interpret the math statement as saying that M is invertible if it has a right inverse 😆

Mathlib/RingTheory/PicardGroup.lean

kckennylau · 2025-06-01T21:51:30Z

Mathlib/RingTheory/PicardGroup.lean

+- All unique factorization domains have trivial Picard group.
+
+- Establish other characterizations of invertible modules, e.g. they are modules that
+  becomes free of rank one when localized at every prime ideal.


Suggested change

becomes free of rank one when localized at every prime ideal.

become free of rank one when localized at any prime ideal.

"any" doesn't feel right to me. "at all prime ideals" is an alternative.

Mathlib/RingTheory/PicardGroup.lean

kckennylau · 2025-06-01T22:17:33Z

LGTM! I would be very happy to be able to use Pic in Mathlib4!

riccardobrasca

This can probably be improved a bit, but I think it's easier to have it and work on lit later, thanks!

bors d+

Mathlib/RingTheory/Finiteness/Cardinality.lean

Mathlib/RingTheory/PicardGroup.lean

mathlib-bors · 2025-08-13T12:30:47Z

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

alreadydone · 2025-08-13T15:39:49Z

Mathlib/RingTheory/PicardGroup.lean

+/- TODO: generalize ≤ to arbitrary invertible modules over any commutative semiring by considering
+the localization at a prime, once we show inverible modules over local semirings are free.
+It is not clear whether ≥ holds in general but it holds for domains. -/
+theorem finrank_eq_one [StrongRankCondition R] [Free R M] : finrank R M = 1 := by


If we define the rank of a module to be the maximum or minimum of local ranks, then every invertible module (not necessarily free) has rank 1. But in mathlib ranks are defined in terms of size of linearly independent sets, and I'm not sure whether one of the directions holds in full generality (my AIs fail to give a counterexample so far).

The TODO comment isn't completely substantiated as I don't know whether local comm. semirings satisfy the strong rank condition, so the wording has been changed. If there's no further comments I'll merge in one day.

Mathlib/RingTheory/PicardGroup.lean

alreadydone · 2025-08-15T22:13:00Z

Thanks 🎉
bors r+

mathlib-bors · 2025-08-15T23:28:09Z

Build failed (retrying...):

CI Success

mathlib-bors · 2025-08-15T23:53:08Z

Canceled.

alreadydone · 2025-08-16T07:55:15Z

bors r+

mathlib-bors · 2025-08-16T08:33:41Z

Pull request successfully merged into master.

Build succeeded:

CI Success

* origin/master: (508 commits) feat(Logic/Basic): forall_and_index (leanprover-community#27737) feat(Algebra/intNorm): `x` divides `intNorm x` (leanprover-community#28021) feat(RingTheory/MvPolynomial/MonomialOrder): some lemmas about degree (leanprover-community#26000) chore: more elementary Motzkin polynomial proof (leanprover-community#28482) feat: e-seminormed monoid (leanprover-community#27385) feat(RingTheory): ` (⊥ : Ideal R) ^ n = ⊥` (leanprover-community#28171) fix(LinearAlgebra/Dimension/ErdosKaplansky): authorship (leanprover-community#28513) chore: golf entire `X_pow_eq_monomial` (leanprover-community#28504) feat(RingTheory): invertible modules and Picard group (leanprover-community#25337) chore: use delta `deriving` for leanprover-community#380 (leanprover-community#28498) feat: add bilinear maps for vector/matrix products (leanprover-community#28130) feat(Counterexamples): topologists' sine curve (leanprover-community#25833) feat(Analysis/Convex): doubly stochastic matrices have operator norm at most one (leanprover-community#28453) chore(Topology/Compactification): deprecate duplicate `ultrafilter_pure_injective` (leanprover-community#28436) feat: add `@[simp]` to `Multiset.cons_le_cons` and `Finset.insert_subset_insert` (leanprover-community#28285) feat: make `ring` work for semifields (leanprover-community#28494) feat: filtering lists and bounded quantifiers are primitive recursive (leanprover-community#26295) chore(Analysis/Analytic): split `Analytic.Basic` (leanprover-community#26270) refactor: tidy `mulVec` and `vecMul` lemmas about `•` (leanprover-community#28450) feat(Order/WellFounded): Acc and infinite descending chain (leanprover-community#28120) feat(NumberTheory/Padics): {Int,Rat}.padicValuation (leanprover-community#27667) chore(*): address a few timeout-related porting notes (leanprover-community#28483) feat(Algebra): toAlgebra_algebraMap (leanprover-community#28238) feat(Shrink): `IsCancelMul` instance (leanprover-community#28407) chore(Geometry): golf entire `chart_eq'` and `orthogonalProjection_orthogonalProjection` (leanprover-community#28485) feat: shifted geometric series and a `ProbabilityMeasure` version of `measure_iUnion_le` (leanprover-community#28087) chore(LinearAlgebra/PiTensorProduct): `rw` away use of `erw` in `lifts_zero` (leanprover-community#27554) feat(RingTheory): faithfully flat ring maps (leanprover-community#24530) chore(Geometry/RingedSpace): remove use of `erw` in `stalkSpecializes_stalkMap` (leanprover-community#27656) chore: add the Brownian motion project to downstream_repos.yml (leanprover-community#28459) feat(CategoryTheory/Sites/SheafOfTypes): composition of a sheaf with uliftFunctor is still a sheaf (leanprover-community#27816) feat(Valuation/DiscreteValuationRel): val relations with compatible valuations to Zm0 are IsDiscrete (leanprover-community#27213) chore(*): process a bunch of `aesop`-related porting notes (leanprover-community#28402) feat(CategoryTheory): abstract argument for the stability under transfinite compositions (leanprover-community#26030) chore: bump toolchain to v4.23.0-rc2 (leanprover-community#28454) chore(FieldTheory/Finite): fermat's little theorem in Nat form (leanprover-community#27962) feat(Combinatorics/SimpleGraph/Paths): add theorem `SimpleGraph.Walk.IsPath.concat` (leanprover-community#27582) feat(Slope): slope_pos_iff_of_le and related lemmas (leanprover-community#28039) feat: tactic analysis framework (leanprover-community#26683) chore(Data/EReal): deprecate `add_pos_of_nonneg_of_pos` and `add_ne_top_iff_of_ne_bot` (duplicates) (leanprover-community#28424) feat(MathlibTest/FieldSimp): add a few more tests (leanprover-community#28413) chore(RingTheory/HahnSeries): deprecate duplicate `orderTop_add_orderTop_le_orderTop_mul` (leanprover-community#28231) chore(AlgebraicGeometry/IdealSheaf): deprecate duplicate `AlgebraicGeometry.Scheme.IdealSheafData.Scheme.zeroLocus_radical` (leanprover-community#28202) feat(Algebra/Order): ArchimedeanClass ball (leanprover-community#27885) chore(Geometry/RingedSpace): remove use of `erw` in `isUnit_of_isUnit_germ` (leanprover-community#27660) feat(SkewMonoidAlgebra): coeff_mul lemmas (leanprover-community#27255) chore(LinearAlgebra): golf entire `isUnit_det` (leanprover-community#28438) chore(FieldTheory/IntermediateField): golf entire `coe_sum` and `coe_prod` (leanprover-community#28431) feat: separate linter error message for empty doc-strings (leanprover-community#27895) feat(RingTheory/PowerSeries/Binomial): add basic lemmas, golf (leanprover-community#27497) ...

…munity#25337)

alreadydone requested a review from kckennylau May 31, 2025 20:57

alreadydone added t-algebra Algebra (groups, rings, fields, etc) awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. labels May 31, 2025

alreadydone force-pushed the PicardGroup branch 7 times, most recently from 9f641b2 to a4b406d Compare June 1, 2025 00:00

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 1, 2025

feat(RingTheory): invertible modules and Picard group

396dfb9

alreadydone force-pushed the PicardGroup branch from a4b406d to 396dfb9 Compare June 1, 2025 00:34

erdOne reviewed Jun 1, 2025

View reviewed changes

Mathlib/RingTheory/PicardGroup.lean Show resolved Hide resolved

kckennylau reviewed Jun 1, 2025

View reviewed changes

alreadydone added 4 commits June 1, 2025 16:40

references adjustments

5950a5c

address review

1be4749

rename Module.Invertible.toPic to CommRing.Pic.mk

55809b3

docstring

f9f5e4e

kckennylau reviewed Jun 1, 2025

View reviewed changes

alreadydone added 2 commits June 1, 2025 23:42

address review

da4c535

add FaithfulSMul and bijective_of_surjective

3548d5e

alreadydone force-pushed the PicardGroup branch from e713a94 to 3548d5e Compare June 2, 2025 02:49

leanprover-community-bot-assistant assigned riccardobrasca Aug 4, 2025

grunweg added t-ring-theory Ring theory and removed t-algebra Algebra (groups, rings, fields, etc) labels Aug 5, 2025

riccardobrasca approved these changes Aug 13, 2025

View reviewed changes

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Aug 13, 2025

address review

b65bb25

alreadydone commented Aug 13, 2025

View reviewed changes

fix comment on finrank_eq_one

9e2b429

alreadydone force-pushed the PicardGroup branch from 52a2699 to 9e2b429 Compare August 14, 2025 22:41

alreadydone commented Aug 14, 2025

View reviewed changes

Mathlib/RingTheory/PicardGroup.lean Outdated Show resolved Hide resolved

correction

27dde83

mathlib-bors bot pushed a commit that referenced this pull request Aug 15, 2025

feat(RingTheory): invertible modules and Picard group (#25337)

a77e608

mathlib-bors bot pushed a commit that referenced this pull request Aug 15, 2025

feat(RingTheory): invertible modules and Picard group (#25337)

d52ca9b

Merge branch 'master' into PicardGroup

f16a9c0

fixes

725546c

mathlib-bors bot pushed a commit that referenced this pull request Aug 16, 2025

feat(RingTheory): invertible modules and Picard group (#25337)

c776b59

mathlib-bors bot changed the title ~~feat(RingTheory): invertible modules and Picard group~~ [Merged by Bors] - feat(RingTheory): invertible modules and Picard group Aug 16, 2025

mathlib-bors bot closed this Aug 16, 2025

mathlib-bors bot deleted the PicardGroup branch August 16, 2025 08:33

Paul-Lez pushed a commit to Paul-Lez/mathlib4 that referenced this pull request Aug 23, 2025

feat(RingTheory): invertible modules and Picard group (leanprover-com…

081bbbd

…munity#25337)

pechersky pushed a commit to pechersky/mathlib4 that referenced this pull request Aug 25, 2025

feat(RingTheory): invertible modules and Picard group (leanprover-com…

155cdc0

…munity#25337)

	becomes free of rank one when localized at every prime ideal.
	become free of rank one when localized at any prime ideal.

Conversation

alreadydone commented May 31, 2025

Uh oh!

github-actions bot commented May 31, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 595c2c615b

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

kckennylau left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

kckennylau Jun 1, 2025

Choose a reason for hiding this comment

Uh oh!

alreadydone Jun 1, 2025

Choose a reason for hiding this comment

Uh oh!

kckennylau Jun 1, 2025

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!

kckennylau Jun 1, 2025

Choose a reason for hiding this comment

Uh oh!

alreadydone Jun 1, 2025

Choose a reason for hiding this comment

Uh oh!

Uh oh!

kckennylau commented Jun 1, 2025

Uh oh!

riccardobrasca left a comment

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!

mathlib-bors bot commented Aug 13, 2025

Uh oh!

alreadydone Aug 13, 2025

Choose a reason for hiding this comment

Uh oh!

alreadydone Aug 14, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

alreadydone commented Aug 15, 2025

Uh oh!

mathlib-bors bot commented Aug 15, 2025

Uh oh!

mathlib-bors bot commented Aug 15, 2025

Uh oh!

alreadydone commented Aug 16, 2025

Uh oh!

mathlib-bors bot commented Aug 16, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

github-actions bot commented May 31, 2025 •

edited

Loading

alreadydone Aug 14, 2025 •

edited

Loading