Mathoverflow 507128

Reference: mathoverflow/507128 asked by user Junyan Xu

theorem Mathoverflow507128.exists_isFractionRing_self_ideal_ne_top_invertible : ∃ (R : Type) (x : CommRing R) (_ : IsFractionRing R R) (I : Ideal R), I ≠ ⊤ ∧ Module.Invertible R ↥I

There exists a proper ideal I in a (commutative) total ring R of fractions that is an invertible module. If I ⊊ R is such an example, I must have infinite order in the Picard group, and R must not be Noetherian (otherwise it must be semi-local and therefore have trivial Picard group).