Theorems · Definition · commutative algebra

Valuation.extendToLocalization

{A : Type u_1} →
  [inst : CommRing A] →
    {Γ : Type u_2} →
      [inst_1 : LinearOrderedCommGroupWithZero Γ] →
        (v : Valuation A Γ) →
          {S : Submonoid A} →
            S ≤ v.supp.primeCompl →
              (B : Type u_3) → [inst_2 : CommRing B] → [inst_3 : Algebra A B] → [IsLocalization S B] → Valuation B Γ

We can extend a valuation v on a ring to a localization at a submonoid of the complement of v.supp.

Defined in

Mathlib.RingTheory.Valuation.ExtendToLocalization

Cited by

4 results in Mathlib

Foundations

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

Assumes

CommRingLinearOrderedCommGroupWithZeroCommRingAlgebraIsLocalization