Varying one factor of a list product in a ring

In an R-algebra A, the product of a list is affine in each factor. In particular, shifting one factor a by the scalar algebraMap R A c changes the product by c times the product of the list with that factor deleted. This is the step that centres one letter of a word at a time.

An additive map δ of a possibly noncommutative ring obeying the Leibniz rule δ (a * b) = δ a * b + a * δ b sends an ordered product f 0 * ⋯ * f (n - 1) to the sum, over the positions k, of the same product with the factor f k replaced by δ (f k). The rule covers both a derivation of a commutative ring and the inner derivation ⁅a, -⁆ of an associative ring, which is how the commutator with a Lie generator acts on a word in a universal enveloping algebra.

Main results

• List.prod_append_sub_algebraMap_cons: (l₁ ++ (a - algebraMap R A c) :: l₂).prod = (l₁ ++ a :: l₂).prod - c • (l₁ ++ l₂).prod.
• List.prod_map_snd_mem_span_of_isChain: the product of the second components of a list of labelled letters with no two consecutive equal labels lies in a span determined by the first label, when each admissible letter carries the span of the rest into it.
• AddMonoidHom.map_prod_ofFn_of_leibniz: the Leibniz rule for an ordered product of n factors.

theorem List.prod_append_sub_algebraMap_cons {R : Type u_1} {A : Type u_2} [CommSemiring R] [Ring A] [Algebra R A] (l₁ l₂ : List A) (a : A) (c : R) : (l₁ ++ (a - (algebraMap R A) c) :: l₂).prod = (l₁ ++ a :: l₂).prod - c • (l₁ ++ l₂).prod

Shifting the factor a of the product of l₁ ++ a :: l₂ by the scalar algebraMap R A c subtracts c times the product of l₁ ++ l₂.

theorem List.prod_map_snd_mem_span_of_isChain {R : Type u_3} {A : Type u_4} {κ : Type u_5} [Semiring R] [AddCommMonoid A] [Monoid A] [Module R A] (P : κ × A → Prop) (V T : κ → Set A) (hcons : ∀ (x : κ × A), P x → ∀ q ∈ Submodule.span R (T x.1), x.2 * q ∈ Submodule.span R (V x.1)) (h1 : ∀ (k : κ), 1 ∈ Submodule.span R (T k)) (hVT : ∀ (k k' : κ), k ≠ k' → V k' ⊆ T k) (W : List (κ × A)) (x : κ × A) : IsChain (fun (x1 x2 : κ) => x1 ≠ x2) (map Prod.fst (x :: W)) → (∀ y ∈ x :: W, P y) → (map Prod.snd (x :: W)).prod ∈ Submodule.span R (V x.1)

Induction along a word with no two consecutive equal labels. Let P single out the admissible labelled letters (k, a). If multiplying an admissible letter with label k onto the span of T k lands in the span of V k, the span of each T k contains 1, and V k' ⊆ T k for k ≠ k', then the product of the letters of every admissible word whose consecutive labels differ lies in the span of V k, where k is the label of its first letter.

theorem AddMonoidHom.map_prod_ofFn_of_leibniz {A : Type u_1} [Ring A] (δ : A →+ A) (hδ : ∀ (a b : A), δ (a * b) = δ a * b + a * δ b) {n : ℕ} (f : Fin n → A) : δ (List.ofFn f).prod = ∑ k : Fin n, (List.ofFn (Function.update f k (δ (f k)))).prod

The Leibniz rule for an ordered product. An additive map δ with δ (a * b) = δ a * b + a * δ b sends the product f 0 * ⋯ * f (n - 1) to the sum over k of the same product with its k-th factor replaced by δ (f k). The ring need not be commutative.