Theorems · Definition · commutative algebra

IsDiscreteValuationRing.equivValuationSubring

{A : Type u_1} →
  {K : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : IsDomain A] →
        [inst_2 : IsDiscreteValuationRing A] →
          [inst_3 : Field K] →
            [inst_4 : Algebra A K] →
              [inst_5 : IsFractionRing A K] →
                A ≃+*
                  ↥(IsDedekindDomain.HeightOneSpectrum.valuation K
                        (IsDiscreteValuationRing.maximalIdeal A)).valuationSubring

The ring isomorphism between a DVR A and the valuation subring of a field of fractions of A endowed with the adic valuation of the maximal ideal.

Defined in

Mathlib.RingTheory.Valuation.Discrete.IsDiscreteValuationRing

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingIsDomainIsDiscreteValuationRingFieldAlgebraIsFractionRing