Theorems · Definition · commutative algebra

Submodule.unitsToPic

(R : Type u) →
  (A : Type u_4) →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] → [inst_2 : Algebra R A] → [FaithfulSMul R A] → (Submodule R A)ˣ →* CommRing.Pic R

The group homomorphism from the invertible submodules in a faithful algebra over R to the Picard group of R. See Lemma 2.2 in [RobertsSingh1993].

Defined in

Mathlib.RingTheory.PicardGroup

Cited by

10 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringAlgebraFaithfulSMul