The bar cochain complex

The normalized relative bar complexes of Section 6 (positive-deformations.tex, module bar complex) and Section 7 (Hochschild complex) are both cochains f(a_1, …, a_n) with values in a bimodule X and differential `df(a_1, …, a_{n+1}) = a_1 f(a_2, …) + Σ (-1)^i f(…, a_i a_{i+1}, …)

• (-1)^{n+1} f(a_1, …, a_n) a_{n+1}. For a right module bar complex Hom(M ⊗ Λ̄^{⊗n}, N)takeX = Hom_k(M, N)with `(a·φ)(m) = φ(ma), (φ·b)(m) = φ(m)b`.

Cochains are encoded as functions of sequences ℕ → Λ (only the first n entries matter for the cochains used later); the coface maps then satisfy the cosimplicial identities as identities of sequence operations (coface_comm), and d ∘ d = 0 (d_d) follows by the usual pairing of terms.

structure MultiplicativeBasisDeformations.Bar.Act (Λ : Type u_1) [Ring Λ] (X : Type u_2) [AddCommGroup X] : Type (max u_1 u_2)

Bimodule actions on X: l a x = a·x, r b x = x·b.

• l : Λ → X →+ X
• r : Λ → X →+ X
• l_mul (a b : Λ) (x : X) : (self.l (a * b)) x = (self.l a) ((self.l b) x)
• r_mul (a b : Λ) (x : X) : (self.r b) ((self.r a) x) = (self.r (a * b)) x
• lr (a b : Λ) (x : X) : (self.l a) ((self.r b) x) = (self.r b) ((self.l a) x)

def MultiplicativeBasisDeformations.Bar.sh {Λ : Type u_1} (a : ℕ → Λ) : ℕ → Λ

Shift a sequence.

def MultiplicativeBasisDeformations.Bar.ct {Λ : Type u_1} [Ring Λ] (p : ℕ) (a : ℕ → Λ) : ℕ → Λ

Multiply the entries p, p+1.

def MultiplicativeBasisDeformations.Bar.tr {Λ : Type u_1} [Ring Λ] (n : ℕ) (a : ℕ → Λ) : ℕ → Λ

Truncate after n entries.

theorem MultiplicativeBasisDeformations.Bar.sh_ct_zero {Λ : Type u_1} [Ring Λ] (a : ℕ → Λ) : sh (ct 0 a) = sh (sh a)

theorem MultiplicativeBasisDeformations.Bar.sh_ct {Λ : Type u_1} [Ring Λ] {j : ℕ} (hj : 1 ≤ j) (a : ℕ → Λ) : sh (ct j a) = ct (j - 1) (sh a)

theorem MultiplicativeBasisDeformations.Bar.ct_zero_apply {Λ : Type u_1} [Ring Λ] {j : ℕ} (hj : 1 ≤ j) (a : ℕ → Λ) : ct j a 0 = a 0

theorem MultiplicativeBasisDeformations.Bar.sh_tr {Λ : Type u_1} [Ring Λ] (n : ℕ) (a : ℕ → Λ) : sh (tr (n + 1) a) = tr n (sh a)

theorem MultiplicativeBasisDeformations.Bar.ct_ct {Λ : Type u_1} [Ring Λ] {p j : ℕ} (h : p < j) (a : ℕ → Λ) : ct p (ct j a) = ct (j - 1) (ct p a)

theorem MultiplicativeBasisDeformations.Bar.ct_tr {Λ : Type u_1} [Ring Λ] {p n : ℕ} (h : p < n) (a : ℕ → Λ) : ct p (tr (n + 1) a) = tr n (ct p a)

theorem MultiplicativeBasisDeformations.Bar.tr_tr {Λ : Type u_1} [Ring Λ] (n : ℕ) (a : ℕ → Λ) : tr n (tr (n + 1) a) = tr n a

theorem MultiplicativeBasisDeformations.Bar.tr_ct {Λ : Type u_1} [Ring Λ] (n : ℕ) (a : ℕ → Λ) : tr n (ct n a) = tr n a

theorem MultiplicativeBasisDeformations.Bar.ct_apply_of_lt {Λ : Type u_1} [Ring Λ] {p n : ℕ} (h : p < n) (a : ℕ → Λ) : ct p a n = a (n + 1)

theorem MultiplicativeBasisDeformations.Bar.ct_apply_self {Λ : Type u_1} [Ring Λ] (n : ℕ) (a : ℕ → Λ) : ct n a n = a n * a (n + 1)

theorem MultiplicativeBasisDeformations.Bar.tr_apply_lt {Λ : Type u_1} [Ring Λ] {n k : ℕ} (h : k < n) (a : ℕ → Λ) : tr n a k = a k

Sequence operations and updates

theorem MultiplicativeBasisDeformations.Bar.sh_update_succ {Λ : Type u_1} [Ring Λ] (a : ℕ → Λ) (i : ℕ) (x : Λ) : sh (Function.update a (i + 1) x) = Function.update (sh a) i x

theorem MultiplicativeBasisDeformations.Bar.sh_update_zero {Λ : Type u_1} [Ring Λ] (a : ℕ → Λ) (x : Λ) : sh (Function.update a 0 x) = sh a

theorem MultiplicativeBasisDeformations.Bar.ct_update_lt {Λ : Type u_1} [Ring Λ] {p i : ℕ} (h : i < p) (a : ℕ → Λ) (x : Λ) : ct p (Function.update a i x) = Function.update (ct p a) i x

theorem MultiplicativeBasisDeformations.Bar.ct_update_gt {Λ : Type u_1} [Ring Λ] {p i : ℕ} (h : p + 1 < i) (a : ℕ → Λ) (x : Λ) : ct p (Function.update a i x) = Function.update (ct p a) (i - 1) x

theorem MultiplicativeBasisDeformations.Bar.ct_update_left {Λ : Type u_1} [Ring Λ] (p : ℕ) (a : ℕ → Λ) (x : Λ) : ct p (Function.update a p x) = Function.update (ct p a) p (x * a (p + 1))

theorem MultiplicativeBasisDeformations.Bar.ct_update_right {Λ : Type u_1} [Ring Λ] (p : ℕ) (a : ℕ → Λ) (x : Λ) : ct p (Function.update a (p + 1) x) = Function.update (ct p a) p (a p * x)

theorem MultiplicativeBasisDeformations.Bar.tr_update_lt {Λ : Type u_1} [Ring Λ] {n i : ℕ} (h : i < n) (a : ℕ → Λ) (x : Λ) : tr n (Function.update a i x) = Function.update (tr n a) i x

theorem MultiplicativeBasisDeformations.Bar.tr_update_ge {Λ : Type u_1} [Ring Λ] {n i : ℕ} (h : n ≤ i) (a : ℕ → Λ) (x : Λ) : tr n (Function.update a i x) = tr n a

def MultiplicativeBasisDeformations.Bar.cons {Λ : Type u_1} (x : Λ) (a : ℕ → Λ) : ℕ → Λ

Prepend an entry.

theorem MultiplicativeBasisDeformations.Bar.cons_zero {Λ : Type u_1} [Ring Λ] (x : Λ) (a : ℕ → Λ) : cons x a 0 = x

theorem MultiplicativeBasisDeformations.Bar.sh_cons {Λ : Type u_1} [Ring Λ] (x : Λ) (a : ℕ → Λ) : sh (cons x a) = a

theorem MultiplicativeBasisDeformations.Bar.ct_zero_cons {Λ : Type u_1} [Ring Λ] (x : Λ) (a : ℕ → Λ) : ct 0 (cons x a) = cons (x * a 0) (sh a)

theorem MultiplicativeBasisDeformations.Bar.ct_succ_cons {Λ : Type u_1} [Ring Λ] (p : ℕ) (x : Λ) (a : ℕ → Λ) : ct (p + 1) (cons x a) = cons x (ct p a)

theorem MultiplicativeBasisDeformations.Bar.tr_cons {Λ : Type u_1} [Ring Λ] (n : ℕ) (x : Λ) (a : ℕ → Λ) : tr (n + 1) (cons x a) = cons x (tr n a)

theorem MultiplicativeBasisDeformations.Bar.cons_succ {Λ : Type u_1} [Ring Λ] (x : Λ) (a : ℕ → Λ) (k : ℕ) : cons x a (k + 1) = a k

theorem MultiplicativeBasisDeformations.Bar.update_cons_succ {Λ : Type u_1} [Ring Λ] (x : Λ) (a : ℕ → Λ) (i : ℕ) (y : Λ) : Function.update (cons x a) (i + 1) y = cons x (Function.update a i y)

theorem MultiplicativeBasisDeformations.Bar.update_cons_zero {Λ : Type u_1} [Ring Λ] (x : Λ) (a : ℕ → Λ) (y : Λ) : Function.update (cons x a) 0 y = cons y a

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.Bar.Cochain (Λ : Type u_1) (X : Type u_2) : Type (max u_1 u_2)

Cochains: functions of sequences.

def MultiplicativeBasisDeformations.Bar.coface {Λ : Type u_1} [Ring Λ] {X : Type u_2} [AddCommGroup X] (A : Act Λ X) (n i : ℕ) : Cochain Λ X →+ Cochain Λ X

The coface maps δ_i : Cⁿ → Cⁿ⁺¹.

theorem MultiplicativeBasisDeformations.Bar.coface_zero {Λ : Type u_1} [Ring Λ] {X : Type u_2} [AddCommGroup X] (A : Act Λ X) (n : ℕ) (F : Cochain Λ X) (a : ℕ → Λ) : (coface A n 0) F a = (A.l (a 0)) (F (sh a))

theorem MultiplicativeBasisDeformations.Bar.coface_mid {Λ : Type u_1} [Ring Λ] {X : Type u_2} [AddCommGroup X] (A : Act Λ X) {n i : ℕ} (h1 : 1 ≤ i) (h2 : i ≤ n) (F : Cochain Λ X) (a : ℕ → Λ) : (coface A n i) F a = F (ct (i - 1) a)

theorem MultiplicativeBasisDeformations.Bar.coface_last {Λ : Type u_1} [Ring Λ] {X : Type u_2} [AddCommGroup X] (A : Act Λ X) (n : ℕ) (F : Cochain Λ X) (a : ℕ → Λ) : (coface A n (n + 1)) F a = (A.r (a n)) (F (tr n a))

theorem MultiplicativeBasisDeformations.Bar.coface_comm {Λ : Type u_1} [Ring Λ] {X : Type u_2} [AddCommGroup X] (A : Act Λ X) {n i j : ℕ} (hij : i ≤ j) (hj : j ≤ n + 1) (F : Cochain Λ X) : (coface A (n + 1) (j + 1)) ((coface A n i) F) = (coface A (n + 1) i) ((coface A n j) F)

The cosimplicial identities δ_{j+1} δ_i = δ_i δ_j for i ≤ j.

def MultiplicativeBasisDeformations.Bar.d {Λ : Type u_1} [Ring Λ] {X : Type u_2} [AddCommGroup X] (A : Act Λ X) (n : ℕ) : Cochain Λ X →+ Cochain Λ X

The differential d = Σ (-1)^i δ_i.

theorem MultiplicativeBasisDeformations.Bar.d_apply {Λ : Type u_1} [Ring Λ] {X : Type u_2} [AddCommGroup X] (A : Act Λ X) (n : ℕ) (F : Cochain Λ X) : (d A n) F = ∑ i ∈ Finset.range (n + 2), (-1) ^ i • (coface A n i) F

theorem MultiplicativeBasisDeformations.Bar.d_d {Λ : Type u_1} [Ring Λ] {X : Type u_2} [AddCommGroup X] (A : Act Λ X) (n : ℕ) (F : Cochain Λ X) : (d A (n + 1)) ((d A n) F) = 0

d ∘ d = 0.

Low degrees

theorem MultiplicativeBasisDeformations.Bar.d_zero_apply {Λ : Type u_1} [Ring Λ] {X : Type u_2} [AddCommGroup X] (A : Act Λ X) (F : Cochain Λ X) (a : ℕ → Λ) : (d A 0) F a = (A.l (a 0)) (F (sh a)) - (A.r (a 0)) (F (tr 0 a))

theorem MultiplicativeBasisDeformations.Bar.d_one_apply {Λ : Type u_1} [Ring Λ] {X : Type u_2} [AddCommGroup X] (A : Act Λ X) (F : Cochain Λ X) (a : ℕ → Λ) : (d A 1) F a = (A.l (a 0)) (F (sh a)) - F (ct 0 a) + (A.r (a 1)) (F (tr 1 a))

theorem MultiplicativeBasisDeformations.Bar.d_two_apply {Λ : Type u_1} [Ring Λ] {X : Type u_2} [AddCommGroup X] (A : Act Λ X) (F : Cochain Λ X) (a : ℕ → Λ) : (d A 2) F a = (A.l (a 0)) (F (sh a)) - F (ct 0 a) + F (ct 1 a) - (A.r (a 2)) (F (tr 2 a))