feat(Counterexamples): invertible module not isomorphic to any ideal (leanprover-community#32027)

Author: alreadydone

Counterexamples.lean

@@ -11,6 +11,7 @@ import Counterexamples.GameMultiplication
 import Counterexamples.Girard
 import Counterexamples.HeawoodUnitDistance
 import Counterexamples.HomogeneousPrimeNotPrime
+import Counterexamples.InvertibleModuleNotIdeal
 import Counterexamples.IrrationalPowerOfIrrational
 import Counterexamples.MapFloor
 import Counterexamples.MonicNonRegular

Counterexamples/InvertibleModuleNotIdeal.lean

@@ -0,0 +1,56 @@
+/-
+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.Algebra.TrivSqZeroExt
+import Mathlib.Data.DFinsupp.Module
+import Mathlib.RingTheory.PicardGroup
+
+/-!
+# A class of examples of invertible modules that are not isomorphic to ideals
+
+References: https://math.stackexchange.com/a/5090562 or https://mathoverflow.net/a/499258
+-/
+
+variable (R : Type*) [CommRing R]
+
+/-- The trivial square-zero extension of a commutative ring R given by the direct sum
+R ⊕ ⨁ₘ R⧸m where m ranges over maximal ideals of R. -/
+abbrev SqZeroExtQuotMax := TrivSqZeroExt R (Π₀ m : MaximalSpectrum R, R ⧸ m.1)
+
+instance : IsFractionRing (SqZeroExtQuotMax R) (SqZeroExtQuotMax R) :=
+  IsFractionRing.self_iff_nonZeroDivisors_le_isUnit.mpr fun x hx ↦
+    TrivSqZeroExt.isUnit_iff_isUnit_fst.mpr <| of_not_not fun hr ↦ by
+    have ⟨M, hM, hrM⟩ := exists_max_ideal_of_mem_nonunits hr
+    classical
+    have := hx.1 (.inr <| .single ⟨M, hM⟩ 1) <| by
+      ext1; · simp
+      simpa [-DFinsupp.single_apply, ← DFinsupp.single_smul, DFinsupp.single_eq_zero]
+        using (Ideal.Quotient.mk_eq_mk_iff_sub_mem ..).mpr (by simpa)
+    simpa using congr(($this).snd)
+
+/-- R as an algebra over `SqZeroExtQuotMax R`. -/
+abbrev SqZeroExtQuotMax.algebraBase : Algebra (SqZeroExtQuotMax R) R := TrivSqZeroExt.algebraBase ..
+
+open CommRing (Pic) in
+/-- If the Picard group of a commutative ring R is nontrivial, then `SqZeroExtQuotMax R`
+has an invertible module (which is the base change of an invertible ideal of R)
+not isomorphic to any ideal. -/
+theorem SqZeroExtQuotMax.not_exists_linearEquiv_ideal_of_invertible [Nontrivial (Pic R)] :
+    ∃ M : Pic (SqZeroExtQuotMax R),
+    ¬ ∃ I : Ideal (SqZeroExtQuotMax R), Nonempty (M ≃ₗ[SqZeroExtQuotMax R] I) := by
+  by_contra! h
+  have ⟨M, hM⟩ := exists_ne (1 : Pic R)
+  have ⟨I, ⟨eI⟩⟩ := h (M.mapAlgebra R _)
+  have ⟨J, ⟨eJ⟩⟩ := h (M⁻¹.mapAlgebra R _)
+  have := Module.Invertible.congr eI
+  have := Module.Invertible.congr eJ
+  obtain ⟨rfl | rfl⟩ := I.eq_top_of_mk_tensor_eq_one J <| by
+    rw [Pic.mk_tensor, ← Pic.mk_eq_mk_iff.mpr ⟨eI⟩, ← Pic.mk_eq_mk_iff.mpr ⟨eJ⟩,
+      Pic.mk_eq_self, Pic.mk_eq_self, ← map_mul, mul_inv_cancel, map_one]
+  have eq := Pic.mk_eq_one_iff.mpr ⟨eI ≪≫ₗ Submodule.topEquiv⟩
+  rw [Pic.mk_eq_self] at eq
+  let := TrivSqZeroExt.algebraBase
+  have eq := congr(Pic.mapAlgebra (SqZeroExtQuotMax R) R $eq)
+  exact hM <| by rwa [map_one, Pic.mapAlgebra_mapAlgebra, Pic.mapAlgebra_self] at eq

Mathlib/Algebra/TrivSqZeroExt.lean

@@ -894,6 +894,18 @@ def fstHom : tsze R M →ₐ[S] R where
   map_add' := fst_add
   commutes' _r := fst_inl M _
 
+/-- `R'` as an algebra over `TrivSqZeroExt R' M`. Not an instance since it creates a different
+`Algebra (TrivSqZeroExt R' M) (TrivSqZeroExt R' M)` instance from `TrivSqZeroExt.algebra'`. -/
+abbrev algebraBase : Algebra (tsze R' M) R' where
+  algebraMap := (fstHom R' R' M).toRingHom
+  smul x r := x.fst * r
+  commutes' _ _ := mul_comm ..
+  smul_def' _ _ := rfl
+
+attribute [local instance] algebraBase in
+instance : IsScalarTower R' (tsze R' M) R' where
+  smul_assoc _ _ _ := mul_assoc ..
+
 /-- The canonical `S`-algebra inclusion `R → TrivSqZeroExt R M`. -/
 @[simps]
 def inlAlgHom : R →ₐ[S] tsze R M where

Mathlib/RingTheory/PicardGroup.lean

@@ -8,7 +8,7 @@ module
 public import Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
 public import Mathlib.CategoryTheory.Monoidal.Skeleton
 public import Mathlib.LinearAlgebra.Contraction
-public import Mathlib.LinearAlgebra.TensorProduct.Submodule
+public import Mathlib.LinearAlgebra.LinearDisjoint
 public import Mathlib.RingTheory.ClassGroup
 public import Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
 public import Mathlib.RingTheory.LocalRing.Module
@@ -525,7 +525,7 @@ variable (R) (A B : Type*) [CommSemiring A] [CommSemiring B] [Algebra R A]
 
 open AlgebraTensorModule in
 /-- Every `R`-algebra `A` gives rise to a homomorphism between Picard groups of `R` and `A`. -/
-@[simps] noncomputable def mapAlgebra [Algebra R A] : Pic R →* Pic A where
+@[simps] noncomputable def mapAlgebra : Pic R →* Pic A where
   toFun M := .mk A (A ⊗[R] M)
   map_one' := mk_eq_one_iff.mpr (Invertible.free_iff_linearEquiv.mp inferInstance)
   map_mul' _ _ := by
@@ -859,7 +859,9 @@ open CommRing Pic
 
 section Ideal
 
-variable (R M : Type*) [CommRing R] [AddCommGroup M] [Module R M] [Module.Invertible R M]
+variable (R M N : Type*) [CommRing R]
+variable [AddCommGroup M] [Module R M] [Module.Invertible R M]
+variable [AddCommGroup N] [Module R N] [Module.Invertible R N]
 
 /-- If `FractionRing R` has trivial Picard group,
 every invertible `R`-module is isomorphic to an ideal. -/
@@ -880,4 +882,22 @@ See https://mathoverflow.net/a/499611. -/
 example [IsNoetherianRing R] : ∃ I : Ideal R, Nonempty (M ≃ₗ[R] I) :=
   Module.Invertible.exists_linearEquiv_ideal R M
 
+variable {R} in
+/-- In a total ring of fractions, if two ideals are inverse to each other in the Picard group,
+the only possibility is that they are both the whole ring. -/
+theorem Ideal.eq_top_of_mk_tensor_eq_one [IsFractionRing R R] (I J : Ideal R)
+    [Module.Invertible R I] [Module.Invertible R J] (h : Pic.mk R (I ⊗[R] J) = 1) :
+    I = ⊤ ∧ J = ⊤ := by
+  have ⟨e⟩ := mk_eq_one_iff.mp h
+  have e := e.symm ≪≫ₗ Submodule.LinearDisjoint.mulMap
+    (.of_left_le_one_of_flat I J <| le_top.trans one_eq_top.ge)
+  have : IsUnit (e 1 : R) := IsFractionRing.self_iff_nonZeroDivisors_le_isUnit.mp ‹_› <|
+      IsRegular.mem_nonZeroDivisors <| isRightRegular_iff_isRegular.mp <| by
+    rw [IsRightRegular]
+    convert Subtype.val_injective.comp e.injective using 2
+    rw [← smul_eq_mul, ← Submodule.coe_smul, ← map_smul, smul_eq_mul, mul_one]
+    rfl
+  constructor <;> refine eq_top_of_isUnit_mem _ ?_ this
+  exacts [mul_le_right (e 1).2, mul_le_left (e 1).2]
+
 end Ideal