structure TensorCategories.HigherDerivationSystem (k : Type w) [Field k] (A : Type w) [Ring A] [Algebra k A] (ε : A →ₐ[k] k) : Type w

A higher derivation system on a k-algebra A augmented by ε : A →ₐ[k] k: a sequence of k-linear functionals χ n : A → k with χ 0 = ε and the Leibniz-type product formula χ_n(ab) = ∑_j (n choose j) χ_j(a) χ_{n-j}(b). Used to prove vanishing of higher derivations on finite-dimensional algebras in characteristic zero.

• χ : ℕ → A →ₗ[k] k
• χ_zero : self.χ 0 = ε.toLinearMap
• χ_mul (n : ℕ) (a b : A) : (self.χ n) (a * b) = ∑ j ∈ Finset.range (n + 1), ↑(n.choose j) * (self.χ j) a * (self.χ (n - j)) b

theorem TensorCategories.HigherDerivationSystem.χ_one_mul {k : Type w} [Field k] {A : Type w} [Ring A] [Algebra k A] {ε : A →ₐ[k] k} (hds : HigherDerivationSystem k A ε) (a b : A) : (hds.χ 1) (a * b) = (hds.χ 1) a * ε b + ε a * (hds.χ 1) b

Leibniz rule at level one: χ_1 is an ε-twisted derivation.

theorem TensorCategories.HigherDerivationSystem.χ_apply_zero {k : Type w} [Field k] {A : Type w} [Ring A] [Algebra k A] {ε : A →ₐ[k] k} (hds : HigherDerivationSystem k A ε) (a : A) : (hds.χ 0) a = ε a

The zeroth functional χ 0 agrees with the augmentation ε.

theorem TensorCategories.HigherDerivationSystem.χ_one_one {k : Type w} [Field k] {A : Type w} [Ring A] [Algebra k A] {ε : A →ₐ[k] k} (hds : HigherDerivationSystem k A ε) : (hds.χ 1) 1 = 0

χ 1 vanishes on the unit of A.

theorem TensorCategories.HigherDerivationSystem.χ_one_algebraMap {k : Type w} [Field k] {A : Type w} [Ring A] [Algebra k A] {ε : A →ₐ[k] k} (hds : HigherDerivationSystem k A ε) (r : k) : (hds.χ 1) ((algebraMap k A) r) = 0

χ 1 vanishes on scalars from k.

theorem TensorCategories.HigherDerivationSystem.χ_pow_vanish {k : Type w} [Field k] {A : Type w} [Ring A] [Algebra k A] {ε : A →ₐ[k] k} (hds : HigherDerivationSystem k A ε) {a : A} (ha : ε a = 0) (m n : ℕ) (hmn : m < n) : (hds.χ m) (a ^ n) = 0

For a in the augmentation ideal, χ_m (a^n) = 0 whenever m < n.

theorem TensorCategories.HigherDerivationSystem.χ_pow_diagonal {k : Type w} [Field k] {A : Type w} [Ring A] [Algebra k A] {ε : A →ₐ[k] k} (hds : HigherDerivationSystem k A ε) {a : A} (ha : ε a = 0) (n : ℕ) : (hds.χ n) (a ^ n) = ↑n.factorial * (hds.χ 1) a ^ n

For a in the augmentation ideal, χ_n (a^n) = n! · (χ_1 a)^n.

theorem TensorCategories.HigherDerivationSystem.coeff_zero_of_sum_pow_eq_zero {k : Type w} [Field k] {A : Type w} [Ring A] [Algebra k A] {ε : A →ₐ[k] k} (hds : HigherDerivationSystem k A ε) [CharZero k] {a : A} (ha : ε a = 0) (hne : (hds.χ 1) a ≠ 0) (s : Finset ℕ) (g : ℕ → k) (hzero : ∑ j ∈ s, g j • a ^ j = 0) (i : ℕ) (hi : i ∈ s) : g i = 0

In characteristic zero, any nontrivial polynomial relation ∑ g_j • a^j = 0 among the powers of an augmentation-ideal element with χ_1 a ≠ 0 forces all coefficients to vanish.

theorem TensorCategories.HigherDerivationSystem.powers_linearIndependent {k : Type w} [Field k] {A : Type w} [Ring A] [Algebra k A] {ε : A →ₐ[k] k} (hds : HigherDerivationSystem k A ε) [CharZero k] {a : A} (ha : ε a = 0) (hne : (hds.χ 1) a ≠ 0) : LinearIndependent k fun (n : ℕ) => a ^ n

In characteristic zero, the powers of a are k-linearly independent whenever a lies in the augmentation ideal and χ_1 a ≠ 0.

theorem TensorCategories.HigherDerivationSystem.higher_derivation_vanishes {k : Type w} [Field k] {A : Type w} [Ring A] [Algebra k A] {ε : A →ₐ[k] k} (hds : HigherDerivationSystem k A ε) [CharZero k] [FiniteDimensional k A] : hds.χ 1 = 0

Main vanishing theorem (used in the proof of Theorem 1.27.4): on a finite-dimensional algebra in characteristic zero, the first higher derivation χ 1 of any system is zero.

class TensorCategories.HasHigherDerivationContradiction (k : Type w) [Field k] [CharZero k] : Prop

Typeclass packaging the vanishing of χ 1 for every higher derivation system on every finite-dimensional k-algebra, used as a hypothesis in higher-level results.

• higher_derivation_vanishes (A : Type w) [Ring A] [Algebra k A] [FiniteDimensional k A] (ε : A →ₐ[k] k) (hds : HigherDerivationSystem k A ε) : hds.χ 1 = 0

instance TensorCategories.instHasHigherDerivationContradiction (k : Type w) [Field k] [CharZero k] : HasHigherDerivationContradiction k

Any field of characteristic zero satisfies HasHigherDerivationContradiction, via the vanishing theorem higher_derivation_vanishes.