LaurentDerivationTransport.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Transport of the actual graded-hypersurface derivation to its Laurent model

This is the concrete bridge between the graded leading derivation and descent to the quadric. The invariant denominator is the actual generator gX k 0; all maps use the explicit equivalence proved in LaurentPresentation.

def OAI.StableCoordinate.LaurentDerivationTransport.lift line 23
Source documentation
Extend to the actual p-localization and transport to the Laurent model.
```
noncomputable def lift : Derivation k (LaurentPresentation.Laurent k)
    (LaurentPresentation.Laurent k) :=
…
```
Mentions: OAI.StableCoordinate.LaurentPresentation.Laurent
theorem OAI.StableCoordinate.LaurentDerivationTransport.lift_intertwine line 30
Source documentation
Intertwining holds on every element of the actual graded presentation.
```
theorem lift_intertwine (r : G k) :
    lift D hp (toLaurentBase k r) = toLaurentBase k (D r) := by
…
```
Mentions: OAI.StableCoordinate.LaurentDerivationTransport.lift
theorem OAI.StableCoordinate.LaurentDerivationTransport.lift_C line 43
Source documentation
The exact coefficient-input formula used by homogeneous Laurent descent.
```
theorem lift_C (b : B k) :
    lift D hp (LaurentPolynomial.C b) = toLaurentBase k (D (baseMap k b)) := by
…
```
Mentions: OAI.StableCoordinate.LaurentDerivationTransport.lift
theorem OAI.StableCoordinate.LaurentDerivationTransport.lift_T_one line 48
Source documentation
The distinguished Laurent variable is invariant.
```
@[simp] theorem lift_T_one : lift D hp (LaurentPolynomial.T 1) = 0 := by
…
```
Mentions: OAI.StableCoordinate.LaurentDerivationTransport.lift
theorem OAI.StableCoordinate.LaurentDerivationTransport.lift_kills line 54
Source documentation
Invariant source elements remain invariant after Laurent transport.
```
theorem lift_kills (r : G k) (hr : D r = 0) :
    lift D hp (toLaurentBase k r) = 0 := by rw [lift_intertwine, hr, map_zero]
```
Mentions: OAI.StableCoordinate.LaurentDerivationTransport.lift, OAI.StableCoordinate.LaurentDerivationTransport.lift_intertwine
theorem OAI.StableCoordinate.LaurentDerivationTransport.lift_iterate line 58
Source documentation
Iteration commutes with the concrete presentation map.
```
theorem lift_iterate (n : ℕ) (r : G k) :
    (lift D hp : LaurentPresentation.Laurent k → LaurentPresentation.Laurent k)^[n]
      (toLaurentBase k r) = toLaurentBase k ((D : G k → G k)^[n] r) := by
…
```
Mentions: OAI.StableCoordinate.LaurentDerivationTransport.lift, OAI.StableCoordinate.LaurentPresentation.Laurent
theorem OAI.StableCoordinate.LaurentDerivationTransport.lift_locallyNilpotent line 67
Source documentation
Local nilpotence needs no additional domain or characteristic hypothesis.
```
theorem lift_locallyNilpotent
    (hD : ∀ r : G k, ∃ n : ℕ, (D : G k → G k)^[n] r = 0) :
    ∀ r : LaurentPresentation.Laurent k, ∃ n : ℕ,
      (lift D hp : LaurentPresentation.Laurent k → LaurentPresentation.Laurent k)^[n] r = 0 :=
…
```
Mentions: OAI.StableCoordinate.LaurentPresentation.Laurent, OAI.StableCoordinate.LaurentDerivationTransport.lift
theorem OAI.StableCoordinate.LaurentDerivationTransport.toLaurentBase_injective line 80
Source documentation
The literal source-to-Laurent map is injective; no IsDomain G circularity.
```
theorem toLaurentBase_injective : Function.Injective (toLaurentBase k) := by
…
```
theorem OAI.StableCoordinate.LaurentDerivationTransport.lift_ne_zero line 88
Source documentation
A nonzero leading derivation cannot disappear under the concrete transport.
```
theorem lift_ne_zero (D : Derivation k (G k) (G k)) (hp : D (gX k 0) = 0)
    (hD : D ≠ 0) : lift D hp ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.LaurentDerivationTransport.lift
theorem OAI.StableCoordinate.LaurentDerivationTransport.lift_nonzero_invariant line 99
Source documentation
Source-invariant nonzero elements stay nonzero and invariant in the Laurent model.
```
theorem lift_nonzero_invariant (D : Derivation k (G k) (G k)) (hp : D (gX k 0) = 0)
    (r : G k) (hr : r ≠ 0) (hDr : D r = 0) :
    toLaurentBase k r ≠ 0 ∧ lift D hp (toLaurentBase k r) = 0 := by
…
```
Mentions: OAI.StableCoordinate.LaurentDerivationTransport.lift