Theorems · Definition · commutative algebra

CommRing.Pic.mapAlgebra

(R : Type u) →
  [inst : CommSemiring R] →
    (A : Type u_5) → [inst_1 : CommSemiring A] → [Algebra R A] → CommRing.Pic R →* CommRing.Pic A

Every R-algebra A gives rise to a homomorphism between Picard groups of R and A.

Defined in

Mathlib.RingTheory.PicardGroup

Cited by

10 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebra