ReesCoefficientCriterion.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Coefficientwise vanishing in an associated graded algebra

The principal Rees ideal (T) consists precisely of Laurent polynomials whose coefficient in degree d belongs to F (d-1). This gives an actual coefficientwise kernel test for the Rees model, including negative degrees.

theorem OAI.StableCoordinate.FilteredRees.mem_parameterIdeal_iff line 21
Source documentation
The complete defining-ideal membership criterion for the Rees special fiber.
```
theorem mem_parameterIdeal_iff (hmono : Monotone F) (p : rees F) :
    p ∈ parameterIdeal F hmono ↔
      ∀ d : ℤ, (p : LaurentPolynomial A).coeff d ∈ F (d - 1) := by
…
```
Mentions: OAI.StableCoordinate.FilteredRees.rees, OAI.StableCoordinate.FilteredRees.parameterIdeal
theorem OAI.StableCoordinate.FilteredRees.quotient_mk_eq_zero_iff line 51
Source documentation
A Rees representative vanishes in the associated graded algebra iff each coefficient has dropped one filtration step.
```
theorem quotient_mk_eq_zero_iff (hmono : Monotone F) (p : rees F) :
    Ideal.Quotient.mk (parameterIdeal F hmono) p = 0 ↔
      ∀ d : ℤ, (p : LaurentPolynomial A).coeff d ∈ F (d - 1) := by
…
```
Mentions: OAI.StableCoordinate.FilteredRees.rees, OAI.StableCoordinate.FilteredRees.parameterIdeal
theorem OAI.StableCoordinate.FilteredRees.quotient_mk_eq_iff line 58
Source documentation
Two arbitrary Rees representatives determine the same graded element iff their coefficientwise difference lies one step lower.
```
theorem quotient_mk_eq_iff (hmono : Monotone F) (p q : rees F) :
    Ideal.Quotient.mk (parameterIdeal F hmono) p =
        Ideal.Quotient.mk (parameterIdeal F hmono) q ↔
      ∀ d : ℤ, (p : LaurentPolynomial A).coeff d - (q : LaurentPolynomial A).coeff d ∈
        F (d - 1) := by
…
```
Mentions: OAI.StableCoordinate.FilteredRees.rees, OAI.StableCoordinate.FilteredRees.parameterIdeal