Normalized relative Hochschild cochains

For a length-graded algebra Λ with vertex idempotents e_i spanning S = Λ₀: normalized S-relative one- and two-cochains of internal degree q, the coboundary df(a,b) = af(b) - f(ab) + f(a)b (characteristic-two-construction.tex) and the cocycle equation dμ(a,b,c) = aμ(b,c) - μ(ab,c) + μ(a,bc) - μ(a,b)c = 0 (binary-families.tex). Classes in HH²(Λ)_q are cocycles of degree q modulo coboundaries of degree-q one-cochains.

Also: a degree calculus for maps raising the length grading (Raises₁, Raises₂) used by the normalization arguments.

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

A normalized S-relative one-cochain.

• left (i : Fin V.n) (a : Λ) : f (V.e i * a) = V.e i * f a
• right (i : Fin V.n) (a : Λ) : f (a * V.e i) = f a * V.e i
• unit (i : Fin V.n) : f (V.e i) = 0

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

A normalized S-relative two-cochain.

• left (i : Fin V.n) (a b : Λ) : (μ (V.e i * a)) b = V.e i * (μ a) b
• mid (i : Fin V.n) (a b : Λ) : (μ (a * V.e i)) b = (μ a) (V.e i * b)
• right (i : Fin V.n) (a b : Λ) : (μ a) (b * V.e i) = (μ a) b * V.e i
• unitL (i : Fin V.n) (b : Λ) : (μ (V.e i)) b = 0
• unitR (i : Fin V.n) (a : Λ) : (μ a) (V.e i) = 0

def MultiplicativeBasisDeformations.LenGrading.HasDeg₁ {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (G : LenGrading k Λ) (q : ℕ) (f : Λ →ₗ[k] Λ) : Prop

A one-cochain of internal degree q.

def MultiplicativeBasisDeformations.LenGrading.HasDeg₂ {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (G : LenGrading k Λ) (q : ℕ) (μ : Λ →ₗ[k] Λ →ₗ[k] Λ) : Prop

A two-cochain of internal degree q.

def MultiplicativeBasisDeformations.LenGrading.IsCocycle₂ {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (μ : Λ →ₗ[k] Λ →ₗ[k] Λ) : Prop

The Hochschild cocycle equation.

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

The coboundary df(a,b) = a f(b) - f(ab) + f(a) b.

theorem MultiplicativeBasisDeformations.LenGrading.cobdry_apply {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (f : Λ →ₗ[k] Λ) (a b : Λ) : ((cobdry k f) a) b = a * f b - f (a * b) + f a * b

Degree calculus

def MultiplicativeBasisDeformations.LenGrading.Raises₁ {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (G : LenGrading k Λ) (q : ℕ) (f : Λ →ₗ[k] Λ) : Prop

A one-cochain raising degree by at least q.

def MultiplicativeBasisDeformations.LenGrading.Raises₂ {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (G : LenGrading k Λ) (q : ℕ) (μ : Λ →ₗ[k] Λ →ₗ[k] Λ) : Prop

A two-cochain raising total degree by at least q.

theorem MultiplicativeBasisDeformations.LenGrading.ge_sum {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {m : ℕ} {ι : Type u_1} (s : Finset ι) (f : ι → Λ) (h : ∀ i ∈ s, G.Ge m (f i)) : G.Ge m (∑ i ∈ s, f i)

theorem MultiplicativeBasisDeformations.LenGrading.ge_neg {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {m : ℕ} {a : Λ} (ha : G.Ge m a) : G.Ge m (-a)

theorem MultiplicativeBasisDeformations.LenGrading.ge_sub {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {m : ℕ} {a b : Λ} (ha : G.Ge m a) (hb : G.Ge m b) : G.Ge m (a - b)

theorem MultiplicativeBasisDeformations.LenGrading.ge_zero' {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (m : ℕ) : G.Ge m 0

theorem MultiplicativeBasisDeformations.LenGrading.Raises₁.ge {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {q : ℕ} {f : Λ →ₗ[k] Λ} (hf : G.Raises₁ q f) {d : ℕ} {a : Λ} (ha : G.Ge d a) : G.Ge (d + q) (f a)

theorem MultiplicativeBasisDeformations.LenGrading.Raises₂.ge {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {q : ℕ} {μ : Λ →ₗ[k] Λ →ₗ[k] Λ} (hμ : G.Raises₂ q μ) {d e : ℕ} {a b : Λ} (ha : G.Ge d a) (hb : G.Ge e b) : G.Ge (d + e + q) ((μ a) b)

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

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

theorem MultiplicativeBasisDeformations.LenGrading.Raises₂.mono {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {q q' : ℕ} {μ : Λ →ₗ[k] Λ →ₗ[k] Λ} (hμ : G.Raises₂ q μ) (h : q' ≤ q) : G.Raises₂ q' μ

theorem MultiplicativeBasisDeformations.LenGrading.raises_mul {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} : G.Raises₂ 0 (LinearMap.mul k Λ)

theorem MultiplicativeBasisDeformations.LenGrading.eq_zero_of_raises {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {q : ℕ} {μ : Λ →ₗ[k] Λ →ₗ[k] Λ} (hμ : G.Raises₂ q μ) (hq : G.N ≤ q) (a b : Λ) : (μ a) b = 0

A bilinear map vanishing in degrees < d + e + q on homogeneous inputs of large degree is zero.

def MultiplicativeBasisDeformations.LenGrading.degPart {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (q : ℕ) (μ : Λ →ₗ[k] Λ →ₗ[k] Λ) : Λ →ₗ[k] Λ →ₗ[k] Λ

The degree-(d+e+q) component of μ on homogeneous inputs.

theorem MultiplicativeBasisDeformations.LenGrading.degPart_hom {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {q d e : ℕ} (μ : Λ →ₗ[k] Λ →ₗ[k] Λ) {a b : Λ} (ha : G.IsHom d a) (hb : G.IsHom e b) : ((degPart q μ) a) b = (G.proj (d + e + q)) ((μ a) b)

theorem MultiplicativeBasisDeformations.LenGrading.degPart_hasDeg {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (q : ℕ) (μ : Λ →ₗ[k] Λ →ₗ[k] Λ) : G.HasDeg₂ q (degPart q μ)

theorem MultiplicativeBasisDeformations.LenGrading.sub_degPart {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {q : ℕ} {μ : Λ →ₗ[k] Λ →ₗ[k] Λ} (hμ : G.Raises₂ q μ) : G.Raises₂ (q + 1) (μ - degPart q μ)