OAI/AlgebraicGeometry/StableCoordinate/LNDExponential.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Polynomial exponentials of locally nilpotent derivations

The exponential of a locally nilpotent derivation in characteristic zero is an actual polynomial algebra homomorphism, not a formal power series. This is the forward algebraic interface for the additive-action step in Section 4.

  1. def OAI.StableCoordinate.LNDExponential.dividedIterate line 24

    Source documentation

    The factorially divided nth iterate of a derivation.

    def dividedIterate (D : Derivation k A A) (a : A) (n : ℕ) : A :=
…
  2. lemma OAI.StableCoordinate.LNDExponential.dividedIterate_finiteSupport line 27
  3. def OAI.StableCoordinate.LNDExponential.polynomial line 38

    Source documentation

    A finite-support construction of exp(T D)(a).

    def polynomial (D : Derivation k A A) (hD : IsLocallyNilpotent D) (a : A) : A[X] :=
…

    Mentions: OAI.StableCoordinate.IsLocallyNilpotent

  4. lemma OAI.StableCoordinate.LNDExponential.coeff_polynomial line 43
  5. lemma OAI.StableCoordinate.LNDExponential.iterate_add line 47
  6. lemma OAI.StableCoordinate.LNDExponential.iterate_smul line 53
  7. lemma OAI.StableCoordinate.LNDExponential.polynomial_add line 59
  8. lemma OAI.StableCoordinate.LNDExponential.polynomial_smul line 64
  9. lemma OAI.StableCoordinate.LNDExponential.polynomial_one line 69
  10. lemma OAI.StableCoordinate.LNDExponential.inverse_factorial_mul_choose line 81
  11. lemma OAI.StableCoordinate.LNDExponential.dividedIterate_mul line 90
  12. lemma OAI.StableCoordinate.LNDExponential.polynomial_mul line 104
  13. def OAI.StableCoordinate.LNDExponential.exponential line 110

    Source documentation

    The polynomial exponential is a coefficient-field algebra homomorphism.

    def exponential (D : Derivation k A A) (hD : IsLocallyNilpotent D) : A →ₐ[k] A[X] where
…

    Mentions: OAI.StableCoordinate.IsLocallyNilpotent

  14. lemma OAI.StableCoordinate.LNDExponential.coeff_exponential line 123
  15. lemma OAI.StableCoordinate.LNDExponential.coeff_exponential_zero line 129
  16. lemma OAI.StableCoordinate.LNDExponential.coeff_exponential_one line 133