OAI/AlgebraicGeometry/CartierSections/ExpansionValuation.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Valuations induced by formal expansions

A formal coordinate expansion pulls back the monomial valuation to the original ring. Injective expansions give finite values on nonzero elements.

  1. def OAI.CartierSections.seriesWeight line 20

    Source documentation

    The infimum of the real weights of nonzero coefficients.

    def seriesWeight (w : σ → ℝ) (f : MvPowerSeries σ k) : ENNReal :=
…
  2. def OAI.CartierSections.IsMonomialInExpansion line 23
  3. lemma OAI.CartierSections.coe_finsupp_weight line 27
  4. lemma OAI.CartierSections.formalValue_eq_seriesWeight line 32
  5. def OAI.CartierSections.expansionValuation line 42

    Source documentation

    Pull back a formal monomial valuation along an expansion homomorphism.

    def expansionValuation (θ : R →ₐ[k] MvPowerSeries σ k) (w : σ → ℝ≥0) :
    AddValuation R ENNReal := (FormalMonomial.valuation w).comap θ.toRingHom

    Mentions: OAI.CartierSections.FormalMonomial.valuation

  6. lemma OAI.CartierSections.expansionValuation_monomial line 45
  7. lemma OAI.CartierSections.expansionValuation_finite line 50