feat(RingTheory): finite flat constant rank module over semilocal ring is free (#31241)

https://stacks.math.columbia.edu/tag/02M9

As a consequence, the Picard group of any semilocal ring is trivial.

Author: alreadydone

Mathlib.lean

@@ -5734,6 +5734,7 @@ import Mathlib.RingTheory.Ideal.Pointwise
 import Mathlib.RingTheory.Ideal.Prime
 import Mathlib.RingTheory.Ideal.Prod
 import Mathlib.RingTheory.Ideal.Quotient.Basic
+import Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
 import Mathlib.RingTheory.Ideal.Quotient.Defs
 import Mathlib.RingTheory.Ideal.Quotient.Index
 import Mathlib.RingTheory.Ideal.Quotient.Nilpotent

Mathlib/LinearAlgebra/TensorProduct/Pi.lean

@@ -105,6 +105,11 @@ lemma piRight_symm_single (x : N) (i : ι) (m : M i) :
     (piRight R S N M).symm (Pi.single i (x ⊗ₜ m)) = x ⊗ₜ Pi.single i m := by
   simp [piRight]
 
+/-- Tensor product commutes with finite products on the left.
+TODO: generalize to `S`-linear. -/
+@[simp] def piLeft : (∀ i, M i) ⊗[R] N ≃ₗ[R] ∀ i, M i ⊗[R] N :=
+  TensorProduct.comm .. ≪≫ₗ piRight .. ≪≫ₗ .piCongrRight fun _ ↦ TensorProduct.comm ..
+
 end
 
 private def piScalarRightHomBil : N →ₗ[S] (ι → R) →ₗ[R] (ι → N) where

Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean

@@ -290,7 +290,7 @@ theorem lTensor_exact : Exact (lTensor Q f) (lTensor Q g) := by
 
 /-- Right-exactness of tensor product -/
 lemma lTensor_mkQ (N : Submodule R M) :
-    ker (lTensor Q (N.mkQ)) = range (lTensor Q N.subtype) := by
+    ker (lTensor Q N.mkQ) = range (lTensor Q N.subtype) := by
   rw [← exact_iff]
   exact lTensor_exact Q (LinearMap.exact_subtype_mkQ N) (Submodule.mkQ_surjective N)
 

Mathlib/RingTheory/Ideal/Quotient/ChineseRemainder.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2025 Junyan Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Junyan Xu
+-/
+import Mathlib.LinearAlgebra.TensorProduct.Pi
+import Mathlib.LinearAlgebra.TensorProduct.RightExactness
+import Mathlib.RingTheory.Ideal.Quotient.Operations
+
+/-! # Module version of Chinese remainder theorem
+-/
+
+open Function
+
+variable {R : Type*} [CommRing R] {ι : Type*}
+variable (M : Type*) [AddCommGroup M] [Module R M]
+variable (I : ι → Ideal R) (hI : Pairwise (IsCoprime on I))
+
+namespace Ideal
+
+open TensorProduct LinearMap
+
+lemma pi_mkQ_rTensor [Fintype ι] [DecidableEq ι] :
+    (LinearMap.pi fun i ↦ (I i).mkQ).rTensor M = (piLeft ..).symm.toLinearMap ∘ₗ
+      .pi (fun i ↦ TensorProduct.mk R (R ⧸ I i) M 1) ∘ₗ TensorProduct.lid R M := by
+  ext; simp [LinearMap.pi, LinearEquiv.piCongrRight]
+
+variable [Finite ι]
+include hI
+
+attribute [local instance] Fintype.ofFinite
+
+/-- A form of Chinese remainder theorem for modules, part I: if ideals `Iᵢ` of `R` are pairwise
+coprime, then for any `R`-module `M`, the natural map `M → Πᵢ (R ⧸ Iᵢ) ⊗[R] M` is surjective. -/
+theorem pi_tensorProductMk_quotient_surjective :
+    Surjective (LinearMap.pi fun i ↦ TensorProduct.mk R (R ⧸ I i) M 1) := by
+  have := rTensor_surjective M (pi_mkQ_surjective hI)
+  classical rw [pi_mkQ_rTensor] at this
+  simpa using this
+
+/-- A form of Chinese remainder theorem for modules, part II: if ideals `Iᵢ` of `R` are pairwise
+coprime, then for any `R`-module `M`, the kernel of `M → Πᵢ (R ⧸ Iᵢ) ⊗[R] M` equals `(⋂ᵢ Iᵢ) • M`.
+-/
+theorem ker_tensorProductMk_quotient :
+    ker (LinearMap.pi fun i ↦ TensorProduct.mk R (R ⧸ I i) M 1) =
+      (⨅ i, I i) • (⊤ : Submodule R M) := by
+  have := rTensor_exact M (exact_subtype_ker_map _) (pi_mkQ_surjective hI)
+  rw [← (TensorProduct.lid R M).conj_exact_iff_exact, exact_iff] at this
+  convert this
+  · classical simp [pi_mkQ_rTensor, LinearMap.comp_assoc]
+  refine le_antisymm (Submodule.smul_le.mpr fun r hr m _ ↦ ⟨⟨r, ?_⟩ ⊗ₜ m, rfl⟩) ?_
+  · simpa only [ker_pi, Submodule.ker_mkQ]
+  rintro _ ⟨x, rfl⟩
+  refine x.induction_on (by simp) (fun r m ↦ Submodule.smul_mem_smul ?_ ⟨⟩) fun _ _ ↦ ?_
+  · simpa only [← (I _).ker_mkQ, ← ker_pi] using Subtype.mem _
+  · simpa using add_mem
+
+end Ideal

Mathlib/RingTheory/Ideal/Quotient/Operations.lean

@@ -238,17 +238,21 @@ noncomputable def quotientInfRingEquivPiQuotient (f : ι → Ideal R)
 /-- Corollary of Chinese Remainder Theorem: if `Iᵢ` are pairwise coprime ideals in a
 commutative ring then the canonical map `R → ∏ (R ⧸ Iᵢ)` is surjective. -/
 lemma pi_quotient_surjective {I : ι → Ideal R}
-    (hf : Pairwise fun i j ↦ IsCoprime (I i) (I j)) (x : (i : ι) → R ⧸ I i) :
+    (hf : Pairwise (IsCoprime on I)) (x : (i : ι) → R ⧸ I i) :
     ∃ r : R, ∀ i, r = x i := by
   obtain ⟨y, rfl⟩ := Ideal.quotientInfToPiQuotient_surj hf x
   obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective y
   exact ⟨r, fun i ↦ rfl⟩
 
+lemma pi_mkQ_surjective {I : ι → Ideal R} (hI : Pairwise (IsCoprime on I)) :
+    Surjective (LinearMap.pi fun i ↦ (I i).mkQ) :=
+  fun x ↦ have ⟨r, eq⟩ := pi_quotient_surjective hI x; ⟨r, funext eq⟩
+
 -- variant of `IsDedekindDomain.exists_forall_sub_mem_ideal` which doesn't assume Dedekind domain!
 /-- Corollary of Chinese Remainder Theorem: if `Iᵢ` are pairwise coprime ideals in a
 commutative ring then given elements `xᵢ` you can find `r` with `r - xᵢ ∈ Iᵢ` for all `i`. -/
 lemma exists_forall_sub_mem_ideal
-    {I : ι → Ideal R} (hI : Pairwise fun i j ↦ IsCoprime (I i) (I j)) (x : ι → R) :
+    {I : ι → Ideal R} (hI : Pairwise (IsCoprime on I)) (x : ι → R) :
     ∃ r : R, ∀ i, r - x i ∈ I i := by
   obtain ⟨y, hy⟩ := Ideal.pi_quotient_surjective hI (fun i ↦ x i)
   exact ⟨y, fun i ↦ (Submodule.Quotient.eq (I i)).mp <| hy i⟩

Mathlib/RingTheory/LocalProperties/Exactness.lean

@@ -28,9 +28,15 @@ variable {R M N L : Type*} [CommSemiring R] [AddCommMonoid M] [Module R M]
   [AddCommMonoid N] [Module R N] [AddCommMonoid L] [Module R L]
 
 variable
+  (Rₚ : ∀ (P : Ideal R) [P.IsMaximal], Type*)
+  [∀ (P : Ideal R) [P.IsMaximal], CommSemiring (Rₚ P)]
+  [∀ (P : Ideal R) [P.IsMaximal], Algebra R (Rₚ P)]
+  [∀ (P : Ideal R) [P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P]
   (Mₚ : ∀ (P : Ideal R) [P.IsMaximal], Type*)
   [∀ (P : Ideal R) [P.IsMaximal], AddCommMonoid (Mₚ P)]
   [∀ (P : Ideal R) [P.IsMaximal], Module R (Mₚ P)]
+  [∀ (P : Ideal R) [P.IsMaximal], Module (Rₚ P) (Mₚ P)]
+  [∀ (P : Ideal R) [P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)]
   (f : ∀ (P : Ideal R) [P.IsMaximal], M →ₗ[R] Mₚ P)
   [∀ (P : Ideal R) [P.IsMaximal], IsLocalizedModule.AtPrime P (f P)]
   (Nₚ : ∀ (P : Ideal R) [P.IsMaximal], Type*)
@@ -76,6 +82,17 @@ theorem exact_of_isLocalized_maximal (H : ∀ (J : Ideal R) [J.IsMaximal],
   simp only [mem_range, mem_ker] at this ⊢
   exact this x
 
+theorem LinearIndependent.of_isLocalized_maximal {ι} (v : ι → M)
+    (H : ∀ (P : Ideal R) [P.IsMaximal], LinearIndependent (Rₚ P) (f P ∘ v)) :
+    LinearIndependent R v :=
+  let l (P) [IsMaximal P] := Finsupp.mapRange.linearMap (α := ι) (Algebra.linearMap R (Rₚ P))
+  injective_of_isLocalized_maximal _ (fun P _ ↦ l P) _ f _ fun P _ ↦ by
+    simp_rw [LinearIndependent, ← LinearMap.coe_restrictScalars R (S := Rₚ _)] at H
+    convert H P
+    apply linearMap_ext (S := P.primeCompl) (l P) (f P)
+    ext
+    simp [IsLocalizedModule.map_comp, l]
+
 end isLocalized_maximal
 
 section localized_maximal

Mathlib/RingTheory/LocalRing/Module.lean

@@ -8,10 +8,13 @@ import Mathlib.Algebra.Module.Torsion
 import Mathlib.LinearAlgebra.Dual.Lemmas
 import Mathlib.RingTheory.FiniteType
 import Mathlib.RingTheory.Flat.EquationalCriterion
+import Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder
+import Mathlib.RingTheory.LocalProperties.Exactness
 import Mathlib.RingTheory.LocalRing.ResidueField.Basic
 import Mathlib.RingTheory.LocalRing.ResidueField.Ideal
 import Mathlib.RingTheory.Nakayama
 import Mathlib.RingTheory.Support
+import Mathlib.RingTheory.TensorProduct.Free
 
 /-!
 # Finite modules over local rings
@@ -364,3 +367,59 @@ theorem IsLocalRing.split_injective_iff_lTensor_residueField_injective [IsLocalR
     exact Module.projective_lifting_property _ _ (Submodule.mkQ_surjective _)
 
 end
+
+namespace Module
+
+open Ideal TensorProduct Submodule
+
+variable (R M) [Finite (MaximalSpectrum R)] [AddCommGroup M] [Module R M]
+
+/-- If `M` is a finite flat module over a commutative semilocal ring `R` that has the same rank `n`
+at every maximal ideal, then `M` is free of rank `n`. -/
+@[stacks 02M9] theorem nonempty_basis_of_flat_of_finrank_eq [Module.Finite R M] [Flat R M]
+    (n : ℕ) (rk : ∀ P : MaximalSpectrum R, finrank (R ⧸ P.1) ((R ⧸ P.1) ⊗[R] M) = n) :
+    Nonempty (Basis (Fin n) R M) := by
+  let := @Quotient.field
+  have coprime : Pairwise fun I J : MaximalSpectrum R ↦ IsCoprime I.1 J.1 :=
+    fun _ _ ne ↦ isCoprime_of_isMaximal (MaximalSpectrum.ext_iff.ne.mp ne)
+  /- For every maximal ideal `P`, `R⧸P ⊗[R] M` is an `n`-dimensional vector space over the field
+    `R⧸P` by assumption, so we can choose a basis `b' P` indexed by `Fin n`. -/
+  have b' (P) := Module.finBasisOfFinrankEq _ _ (rk P)
+  /- By Chinese remainder theorem for modules, there exist `n` elements `b i : M` that reduces
+    to `b' P i` modulo each maximal ideal `P`. -/
+  choose b hb using fun i ↦ pi_tensorProductMk_quotient_surjective M _ coprime (b' · i)
+  /- It suffices to show `b` spans `M` and is linearly independent when localized at each
+    maximal ideal. -/
+  refine ⟨.mk (v := b) (.of_isLocalized_maximal (fun P _ ↦ Localization P.primeCompl) _
+    (fun P _ ↦ TensorProduct.mk R (Localization P.primeCompl) M 1) _ fun P _ ↦ ?_) ?_⟩
+  · /- Since `M` is finite flat, linear independence in `Rₚ ⊗[R] M` is equivalent to linear
+      independence in `Rₚ⧸PRₚ ⊗[Rₚ] (Rₚ ⊗[R] M) ≃ Rₚ⧸PRₚ ⊗[R⧸P] (R⧸P ⊗[R] M)`. -/
+    apply IsLocalRing.linearIndependent_of_flat
+    rw [← LinearMap.linearIndependent_iff _ (AlgebraTensorModule.cancelBaseChange R _ _ _ M).ker]
+    convert LinearMap.linearIndependent_iff _ (AlgebraTensorModule.cancelBaseChange R _ _ _ M).ker
+      |>.mpr (Algebra.TensorProduct.basis P.ResidueField (b' ⟨P, ‹_›⟩)).linearIndependent
+    ext
+    simp [← funext_iff.mp (hb _)]
+  · -- To show `b` spans `M`, it suffices to show `M = Rb + J(R)M` by Nakayama.
+    refine Submodule.le_of_le_smul_of_le_jacobson_bot (Module.finite_def.mp ‹_›) le_rfl fun m _ ↦ ?_
+    /- For each `m : M` and maximal ideal `P`, `1 ⊗ₜ m : R⧸P ⊗[R] M` is in the span of `b' P`.
+      By Chinese remainder theorem for rings, we may lift the coefficients `r i : R`. -/
+    choose r hr using fun i ↦ pi_quotient_surjective coprime fun P ↦ (b' P).repr (1 ⊗ₜ m) i
+    rw [← add_sub_cancel (∑ i, r i • b i) m]
+    /- It suffices to show `m - ∑ i, r i • b i` is `J(R)M`, which equals the kernel of
+      `M → Πₚ R⧸P ⊗[R] M` by Chinese remainder theorem for modules. -/
+    refine Submodule.add_mem_sup (sum_mem fun i _ ↦ smul_mem _ _ <| subset_span ⟨i, rfl⟩) <|
+      ((ker_tensorProductMk_quotient M _ coprime).le.trans <| smul_mono_left <|
+        le_sInf fun i hi ↦ iInf_le_of_le ⟨i, hi.2⟩ le_rfl) ?_
+    ext P
+    simp_rw [map_sub, map_sum, map_smul, hb, Pi.sub_apply]
+    refine sub_eq_zero.mpr (((b' P).sum_repr _).symm.trans ?_)
+    simp [← hr, ← Quotient.algebraMap_eq]
+
+@[stacks 02M9] theorem free_of_flat_of_finrank_eq [Module.Finite R M] [Flat R M]
+    (n : ℕ) (rk : ∀ P : MaximalSpectrum R, finrank (R ⧸ P.1) ((R ⧸ P.1) ⊗[R] M) = n) :
+    Free R M :=
+  have ⟨b⟩ := nonempty_basis_of_flat_of_finrank_eq R M n rk
+  .of_basis b
+
+end Module

Mathlib/RingTheory/Localization/BaseChange.lean

@@ -139,14 +139,14 @@ lemma Algebra.isPushout_of_isLocalization [IsLocalization (Algebra.algebraMapSub
     Algebra.IsPushout R T A B :=
   (Algebra.isLocalization_iff_isPushout S _).mp inferInstance
 
+variable (R M) in
 open TensorProduct in
-instance (R M : Type*) [CommRing R] [AddCommGroup M] [Module R M]
-    {α} (S : Submonoid R) {Mₛ} [AddCommGroup Mₛ] [Module R Mₛ] (f : M →ₗ[R] Mₛ)
-    [IsLocalizedModule S f] : IsLocalizedModule S (Finsupp.mapRange.linearMap (α := α) f) := by
+instance {α} [IsLocalizedModule S f] :
+    IsLocalizedModule S (Finsupp.mapRange.linearMap (α := α) f) := by
   classical
-  let e : Localization S ⊗[R] M ≃ₗ[R] Mₛ :=
+  let e : Localization S ⊗[R] M ≃ₗ[R] M' :=
     (LocalizedModule.equivTensorProduct S M).symm.restrictScalars R ≪≫ₗ IsLocalizedModule.iso S f
-  let e' : Localization S ⊗[R] (α →₀ M) ≃ₗ[R] (α →₀ Mₛ) :=
+  let e' : Localization S ⊗[R] (α →₀ M) ≃ₗ[R] (α →₀ M') :=
     finsuppRight R (Localization S) M α ≪≫ₗ Finsupp.mapRange.linearEquiv e
   suffices IsLocalizedModule S (e'.symm.toLinearMap ∘ₗ Finsupp.mapRange.linearMap f) by
     convert this.of_linearEquiv (e := e')

Mathlib/RingTheory/PicardGroup.lean

@@ -47,7 +47,6 @@ invertible `R`-modules (in the sense that `M` is invertible if there exists anot
 
 Show:
 - The Picard group of a commutative domain is isomorphic to its ideal class group.
-- All commutative semi-local rings, in particular Artinian rings, have trivial Picard group.
 - All unique factorization domains have trivial Picard group.
 - Invertible modules over a commutative ring have the same cardinality as the ring.
 
@@ -246,13 +245,13 @@ 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 without embedded
 components, see https://math.stackexchange.com/q/5089900. -/
-theorem finrank_eq_one [StrongRankCondition R] [Free R M] : finrank R M = 1 := by
+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]
 
 theorem rank_eq_one [StrongRankCondition R] [Free R M] : Module.rank R M = 1 :=
-  rank_eq_one_iff_finrank_eq_one.mpr (finrank_eq_one R M)
+  rank_eq_one_iff_finrank_eq_one.mpr (Invertible.finrank_eq_one R M)
 
 open TensorProduct (comm lid) in
 theorem toModuleEnd_bijective : Function.Bijective (toModuleEnd R (S := R) M) := by
@@ -499,6 +498,11 @@ instance [Subsingleton (Pic R)] : Free R M :=
 instance [IsLocalRing R] : Subsingleton (Pic R) :=
   subsingleton_iff.mpr fun _ _ _ _ ↦ free_of_flat_of_isLocalRing
 
+/-- The Picard group of a semilocal ring is trivial. -/
+instance [Finite (MaximalSpectrum R)] : Subsingleton (Pic R) :=
+  subsingleton_iff.mpr fun _ _ _ _ ↦ free_of_flat_of_finrank_eq _ _ 1
+    fun _ ↦ let _ := @Ideal.Quotient.field; Invertible.finrank_eq_one ..
+
 end CommRing.Pic
 
 end CommRing