LNDAction.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The algebraic additive action of a locally nilpotent derivation

This file combines the finite polynomial exponential with its proved additive group law. It constructs an actual polynomial coaction from any locally nilpotent derivation in characteristic zero and proves both round-trip laws.

def OAI.StableCoordinate.exponentialAction line 25
Source documentation
The algebraic additive action corresponding to a locally nilpotent derivation.
```
def exponentialAction (D : Derivation k A A) (hD : IsLocallyNilpotent D) :
    PolynomialAdditiveAction k A :=
…
```
Mentions: OAI.StableCoordinate.IsLocallyNilpotent
theorem OAI.StableCoordinate.exponentialAction_toAlgHom line 32
theorem OAI.StableCoordinate.exponentialAction_derivation line 37
Source documentation
Differentiating the exponential algebraic action recovers the derivation.
```
@[simp] theorem exponentialAction_derivation
    (D : Derivation k A A) (hD : IsLocallyNilpotent D) :
    (exponentialAction D hD).derivation = D := by
…
```
Mentions: OAI.StableCoordinate.IsLocallyNilpotent, OAI.StableCoordinate.exponentialAction

theorem OAI.StableCoordinate.exponentialAction_group_law line 44

Source documentation

Full polynomial coassociativity, not merely the coefficient specification.

theorem exponentialAction_group_law
    (D : Derivation k A A) (hD : IsLocallyNilpotent D) (a : A) :
    (LNDExponential.exponential D hD a).map (LNDExponential.exponential D hD).toRingHom =
      taylor (X : A[X]) ((LNDExponential.exponential D hD a).map C) :=
…

Mentions: OAI.StableCoordinate.IsLocallyNilpotent, OAI.StableCoordinate.LNDExponential.exponential

theorem OAI.StableCoordinate.exponentialAction_fixed_iff line 52
Source documentation
Action invariants are exactly elements annihilated by the derivation. No domain hypothesis is required here.
```
theorem exponentialAction_fixed_iff
    (D : Derivation k A A) (hD : IsLocallyNilpotent D) (a : A) :
    (exponentialAction D hD).toAlgHom a = C a ↔ D a = 0 :=
…
```
Mentions: OAI.StableCoordinate.IsLocallyNilpotent, OAI.StableCoordinate.exponentialAction
theorem OAI.StableCoordinate.exponential_derivation_eq line 60
Source documentation
A polynomial additive action is recovered by exponentiating its infinitesimal derivation, over every characteristic-zero field algebra.
```
theorem exponential_derivation_eq (ρ : PolynomialAdditiveAction k A) :
    LNDExponential.exponential ρ.derivation ρ.locallyNilpotent = ρ.toAlgHom := by
…
```
Mentions: OAI.StableCoordinate.LNDExponential.exponential
theorem OAI.StableCoordinate.exists_additiveCoaction_of_locallyNilpotent line 74
Source documentation
Existence of the action is unconditional once local nilpotence is proved.
```
theorem exists_additiveCoaction_of_locallyNilpotent
    (D : Derivation k A A) (hD : IsLocallyNilpotent D) :
    ∃ ρ : PolynomialAdditiveAction k A, ρ.derivation = D :=
…
```
Mentions: OAI.StableCoordinate.IsLocallyNilpotent
theorem OAI.StableCoordinate.additiveCoaction_ext line 81
Source documentation
Equality of additive coactions is determined by their actual algebra maps.
```
theorem additiveCoaction_ext {ρ σ : PolynomialAdditiveAction k A}
    (h : ρ.toAlgHom = σ.toAlgHom) : ρ = σ := by
…
```
def OAI.StableCoordinate.locallyNilpotentEquivAdditiveCoaction line 90
Source documentation
The full characteristic-zero correspondence between locally nilpotent algebra derivations and algebraic additive polynomial coactions.
```
def locallyNilpotentEquivAdditiveCoaction :
    {D : Derivation k A A // IsLocallyNilpotent D} ≃ PolynomialAdditiveAction k A where
…
```
Mentions: OAI.StableCoordinate.IsLocallyNilpotent

theorem OAI.StableCoordinate.derivation_iterate_naturality line 104

Source documentation

Intertwining derivations intertwines every iterate.

theorem derivation_iterate_naturality
    (D : Derivation k A A) (E : Derivation k B B) (f : A →ₐ[k] B)
    (h : ∀ a, E (f a) = f (D a)) (n : ℕ) (a : A) :
    (E : B → B)^[n] (f a) = f ((D : A → A)^[n] a) := by
…

Mentions: OAI.StableCoordinate.f

theorem OAI.StableCoordinate.exponentialAction_naturality line 114

Source documentation

A homomorphism intertwining locally nilpotent derivations is equivariant for the corresponding algebraic additive actions.

theorem exponentialAction_naturality
    (D : Derivation k A A) (E : Derivation k B B)
    (hD : IsLocallyNilpotent D) (hE : IsLocallyNilpotent E)
    (f : A →ₐ[k] B) (h : ∀ a, E (f a) = f (D a)) (a : A) :
    (exponentialAction E hE).toAlgHom (f a) =
      ((exponentialAction D hD).toAlgHom a).map f.toRingHom := by
…

Mentions: OAI.StableCoordinate.IsLocallyNilpotent, OAI.StableCoordinate.f, OAI.StableCoordinate.exponentialAction