Theorems · Definition · commutative algebra

ValuativeExtension.mapPosSubmonoid

(A : Type u_1) →
  (B : Type u_2) →
    [inst : CommSemiring A] →
      [inst_1 : Semiring B] →
        [inst_2 : ValuativeRel A] →
          [inst_3 : ValuativeRel B] →
            [inst_4 : Algebra A B] →
              [ValuativeExtension A B] → ↥(ValuativeRel.posSubmonoid A) →* ↥(ValuativeRel.posSubmonoid B)

The morphism of posSubmonoids associated to an algebra map. This is used in constructing ValuativeExtension.mapValueGroupWithZero.

Defined in

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommSemiringSemiringValuativeRelValuativeRelAlgebraValuativeExtension