Skip to content

chore(RingTheory/PicardGroup): drop StrongRankCondition assumptions in two lemmas #39231

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
mbkybky wants to merge 3 commits into
base: master
Choose a base branch
from
+3 −6
Open

chore(RingTheory/PicardGroup): drop StrongRankCondition assumptions in two lemmas #39231

Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
5117a8b
drop `StrongRankCondition` in two lemmas
mbkybky May 12, 2026
78085a6
Update PicardGroup.lean
mbkybky May 12, 2026
ec5f149
min_imports
mbkybky May 12, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
9 changes: 3 additions & 6 deletions Mathlib/RingTheory/PicardGroup.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,6 @@ public import Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
public import Mathlib.CategoryTheory.Monoidal.Skeleton
public import Mathlib.LinearAlgebra.Contraction
public import Mathlib.LinearAlgebra.LinearDisjoint
public import Mathlib.RingTheory.ClassGroup
public import Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
public import Mathlib.RingTheory.LocalRing.Module
public import Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
Expand Down Expand Up @@ -250,12 +249,10 @@ theorem free_iff_linearEquiv : Free R M ↔ Nonempty (M ≃ₗ[R] R) := by
considering the localization at a prime (which is free of rank 1) using the strong rank condition.
The ≥ direction fails in general but holds for domains and Noetherian rings,
see https://math.stackexchange.com/q/5089900 and https://mathoverflow.net/a/499611. -/
protected theorem finrank_eq_one [StrongRankCondition R] [Free R M] : finrank R M = 1 := by
cases subsingleton_or_nontrivial R
· rw [← rank_eq_one_iff_finrank_eq_one, rank_subsingleton]
· rw [(free_iff_linearEquiv.mp ‹_›).some.finrank_eq, finrank_self]
protected theorem finrank_eq_one [Free R M] : finrank R M = 1 := by
rw [(free_iff_linearEquiv.mp ‹_›).some.finrank_eq, CommSemiring.finrank_self]

theorem rank_eq_one [StrongRankCondition R] [Free R M] : Module.rank R M = 1 :=
theorem rank_eq_one [Free R M] : Module.rank R M = 1 :=
rank_eq_one_iff_finrank_eq_one.mpr (Invertible.finrank_eq_one R M)

open TensorProduct (comm lid) in
Expand Down
Loading