ReesToDegeneration.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Homogeneous transport from the actual Rees algebra to the degeneration

The concrete presentation equivalence preserves every integer degree in both directions. This is proved from homogeneous polynomial representatives and the exact lower-step criterion for initial forms. Consequently actual leading derivations, including their nonzero positive-degree invariants, transport to the canonical degeneration ring without any additional grading assumptions.

theorem OAI.StableCoordinate.ReesToDegeneration.homogeneous_mem_piece line 28
Source documentation
Homogeneous source polynomials belong to their exact filtration piece.
```
theorem homogeneous_mem_piece {p : P k 5} {d : ℤ}
    (hp : p.IsWeightedHomogeneous presentationWeight d) : p ∈ piece k d := by
…
```
theorem OAI.StableCoordinate.ReesToDegeneration.sub_top_mem_piece line 35
Source documentation
Removing the degree-d part of a bounded source polynomial lowers its filtration index by one, even if d is negative.
```
theorem sub_top_mem_piece {p : P k 5} {d : ℤ} (hp : p ∈ piece k d) :
    p - weightedHomogeneousComponent presentationWeight d p ∈ piece k (d - 1) := by
…
```

theorem OAI.StableCoordinate.ReesToDegeneration.sourceInitial_eq_gradedMap_component line 42

Source documentation

The homogeneous component's symbol is exactly the symbol of any bounded representative in the same degree.

theorem sourceInitial_eq_gradedMap_component
    (φ : P k 5 →ₐ[k] A) (d : ℤ) (p : piece k d) :
    sourceInitial φ d p =
      gradedMap φ (weightedHomogeneousComponent presentationWeight d (p : P k 5)) := by
…

theorem OAI.StableCoordinate.ReesToDegeneration.initial_has_homogeneous_representative line 65

Source documentation

Every initial form has a homogeneous polynomial representative in exactly the same integer degree.

theorem initial_has_homogeneous_representative
    (φ : P k 5 →ₐ[k] A) (d : ℤ) (a : imagePiece φ d) :
    ∃ p : P k 5, p.IsWeightedHomogeneous presentationWeight d ∧
      gradedMap φ p = initial (imagePiece φ) (imagePiece_mono φ) d a := by
…

theorem OAI.StableCoordinate.ReesToDegeneration.mem_gPiece_iff line 78

Source documentation

The concrete quotient equivalence preserves a homogeneous piece in both directions; its image is precisely the set of degree-d initial forms.

theorem mem_gPiece_iff (d : ℤ) (g : G k) :
    g ∈ gPiece k d ↔ ∃ a : imagePiece (quotientMap k) d,
      associatedGradedEquiv k g =
        initial (imagePiece (quotientMap k)) (imagePiece_mono (quotientMap k)) d a := by
…

theorem OAI.StableCoordinate.ReesToDegeneration.source_degreeZeroSubalgebra_ne_top line 102
Source documentation
The actual degree-zero source subalgebra is proper: the initial symbol of the positive-weight variable F (index three) is provably nonzero.
```
theorem source_degreeZeroSubalgebra_ne_top :
    degreeZeroSubalgebra (imagePiece (quotientMap k)) ≠ ⊤ := by
…
```
def OAI.StableCoordinate.ReesToDegeneration.transportDerivation line 114
Source documentation
Conjugation through the proved, concrete associated-graded equivalence.
```
def transportDerivation (D : Derivation k (associatedGraded k) (associatedGraded k)) :
    Derivation k (G k) (G k) :=
…
```
theorem OAI.StableCoordinate.ReesToDegeneration.transportDerivation_apply line 118
theorem OAI.StableCoordinate.ReesToDegeneration.transportDerivation_locallyNilpotent line 124
Source documentation
Local nilpotence is retained under the concrete transport.
```
theorem transportDerivation_locallyNilpotent
    (D : Derivation k (associatedGraded k) (associatedGraded k))
    (hD : IsLocallyNilpotent (k := k) (A := associatedGraded k) D) :
…
```
Mentions: OAI.StableCoordinate.IsLocallyNilpotent
theorem OAI.StableCoordinate.ReesToDegeneration.transportDerivation_ne_zero line 132
Source documentation
A nonzero leading derivation remains nonzero in the canonical presentation.
```
theorem transportDerivation_ne_zero
    (D : Derivation k (associatedGraded k) (associatedGraded k)) (hD : D ≠ 0) :
    transportDerivation k D ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.ReesToDegeneration.transportDerivation

theorem OAI.StableCoordinate.ReesToDegeneration.transportDerivation_homogeneous line 140

Source documentation

The integer shift on initial forms is the actual gPiece shift on the canonical degeneration, with no reversal or truncation of negative degrees.

theorem transportDerivation_homogeneous
    (D : Derivation k (associatedGraded k) (associatedGraded k)) (m : ℤ)
    (hD : ∀ (d : ℤ) (a : imagePiece (quotientMap k) d),
      ∃ b : imagePiece (quotientMap k) (d + m),
        D (initial (imagePiece (quotientMap k)) (imagePiece_mono (quotientMap k)) d a) =
          initial (imagePiece (quotientMap k)) (imagePiece_mono (quotientMap k)) (d + m) b) :
    ∀ (d : ℤ) (g : G k), g ∈ gPiece k d →
      transportDerivation k D g ∈ gPiece k (d + m) := by
…

Mentions: OAI.StableCoordinate.ReesToDegeneration.transportDerivation

theorem OAI.StableCoordinate.ReesToDegeneration.associatedGradedEquiv_p line 155

Source documentation

The negative distinguished symbol is exactly the image of gX 0.

theorem associatedGradedEquiv_p :
    associatedGradedEquiv k (gX k 0) =
      initial (imagePiece (quotientMap k)) (imagePiece_mono (quotientMap k)) (-1)
        ⟨quotientMap k (X 0), image_X_zero_mem_neg_one (quotientMap k)⟩ := by
…

theorem OAI.StableCoordinate.ReesToDegeneration.coordinate_produces_degeneration_lnd line 169
Source documentation
A hypothetical polynomial coordinate system in the source ring produces the exact nonzero homogeneous LND and positive homogeneous invariant needed by the canonical degeneration-to-quadric argument. Properness, separation, and homogeneous compatibility are all proved, not added as assumptions.
```
theorem coordinate_produces_degeneration_lnd [IsNoetherianRing k]
    (e : P k 4 ≃ₐ[k] Obstruction.A k) (hp : e (X 0) = aX k 0) :
    ∃ (m : ℤ) (D : Derivation k (G k) (G k)),
      D ≠ 0 ∧ IsLocallyNilpotent D ∧
      (∀ (n : ℤ) (g : G k), g ∈ gPiece k n → D g ∈ gPiece k (n + m)) ∧
      D (gX k 0) = 0 ∧
      ∃ (d : ℤ) (η : G k), 0 < d ∧ η ∈ gPiece k d ∧ η ≠ 0 ∧ D η = 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.A, OAI.StableCoordinate.IsLocallyNilpotent