The Hochschild complex of OP in one character

integral-deformations.tex: "We put A^{(2)} = 𝔽₂P and A^{(4)} = 𝒪P; all cochains are normalized relative to the vertex identities and respect the categorical grading and the integer ray weights."

For a ray system with weights and a character χ, a normalized relative cochain of character χ on the linearization OP (any commutative ring O) sends a composable pair of nonidentity rays (u, v) to a multiple of the ray w₂(u, v) with the endpoints of uv and weight ℓ(u) + ℓ(v) + χ (unique by sep). Such cochains are coefficient functions on the pairs for which w₂ exists (C2); one-cochains are coefficient functions on the shiftable rays (C1). Their realizations Φ₁, Φ₂ as linear and bilinear maps of OP, and the coboundary d₁ in coefficients (d1), with hcobdry (Φ₁ f) = Φ₂ (d₁ f).

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.w2 {V R L : Type} [AddCommGroup L] [DecidableEq L] [DecidableEq V] [Fintype R] (S : Sys V R L) (χ : L) (u v : R) : Option R

The ray with the endpoints of uv and weight ℓ(u) + ℓ(v) + χ, if any.

theorem MultiplicativeBasisDeformations.RaySys.Sys.w2_eq_some {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) {u v t : R} : S.w2 χ u v = some t ↔ S.P.src t = S.P.src u ∧ S.P.tgt t = S.P.tgt v ∧ S.P.wt t = S.P.wt u + S.P.wt v + χ

def MultiplicativeBasisDeformations.RaySys.Sys.I2 {V R L : Type} [AddCommGroup L] [DecidableEq L] [DecidableEq V] [Fintype R] (S : Sys V R L) (χ : L) (p : R × R) : Prop

The index set of normalized relative two-cochains of character χ.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.RaySys.Sys.C1 {V R L : Type} [AddCommGroup L] (S : Sys V R L) (χ : L) (O : Type u) : Type u

Coefficient one-cochains: functions on the shiftable rays.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.RaySys.Sys.C2 {V R L : Type} [AddCommGroup L] [DecidableEq L] [DecidableEq V] [Fintype R] (S : Sys V R L) (χ : L) (O : Type u) : Type u

Coefficient two-cochains: functions on the composable nonidentity pairs with a target.

def MultiplicativeBasisDeformations.RaySys.Sys.vecW {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (O : Type u) [CommRing O] [Nontrivial O] (o : Option R) : ↥(S.P.Lin O)

The vector of a ray, or zero.

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.Φ1 {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (O : Type u) [CommRing O] [Nontrivial O] (f : S.C1 χ O) : ↥(S.P.Lin O) →ₗ[O] ↥(S.P.Lin O)

The realization of a one-cochain as a linear map of OP.

theorem MultiplicativeBasisDeformations.RaySys.Sys.Φ1_b {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (O : Type u) [CommRing O] [Nontrivial O] (f : S.C1 χ O) (r : R) : (S.Φ1 χ O f) (S.P.b O r) = if h : S.Shift χ r then f ⟨r, h⟩ • S.P.b O (S.succ χ r) else 0

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.Φ2 {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (O : Type u) [CommRing O] [Nontrivial O] (c : S.C2 χ O) : ↥(S.P.Lin O) →ₗ[O] ↥(S.P.Lin O) →ₗ[O] ↥(S.P.Lin O)

The realization of a two-cochain as a bilinear map of OP.

theorem MultiplicativeBasisDeformations.RaySys.Sys.Φ2_b {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (O : Type u) [CommRing O] [Nontrivial O] (c : S.C2 χ O) (u v : R) : ((S.Φ2 χ O c) (S.P.b O u)) (S.P.b O v) = if h : S.I2 χ (u, v) then c ⟨(u, v), h⟩ • S.vecW O (S.w2 χ u v) else 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.b_mul_b_opt {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (O : Type u) [CommRing O] [Nontrivial O] (u v : R) : S.P.b O u * S.P.b O v = S.vecW O (S.P.mul u v)

theorem MultiplicativeBasisDeformations.RaySys.Sys.vecW_none {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (O : Type u) [CommRing O] [Nontrivial O] : S.vecW O none = 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.vecW_some {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (O : Type u) [CommRing O] [Nontrivial O] (t : R) : S.vecW O (some t) = S.P.b O t

theorem MultiplicativeBasisDeformations.RaySys.Sys.w2_of_mul_succ_right {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {u v t : R} (hv : S.Shift χ v) (h : S.P.mul u (S.succ χ v) = some t) : S.w2 χ u v = some t

A product of a ray with a successor lands on w₂.

theorem MultiplicativeBasisDeformations.RaySys.Sys.w2_of_mul_succ_left {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {u v t : R} (hu : S.Shift χ u) (h : S.P.mul (S.succ χ u) v = some t) : S.w2 χ u v = some t

theorem MultiplicativeBasisDeformations.RaySys.Sys.w2_of_mul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {u v t : R} (h : S.P.mul u v = some t) (ht : S.Shift χ t) : S.w2 χ u v = some (S.succ χ t)

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.d1raw {V R L : Type} [AddCommGroup L] [DecidableEq L] [DecidableEq V] [Fintype R] (S : Sys V R L) (χ : L) (O : Type u) [CommRing O] (f : S.C1 χ O) (u v : R) : O

The coboundary of a one-cochain, in coefficients (three substitution terms).

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.d1 {V R L : Type} [AddCommGroup L] [DecidableEq L] [DecidableEq V] [Fintype R] (S : Sys V R L) (χ : L) (O : Type u) [CommRing O] (f : S.C1 χ O) : S.C2 χ O

The coboundary d₁ in coefficients.

theorem MultiplicativeBasisDeformations.RaySys.Sys.term1 {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (O : Type u) [CommRing O] [Nontrivial O] (f : S.C1 χ O) (u v : R) : S.P.b O u * (S.Φ1 χ O f) (S.P.b O v) = (if h : S.Shift χ v ∧ (S.P.mul u (S.succ χ v)).isSome = true then f ⟨v, ⋯⟩ else 0) • S.vecW O (S.w2 χ u v)

theorem MultiplicativeBasisDeformations.RaySys.Sys.term3 {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (O : Type u) [CommRing O] [Nontrivial O] (f : S.C1 χ O) (u v : R) : (S.Φ1 χ O f) (S.P.b O u) * S.P.b O v = (if h : S.Shift χ u ∧ (S.P.mul (S.succ χ u) v).isSome = true then f ⟨u, ⋯⟩ else 0) • S.vecW O (S.w2 χ u v)

theorem MultiplicativeBasisDeformations.RaySys.Sys.term2 {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (O : Type u) [CommRing O] [Nontrivial O] (f : S.C1 χ O) (u v : R) : (S.Φ1 χ O f) (S.P.b O u * S.P.b O v) = (match S.P.mul u v with | some t => if ht : S.Shift χ t then f ⟨t, ht⟩ else 0 | none => 0) • S.vecW O (S.w2 χ u v)

theorem MultiplicativeBasisDeformations.RaySys.Sys.not_shift_e {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (x : V) : ¬S.Shift χ (S.P.e x)

theorem MultiplicativeBasisDeformations.RaySys.Sys.not_shift_of_eq_e {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) {r : R} (h : r = S.P.e (S.P.src r)) : ¬S.Shift χ r

theorem MultiplicativeBasisDeformations.RaySys.Sys.d1raw_eq_zero_of_not {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (O : Type u) [CommRing O] [Nontrivial O] (f : S.C1 χ O) {u v : R} (h : ¬S.I2 χ (u, v)) (hw : (S.w2 χ u v).isSome = true) : S.d1raw χ O f u v = 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.hcobdry_Φ1 {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (O : Type u) [CommRing O] [Nontrivial O] (f : S.C1 χ O) : GExt.hcobdry (S.Φ1 χ O f) = S.Φ2 χ O (S.d1 χ O f)

d(Φ₁ f) = Φ₂(d₁ f).

The cocycle condition in coefficients

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.w3 {V R L : Type} [AddCommGroup L] [DecidableEq L] [DecidableEq V] [Fintype R] (S : Sys V R L) (χ : L) (u v w : R) : Option R

The ray with the endpoints of uvw and weight ℓ(u) + ℓ(v) + ℓ(w) + χ, if any.

theorem MultiplicativeBasisDeformations.RaySys.Sys.w3_eq_some {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) {u v w t : R} : S.w3 χ u v w = some t ↔ S.P.src t = S.P.src u ∧ S.P.tgt t = S.P.tgt w ∧ S.P.wt t = S.P.wt u + S.P.wt v + S.P.wt w + χ

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.d2raw {V R L : Type} [AddCommGroup L] [DecidableEq L] [DecidableEq V] [Fintype R] (S : Sys V R L) (χ : L) (O : Type u) [CommRing O] (c : S.C2 χ O) (u v w : R) : O

The Hochschild coboundary of a two-cochain, in coefficients (four terms).

theorem MultiplicativeBasisDeformations.RaySys.Sys.w3_of_left {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {u v w t t₁ : R} (ht : S.w2 χ v w = some t) (h : S.P.mul u t = some t₁) : S.w3 χ u v w = some t₁

theorem MultiplicativeBasisDeformations.RaySys.Sys.w3_of_mulL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {u v w t t₁ : R} (ht : S.P.mul u v = some t) (h : S.w2 χ t w = some t₁) : S.w3 χ u v w = some t₁

theorem MultiplicativeBasisDeformations.RaySys.Sys.w3_of_mulR {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {u v w t t₁ : R} (ht : S.P.mul v w = some t) (h : S.w2 χ u t = some t₁) : S.w3 χ u v w = some t₁

theorem MultiplicativeBasisDeformations.RaySys.Sys.w3_of_right {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {u v w t t₁ : R} (ht : S.w2 χ u v = some t) (h : S.P.mul t w = some t₁) : S.w3 χ u v w = some t₁

theorem MultiplicativeBasisDeformations.RaySys.Sys.I2_isSome {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) {p : R × R} (h : S.I2 χ p) : ∃ (t : R), S.w2 χ p.1 p.2 = some t

theorem MultiplicativeBasisDeformations.RaySys.Sys.hoch_b {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (O : Type u) [CommRing O] [Nontrivial O] (c : S.C2 χ O) (u v w : R) : S.P.b O u * ((S.Φ2 χ O c) (S.P.b O v)) (S.P.b O w) - ((S.Φ2 χ O c) (S.P.b O u * S.P.b O v)) (S.P.b O w) + ((S.Φ2 χ O c) (S.P.b O u)) (S.P.b O v * S.P.b O w) - ((S.Φ2 χ O c) (S.P.b O u)) (S.P.b O v) * S.P.b O w = S.d2raw χ O c u v w • S.vecW O (S.w3 χ u v w)

The Hochschild coboundary of Φ₂ c on basis triples.

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

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

theorem MultiplicativeBasisDeformations.RaySys.Sys.isHCocycle_Φ2_iff {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (O : Type u) [CommRing O] [Nontrivial O] (c : S.C2 χ O) : GExt.IsHCocycle (S.Φ2 χ O c) ↔ ∀ (u v w : R), (S.w3 χ u v w).isSome = true → S.d2raw χ O c u v w = 0

The cocycle condition in coefficients.

Naturality in the coefficients

theorem MultiplicativeBasisDeformations.RaySys.Sys.d1_map {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (O : Type u) [CommRing O] [Nontrivial O] {O' : Type u'} [CommRing O'] [Nontrivial O'] (φ : O →+ O') (f : S.C1 χ O) : S.d1 χ O' (⇑φ ∘ f) = ⇑φ ∘ S.d1 χ O f

d₁ commutes with additive maps of coefficients.

theorem MultiplicativeBasisDeformations.RaySys.Sys.d2raw_map {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (O : Type u) [CommRing O] [Nontrivial O] {O' : Type u'} [CommRing O'] [Nontrivial O'] (φ : O →+ O') (c : S.C2 χ O) (u v w : R) : S.d2raw χ O' (⇑φ ∘ c) u v w = φ (S.d2raw χ O c u v w)

The cocycle formula commutes with additive maps of coefficients.

theorem MultiplicativeBasisDeformations.RaySys.Sys.d1_add {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (O : Type u) [CommRing O] [Nontrivial O] (f g : S.C1 χ O) : S.d1 χ O (f + g) = S.d1 χ O f + S.d1 χ O g

theorem MultiplicativeBasisDeformations.RaySys.Sys.d1_smul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (O : Type u) [CommRing O] [Nontrivial O] (a : O) (f : S.C1 χ O) : S.d1 χ O (a • f) = a • S.d1 χ O f

theorem MultiplicativeBasisDeformations.RaySys.Sys.d1_sum {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (O : Type u) [CommRing O] [Nontrivial O] {ι : Type u_1} (s : Finset ι) (f : ι → S.C1 χ O) : S.d1 χ O (∑ i ∈ s, f i) = ∑ i ∈ s, S.d1 χ O (f i)

theorem MultiplicativeBasisDeformations.RaySys.Sys.d2raw_add {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (O : Type u) [CommRing O] [Nontrivial O] (c c' : S.C2 χ O) (u v w : R) : S.d2raw χ O (c + c') u v w = S.d2raw χ O c u v w + S.d2raw χ O c' u v w

theorem MultiplicativeBasisDeformations.RaySys.Sys.d2raw_smul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (O : Type u) [CommRing O] [Nontrivial O] (a : O) (c : S.C2 χ O) (u v w : R) : S.d2raw χ O (a • c) u v w = a * S.d2raw χ O c u v w