Weighted derivations of monoid algebras

DefinitionWeighted derivation of an additive monoid algebra#✓fully proved

Multiply the coefficient at each exponent by an additive weight of that exponent.

AddMonoidAlgebra.weightedDerivation · 25 lines

noncomputable def weightedDerivation (w : Γ →+ R) :
    Derivation R (AddMonoidAlgebra R Γ) (AddMonoidAlgebra R Γ) :=
  let D : AddMonoidAlgebra R Γ →ₗ[R] AddMonoidAlgebra R Γ :=
    (coeffLinearEquiv R).symm.toLinearMap ∘ₗ
      Finsupp.lsum R (fun g ↦ (Finsupp.lsingle g).comp (LinearMap.mulLeft R (w g))) ∘ₗ
      (coeffLinearEquiv R).toLinearMap
  Derivation.mk' D fun f h ↦ by
    simp only [smul_eq_mul]
    induction f using AddMonoidAlgebra.induction_linear with
    | zero => simp
    | add f g hf hg =>
      rw [add_mul, map_add, hf, hg, map_add]
      ring
    | single g r =>
      induction h using AddMonoidAlgebra.induction_linear with
      | zero => simp
      | add f h hf hh =>
        rw [mul_add, map_add, hf, hh, map_add]
        ring
      | single k s =>
        ext x
        by_cases hx : x = g + k
        · simp [D, w.map_add, single_mul_single, add_comm, add_mul, hx]
          ring
        · simp [D, w.map_add, single_mul_single, add_comm, add_mul, hx]

Used by 3

Used byCoefficients of a weighted derivation · Weighted derivation of a basis term · Weighted derivation with zero weight

TheoremCoefficients of a weighted derivation#✓fully proved

The coefficient at g is multiplied by the weight of g.

@[simp] theorem coeff_weightedDerivation (w : Γ →+ R)
    (f : AddMonoidAlgebra R Γ) (g : Γ) :
    (weightedDerivation w f).coeff g = w g * f.coeff g

Uses 1 · Used by 2

Statement usesWeighted derivation of an additive monoid algebra

Used byWeighted derivation of a basis term · Weighted derivation with zero weight

TheoremWeighted derivation of a basis term#✓fully proved

A basis term keeps its exponent and has its coefficient multiplied by the weight.

@[simp] theorem weightedDerivation_single (w : Γ →+ R) (g : Γ) (r : R) :
    weightedDerivation w (single g r) = single g (w g * r)

Uses 2

Statement usesWeighted derivation of an additive monoid algebra

Proof usesCoefficients of a weighted derivation

TheoremWeighted derivation with zero weight#✓fully proved

The zero weight determines the zero derivation.

@[simp] theorem weightedDerivation_zero :
    weightedDerivation (0 : Γ →+ R) = 0

Uses 2

Statement usesWeighted derivation of an additive monoid algebra

Proof usesCoefficients of a weighted derivation

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.