CoactionLND.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Differentiating polynomial additive actions

This file supplies the algebraic additive-action to locally nilpotent derivation interface used when the line-bundle lift is restricted to its punctured total space. The action law is an equality of bivariate polynomials, not a merely pointwise identity. No reducedness or characteristic-zero hypothesis is needed for the forward implication.

structure OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction line 28
Source documentation
A polynomial additive-group action on an affine algebra, in contravariant form. In coassoc, the outer polynomial variable is the second parameter and the inner variable is the first parameter.
```
structure PolynomialAdditiveAction where
…
```
lemma OAI.StableCoordinate.CoactionLND.hasseDeriv_map line 38
Source documentation
Hasse derivatives commute with coefficient homomorphisms.
```
lemma hasseDeriv_map {B : Type*} [CommRing B] (f : A →+* B)
    (p : A[X]) (n : ℕ) :
    hasseDeriv n (p.map f) = (hasseDeriv n p).map f := by
…
```
Mentions: OAI.StableCoordinate.f
lemma OAI.StableCoordinate.CoactionLND.coeff_universal_translate line 46
Source documentation
Reading the outer coefficient of the universal translate gives a Hasse derivative in the inner variable.
```
lemma coeff_universal_translate (p : A[X]) (n : ℕ) :
    (taylor (X : A[X]) (p.map (C : A →+* A[X]))).coeff n =
      hasseDeriv n p := by
…
```
def OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction.derivation line 56
Source documentation
The coefficient of the action parameter is its infinitesimal derivation.
```
def derivation : Derivation k A A where
…
```
theorem OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction.derivation_apply line 66
theorem OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction.action_coeff line 70
Source documentation
Coassociativity written coefficientwise.
```
theorem action_coeff (a : A) (n : ℕ) :
    α.toAlgHom ((α.toAlgHom a).coeff n) = hasseDeriv n (α.toAlgHom a) := by
…
```
theorem OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction.derivation_coeff line 76
Source documentation
The infinitesimal action advances action coefficients by one index.
```
theorem derivation_coeff (a : A) (n : ℕ) :
    α.derivation ((α.toAlgHom a).coeff n) =
      (n + 1) • (α.toAlgHom a).coeff (n + 1) := by
…
```
theorem OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction.iterate_derivation line 83
Source documentation
The iterates are factorial multiples of action coefficients.
```
theorem iterate_derivation (a : A) (n : ℕ) :
    (α.derivation : A → A)^[n] a = n.factorial • (α.toAlgHom a).coeff n := by
…
```
theorem OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction.iterate_derivation_eq_zero line 94
Source documentation
An algebraic additive action differentiates to a locally nilpotent derivation; its action polynomial gives an explicit nilpotence bound.
```
theorem iterate_derivation_eq_zero (a : A) :
    (α.derivation : A → A)^[(α.toAlgHom a).natDegree + 1] a = 0 := by
…
```
theorem OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction.locallyNilpotent line 100
Source documentation
Pointwise local nilpotence in the common interface used by the project.
```
theorem locallyNilpotent : ∀ a, ∃ n : ℕ, (α.derivation : A → A)^[n] a = 0 :=
…
```
theorem OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction.action_eq_C_of_derivation_eq_zero line 105
Source documentation
In characteristic zero over a domain, a vanishing infinitesimal action forces the entire polynomial action to be trivial.
```
theorem action_eq_C_of_derivation_eq_zero [NoZeroDivisors A] [CharZero A]
    (h : α.derivation = 0) (a : A) : α.toAlgHom a = C a := by
…
```
theorem OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction.derivation_ne_zero_of_nontrivial line 121
Source documentation
A nontrivial polynomial additive action has a nonzero infinitesimal derivation in characteristic zero over a domain.
```
theorem derivation_ne_zero_of_nontrivial [NoZeroDivisors A] [CharZero A]
    (h : ∃ a, α.toAlgHom a ≠ C a) : α.derivation ≠ 0 := by
…
```
theorem OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction.derivation_naturality line 130
Source documentation
Equivariance of additive actions differentiates to equivariance of their derivations. In particular, a lifted action differentiates to an extension of the original derivation.
```
theorem derivation_naturality {B : Type*} [CommRing B] [Algebra k B]
    (β : PolynomialAdditiveAction k B) (f : A →ₐ[k] B)
    (hf : ∀ a, β.toAlgHom (f a) = (α.toAlgHom a).map f.toRingHom) (a : A) :
    β.derivation (f a) = f (α.derivation a) := by
…
```
Mentions: OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction, OAI.StableCoordinate.f
theorem OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction.derivation_ne_zero_of_injective line 139
Source documentation
An injective equivariant algebra extension preserves nontriviality of the infinitesimal derivation.
```
theorem derivation_ne_zero_of_injective {B : Type*} [CommRing B] [Algebra k B]
    (β : PolynomialAdditiveAction k B) (f : A →ₐ[k] B)
    (hf : ∀ a, β.toAlgHom (f a) = (α.toAlgHom a).map f.toRingHom)
    (hinj : Function.Injective f) (hα : α.derivation ≠ 0) : β.derivation ≠ 0 := by
…
```
Mentions: OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction, OAI.StableCoordinate.f