Theorems · Theorem · commutative algebra

Ideal.eq_top_of_mk_tensor_eq_one

∀ {R : Type u_5} [inst : CommRing R] [IsFractionRing R R] (I J : Ideal R) [inst_2 : Module.Invertible R ↥I]
  [inst_3 : Module.Invertible R ↥J], CommRing.Pic.mk R (TensorProduct R ↥I ↥J) = 1 → I = ⊤ ∧ J = ⊤

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.

Defined in

Mathlib.RingTheory.PicardGroup

Cited by

0 results in Mathlib

Foundations

Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingIsFractionRingModule.InvertibleModule.Invertible