FieldTopology.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Continuity of valuations on fraction fields

Local algebra for uniform Cartier sections.

lemma OAI.CartierSections.nonnegToExtendedReal_eq_coe_toReal line 24
lemma OAI.CartierSections.continuous_fractionValuation_apply line 38
Source documentation
A continuous family of finite local-ring valuations extends continuously in the pointwise topology to the actual fraction field. The value at zero is infinity; for a nonzero fraction this is the difference of two finite real continuous functions. In particular, we do not apply continuity of subtraction at infinity minus infinity.
```
lemma continuous_fractionValuation_apply
    (v : T → AddValuation A ENNReal)
    (hv : ∀ t a, a ≠ 0 → v t a ≠ ⊤)
    (hc : ∀ a, Continuous (fun t => v t a)) (x : K) :
    Continuous (fun t => fractionValuation (v t) (hv t) x) := by
…
```
Mentions: OAI.CartierSections.fractionValuation
lemma OAI.CartierSections.continuous_fractionValuation_evaluations line 68
def OAI.CartierSections.expandedFractionValuation line 83
Source documentation
A genuine monomial valuation on a fraction field, constructed from an injective formal-coordinate expansion of its local ring.
```
noncomputable def expandedFractionValuation
    (θ : A →ₐ[k] MvPowerSeries σ k) (hθ : Function.Injective θ)
    (w : σ → NNReal) : AddValuation K (WithTop ℝ) :=
…
```
lemma OAI.CartierSections.expandedFractionValuation_regular line 89
lemma OAI.CartierSections.continuous_expandedFractionValuation_evaluations line 96
lemma OAI.CartierSections.isCompact_expandedFractionValuation_cone line 106
Source documentation
Compactness in pointwise rational-function evaluation, including zero weights, ties between monomials, and fractions having negative value.
```
lemma isCompact_expandedFractionValuation_cone
    (θ : A →ₐ[k] MvPowerSeries σ k) (hθ : Function.Injective θ)
    (a : σ → NNReal) (ha : ∀ i, 0 < a i) :
    IsCompact ((fun w : σ → NNReal => fun x : K =>
      expandedFractionValuation θ hθ w x) '' normalizedWeights a) :=
…
```
Mentions: OAI.CartierSections.expandedFractionValuation, OAI.CartierSections.normalizedWeights