OAI/AlgebraicGeometry/CartierSections/Weights.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Real weights of exponent vectors

Real weights are additive on exponent vectors. Positive weights have finite sublevel sets, and rationally independent weights distinguish exponents.

  1. def OAI.CartierSections.realWeight line 22
  2. theorem OAI.CartierSections.realWeight_zero line 25
  3. theorem OAI.CartierSections.realWeight_add line 28
  4. theorem OAI.CartierSections.realWeight_nsmul line 32
  5. theorem OAI.CartierSections.realWeight_nonneg line 36
  6. theorem OAI.CartierSections.realWeight_injective line 40
  7. theorem OAI.CartierSections.finite_weight_sublevel line 50

    Source documentation

    Positive weights give finite sublevel sets of exponent vectors.

    theorem finite_weight_sublevel {w : ι → ℝ} (hw : ∀ i, 0 < w i) (L : ℝ) :
    {d : ι →₀ ℕ | realWeight w d ≤ L}.Finite := by
…

    Mentions: OAI.CartierSections.realWeight