SourceInvariant.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A homogeneous source invariant gives an invariant in the quadric center

This is the last passage in Section 3's coordinate obstruction. Everything here takes place in the literal source rings G, B, and I: the Laurent extension is constructed, its homogeneity is proved from the source grading, and its positive-degree invariant has a nonzero numerator in the actual center ideal. No domain or localization injectivity assumption is added to the source data.

theorem OAI.StableCoordinate.SourceInvariant.exists_quadric_lnd_invariant line 31

Source documentation

The final source-specific Laurent descent step. A nonzero homogeneous locally nilpotent derivation of the actual degeneration ring, fixing the parameter and a nonzero positive-degree element, produces the nonzero quadric derivation and center-ideal invariant required in the obstruction.

theorem exists_quadric_lnd_invariant
    (D : Derivation k (G k) (G k)) (m : ℤ)
    (hshift : ∀ (n : ℤ) (r : G k), r ∈ gPiece k n → D r ∈ gPiece k (n + m))
    (hD : IsLocallyNilpotent D) (hDne : D ≠ 0) (hp : D (gX k 0) = 0)
    {η : G k} {ℓ : ℤ} (hℓ : 0 < ℓ) (hη : η ∈ gPiece k ℓ)
    (hηne : η ≠ 0) (hDη : D η = 0) :
    ∃ E : Derivation k (B k) (B k),
      IsLocallyNilpotent E ∧ E ≠ 0 ∧
      ∃ h : B k, h ∈ I k ∧ h ≠ 0 ∧ E h = 0 := by
…

Mentions: OAI.StableCoordinate.IsLocallyNilpotent