Indicator cocycles on zero products (Section 11)

lem:two-associative-tables, prop:indicator-cocycles and the associativity part of prop:zero-product-family (binary-families.tex), for A₀ = kP.

The correction ε(r, s) = r * s on pairs with rs = 0 (and 0 otherwise) is the difference of the stem product (associative, Prop 8.12) and the ray product. The identity dε = 0 of the proof of Lemma 11.1 is proved here in the monoid with zero M P, case by case on the table of that proof; nested insertions vanish by Cor 8.11.

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.eps {V R L : Type} [AddCommGroup L] [DecidableEq R] (S : Sys V R L) (u v : R) : M S.P.toMult

The correction ε(r, s): the stem product on zero pairs, zero otherwise.

theorem MultiplicativeBasisDeformations.RaySys.Sys.eps_cases {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (u v : R) : S.eps u v = 0 ∨ ∃ (w : R), S.eps u v = S.rr w

theorem MultiplicativeBasisDeformations.RaySys.Sys.eps_of_mul_ne {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {u v : R} (h : S.rr u * S.rr v ≠ 0) : S.eps u v = 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.eps_of_mul_eq {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {u v : R} (h : S.rr u * S.rr v = 0) : S.eps u v = S.stem u v

theorem MultiplicativeBasisDeformations.RaySys.Sys.stem_of_killed_tgt {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {t w : R} (h : S.rr t * S.q (S.P.tgt t) = 0) : S.stem t w = S.rr t * S.rr w

The stem product with a ray killed by its target radical is the ray product.

theorem MultiplicativeBasisDeformations.RaySys.Sys.qpow_mul_of_ne {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {y : V} {t : R} (hy : y ≠ S.P.src t) {n : ℕ} (hn : 1 ≤ n) : S.q y ^ n * S.rr t = 0

A positive local power at a vertex other than the source of a ray kills it.

theorem MultiplicativeBasisDeformations.RaySys.Sys.stem_of_killed_src {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {t w : R} (h : S.q (S.P.src t) * S.rr t = 0) : S.stem w t = S.rr w * S.rr t

The stem product with a ray killed by its source radical is the ray product.

theorem MultiplicativeBasisDeformations.RaySys.Sys.eps_killed {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) {u v t : R} (h : S.eps u v = S.rr t) : S.rr t * S.q (S.P.tgt t) = 0 ∧ S.q (S.P.src t) * S.rr t = 0

A correction value is killed by both endpoint radicals (Cor 8.13).

theorem MultiplicativeBasisDeformations.RaySys.Sys.stemL_eps {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (u v w : R) : S.stemL (S.eps u v) w = S.eps u v * S.rr w

The stem product of a correction value with a ray.

theorem MultiplicativeBasisDeformations.RaySys.Sys.stemR_eps {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (u v w : R) : S.stemR u (S.eps v w) = S.rr u * S.eps v w

The stem product of a ray with a correction value.

theorem MultiplicativeBasisDeformations.RaySys.Sys.deps_zero {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (u v w : R) : (S.rr u * S.rr v = 0 → S.rr v * S.rr w = 0 → S.eps u v * S.rr w = S.rr u * S.eps v w) ∧ (∀ (t' : R), S.rr u * S.rr v = 0 → S.rr v * S.rr w = S.rr t' → S.eps u v * S.rr w = S.eps u t') ∧ (∀ (t : R), S.rr u * S.rr v = S.rr t → S.rr v * S.rr w = 0 → S.eps t w = S.rr u * S.eps v w) ∧ ∀ (t t' : R), S.rr u * S.rr v = S.rr t → S.rr v * S.rr w = S.rr t' → S.eps t w = S.eps u t'

dε = 0 (proof of Lemma 11.1), the four cases of its table.

theorem MultiplicativeBasisDeformations.RaySys.Sys.eps_nested {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) {u v t : R} (h : S.eps u v = S.rr t) (w : R) : S.eps t w = 0 ∧ S.eps w t = 0

Nested insertions vanish (Prop 11.2(3)).

theorem MultiplicativeBasisDeformations.RaySys.Sys.eps_ne_zero_spec {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) {u v : R} (h : S.eps u v ≠ 0) : S.rr u * S.rr v = 0 ∧ S.IsGen u ∧ S.IsGen v ∧ S.P.tgt u = S.P.src v ∧ S.eps u v = S.rr u * S.q (S.P.tgt u) * S.rr v

A nonzero correction is r q_y s on a composable zero pair of generating rays.

theorem MultiplicativeBasisDeformations.RaySys.Sys.eps_local_left {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) {u : R} (hu : S.P.src u = S.P.tgt u) (v : R) : S.eps u v = 0

Corrections vanish on local left inputs (proof of Prop 11.3(3)).

theorem MultiplicativeBasisDeformations.RaySys.Sys.eps_local_right {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (u : R) {v : R} (hv : S.P.src v = S.P.tgt v) : S.eps u v = 0

Corrections vanish on local right inputs.

Cochains supported on zero pairs

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.vecM {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (K : Type u) [Field K] (x : M S.P.toMult) : ↥(S.P.Lin K)

The basis vector of a ray, and zero.

theorem MultiplicativeBasisDeformations.RaySys.Sys.vecM_rr {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (K : Type u) [Field K] (r : R) : S.vecM K (S.rr r) = S.P.b K r

theorem MultiplicativeBasisDeformations.RaySys.Sys.vecM_zero {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (K : Type u) [Field K] : S.vecM K 0 = 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.b_mul_b {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (K : Type u) [Field K] (u v : R) : S.P.b K u * S.P.b K v = S.vecM K (S.rr u * S.rr v)

theorem MultiplicativeBasisDeformations.RaySys.Sys.b_mul_vecM {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (K : Type u) [Field K] (u : R) {x : M S.P.toMult} (hx : x = 0 ∨ ∃ (w : R), x = S.rr w) : S.P.b K u * S.vecM K x = S.vecM K (S.rr u * x)

theorem MultiplicativeBasisDeformations.RaySys.Sys.vecM_mul_b {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (K : Type u) [Field K] (w : R) {x : M S.P.toMult} (hx : x = 0 ∨ ∃ (u : R), x = S.rr u) : S.vecM K x * S.P.b K w = S.vecM K (x * S.rr w)

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.coch {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (K : Type u) [Field K] (a : R → R → K) : ↥(S.P.Lin K) →ₗ[K] ↥(S.P.Lin K) →ₗ[K] ↥(S.P.Lin K)

The cochain Σ a_z ε_z with coefficients a : R → R → K (supported on zero pairs).

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_b {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (K : Type u) [Field K] (a : R → R → K) (u v : R) : ((S.coch K a) (S.P.b K u)) (S.P.b K v) = a u v • S.vecM K (S.eps u v)

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_vecM {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (K : Type u) [Field K] (a : R → R → K) {x : M S.P.toMult} (hx : x = 0 ∨ ∃ (u : R), x = S.rr u) (w : R) : ((S.coch K a) (S.vecM K x)) (S.P.b K w) = match x, hx with | Elt.ray u, hx => a u w • S.vecM K (S.eps u w) | x, hx => 0

def MultiplicativeBasisDeformations.RaySys.Sys.posP {V R L : Type} [AddCommGroup L] (S : Sys V R L) (u v w : R) : R × R

The pair carrying the positive term of the cocycle equation at (u, v, w).

def MultiplicativeBasisDeformations.RaySys.Sys.negP {V R L : Type} [AddCommGroup L] (S : Sys V R L) (u v w : R) : R × R

The pair carrying the negative term.

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.Xv {V R L : Type} [AddCommGroup L] [DecidableEq R] (S : Sys V R L) (u v w : R) : M S.P.toMult

The common value of the two terms.

theorem MultiplicativeBasisDeformations.RaySys.Sys.Xv_cases {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (u v w : R) : S.Xv u v w = 0 ∨ ∃ (t : R), S.Xv u v w = S.rr t

theorem MultiplicativeBasisDeformations.RaySys.Sys.eq_zero_of_basis3 {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (K : Type u) [Field K] {N : Type u_1} [AddCommGroup N] [Module K N] (E : ↥(S.P.Lin K) → ↥(S.P.Lin K) → ↥(S.P.Lin K) → N) (h1 : ∀ (a a' b c : ↥(S.P.Lin K)), E (a + a') b c = E a b c + E a' b c) (h1' : ∀ (t : K) (a b c : ↥(S.P.Lin K)), E (t • a) b c = t • E a b c) (h2 : ∀ (a b b' c : ↥(S.P.Lin K)), E a (b + b') c = E a b c + E a b' c) (h2' : ∀ (t : K) (a b c : ↥(S.P.Lin K)), E a (t • b) c = t • E a b c) (h3 : ∀ (a b c c' : ↥(S.P.Lin K)), E a b (c + c') = E a b c + E a b c') (h3' : ∀ (t : K) (a b c : ↥(S.P.Lin K)), E a b (t • c) = t • E a b c) (hh : ∀ (u v w : R), E (S.P.b K u) (S.P.b K v) (S.P.b K w) = 0) (a b c : ↥(S.P.Lin K)) : E a b c = 0

A function linear in each of three arguments vanishes if it vanishes on basis triples.

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_expr {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] [IsAlgClosed k] (K : Type u) [Field K] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (a : R → R → K) (u v w : R) : S.P.b K u * ((S.coch K a) (S.P.b K v)) (S.P.b K w) - ((S.coch K a) (S.P.b K u * S.P.b K v)) (S.P.b K w) + ((S.coch K a) (S.P.b K u)) (S.P.b K v * S.P.b K w) - ((S.coch K a) (S.P.b K u)) (S.P.b K v) * S.P.b K w = (a (S.posP u v w).1 (S.posP u v w).2 - a (S.negP u v w).1 (S.negP u v w).2) • S.vecM K (S.Xv u v w)

The cocycle equation on a basis triple (proof of Lemma 11.1): one positive and one negative term, with the same value.

def MultiplicativeBasisDeformations.RaySys.Sys.EdgeOK {V R L : Type} [AddCommGroup L] [DecidableEq R] (S : Sys V R L) (K : Type u) (a : R → R → K) : Prop

The coefficient condition: equal coefficients on the two terms of every equation.

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_isCocycle_iff {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] [IsAlgClosed k] (K : Type u) [Field K] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (a : R → R → K) : LenGrading.IsCocycle₂ (S.coch K a) ↔ S.EdgeOK K a

Prop 11.2(1): the supported cochain is a cocycle iff its coefficients satisfy the equalities.

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_add {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (K : Type u) [Field K] (a a' : R → R → K) : S.coch K (a + a') = S.coch K a + S.coch K a'

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_smul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (K : Type u) [Field K] (t : K) (a : R → R → K) : S.coch K (t • a) = t • S.coch K a

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_sum {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (K : Type u) [Field K] {ι : Type u_1} (s : Finset ι) (a : ι → R → R → K) : S.coch K (∑ i ∈ s, a i) = ∑ i ∈ s, S.coch K (a i)

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_nested {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] [IsAlgClosed k] (K : Type u) [Field K] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (a b : R → R → K) (x y z : ↥(S.P.Lin K)) : ((S.coch K a) (((S.coch K b) x) y)) z = 0 ∧ ((S.coch K a) x) (((S.coch K b) y) z) = 0

Mixed insertions vanish (eq:mixed-insertions-zero).

theorem MultiplicativeBasisDeformations.RaySys.Sys.family_assoc {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] [IsAlgClosed k] (K : Type u) [Field K] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) {a : R → R → K} (ha : S.EdgeOK K a) (x y z : ↥(S.P.Lin K)) : (x * y + ((S.coch K a) x) y) * z + ((S.coch K a) (x * y + ((S.coch K a) x) y)) z = x * (y * z + ((S.coch K a) y) z) + ((S.coch K a) x) (y * z + ((S.coch K a) y) z)

Prop 11.3(1): m + Σ a_z ε_z is associative when the coefficients satisfy the equalities.

Indicator classes (Prop 11.2(2))

def MultiplicativeBasisDeformations.RaySys.Sys.Edge {V R L : Type} [AddCommGroup L] [DecidableEq R] (S : Sys V R L) (z z' : R × R) : Prop

Two pairs carry the two terms of one cocycle equation.

def MultiplicativeBasisDeformations.RaySys.Sys.pairSetoid {V R L : Type} [AddCommGroup L] [DecidableEq R] (S : Sys V R L) : Setoid (R × R)

The equivalence relation generated by the cocycle equations.

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.ind {V R L : Type} [AddCommGroup L] [DecidableEq R] (S : Sys V R L) (K : Type u) [Field K] (c : Quotient S.pairSetoid) : R → R → K

The indicator coefficients of a class.

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.muE {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (K : Type u) [Field K] (c : Quotient S.pairSetoid) : ↥(S.P.Lin K) →ₗ[K] ↥(S.P.Lin K) →ₗ[K] ↥(S.P.Lin K)

The indicator cocycle μ_E (eq:indicator-cocycles).

theorem MultiplicativeBasisDeformations.RaySys.Sys.edgeOK_ind {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (K : Type u) [Field K] (c : Quotient S.pairSetoid) : S.EdgeOK K (S.ind K c)

theorem MultiplicativeBasisDeformations.RaySys.Sys.const_of_edgeOK {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (K : Type u) [Field K] {a : R → R → K} (ha : S.EdgeOK K a) {z z' : R × R} (h : ⟦z⟧ = ⟦z'⟧) : a z.1 z.2 = a z'.1 z'.2

Coefficients satisfying the equalities are constant on classes.

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_eq_sum_muE {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] [IsAlgClosed k] (K : Type u) [Field K] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) {a : R → R → K} (ha : LenGrading.IsCocycle₂ (S.coch K a)) [Fintype (Quotient S.pairSetoid)] : S.coch K a = ∑ c : Quotient S.pairSetoid, a c.out.1 c.out.2 • S.muE K c

Prop 11.2(2): a supported cocycle is a combination of indicator cocycles.