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

@[reducible, inline]

abbrev SqZeroExtQuotMax (R : Type u_1) [CommRing R] : Type u_1

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.

Equations

• SqZeroExtQuotMax R = TrivSqZeroExt R (Π₀ (m : MaximalSpectrum R), R ⧸ m.asIdeal)

instance instIsFractionRingSqZeroExtQuotMax (R : Type u_1) [CommRing R] : IsFractionRing (SqZeroExtQuotMax R) (SqZeroExtQuotMax R)

@[reducible, inline]

abbrev SqZeroExtQuotMax.algebraBase (R : Type u_1) [CommRing R] : Algebra (SqZeroExtQuotMax R) R

R as an algebra over SqZeroExtQuotMax R.

Equations

• SqZeroExtQuotMax.algebraBase R = TrivSqZeroExt.algebraBase R (Π₀ (m : MaximalSpectrum R), R ⧸ m.asIdeal)

theorem SqZeroExtQuotMax.not_exists_linearEquiv_ideal_of_invertible (R : Type u_1) [CommRing R] [Nontrivial (CommRing.Pic R)] : ∃ (M : CommRing.Pic (SqZeroExtQuotMax R)), ¬∃ (I : Ideal (SqZeroExtQuotMax R)), Nonempty (M.AsModule ≃ₗ[SqZeroExtQuotMax R] ↥I)

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.