WeightedInitialIdeal.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Principal initial ideals for integer-weighted polynomial rings

This module uses the canonical weighted-product API to prove that the ideal of leading relations of a principal polynomial ideal is generated by the leading form of its generator. The weights are arbitrary integers.

def OAI.StableCoordinate.WeightedInitial.IsTopDegree line 24
Source documentation
d is the largest weight of a nonzero polynomial, including negative weights.
```
def IsTopDegree (w : σ → ℤ) (p : MvPolynomial σ R) (d : ℤ) : Prop :=
…
```
Mentions: OAI.StableCoordinate.R
lemma OAI.StableCoordinate.WeightedInitial.homogeneous_bounded line 27
lemma OAI.StableCoordinate.WeightedInitial.IsTopDegree.ne_zero line 30
lemma OAI.StableCoordinate.WeightedInitial.IsTopDegree.of_homogeneous line 34
lemma OAI.StableCoordinate.WeightedInitial.IsTopDegree.unique line 39
lemma OAI.StableCoordinate.WeightedInitial.component_mul_homogeneous_left line 48
Source documentation
Projection through multiplication by a homogeneous polynomial. This needs no bound on the other factor and allows negative degree shifts.
```
lemma component_mul_homogeneous_left (hp : p.IsWeightedHomogeneous w d) (q : MvPolynomial σ R)
    (e : ℤ) :
    weightedHomogeneousComponent w (d + e) (p * q) =
      p * weightedHomogeneousComponent w e q := by
…
```
Mentions: OAI.StableCoordinate.R
def OAI.StableCoordinate.WeightedInitial.initialIdeal line 71
Source documentation
The initial ideal contains leading forms at the actual largest weights, not all homogeneous components of the relation ideal.
```
def initialIdeal (w : σ → ℤ) (I : Ideal (MvPolynomial σ R)) : Ideal (MvPolynomial σ R) :=
…
```
Mentions: OAI.StableCoordinate.R
theorem OAI.StableCoordinate.WeightedInitial.initialIdeal_span_singleton line 76
Source documentation
A principal relation has a principal weighted initial ideal.
```
theorem initialIdeal_span_singleton (hH : IsTopDegree w q e) :
    initialIdeal w (Ideal.span ({q} : Set (MvPolynomial σ R))) =
      Ideal.span ({weightedHomogeneousComponent w e q} : Set (MvPolynomial σ R)) := by
…
```
Mentions: OAI.StableCoordinate.WeightedInitial.IsTopDegree, OAI.StableCoordinate.WeightedInitial.initialIdeal, OAI.StableCoordinate.R