ReesCoefficientKernel.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Coefficientwise kernel and homogeneous independence for the Rees model

The kernel of the Rees specialization is detected one coefficient at a time. This supplies the directness of homogeneous components without assuming an associated-graded decomposition as an extra interface.

theorem OAI.StableCoordinate.FilteredRees.mk_eq_zero_iff_coeff line 23
Source documentation
An arbitrary Rees element vanishes after specialization by T exactly when each coefficient belongs to the previous filtration step.
```
theorem mk_eq_zero_iff_coeff (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.sum_initial_eq_zero_iff line 53
Source documentation
A finite sum of distinct homogeneous initial forms vanishes if and only if all of those initial forms vanish, expressed by lower-filtration membership.
```
theorem sum_initial_eq_zero_iff (hmono : Monotone F) (s : Finset ℤ)
    (a : (d : ℤ) → F d) :
    (∑ d ∈ s, initial F hmono d (a d)) = 0 ↔
      ∀ d ∈ s, (a d : A) ∈ F (d - 1) := by
…
```
Mentions: OAI.StableCoordinate.FilteredRees.initial
theorem OAI.StableCoordinate.FilteredRees.sum_initial_eq_zero_iff_individual line 81
Source documentation
The homogeneous pieces are linearly independent in the actual Rees quotient.
```
theorem sum_initial_eq_zero_iff_individual (hmono : Monotone F) (s : Finset ℤ)
    (a : (d : ℤ) → F d) :
    (∑ d ∈ s, initial F hmono d (a d)) = 0 ↔
      ∀ d ∈ s, initial F hmono d (a d) = 0 := by
…
```
Mentions: OAI.StableCoordinate.FilteredRees.initial