Module

DVRFractionFieldAway.lean

Nyll.SchemeTheory.RingTheory.DVRFractionFieldAway

1 declaration indexed from sourceView source ↗

Module documentation

A DVR fraction field is a principal localization

Every nonzero denominator divides a power of any fixed nonzero nonunit: a uniformizer divides that nonunit, while each denominator is associated to a power of the uniformizer. Thus localization at that nonunit already inverts all nonzero elements.

Imports3

Mathlib.RingTheory.DiscreteValuationRing.Basic
Mathlib.RingTheory.Localization.Away.Basic
Mathlib.RingTheory.Localization.FractionRing

Imported by5

theorem

isLocalizationAway_fractionField_of_isDiscreteValuationRing

L28 ↗

SchemeTheory.isLocalizationAway_fractionField_of_isDiscreteValuationRing

Documentation

Inverting a nonzero nonunit of a discrete valuation ring gives its actual fraction field, with its existing algebra map.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace SchemeTheory
open scoped nonZeroDivisors
universe u v

Lean source · statement

theorem isLocalizationAway_fractionField_of_isDiscreteValuationRing
    (R : Type u) [CommRing R] [IsDomain R] [IsDiscreteValuationRing R]
    (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K]
    (a : R) (ha0 : a ≠ 0) (ha : ¬ IsUnit a) :
    IsLocalization.Away a K

Module documentation

A DVR fraction field is a principal localization

Declarations

isLocalizationAway_fractionField_of_isDiscreteValuationRing