OAI/AlgebraicGeometry/CartierSections/FormalValuation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Weighted valuations on formal power series

Dickson finiteness gives an exponent of least weight, even when some weights vanish. Initial homogeneous series prove multiplicativity without requiring a unique exponent of least weight.

  1. def OAI.CartierSections.FormalMonomial.value line 23

    Source documentation

    Literal coefficient-weight infimum of a formal power series.

    def value (w : σ → ℝ≥0) (f : MvPowerSeries σ k) : ENNReal :=
…
  2. lemma OAI.CartierSections.FormalMonomial.le_value_iff line 26
  3. lemma OAI.CartierSections.FormalMonomial.value_le_weight line 31
  4. lemma OAI.CartierSections.FormalMonomial.finite_dominated_generators line 36

    Source documentation

    Dickson finiteness gives finitely many minimal exponent vectors.

    lemma finite_dominated_generators [Fintype σ] (S : Set (σ →₀ ℕ)) :
    ∃ T : Finset (σ →₀ ℕ), (↑T : Set (σ →₀ ℕ)) ⊆ S ∧
      ∀ d ∈ S, ∃ e ∈ T, e ≤ d := by
…
  5. lemma OAI.CartierSections.FormalMonomial.weight_mono line 52
  6. lemma OAI.CartierSections.FormalMonomial.exists_initial line 58
  7. lemma OAI.CartierSections.FormalMonomial.value_eq_of_initial line 76
  8. lemma OAI.CartierSections.FormalMonomial.value_attained line 83
  9. lemma OAI.CartierSections.FormalMonomial.value_zero line 88
  10. lemma OAI.CartierSections.FormalMonomial.value_one line 91
  11. lemma OAI.CartierSections.FormalMonomial.value_add line 96
  12. lemma OAI.CartierSections.FormalMonomial.le_value_mul line 107
  13. def OAI.CartierSections.FormalMonomial.component line 121

    Source documentation

    The initial homogeneous series of a given weight.

    def component (w : σ → ℝ≥0) (a : ℝ≥0) (f : MvPowerSeries σ k) : MvPowerSeries σ k :=
…
  14. lemma OAI.CartierSections.FormalMonomial.coeff_component line 124
  15. lemma OAI.CartierSections.FormalMonomial.component_mul_at_lower_bounds line 129
  16. lemma OAI.CartierSections.FormalMonomial.component_ne_zero line 169
  17. lemma OAI.CartierSections.FormalMonomial.value_mul line 182
  18. def OAI.CartierSections.FormalMonomial.valuation line 213

    Source documentation

    Genuine monomial valuation on the formal regular local ring, including faces with zero weights.

    def valuation (w : σ → ℝ≥0) : AddValuation (MvPowerSeries σ k) ENNReal :=
…
  19. lemma OAI.CartierSections.FormalMonomial.valuation_apply line 216
  20. lemma OAI.CartierSections.FormalMonomial.combine_dominates line 220

    Source documentation

    Nonnegative combinations of weights dominate the corresponding values.

    lemma combine_dominates {ι : Type*} (s : Finset ι) (c : ι → ℝ≥0)
    (w : ι → σ → ℝ≥0) (f : MvPowerSeries σ k) :
    ∑ i ∈ s, (c i : ENNReal) * valuation (w i) f ≤
      valuation (Monomial.combine s c w) f := by
…

    Mentions: OAI.CartierSections.FormalMonomial.valuation, OAI.CartierSections.Monomial.combine