WeightIdeals.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Monomial weight ideals

The monomial ideal above a weight bound is finitely generated. Its elements vanish at all exponents below the bound, so the initial monomial does not belong to this ideal.

def OAI.CartierSections.weightVanishingIdeal line 21
Source documentation
The ideal of series whose coefficients vanish up to the specified weight.
```
noncomputable def weightVanishingIdeal (w : ι → ℝ) (hw : ∀ i, 0 ≤ w i) (L : ℝ) :
    Ideal (MvPowerSeries ι k) where
…
```
theorem OAI.CartierSections.boundaryWeightIdeal_le_weightVanishingIdeal line 41

theorem OAI.CartierSections.initial_monomial_not_mem_boundaryWeightIdeal line 53

Source documentation

An initial monomial does not belong to the ideal of strictly higher weight.

theorem initial_monomial_not_mem_boundaryWeightIdeal
    (B : Finset ι) (w : ι → ℝ) (hw : ∀ i, 0 ≤ w i) (α : ι →₀ ℕ) :
    (MvPowerSeries.monomial α 1 : MvPowerSeries ι k) ∉
      boundaryWeightIdeal B w (realWeight w α) := by
…

Mentions: OAI.CartierSections.boundaryWeightIdeal, OAI.CartierSections.realWeight

theorem OAI.CartierSections.boundaryWeightIdeal_fg line 61