Theorems · Definition · commutative algebra

Submodule.unitsQuotEquivRelPic

(R : Type u) →
  (A : Type u_4) →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring A] →
        [inst_2 : Algebra R A] →
          [FaithfulSMul R A] →
            (Submodule R A)ˣ ⧸ (Units.map ↑(Submodule.spanSingleton R)).range ≃* ↥(CommRing.relPic R A)

If A is a faithful R-algebra, the relative Picard group Pic(A/R) is isomorphic to the group of the invertible R-submodules in A modulo the principal submodules.

Defined in

Mathlib.RingTheory.PicardGroup

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebraFaithfulSMul