OAI/AlgebraicGeometry/StableCoordinate/ExponentialShift.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Explicit polynomial exponential shift

This file proves the exponential substitution used in Section 2 of the source, without presupposing any locally nilpotent derivation infrastructure. The six variables are ordered p, s, u, F, J, w. All formulas work over any commutative ring: no characteristic-zero or field hypothesis is required for this step.

  1. abbrev OAI.StableCoordinate.ExponentialShift.P line 21
  2. def OAI.StableCoordinate.ExponentialShift.p line 23
  3. def OAI.StableCoordinate.ExponentialShift.s line 24
  4. def OAI.StableCoordinate.ExponentialShift.u line 25
  5. def OAI.StableCoordinate.ExponentialShift.F line 26
  6. def OAI.StableCoordinate.ExponentialShift.J line 27
  7. def OAI.StableCoordinate.ExponentialShift.w line 28
  8. def OAI.StableCoordinate.ExponentialShift.x line 30
  9. def OAI.StableCoordinate.ExponentialShift.H line 31
  10. def OAI.StableCoordinate.ExponentialShift.t line 34
  11. def OAI.StableCoordinate.ExponentialShift.d line 35
  12. def OAI.StableCoordinate.ExponentialShift.substitution line 37
  13. def OAI.StableCoordinate.ExponentialShift.shift line 45
  14. theorem OAI.StableCoordinate.ExponentialShift.shift_p line 48
  15. theorem OAI.StableCoordinate.ExponentialShift.shift_s line 50
  16. theorem OAI.StableCoordinate.ExponentialShift.shift_u line 52
  17. theorem OAI.StableCoordinate.ExponentialShift.shift_F line 54
  18. theorem OAI.StableCoordinate.ExponentialShift.shift_J line 57
  19. theorem OAI.StableCoordinate.ExponentialShift.shift_w line 59
  20. theorem OAI.StableCoordinate.ExponentialShift.shift_t line 61
  21. theorem OAI.StableCoordinate.ExponentialShift.t_neg line 63
  22. theorem OAI.StableCoordinate.ExponentialShift.quadratic_invariant line 66
  23. theorem OAI.StableCoordinate.ExponentialShift.shift_x line 75
  24. theorem OAI.StableCoordinate.ExponentialShift.shift_d_neg line 79
  25. theorem OAI.StableCoordinate.ExponentialShift.inverse_F line 83
  26. theorem OAI.StableCoordinate.ExponentialShift.shift_comp_neg line 88
  27. def OAI.StableCoordinate.ExponentialShift.shiftEquiv line 112

    Source documentation

    The explicit exponential substitution, with inverse obtained by negating its parameter.

    noncomputable def shiftEquiv (c : k) : P k ≃ₐ[k] P k :=
…

    Mentions: OAI.StableCoordinate.ExponentialShift.P

  28. theorem OAI.StableCoordinate.ExponentialShift.shiftEquiv_apply line 116
  29. theorem OAI.StableCoordinate.ExponentialShift.equation_shift line 119
  30. theorem OAI.StableCoordinate.ExponentialShift.shift_H line 128

    Source documentation

    The crucial equation transport: the automorphism adds p * c * w to H.

    theorem shift_H (c : k) : shift k c (H k) = H k + p k * t k c := by
…

    Mentions: OAI.StableCoordinate.ExponentialShift.shift, OAI.StableCoordinate.ExponentialShift.H, OAI.StableCoordinate.ExponentialShift.p, OAI.StableCoordinate.ExponentialShift.t

  31. theorem OAI.StableCoordinate.ExponentialShift.exponential_shift_exists line 135

    Source documentation

    Section 2's exp(w Δ) is an actual algebra automorphism fixing p and sending H to H + p*w.

    theorem exponential_shift_exists :
    ∃ e : P k ≃ₐ[k] P k, e (p k) = p k ∧ e (H k) = H k + p k * w k := by
…

    Mentions: OAI.StableCoordinate.ExponentialShift.P, OAI.StableCoordinate.ExponentialShift.p, OAI.StableCoordinate.ExponentialShift.H, OAI.StableCoordinate.ExponentialShift.w