ActionWeightDerivative.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Differentiating a polynomial action commuting with fiber scaling

The manuscript's lifting argument obtains a polynomial additive action on the line-bundle torsor which commutes with its multiplicative fiber scaling. This file proves the coefficient-level implication: differentiation at parameter zero preserves every integral fiber-weight space. The commutation hypothesis is an equality of genuine ring maps into a two-parameter polynomial/Laurent ring, not a hypothesis that the differentiated map already preserves weights.

def OAI.StableCoordinate.ActionWeightDerivative.swap line 29
Source documentation
Interchange the ordinary polynomial parameter and the Laurent parameter.
```
def swap : Polynomial (LaurentPolynomial A) →+* LaurentPolynomial (Polynomial A) :=
…
```
theorem OAI.StableCoordinate.ActionWeightDerivative.coeff_coeff_swap line 34
Source documentation
The interchange map transposes the two coefficient indices.
```
theorem coeff_coeff_swap (p : Polynomial (LaurentPolynomial A)) (m : ℕ) (n : ℤ) :
    ((swap p).coeff n).coeff m = (p.coeff m).coeff n := by
…
```
Mentions: OAI.StableCoordinate.ActionWeightDerivative.swap
def OAI.StableCoordinate.ActionWeightDerivative.swapAlgHom line 52
Source documentation
The parameter interchange respects an arbitrary coefficient algebra.
```
def swapAlgHom : Polynomial (LaurentPolynomial A) →ₐ[k] LaurentPolynomial (Polynomial A) where
…
```
def OAI.StableCoordinate.ActionWeightDerivative.CommutesWithWeights line 65
Source documentation
A polynomial family commutes with a Laurent weight coaction if the two orders of applying their coefficient maps agree, after interchanging parameters.
```
def CommutesWithWeights (ρ : A →ₐ[k] LaurentPolynomial A)
    (α : A →ₐ[k] Polynomial A) : Prop :=
…
```
theorem OAI.StableCoordinate.ActionWeightDerivative.commute_coeff line 71
Source documentation
The two-parameter commutation identity can be read coefficient by coefficient.
```
theorem commute_coeff (ρ : A →ₐ[k] LaurentPolynomial A) (α : A →ₐ[k] Polynomial A)
    (hcomm : CommutesWithWeights ρ α) (a : A) (m : ℕ) (n : ℤ) :
    (ρ ((α a).coeff m)).coeff n = (α ((ρ a).coeff n)).coeff m := by
…
```
Mentions: OAI.StableCoordinate.ActionWeightDerivative.CommutesWithWeights

theorem OAI.StableCoordinate.ActionWeightDerivative.coeff_preserves_weight line 82

Source documentation

Every parameter coefficient of an equivariant polynomial family preserves an integral weight, including negative weights.

theorem coeff_preserves_weight (ρ : A →ₐ[k] LaurentPolynomial A)
    (α : A →ₐ[k] Polynomial A) (hcomm : CommutesWithWeights ρ α)
    {a : A} {n : ℤ} (ha : ρ a = AddMonoidAlgebra.single n a) (m : ℕ) :
    ρ ((α a).coeff m) = AddMonoidAlgebra.single n ((α a).coeff m) := by
…

Mentions: OAI.StableCoordinate.ActionWeightDerivative.CommutesWithWeights

theorem OAI.StableCoordinate.ActionWeightDerivative.commutesWithWeights_of_generators line 94

Source documentation

It suffices to check equivariance coefficientwise on a set of algebra generators. This converts frame-coordinate weights into equivariance of the whole lifted polynomial action.

theorem commutesWithWeights_of_generators {σ : Type*}
    (ρ : A →ₐ[k] LaurentPolynomial A) (α : A →ₐ[k] Polynomial A)
    (g : σ → A) (w : σ → ℤ) (hgen : Algebra.adjoin k (Set.range g) = ⊤)
    (hρ : ∀ i, ρ (g i) = AddMonoidAlgebra.single (w i) (g i))
    (hα : ∀ i m, ρ ((α (g i)).coeff m) =
      AddMonoidAlgebra.single (w i) ((α (g i)).coeff m)) :
    CommutesWithWeights ρ α := by
…

Mentions: OAI.StableCoordinate.ActionWeightDerivative.CommutesWithWeights

theorem OAI.StableCoordinate.ActionWeightDerivative.derivation_preserves_weight line 124

Source documentation

Differentiation at parameter zero preserves all weights. The derivation may be supplied by any proved additive-action/LND correspondence.

theorem derivation_preserves_weight (ρ : A →ₐ[k] LaurentPolynomial A)
    (α : A →ₐ[k] Polynomial A) (hcomm : CommutesWithWeights ρ α)
    (D : Derivation k A A) (hD : ∀ a, D a = (α a).coeff 1)
    {a : A} {n : ℤ} (ha : ρ a = AddMonoidAlgebra.single n a) :
    ρ (D a) = AddMonoidAlgebra.single n (D a) := by
…

Mentions: OAI.StableCoordinate.ActionWeightDerivative.CommutesWithWeights