LNDExponentialLaw.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Additive group law for the polynomial exponential of a derivation

For any polynomial algebra map whose coefficients are the factorially divided iterates of a derivation, this file proves the iterative coefficient law. The construction of the polynomial map from local nilpotence is kept separate.

lemma OAI.StableCoordinate.LNDExponentialLaw.iterate_smul line 25
lemma OAI.StableCoordinate.LNDExponentialLaw.inv_factorial_mul_inv_factorial line 33

theorem OAI.StableCoordinate.LNDExponentialLaw.coefficient_iterative line 44

Source documentation

The coefficient law of the additive group, derived from divided iterates.

theorem coefficient_iterative
    (D : Derivation k A A) (E : A →ₐ[k] A[X])
    (hE : ∀ a n, (E a).coeff n = (n.factorial : k)⁻¹ • ((D : A → A)^[n]) a)
    (a : A) (n m : ℕ) :
    (E ((E a).coeff m)).coeff n =
      (n + m).choose n • (E a).coeff (n + m) := by
…

theorem OAI.StableCoordinate.LNDExponentialLaw.coefficient_zero line 58

Source documentation

Normalization at the identity of the additive group.

theorem coefficient_zero
    (D : Derivation k A A) (E : A →ₐ[k] A[X])
    (hE : ∀ a n, (E a).coeff n = (n.factorial : k)⁻¹ • ((D : A → A)^[n]) a)
    (a : A) : (E a).coeff 0 = a := by
…

theorem OAI.StableCoordinate.LNDExponentialLaw.coefficient_one line 66

Source documentation

Extracting the linear coefficient recovers the infinitesimal derivation.

theorem coefficient_one
    (D : Derivation k A A) (E : A →ₐ[k] A[X])
    (hE : ∀ a n, (E a).coeff n = (n.factorial : k)⁻¹ • ((D : A → A)^[n]) a)
    (a : A) : (E a).coeff 1 = D a := by
…

lemma OAI.StableCoordinate.LNDExponentialLaw.iterate_zero line 73
lemma OAI.StableCoordinate.LNDExponentialLaw.iterate_eq_zero_of_pos line 80

theorem OAI.StableCoordinate.LNDExponentialLaw.fixed_iff line 87

Source documentation

Invariants of the infinitesimal derivation are exactly fixed elements of its exponential.

theorem fixed_iff
    (D : Derivation k A A) (E : A →ₐ[k] A[X])
    (hE : ∀ a n, (E a).coeff n = (n.factorial : k)⁻¹ • ((D : A → A)^[n]) a)
    (a : A) : E a = C a ↔ D a = 0 := by
…

theorem OAI.StableCoordinate.LNDExponentialLaw.eval_zero line 105

Source documentation

Evaluation at parameter zero is the identity.

theorem eval_zero
    (D : Derivation k A A) (E : A →ₐ[k] A[X])
    (hE : ∀ a n, (E a).coeff n = (n.factorial : k)⁻¹ • ((D : A → A)^[n]) a)
    (a : A) : (E a).eval 0 = a := by
…