Indicator cochains: relativity and characters

Two facts used in the proofs of Propositions 11.2 and 11.3 (binary-families.tex):

• the supported cochains are normalized S-relative (their values vanish on identity inputs and they commute with the vertex idempotents);
• "Every indicator has a single positive character c_E = ℓ(r*s) − ℓ(r) − ℓ(s) = ℓ(q_y). All pairs in one class E have the same character, since each equation a_z = a_{z'} comes from a homogeneous cocycle equation." (pairChar_edge)

theorem MultiplicativeBasisDeformations.RaySys.Sys.eps_endpoints {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.P.src t = S.P.src u ∧ S.P.tgt t = S.P.tgt v

A nonzero correction has the endpoints of its pair.

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

The character of a pair: ℓ(r*s) − ℓ(r) − ℓ(s).

theorem MultiplicativeBasisDeformations.RaySys.Sys.wtM_vecM_ne {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x : M S.P.toMult} (hx : x ≠ 0) (hx' : x = 0 ∨ ∃ (t : R), x = S.rr t) : ∃ (t : R), x = S.rr t

theorem MultiplicativeBasisDeformations.RaySys.Sys.pairChar_edge {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)) {z z' : R × R} (h : S.Edge z z') : S.eps z.1 z.2 ≠ 0 ∧ S.eps z'.1 z'.2 ≠ 0 ∧ S.pairChar z = S.pairChar z'

The two pairs of a cocycle equation have nonzero corrections and the same character.

theorem MultiplicativeBasisDeformations.RaySys.Sys.pairChar_class {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)) {z z' : R × R} (h : ⟦z⟧ = ⟦z'⟧) (hz : S.eps z.1 z.2 ≠ 0) : S.eps z'.1 z'.2 ≠ 0 ∧ S.pairChar z = S.pairChar z'

Pairs of one class with nonzero corrections have the same character.

The supported cochains are relative

theorem MultiplicativeBasisDeformations.RaySys.Sys.bilin_ext {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] {f g : ↥(S.P.Lin k) →ₗ[k] ↥(S.P.Lin k) →ₗ[k] ↥(S.P.Lin k)} (h : ∀ (u v : R), (f (S.P.b k u)) (S.P.b k v) = (g (S.P.b k u)) (S.P.b k v)) : f = g

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_e_mul {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)) (c : R → R → k) (x : V) (a z : ↥(S.P.Lin k)) : ((S.coch k c) (S.P.b k (S.P.e x) * a)) z = S.P.b k (S.P.e x) * ((S.coch k c) a) z

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_mul_e {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)) (c : R → R → k) (x : V) (a z : ↥(S.P.Lin k)) : ((S.coch k c) (a * S.P.b k (S.P.e x))) z = ((S.coch k c) a) (S.P.b k (S.P.e x) * z)

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_mul_e_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)) (c : R → R → k) (x : V) (a z : ↥(S.P.Lin k)) : ((S.coch k c) a) (z * S.P.b k (S.P.e x)) = ((S.coch k c) a) z * S.P.b k (S.P.e x)

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_e_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)) (c : R → R → k) (x : V) (z : ↥(S.P.Lin k)) : ((S.coch k c) (S.P.b k (S.P.e x))) z = 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_e_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)) (c : R → R → k) (x : V) (a : ↥(S.P.Lin k)) : ((S.coch k c) a) (S.P.b k (S.P.e x)) = 0

Values of the indicator cocycles

theorem MultiplicativeBasisDeformations.RaySys.Sys.muE_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] [IsAlgClosed k] (E : Quotient S.pairSetoid) (u v : R) : ((S.muE k E) (S.P.b k u)) (S.P.b k v) = if ⟦(u, v)⟧ = E then S.vecM k (S.eps u v) else 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.muE_value {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)) {E : Quotient S.pairSetoid} {χ : L} (hE : ∀ (z : R × R), ⟦z⟧ = E → S.eps z.1 z.2 ≠ 0 → S.pairChar z = χ) (u v : R) : ((S.muE k E) (S.P.b k u)) (S.P.b k v) = 0 ∨ ∃ (t : R), ((S.muE k E) (S.P.b k u)) (S.P.b k v) = S.P.b k t ∧ S.P.wt t = S.P.wt u + S.P.wt v + χ ∧ S.P.src t = S.P.src u ∧ S.P.tgt t = S.P.tgt v

An indicator of a class of character χ shifts weights by χ.