Theorems · Definition · commutative algebra

ClassGroup.extendedHom

(A : Type u_1) →
  (B : Type u_2) →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] →
          [Module.IsTorsionFree A B] → [inst_4 : IsDomain A] → [inst_5 : IsDomain B] → ClassGroup A →* ClassGroup B

The monoid homomorphism ClassGroup A → ClassGroup B induced by an injective extension of domains A → B.

Defined in

Mathlib.RingTheory.ClassGroup.ExtendedHom

Cited by

7 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraModule.IsTorsionFreeIsDomainIsDomain