WeightedInitial.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Highest components for integer-weighted polynomials

The weights may be negative. These lemmas give the top-product identity needed in §3 for the initial ideal of a principal hypersurface relation.

def OAI.StableCoordinate.WeightedInitial.Bounded line 22
Source documentation
Every monomial appearing in p has integer weight at most d.
```
def Bounded (w : σ → ℤ) (p : MvPolynomial σ K) (d : ℤ) : Prop :=
…
```
lemma OAI.StableCoordinate.WeightedInitial.bounded_zero line 25
lemma OAI.StableCoordinate.WeightedInitial.Bounded.mono line 29
lemma OAI.StableCoordinate.WeightedInitial.Bounded.add line 33
lemma OAI.StableCoordinate.WeightedInitial.Bounded.mul line 41
theorem OAI.StableCoordinate.WeightedInitial.bounded_iff_degree_le line 54
Source documentation
Coefficientwise boundedness is exactly the upper bound on weighted total degree.
```
theorem bounded_iff_degree_le {w : σ → ℤ} {p : MvPolynomial σ K} {d : ℤ} :
    Bounded w p d ↔ weightedTotalDegree' w p ≤ (d : WithBot ℤ) := by
…
```
Mentions: OAI.StableCoordinate.WeightedInitial.Bounded
def OAI.StableCoordinate.WeightedInitial.boundedSubmodule line 60
Source documentation
The bounded polynomials form the usual weighted filtration submodule.
```
def boundedSubmodule (w : σ → ℤ) (d : ℤ) : Submodule K (MvPolynomial σ K) where
…
```
lemma OAI.StableCoordinate.WeightedInitial.bounded_monomial line 70
Source documentation
A monomial has the expected weight bound, with arbitrary coefficient.
```
lemma bounded_monomial (w : σ → ℤ) (m : σ →₀ ℕ) (c : K) {d : ℤ}
    (hm : Finsupp.weight w m ≤ d) : Bounded w (monomial m c) d := by
…
```
Mentions: OAI.StableCoordinate.WeightedInitial.Bounded
theorem OAI.StableCoordinate.WeightedInitial.boundedSubmodule_eq_span line 77
Source documentation
The coefficientwise filtration agrees with the span-of-monomials definition.
```
theorem boundedSubmodule_eq_span (w : σ → ℤ) (d : ℤ) :
    boundedSubmodule (K := K) w d = Submodule.span K
…
```
Mentions: OAI.StableCoordinate.WeightedInitial.boundedSubmodule
theorem OAI.StableCoordinate.WeightedInitial.component_mul_of_bounded line 98
Source documentation
The highest possible component of a product is the product of the respective highest possible components. This does not assume their nonvanishing.
```
theorem component_mul_of_bounded {w : σ → ℤ} {p q : MvPolynomial σ K} {d e : ℤ}
    (hp : Bounded w p d) (hq : Bounded w q e) :
    weightedHomogeneousComponent w (d + e) (p * q) =
      weightedHomogeneousComponent w d p * weightedHomogeneousComponent w e q := by
…
```
Mentions: OAI.StableCoordinate.WeightedInitial.Bounded
lemma OAI.StableCoordinate.WeightedInitial.component_eq_zero_of_bounded line 124
Source documentation
A component strictly above a bound vanishes.
```
lemma component_eq_zero_of_bounded {w : σ → ℤ} {p : MvPolynomial σ K} {d e : ℤ}
    (hp : Bounded w p d) (hde : d < e) : weightedHomogeneousComponent w e p = 0 := by
…
```
Mentions: OAI.StableCoordinate.WeightedInitial.Bounded
theorem OAI.StableCoordinate.WeightedInitial.exists_top line 136
Source documentation
Every nonzero polynomial has a highest integer-weight component.
```
theorem exists_top {w : σ → ℤ} {p : MvPolynomial σ K} (hp : p ≠ 0) :
    ∃ d : ℤ, Bounded w p d ∧ weightedHomogeneousComponent w d p ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.WeightedInitial.Bounded
theorem OAI.StableCoordinate.WeightedInitial.degree_eq_of_top line 150
Source documentation
A bound with a nonzero component is exactly the weighted total degree.
```
theorem degree_eq_of_top {w : σ → ℤ} {p : MvPolynomial σ K} {d : ℤ}
    (hb : Bounded w p d) (ht : weightedHomogeneousComponent w d p ≠ 0) :
    weightedTotalDegree' w p = (d : WithBot ℤ) := by
…
```
Mentions: OAI.StableCoordinate.WeightedInitial.Bounded

theorem OAI.StableCoordinate.WeightedInitial.top_mul line 169

Source documentation

Nonzero top components multiply to a nonzero top component over a domain.

theorem top_mul {w : σ → ℤ} {p q : MvPolynomial σ K} {d e : ℤ}
    (hp : Bounded w p d) (hq : Bounded w q e)
    (htp : weightedHomogeneousComponent w d p ≠ 0)
    (htq : weightedHomogeneousComponent w e q ≠ 0) :
    Bounded w (p * q) (d + e) ∧
      weightedHomogeneousComponent w (d + e) (p * q) ≠ 0 := by
…

Mentions: OAI.StableCoordinate.WeightedInitial.Bounded

theorem OAI.StableCoordinate.WeightedInitial.degree_mul line 180
Source documentation
Weighted total degree is additive under multiplication, even with negative weights.
```
theorem degree_mul (w : σ → ℤ) (p q : MvPolynomial σ K) :
    weightedTotalDegree' w (p * q) = weightedTotalDegree' w p + weightedTotalDegree' w q := by
…
```
lemma OAI.StableCoordinate.WeightedInitial.Bounded.neg line 197
lemma OAI.StableCoordinate.WeightedInitial.Bounded.sub line 203
theorem OAI.StableCoordinate.WeightedInitial.bounded_sub_top line 209
Source documentation
Removing the top component lowers an integer weight bound by at least one.
```
theorem bounded_sub_top {w : σ → ℤ} {p : MvPolynomial σ A} {d : ℤ}
    (hp : Bounded w p d) :
    Bounded w (p - weightedHomogeneousComponent w d p) (d - 1) := by
…
```
Mentions: OAI.StableCoordinate.WeightedInitial.Bounded