Relative cochains compute ordinary Hochschild cohomology in degree two

weights-and-parameters.tex: "we use normalized cochains relative to the split vertex algebra […] these relative cochains compute ordinary Hochschild cohomology." The formalization works with normalized S-relative cochains (IsRel₁, IsRel₂). This file proves the claim for HH²(Λ)_q, the only Hochschild group the paper uses:

• every Hochschild two-cocycle of internal degree q is cohomologous, by a degree-q coboundary, to a normalized S-relative one (exists_rel_cohomologous);
• a normalized S-relative two-cochain that is the coboundary of some degree-q one-cochain is the coboundary of a normalized S-relative one (exists_rel_of_cobdry).

So the relative classes are exactly the ordinary classes. In particular the spanning condition on HH²(Λ)_{>0} (Theorem 7.7, Proposition 7.6) reads the same in both forms (span_rel_iff; the hypotheses of Theorem 7.7 in the ordinary form give FamilyHyp, familyHyp_of_ordinary), and so does the nonvanishing of a class (rel_isCobdry_iff).

Small lemmas

theorem MultiplicativeBasisDeformations.LenGrading.isHom_add' {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {d : ℕ} {a b : Λ} (ha : G.IsHom d a) (hb : G.IsHom d b) : G.IsHom d (a + b)

theorem MultiplicativeBasisDeformations.LenGrading.isHom_sub' {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {d : ℕ} {a b : Λ} (ha : G.IsHom d a) (hb : G.IsHom d b) : G.IsHom d (a - b)

theorem MultiplicativeBasisDeformations.LenGrading.isHom_smul' {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {d : ℕ} (c : k) {a : Λ} (ha : G.IsHom d a) : G.IsHom d (c • a)

theorem MultiplicativeBasisDeformations.LenGrading.isCocycle_cobdry {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (f : Λ →ₗ[k] Λ) : IsCocycle₂ (cobdry k f)

theorem MultiplicativeBasisDeformations.LenGrading.isCocycle_sub {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {μ ν : Λ →ₗ[k] Λ →ₗ[k] Λ} (hμ : IsCocycle₂ μ) (hν : IsCocycle₂ ν) : IsCocycle₂ (μ - ν)

theorem MultiplicativeBasisDeformations.LenGrading.cobdry_add' {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (f g : Λ →ₗ[k] Λ) : cobdry k (f + g) = cobdry k f + cobdry k g

theorem MultiplicativeBasisDeformations.LenGrading.cobdry_sub' {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (f g : Λ →ₗ[k] Λ) : cobdry k (f - g) = cobdry k f - cobdry k g

theorem MultiplicativeBasisDeformations.LenGrading.hasDeg₂_cobdry {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {q : ℕ} {f : Λ →ₗ[k] Λ} (hf : G.HasDeg₁ q f) : G.HasDeg₂ q (cobdry k f)

theorem MultiplicativeBasisDeformations.LenGrading.hasDeg₂_sub {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {q : ℕ} {μ ν : Λ →ₗ[k] Λ →ₗ[k] Λ} (hμ : G.HasDeg₂ q μ) (hν : G.HasDeg₂ q ν) : G.HasDeg₂ q (μ - ν)

theorem MultiplicativeBasisDeformations.LenGrading.hasDeg₁_add {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {q : ℕ} {f g : Λ →ₗ[k] Λ} (hf : G.HasDeg₁ q f) (hg : G.HasDeg₁ q g) : G.HasDeg₁ q (f + g)

theorem MultiplicativeBasisDeformations.LenGrading.hasDeg₁_sub {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {q : ℕ} {f g : Λ →ₗ[k] Λ} (hf : G.HasDeg₁ q f) (hg : G.HasDeg₁ q g) : G.HasDeg₁ q (f - g)

theorem MultiplicativeBasisDeformations.LenGrading.ee {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) (i j : Fin V.n) : V.e i * V.e j = if i = j then V.e i else 0

theorem MultiplicativeBasisDeformations.LenGrading.sum_e_mul {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) (x : Λ) : ∑ i : Fin V.n, V.e i * x = x

theorem MultiplicativeBasisDeformations.LenGrading.sum_mul_e {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) (x : Λ) : ∑ i : Fin V.n, x * V.e i = x

theorem MultiplicativeBasisDeformations.LenGrading.isRel₂_of_unit {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) {μ : Λ →ₗ[k] Λ →ₗ[k] Λ} (hμ : IsCocycle₂ μ) (hL : ∀ (i : Fin V.n) (b : Λ), (μ (V.e i)) b = 0) (hR : ∀ (i : Fin V.n) (a : Λ), (μ a) (V.e i) = 0) : IsRel₂ V μ

A cocycle vanishing when either argument is a vertex is normalized S-relative.

Cocycles

def MultiplicativeBasisDeformations.LenGrading.f₁ {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) (μ : Λ →ₗ[k] Λ →ₗ[k] Λ) : Λ →ₗ[k] Λ

f₁(a) = Σ_i e_i μ(e_i, a).

theorem MultiplicativeBasisDeformations.LenGrading.f₁_apply {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) (μ : Λ →ₗ[k] Λ →ₗ[k] Λ) (a : Λ) : (f₁ V μ) a = ∑ i : Fin V.n, V.e i * (μ (V.e i)) a

def MultiplicativeBasisDeformations.LenGrading.f₂ {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) (μ : Λ →ₗ[k] Λ →ₗ[k] Λ) : Λ →ₗ[k] Λ

f₂(a) = Σ_i μ(a, e_i) e_i.

theorem MultiplicativeBasisDeformations.LenGrading.f₂_apply {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) (μ : Λ →ₗ[k] Λ →ₗ[k] Λ) (a : Λ) : (f₂ V μ) a = ∑ i : Fin V.n, (μ a) (V.e i) * V.e i

theorem MultiplicativeBasisDeformations.LenGrading.left_unit {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) {μ : Λ →ₗ[k] Λ →ₗ[k] Λ} (hμ : IsCocycle₂ μ) (j : Fin V.n) (b : Λ) : ((μ - cobdry k (f₁ V μ)) (V.e j)) b = 0

After subtracting d f₁, a cocycle vanishes when its first argument is a vertex.

theorem MultiplicativeBasisDeformations.LenGrading.right_unit {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) {μ : Λ →ₗ[k] Λ →ₗ[k] Λ} (hμ : IsCocycle₂ μ) (hL : ∀ (i : Fin V.n) (b : Λ), (μ (V.e i)) b = 0) : (∀ (i : Fin V.n) (b : Λ), ((μ - cobdry k (f₂ V μ)) (V.e i)) b = 0) ∧ ∀ (j : Fin V.n) (a : Λ), ((μ - cobdry k (f₂ V μ)) a) (V.e j) = 0

After subtracting d f₂, a cocycle that vanishes at a left vertex also vanishes at a right vertex, and still at a left vertex.

theorem MultiplicativeBasisDeformations.LenGrading.exists_rel_cohomologous {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) {q : ℕ} {μ : Λ →ₗ[k] Λ →ₗ[k] Λ} (hμ : IsCocycle₂ μ) (hd : G.HasDeg₂ q μ) : ∃ (f : Λ →ₗ[k] Λ), G.HasDeg₁ q f ∧ IsRel₂ V (μ - cobdry k f)

Every Hochschild two-cocycle of internal degree q is cohomologous to a normalized S-relative one, by the coboundary of a degree-q one-cochain.

Coboundaries

theorem MultiplicativeBasisDeformations.LenGrading.exists_rel_of_cobdry {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) {q : ℕ} {ν : Λ →ₗ[k] Λ →ₗ[k] Λ} (hν : IsRel₂ V ν) {f : Λ →ₗ[k] Λ} (hf : G.HasDeg₁ q f) (hνf : ν = cobdry k f) : ∃ (f' : Λ →ₗ[k] Λ), IsRel₁ V f' ∧ G.HasDeg₁ q f' ∧ ν = cobdry k f'

A normalized S-relative coboundary is the coboundary of a normalized S-relative one-cochain of the same degree.

Consequences

theorem MultiplicativeBasisDeformations.LenGrading.IsRel₂.sub' {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) {μ ν : Λ →ₗ[k] Λ →ₗ[k] Λ} (hμ : IsRel₂ V μ) (hν : IsRel₂ V ν) : IsRel₂ V (μ - ν)

theorem MultiplicativeBasisDeformations.LenGrading.IsRel₂.zero' {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) : IsRel₂ V 0

theorem MultiplicativeBasisDeformations.LenGrading.IsRel₂.add' {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) {μ ν : Λ →ₗ[k] Λ →ₗ[k] Λ} (hμ : IsRel₂ V μ) (hν : IsRel₂ V ν) : IsRel₂ V (μ + ν)

theorem MultiplicativeBasisDeformations.LenGrading.IsRel₂.smul' {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) (c : k) {μ : Λ →ₗ[k] Λ →ₗ[k] Λ} (hμ : IsRel₂ V μ) : IsRel₂ V (c • μ)

theorem MultiplicativeBasisDeformations.LenGrading.IsRel₂.sum' {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) {ι : Type u_1} (s : Finset ι) (μ : ι → Λ →ₗ[k] Λ →ₗ[k] Λ) (h : ∀ i ∈ s, IsRel₂ V (μ i)) : IsRel₂ V (∑ i ∈ s, μ i)

theorem MultiplicativeBasisDeformations.LenGrading.rel_isCobdry_iff {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) {q : ℕ} {ν : Λ →ₗ[k] Λ →ₗ[k] Λ} (hν : IsRel₂ V ν) : (∃ (f : Λ →ₗ[k] Λ), IsRel₁ V f ∧ G.HasDeg₁ q f ∧ ν = cobdry k f) ↔ ∃ (f : Λ →ₗ[k] Λ), G.HasDeg₁ q f ∧ ν = cobdry k f

A normalized S-relative two-cochain is a relative coboundary iff it is an ordinary coboundary (in internal degree q): the nonvanishing of a class reads the same in both forms.

theorem MultiplicativeBasisDeformations.LenGrading.span_rel_iff {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) {n : ℕ} (μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ) (qd : Fin n → ℕ) (hμ : ∀ (i : Fin n), IsRel₂ V (μ i)) (q : ℕ) : (∀ (φ : Λ →ₗ[k] Λ →ₗ[k] Λ), IsRel₂ V φ → G.HasDeg₂ q φ → IsCocycle₂ φ → ∃ (c : Fin n → k) (f : Λ →ₗ[k] Λ), IsRel₁ V f ∧ G.HasDeg₁ q f ∧ φ = ∑ i : Fin n with qd i = q, c i • μ i + cobdry k f) ↔ ∀ (φ : Λ →ₗ[k] Λ →ₗ[k] Λ), G.HasDeg₂ q φ → IsCocycle₂ φ → ∃ (c : Fin n → k) (f : Λ →ₗ[k] Λ), G.HasDeg₁ q f ∧ φ = ∑ i : Fin n with qd i = q, c i • μ i + cobdry k f

The spanning condition on HH²(Λ)_q reads the same with relative and with ordinary cochains, for normalized S-relative μ_i.

theorem MultiplicativeBasisDeformations.LenGrading.familyHyp_of_ordinary {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) {n : ℕ} {μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ} {qd : Fin n → ℕ} (pos : ∀ (i : Fin n), 0 < qd i) (rel : ∀ (i : Fin n), IsRel₂ V (μ i)) (deg : ∀ (i : Fin n), G.HasDeg₂ (qd i) (μ i)) (assoc : ∀ (lam : Fin n → k) (a b c : Λ), ((mLam μ lam) (((mLam μ lam) a) b)) c = ((mLam μ lam) a) (((mLam μ lam) b) c)) (span : ∀ (q : ℕ), 0 < q → ∀ (φ : Λ →ₗ[k] Λ →ₗ[k] Λ), G.HasDeg₂ q φ → IsCocycle₂ φ → ∃ (c : Fin n → k) (f : Λ →ₗ[k] Λ), G.HasDeg₁ q f ∧ φ = ∑ i : Fin n with qd i = q, c i • μ i + cobdry k f) : FamilyHyp V μ qd

The hypotheses of Theorem 7.7 with HH² as ordinary Hochschild cohomology: if the μ_i are normalized S-relative of positive degrees, m + Σ t_i μ_i is associative, and their classes span the ordinary HH²(Λ)_q for every q > 0, then FamilyHyp holds.