DeterminantFinalStep.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The final elementary step of determinant rigidity

A derivation which fixes the three polynomial base generators is determined by a single coefficient. Preservation of the actual fiber grading makes that coefficient have weight -2. If it lies in the polynomial base, whose weights are nonnegative, it vanishes; so does the derivation. The coefficient's polynomiality is supplied separately by the locally nilpotent chart argument.

theorem OAI.StableCoordinate.DeterminantRing.derivation_eq_zero_of_fixed_base_and_coefficient_mem line 22
Source documentation
The actual weight obstruction annihilates every vertical derivation whose coefficient is polynomial in the base variables.
```
theorem derivation_eq_zero_of_fixed_base_and_coefficient_mem
    (D : Derivation k (C k) (C k))
    (ha : D (a k) = 0) (hd : D (d k) = 0) (hu : D (u k) = 0)
    (hgraded : ∀ n : ℤ, ∀ x ∈ Obstruction.fiberPiece k n,
      D x ∈ Obstruction.fiberPiece k n)
    (hq : rigidityCoefficient D (b k) (c k) ∈ (baseMap (k := k)).range) :
…
```
Mentions: OAI.StableCoordinate.DeterminantRing.C, OAI.StableCoordinate.DeterminantRing.a, OAI.StableCoordinate.DeterminantRing.d, OAI.StableCoordinate.DeterminantRing.u, OAI.StableCoordinate.Obstruction.fiberPiece, OAI.StableCoordinate.rigidityCoefficient, OAI.StableCoordinate.DeterminantRing.b, OAI.StableCoordinate.DeterminantRing.c, OAI.StableCoordinate.DeterminantRing.baseMap