LiftObstruction.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The actual weight-preserving locally nilpotent lift

This file completes source Proposition prop:lift for the exact rings B and C. There is no assumed action lift or line-bundle trivialization: the genuine UFD structure of C[T] gives a determinant frame, its constant-unit normalization gives a polynomial family, and normalized-frame uniqueness proves the additive group law. A second use of uniqueness proves fiber-scaling equivariance. Differentiation therefore gives a locally nilpotent derivation that extends the given one and preserves the actual constructed fiber grading.

Finally, injectivity of B → C, the identity IC = (v), and factorial closure of an LND kernel transport a nonzero invariant in I to the condition D(v)=0. All intermediate existence and equivariance interfaces are discharged here.

def OAI.StableCoordinate.Obstruction.liftedAdditiveAction line 36
Source documentation
The actual additive action on the determinant ring lifting a given action on the quadric ring. Its group law is a theorem of normalized-frame uniqueness.
```
def liftedAdditiveAction (α : PolynomialAdditiveAction k (B k)) :
    PolynomialAdditiveAction k (C k) :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.Obstruction.C
theorem OAI.StableCoordinate.Obstruction.liftedAdditiveAction_toAlgHom line 43
theorem OAI.StableCoordinate.Obstruction.liftedAdditiveAction_baseMap line 48
Source documentation
The constructed action is equivariant for the actual injective base map.
```
theorem liftedAdditiveAction_baseMap (α : PolynomialAdditiveAction k (B k))
    (b : B k) :
    (liftedAdditiveAction α).toAlgHom (baseMap k b) =
      (α.toAlgHom b).map (baseMap k).toRingHom :=
…
```
Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.Obstruction.liftedAdditiveAction, OAI.StableCoordinate.Obstruction.baseMap
theorem OAI.StableCoordinate.Obstruction.liftedAdditiveAction_derivation_preserves_fiberPiece line 56
Source documentation
Differentiation of the constructed action preserves every actual fiber weight submodule. The five coefficient laws are proved, not hypothesized.
```
theorem liftedAdditiveAction_derivation_preserves_fiberPiece
    (α : PolynomialAdditiveAction k (B k)) :
    ∀ (n : ℤ) (q : C k), q ∈ fiberPiece k n →
      (liftedAdditiveAction α).derivation q ∈ fiberPiece k n := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.Obstruction.fiberPiece, OAI.StableCoordinate.Obstruction.liftedAdditiveAction
theorem OAI.StableCoordinate.Obstruction.exists_weight_preserving_lnd_lift line 74
Source documentation
Every locally nilpotent derivation on the exact base quadric admits an actual locally nilpotent extension preserving the source's fiber grading. This is the unconditional existence part of source Proposition prop:lift.
```
theorem exists_weight_preserving_lnd_lift
    (E : Derivation k (B k) (B k)) (hE : IsLocallyNilpotent E) :
    ∃ D : Derivation k (C k) (C k), IsLocallyNilpotent D ∧
      (∀ b, D (baseMap k b) = baseMap k (E b)) ∧
      (∀ (n : ℤ) (q : C k), q ∈ fiberPiece k n → D q ∈ fiberPiece k n) := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.IsLocallyNilpotent, OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.Obstruction.baseMap, OAI.StableCoordinate.Obstruction.fiberPiece
theorem OAI.StableCoordinate.Obstruction.lift_invariant line 90
Source documentation
Full source lift proposition, retaining the extension equation as well as the nonzero invariant and grading conclusions required by rigidity.
```
theorem lift_invariant
    (E : Derivation k (B k) (B k)) (hE : IsLocallyNilpotent E) (hE0 : E ≠ 0)
    (hInv : ∃ h : B k, h ∈ I k ∧ h ≠ 0 ∧ E h = 0) :
    ∃ D : Derivation k (C k) (C k), IsLocallyNilpotent D ∧ D ≠ 0 ∧
      (∀ b, D (baseMap k b) = baseMap k (E b)) ∧
      (∀ (n : ℤ) (q : C k), q ∈ fiberPiece k n → D q ∈ fiberPiece k n) ∧
      D (v k) = 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.IsLocallyNilpotent, OAI.StableCoordinate.Obstruction.I, OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.Obstruction.baseMap, OAI.StableCoordinate.Obstruction.fiberPiece, OAI.StableCoordinate.Obstruction.v
theorem OAI.StableCoordinate.Obstruction.exists_nonzero_weight_preserving_lnd_killing_v line 102
Source documentation
The precise existence conclusion needed by the final weight contradiction.
```
theorem exists_nonzero_weight_preserving_lnd_killing_v
    (E : Derivation k (B k) (B k)) (hE : IsLocallyNilpotent E) (hE0 : E ≠ 0)
    (hInv : ∃ h : B k, h ∈ I k ∧ h ≠ 0 ∧ E h = 0) :
    ∃ D : Derivation k (C k) (C k), D ≠ 0 ∧ IsLocallyNilpotent D ∧
      (∀ (n : ℤ) (q : C k), q ∈ fiberPiece k n → D q ∈ fiberPiece k n) ∧
      D (v k) = 0 := by
…
```
Mentions: OAI.StableCoordinate.Obstruction.B, OAI.StableCoordinate.IsLocallyNilpotent, OAI.StableCoordinate.Obstruction.I, OAI.StableCoordinate.Obstruction.C, OAI.StableCoordinate.Obstruction.fiberPiece, OAI.StableCoordinate.Obstruction.v