FractionValuation.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Extending finite valuations to a fraction field

A finite nonnegative valuation on a domain extends uniquely to its fraction field with values in the extended real line.

def OAI.CartierSections.nonnegToExtendedReal line 20
Source documentation
ENNReal, used for nonnegative local-ring values, embedded in the extended real additive group used on the fraction field.
```
def nonnegToExtendedReal : ENNReal →+ WithTop ℝ :=
…
```
theorem OAI.CartierSections.nonnegToExtendedReal_top line 23
theorem OAI.CartierSections.nonnegToExtendedReal_coe line 24
lemma OAI.CartierSections.nonnegToExtendedReal_monotone line 27
lemma OAI.CartierSections.nonnegToExtendedReal_eq_top line 36
def OAI.CartierSections.realLocalValuation line 47
Source documentation
Regard a nonnegative valuation as an extended-real valuation.
```
noncomputable def realLocalValuation (v : AddValuation A ENNReal) : AddValuation A (WithTop ℝ) :=
…
```
lemma OAI.CartierSections.realLocalValuation_apply line 50
lemma OAI.CartierSections.realLocalValuation_denominators line 59
def OAI.CartierSections.fractionValuation line 67
Source documentation
Extend a valuation that is finite on nonzero elements to the fraction field.
```
noncomputable def fractionValuation (v : AddValuation A ENNReal)
    (hv : ∀ a ≠ 0, v a ≠ ⊤) : AddValuation K (WithTop ℝ) :=
…
```
lemma OAI.CartierSections.fractionValuation_algebraMap line 72
lemma OAI.CartierSections.fractionValuation_ratio line 79

lemma OAI.CartierSections.fractionValuation_unique line 86

Source documentation

The extension is unique as a valuation of the function field.

lemma fractionValuation_unique (v : AddValuation A ENNReal)
    (hv : ∀ a ≠ 0, v a ≠ ⊤) (u : AddValuation K (WithTop ℝ))
    (hu : ∀ a, u (algebraMap A K a) = nonnegToExtendedReal (v a)) :
    u = fractionValuation v hv := by
…

Mentions: OAI.CartierSections.nonnegToExtendedReal, OAI.CartierSections.fractionValuation