CoactionAction.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Polynomial additive actions: invariants and scalar automorphisms

Additional interfaces for the genuine two-parameter polynomial coaction from CoactionLND: coefficient-law construction, scalar specializations as algebra automorphisms, pointwise invariants, and characteristic-zero uniqueness.

def OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction.ofCoeffLaw line 20
Source documentation
Construct an additive algebraic action from the coefficient identities of the actual two-parameter additive group law.
```
def ofCoeffLaw (φ : A →ₐ[k] A[X])
    (hzero : ∀ a, (φ a).coeff 0 = a)
    (hadd : ∀ a m n, (φ ((φ a).coeff n)).coeff m =
      (m + n).choose m • (φ a).coeff (m + n)) : PolynomialAdditiveAction k A where
…
```
Mentions: OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction
def OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction.specialize line 35
Source documentation
Evaluate the additive action at a scalar parameter.
```
noncomputable def specialize (ρ : PolynomialAdditiveAction k A) (t : k) : A →ₐ[k] A :=
…
```
Mentions: OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction
theorem OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction.specialize_apply line 39
theorem OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction.map_specialize line 45
Source documentation
Applying a scalar specialization to coefficients translates the action parameter by that scalar.
```
theorem map_specialize (ρ : PolynomialAdditiveAction k A) (t : k) (a : A) :
    (ρ.toAlgHom a).map (ρ.specialize t).toRingHom =
      taylor (algebraMap k A t) (ρ.toAlgHom a) := by
…
```
Mentions: OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction
theorem OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction.specialize_zero line 60
theorem OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction.specialize_add line 66
Source documentation
The two-parameter polynomial group law specializes to the group law on algebra automorphisms.
```
theorem specialize_add (ρ : PolynomialAdditiveAction k A) (s t : k) (a : A) :
    ρ.specialize s (ρ.specialize t a) = ρ.specialize (s + t) a := by
…
```
Mentions: OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction
def OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction.specializeEquiv line 76
Source documentation
An algebraic additive coaction gives genuine algebra automorphisms at all scalar parameters, with inverse parameter -t.
```
noncomputable def specializeEquiv (ρ : PolynomialAdditiveAction k A) (t : k) : A ≃ₐ[k] A :=
…
```
Mentions: OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction
theorem OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction.specializeEquiv_apply line 87
theorem OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction.invariant_iff_derivation_eq_zero line 98
Source documentation
In characteristic zero, the kernel of the infinitesimal derivation is exactly the ring of invariants of the algebraic additive action.
```
theorem invariant_iff_derivation_eq_zero (ρ : PolynomialAdditiveAction k A) (a : A) :
    ρ.toAlgHom a = C a ↔ ρ.derivation a = 0 := by
…
```
Mentions: OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction
theorem OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction.toAlgHom_eq_of_derivation_eq line 118
Source documentation
Over a characteristic-zero domain the infinitesimal derivation determines an additive polynomial coaction.
```
theorem toAlgHom_eq_of_derivation_eq (ρ σ : PolynomialAdditiveAction k A)
    (h : ρ.derivation = σ.derivation) : ρ.toAlgHom = σ.toAlgHom := by
…
```
Mentions: OAI.StableCoordinate.CoactionLND.PolynomialAdditiveAction