Independence of character summands of HH² (Proposition 7.6)

weights-and-parameters.tex: "Proposition 6.1 and the distinct characters χ_i now give the asserted decomposition and the one-dimensionality of every nonzero summand." For cocycles μ_i of pairwise distinct characters χ_i, the character-χ_i part of Σ_j c_j μ_j is c_i μ_i (cpr2_sum_char), and the coboundary commutes with character parts (cobdry_cpr1). Hence, in each internal degree, a combination of classes which are not coboundaries is a coboundary only when all coefficients vanish (coef_eq_zero_of_cobdry), and a cocycle of character χ_i is a multiple of μ_i modulo coboundaries once it lies in the span (eq_smul_add_cobdry).

theorem MultiplicativeBasisDeformations.LatGrading.cpr2_sum_char {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {L : Type} [AddCommGroup L] [DecidableEq L] (W : LatGrading k Λ L) {ι : Type u_1} [DecidableEq ι] (s : Finset ι) (cf : ι → k) (μ : ι → Λ →ₗ[k] Λ →ₗ[k] Λ) {χ : ι → L} (hχ : Function.Injective χ) (hμ : ∀ (j : ι), W.Char₂ (χ j) (μ j)) (i : ι) : W.cpr2 (χ i) (∑ j ∈ s, cf j • μ j) = if i ∈ s then cf i • μ i else 0

The character-χ_i part of a combination of cochains of distinct characters.

theorem MultiplicativeBasisDeformations.LatGrading.cobdry_smul {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (t : k) (f : Λ →ₗ[k] Λ) : LenGrading.cobdry k (t • f) = t • LenGrading.cobdry k f

theorem MultiplicativeBasisDeformations.LatGrading.hasDeg₁_smul {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {q : ℕ} {f : Λ →ₗ[k] Λ} (hf : G.HasDeg₁ q f) (t : k) : G.HasDeg₁ q (t • f)

theorem MultiplicativeBasisDeformations.LatGrading.coef_eq_zero_of_cobdry {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {L : Type} [AddCommGroup L] [DecidableEq L] (W : LatGrading k Λ L) {G : LenGrading k Λ} (compat : ∀ (d : ℕ) (l : L) (x : Λ), (G.proj d) ((W.proj l) x) = (W.proj l) ((G.proj d) x)) {n : ℕ} (μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ) (qd : Fin n → ℕ) {χ : Fin n → L} (hχ : Function.Injective χ) (hμ : ∀ (j : Fin n), W.Char₂ (χ j) (μ j)) (hμnz : ∀ (i : Fin n), ¬∃ (H : Λ →ₗ[k] Λ), G.HasDeg₁ (qd i) H ∧ μ i = LenGrading.cobdry k H) (q : ℕ) (cf : Fin n → k) (f : Λ →ₗ[k] Λ) (hf : G.HasDeg₁ q f) (h : ∑ j : Fin n with qd j = q, cf j • μ j = LenGrading.cobdry k f) (i : Fin n) (hi : qd i = q) : cf i = 0

Independence: in internal degree q, a combination of cocycles of distinct characters which are not coboundaries is a coboundary only with zero coefficients.

theorem MultiplicativeBasisDeformations.LatGrading.eq_smul_add_cobdry {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {L : Type} [AddCommGroup L] [DecidableEq L] (W : LatGrading k Λ L) {G : LenGrading k Λ} (compat : ∀ (d : ℕ) (l : L) (x : Λ), (G.proj d) ((W.proj l) x) = (W.proj l) ((G.proj d) x)) {n : ℕ} (μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ) (qd : Fin n → ℕ) {χ : Fin n → L} (hχ : Function.Injective χ) (hμ : ∀ (j : Fin n), W.Char₂ (χ j) (μ j)) (i : Fin n) {q : ℕ} {φ : Λ →ₗ[k] Λ →ₗ[k] Λ} (hφ : W.Char₂ (χ i) φ) (cf : Fin n → k) (f : Λ →ₗ[k] Λ) (hf : G.HasDeg₁ q f) (h : φ = ∑ j : Fin n with qd j = q, cf j • μ j + LenGrading.cobdry k f) : ∃ (t : k) (f' : Λ →ₗ[k] Λ), G.HasDeg₁ q f' ∧ φ = t • μ i + LenGrading.cobdry k f'

One-dimensionality: a cocycle of character χ_i in the span of the μ_j modulo coboundaries is a multiple of μ_i modulo coboundaries.