Lemma 11.1: two associative tables

binary-families.tex (lem:two-associative-tables): "Let S be a finite set with an absorbing zero, and let m, m_* be associative products on S […] Suppose m_*(a,b) = m(a,b) whenever m(a,b) ≠ 0. Put Z = {(a,b) : m(a,b) = 0, m_*(a,b) ≠ 0} and let ε_z be the bilinear map supported at z = (a,b) with value m_*(a,b) […] Assume all nested insertions vanish. There is an equivalence relation on Z such that, over every commutative ring R, the Hochschild two-cocycles among the cochains ∑ a_z ε_z have basis μ_E = ∑_{z∈E} ε_z, indexed by its classes. The product m + ∑_E T_E μ_E is associative over the polynomial ring in the T_E. When every T_E is zero or one, S ∖ {0} is a multiplicative basis for this product."

Formalization: an R-algebra Λ with a basis b indexed by S (the nonzero elements), b x * b y = b (m x y) or 0 (m : S → S → Option S), and a second associative table ms agreeing with m where m is nonzero. For coefficients a : S → S → R, eps a is ∑_{z ∈ Z} a_z ε_z. Each cocycle equation at a basis triple t has the form (a (L t) − a (Rt t)) • U t = 0 with a common value U t (dEps_eq). Hence a cochain is a cocycle iff a is constant along the relation Rel of the nonvanishing equations (isCocycle_iff); the product m + eps T is associative for such T (assoc_add_eps), and has b as a multiplicative basis when T takes values 0, 1 (mul_basis_of_binary).

noncomputable def MultiplicativeBasisDeformations.TwoTables.ob {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} (b : Module.Basis S R Λ) (o : Option S) : Λ

The basis vector of an optional index.

@[simp]

theorem MultiplicativeBasisDeformations.TwoTables.ob_none {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) : ob b none = 0

@[simp]

theorem MultiplicativeBasisDeformations.TwoTables.ob_some {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (s : S) : ob b (some s) = b s

def MultiplicativeBasisDeformations.TwoTables.InZ {S : Type u_3} (m ms : S → S → Option S) (x y : S) : Prop

The support Z.

@[instance_reducible]

instance MultiplicativeBasisDeformations.TwoTables.instDecidableInZ {S : Type u_3} (m ms : S → S → Option S) (x y : S) : Decidable (InZ m ms x y)

noncomputable def MultiplicativeBasisDeformations.TwoTables.epsVal {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} (b : Module.Basis S R Λ) (m ms : S → S → Option S) (a : S → S → R) (x y : S) : Λ

The values of the supported cochain with coefficients a on basis pairs.

noncomputable def MultiplicativeBasisDeformations.TwoTables.eps {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} (b : Module.Basis S R Λ) (m ms : S → S → Option S) (a : S → S → R) : Λ →ₗ[R] Λ →ₗ[R] Λ

The supported cochain ∑_{z ∈ Z} a_z ε_z.

theorem MultiplicativeBasisDeformations.TwoTables.eps_basis {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (a : S → S → R) (x y : S) : ((eps b m ms a) (b x)) (b y) = epsVal b m ms a x y

theorem MultiplicativeBasisDeformations.TwoTables.eps_ob_left {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (a : S → S → R) (o : Option S) (y : S) : ((eps b m ms a) (ob b o)) (b y) = o.elim 0 fun (x : S) => epsVal b m ms a x y

theorem MultiplicativeBasisDeformations.TwoTables.eps_ob_right {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (a : S → S → R) (x : S) (o : Option S) : ((eps b m ms a) (b x)) (ob b o) = o.elim 0 fun (y : S) => epsVal b m ms a x y

theorem MultiplicativeBasisDeformations.TwoTables.mul_ob {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m : S → S → Option S) (hm : ∀ (x y : S), b x * b y = ob b (m x y)) (x : S) (o : Option S) : b x * ob b o = ob b (o.bind fun (x_1 : S) => m x x_1)

theorem MultiplicativeBasisDeformations.TwoTables.ob_mul {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m : S → S → Option S) (hm : ∀ (x y : S), b x * b y = ob b (m x y)) (o : Option S) (w : S) : ob b o * b w = ob b (o.bind fun (x : S) => m x w)

noncomputable def MultiplicativeBasisDeformations.TwoTables.D {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} (b : Module.Basis S R Λ) (m ms : S → S → Option S) (a : S → S → R) (x y w : S) : Λ

The cocycle defect of eps a at a basis triple.

noncomputable def MultiplicativeBasisDeformations.TwoTables.mstar {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} (b : Module.Basis S R Λ) (ms : S → S → Option S) : Λ →ₗ[R] Λ →ₗ[R] Λ

The second table as a bilinear map.

theorem MultiplicativeBasisDeformations.TwoTables.mstar_basis {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (ms : S → S → Option S) (x y : S) : ((mstar b ms) (b x)) (b y) = ob b (ms x y)

theorem MultiplicativeBasisDeformations.TwoTables.mstar_eq {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (hm : ∀ (x y : S), b x * b y = ob b (m x y)) (hagree : ∀ (x y s : S), m x y = some s → ms x y = some s) (x y : S) : ((mstar b ms) (b x)) (b y) = b x * b y + ((eps b m ms fun (x x_1 : S) => 1) (b x)) (b y)

theorem MultiplicativeBasisDeformations.TwoTables.D_one {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (hm : ∀ (x y : S), b x * b y = ob b (m x y)) (hagree : ∀ (x y s : S), m x y = some s → ms x y = some s) (hms : ∀ (x y w : S), ((ms x y).bind fun (x : S) => ms x w) = (ms y w).bind fun (x_1 : S) => ms x x_1) (hnest : ∀ (x y s : S), InZ m ms x y → ms x y = some s → ∀ (w : S), ¬InZ m ms s w ∧ ¬InZ m ms w s) (x y w : S) : D b m ms (fun (x x_1 : S) => 1) x y w = 0

d ε = 0 for the full cochain ε = ∑_{z ∈ Z} ε_z.

Each cocycle equation compares two coefficients

theorem MultiplicativeBasisDeformations.TwoTables.T1 {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (a : S → S → R) (x y w : S) : b x * ((eps b m ms a) (b y)) (b w) = a y w • (b x * ((eps b m ms fun (x x_1 : S) => 1) (b y)) (b w))

theorem MultiplicativeBasisDeformations.TwoTables.T4 {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (a : S → S → R) (x y w : S) : ((eps b m ms a) (b x)) (b y) * b w = a x y • (((eps b m ms fun (x x_1 : S) => 1) (b x)) (b y) * b w)

theorem MultiplicativeBasisDeformations.TwoTables.T2 {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (x y w : S) : ∃ (p : S × S), ∀ (a : S → S → R), ((eps b m ms a) (ob b (m x y))) (b w) = a p.1 p.2 • ((eps b m ms fun (x x_1 : S) => 1) (ob b (m x y))) (b w)

theorem MultiplicativeBasisDeformations.TwoTables.T3 {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (x y w : S) : ∃ (p : S × S), ∀ (a : S → S → R), ((eps b m ms a) (b x)) (ob b (m y w)) = a p.1 p.2 • ((eps b m ms fun (x x_1 : S) => 1) (b x)) (ob b (m y w))

theorem MultiplicativeBasisDeformations.TwoTables.W1_ob {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (hm : ∀ (x y : S), b x * b y = ob b (m x y)) (x y w : S) : ∃ (o : Option S), b x * ((eps b m ms fun (x x_1 : S) => 1) (b y)) (b w) = ob b o

theorem MultiplicativeBasisDeformations.TwoTables.W3_ob {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (x : S) (o' : Option S) : ∃ (o : Option S), ((eps b m ms fun (x x_1 : S) => 1) (b x)) (ob b o') = ob b o

theorem MultiplicativeBasisDeformations.TwoTables.dEps_eq {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (hm : ∀ (x y : S), b x * b y = ob b (m x y)) (hagree : ∀ (x y s : S), m x y = some s → ms x y = some s) (hms : ∀ (x y w : S), ((ms x y).bind fun (x : S) => ms x w) = (ms y w).bind fun (x_1 : S) => ms x x_1) (hnest : ∀ (x y s : S), InZ m ms x y → ms x y = some s → ∀ (w : S), ¬InZ m ms s w ∧ ¬InZ m ms w s) (x y w : S) : ∃ (zl : S × S) (zr : S × S) (o : Option S), ∀ (a : S → S → R), D b m ms a x y w = (a zl.1 zl.2 - a zr.1 zr.2) • ob b o

The form of a cocycle equation: d(∑ a_z ε_z) at a basis triple is (a_z − a_{z'}) u for two pairs z, z' and a basis vector or zero u.

Cocycles, associativity and binary points

theorem MultiplicativeBasisDeformations.TwoTables.tri_ext {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} (b : Module.Basis S R Λ) (F : Λ → Λ → Λ → Λ) (h1 : ∀ (q r : Λ), ∃ (L : Λ →ₗ[R] Λ), ∀ (p : Λ), F p q r = L p) (h2 : ∀ (p r : Λ), ∃ (L : Λ →ₗ[R] Λ), ∀ (q : Λ), F p q r = L q) (h3 : ∀ (p q : Λ), ∃ (L : Λ →ₗ[R] Λ), ∀ (r : Λ), F p q r = L r) (h0 : ∀ (x y w : S), F (b x) (b y) (b w) = 0) (p q r : Λ) : F p q r = 0

Trilinear expressions vanishing on basis triples vanish.

def MultiplicativeBasisDeformations.TwoTables.Rel {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} (b : Module.Basis S R Λ) (m ms : S → S → Option S) (z z' : S × S) : Prop

The relation of the nonvanishing cocycle equations.

theorem MultiplicativeBasisDeformations.TwoTables.D_eq_zero_of_inv {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (hm : ∀ (x y : S), b x * b y = ob b (m x y)) (hagree : ∀ (x y s : S), m x y = some s → ms x y = some s) (hms : ∀ (x y w : S), ((ms x y).bind fun (x : S) => ms x w) = (ms y w).bind fun (x_1 : S) => ms x x_1) (hnest : ∀ (x y s : S), InZ m ms x y → ms x y = some s → ∀ (w : S), ¬InZ m ms s w ∧ ¬InZ m ms w s) (a : S → S → R) (ha : ∀ (z z' : S × S), Rel b m ms z z' → a z.1 z.2 = a z'.1 z'.2) (x y w : S) : D b m ms a x y w = 0

theorem MultiplicativeBasisDeformations.TwoTables.inv_of_D_eq_zero {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (a : S → S → R) (h0 : ∀ (x y w : S), D b m ms a x y w = 0) (z z' : S × S) (hr : Rel b m ms z z') : a z.1 z.2 = a z'.1 z'.2

theorem MultiplicativeBasisDeformations.TwoTables.eps_lin1 {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (a : S → S → R) (q r : Λ) : ∃ (L : Λ →ₗ[R] Λ), ∀ (p : Λ), p * ((eps b m ms a) q) r - ((eps b m ms a) (p * q)) r + ((eps b m ms a) p) (q * r) - ((eps b m ms a) p) q * r = L p

theorem MultiplicativeBasisDeformations.TwoTables.eps_lin2 {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (a : S → S → R) (p r : Λ) : ∃ (L : Λ →ₗ[R] Λ), ∀ (q : Λ), p * ((eps b m ms a) q) r - ((eps b m ms a) (p * q)) r + ((eps b m ms a) p) (q * r) - ((eps b m ms a) p) q * r = L q

theorem MultiplicativeBasisDeformations.TwoTables.eps_lin3 {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (a : S → S → R) (p q : Λ) : ∃ (L : Λ →ₗ[R] Λ), ∀ (r : Λ), p * ((eps b m ms a) q) r - ((eps b m ms a) (p * q)) r + ((eps b m ms a) p) (q * r) - ((eps b m ms a) p) q * r = L r

theorem MultiplicativeBasisDeformations.TwoTables.isCocycle_eps {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (hm : ∀ (x y : S), b x * b y = ob b (m x y)) (hagree : ∀ (x y s : S), m x y = some s → ms x y = some s) (hms : ∀ (x y w : S), ((ms x y).bind fun (x : S) => ms x w) = (ms y w).bind fun (x_1 : S) => ms x x_1) (hnest : ∀ (x y s : S), InZ m ms x y → ms x y = some s → ∀ (w : S), ¬InZ m ms s w ∧ ¬InZ m ms w s) (a : S → S → R) (ha : ∀ (z z' : S × S), Rel b m ms z z' → a z.1 z.2 = a z'.1 z'.2) (p q r : Λ) : p * ((eps b m ms a) q) r - ((eps b m ms a) (p * q)) r + ((eps b m ms a) p) (q * r) - ((eps b m ms a) p) q * r = 0

Lemma 11.1, cocycles: ∑ a_z ε_z is a Hochschild cocycle when a is constant along Rel.

noncomputable def MultiplicativeBasisDeformations.TwoTables.mT {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} (b : Module.Basis S R Λ) (m ms : S → S → Option S) (T : S → S → R) : Λ →ₗ[R] Λ →ₗ[R] Λ

The deformed product m + ∑ T_z ε_z.

theorem MultiplicativeBasisDeformations.TwoTables.mT_lin1 {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (T : S → S → R) (q r : Λ) : ∃ (L : Λ →ₗ[R] Λ), ∀ (p : Λ), ((mT b m ms T) (((mT b m ms T) p) q)) r - ((mT b m ms T) p) (((mT b m ms T) q) r) = L p

theorem MultiplicativeBasisDeformations.TwoTables.mT_lin2 {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (T : S → S → R) (p r : Λ) : ∃ (L : Λ →ₗ[R] Λ), ∀ (q : Λ), ((mT b m ms T) (((mT b m ms T) p) q)) r - ((mT b m ms T) p) (((mT b m ms T) q) r) = L q

theorem MultiplicativeBasisDeformations.TwoTables.mT_lin3 {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (T : S → S → R) (p q : Λ) : ∃ (L : Λ →ₗ[R] Λ), ∀ (r : Λ), ((mT b m ms T) (((mT b m ms T) p) q)) r - ((mT b m ms T) p) (((mT b m ms T) q) r) = L r

theorem MultiplicativeBasisDeformations.TwoTables.assoc_mT {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (hm : ∀ (x y : S), b x * b y = ob b (m x y)) (hagree : ∀ (x y s : S), m x y = some s → ms x y = some s) (hms : ∀ (x y w : S), ((ms x y).bind fun (x : S) => ms x w) = (ms y w).bind fun (x_1 : S) => ms x x_1) (hnest : ∀ (x y s : S), InZ m ms x y → ms x y = some s → ∀ (w : S), ¬InZ m ms s w ∧ ¬InZ m ms w s) (T : S → S → R) (hT : ∀ (z z' : S × S), Rel b m ms z z' → T z.1 z.2 = T z'.1 z'.2) (p q r : Λ) : ((mT b m ms T) (((mT b m ms T) p) q)) r = ((mT b m ms T) p) (((mT b m ms T) q) r)

Lemma 11.1, associativity: m + ∑ T_z ε_z is associative when T is constant along Rel.

theorem MultiplicativeBasisDeformations.TwoTables.mT_basis_of_binary {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {S : Type u_3} [DecidableEq S] (b : Module.Basis S R Λ) (m ms : S → S → Option S) (hm : ∀ (x y : S), b x * b y = ob b (m x y)) (T : S → S → R) (hT : ∀ (x y : S), T x y = 0 ∨ T x y = 1) (x y : S) : ∃ (o : Option S), ((mT b m ms T) (b x)) (b y) = ob b o

Lemma 11.1, binary points: when T takes the values 0 and 1, the basis is multiplicative for m + ∑ T_z ε_z.