Character decomposition of Hochschild cochains #
weights-and-parameters.tex: "Integer ray weights also grade A₀ and its
Hochschild complex, and we write HH²(A₀)_χ for the component of weight χ ∈ L. Since
deg_J ∈ H_ℤ, this decomposition refines the decomposition by internal degree."
For an algebra Λ with a length grading G, vertex idempotents of weight zero and a
compatible lattice grading W: the character-χ part cpr2 χ φ of a two-cochain is a
cochain of character χ; it is a cocycle, relative, of the same internal degree when
φ is, and φ is the finite sum of its character parts (sum_cpr2). The coboundary
commutes with the character parts (cobdry_cpr1).
Also (exists_rel_cobdry): "Inserting the primitive idempotents contracts the
complementary summands of the bar complex, so these relative cochains compute ordinary
Hochschild cohomology" (weights-and-parameters.tex), in the form used: a
normalized relative cocycle which is the coboundary of some one-cochain of degree q is
the coboundary of a normalized relative one-cochain of degree q. The correction is the
inner derivation of u = ∑ f(e_j) e_j.
theorem
MultiplicativeBasisDeformations.LatGrading.isHom_zero
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
(l : L)
:
W.IsHom l 0
theorem
MultiplicativeBasisDeformations.LatGrading.isHom_add
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
{l : L}
{x y : Λ}
(hx : W.IsHom l x)
(hy : W.IsHom l y)
:
W.IsHom l (x + y)
theorem
MultiplicativeBasisDeformations.LatGrading.isHom_smul
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
{l : L}
(c : k)
{x : Λ}
(hx : W.IsHom l x)
:
W.IsHom l (c • x)
theorem
MultiplicativeBasisDeformations.LatGrading.isHom_sub
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
{l : L}
{x y : Λ}
(hx : W.IsHom l x)
(hy : W.IsHom l y)
:
W.IsHom l (x - y)
theorem
MultiplicativeBasisDeformations.LatGrading.isHom_sum
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
{l : L}
{ι : Type u_1}
(s : Finset ι)
(f : ι → Λ)
(h : ∀ i ∈ s, W.IsHom l (f i))
:
W.IsHom l (∑ i ∈ s, f i)
theorem
MultiplicativeBasisDeformations.LatGrading.eq_zero_of_isHom_out
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
{l : L}
{x : Λ}
(hx : W.IsHom l x)
(hl : l ∉ W.supp)
:
x = 0
theorem
MultiplicativeBasisDeformations.LatGrading.map_eq_sum
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
{N : Type u_1}
[AddCommGroup N]
(f : Λ →+ N)
(x : Λ)
:
Additive maps commute with the weight decomposition.
theorem
MultiplicativeBasisDeformations.LatGrading.proj_mul_left
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
{l : L}
{x : Λ}
(hx : W.IsHom l x)
(l' : L)
(y : Λ)
:
theorem
MultiplicativeBasisDeformations.LatGrading.proj_mul_right
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
{l : L}
{y : Λ}
(hy : W.IsHom l y)
(l' : L)
(x : Λ)
:
theorem
MultiplicativeBasisDeformations.LatGrading.ext_of_hom
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
{N : Type u_1}
[AddCommGroup N]
[Module k N]
{f f' : Λ →ₗ[k] N}
(h : ∀ (l : L) (x : Λ), W.IsHom l x → f x = f' x)
:
f = f'
Linear maps agreeing on homogeneous elements agree.
theorem
MultiplicativeBasisDeformations.LatGrading.eq_zero_of_hom3
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
{N : Type u_1}
[AddCommGroup N]
(E : Λ → Λ → Λ → N)
(h1 : ∀ (a a' b c : Λ), E (a + a') b c = E a b c + E a' b c)
(h2 : ∀ (a b b' c : Λ), E a (b + b') c = E a b c + E a b' c)
(h3 : ∀ (a b c c' : Λ), E a b (c + c') = E a b c + E a b c')
(hh : ∀ (α β γ : L) (a b c : Λ), W.IsHom α a → W.IsHom β b → W.IsHom γ c → E a b c = 0)
(a b c : Λ)
:
E a b c = 0
A function additive in each of three arguments vanishes if it vanishes on homogeneous arguments.
theorem
MultiplicativeBasisDeformations.LatGrading.ext2_of_hom
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
{f f' : Λ →ₗ[k] Λ →ₗ[k] Λ}
(h : ∀ (α β : L) (a b : Λ), W.IsHom α a → W.IsHom β b → (f a) b = (f' a) b)
:
f = f'
Bilinear maps agreeing on homogeneous pairs agree.
Characters of cochains #
def
MultiplicativeBasisDeformations.LatGrading.Char₂
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
(χ : L)
(φ : Λ →ₗ[k] Λ →ₗ[k] Λ)
:
A two-cochain of character χ.
Instances For
def
MultiplicativeBasisDeformations.LatGrading.Char₁
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
(χ : L)
(f : Λ →ₗ[k] Λ)
:
A one-cochain of character χ.
Instances For
def
MultiplicativeBasisDeformations.LatGrading.cpr2
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
(χ : L)
(φ : Λ →ₗ[k] Λ →ₗ[k] Λ)
:
Λ →ₗ[k] Λ →ₗ[k] Λ
The character-χ part of a two-cochain.
Instances For
def
MultiplicativeBasisDeformations.LatGrading.cpr1
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
(χ : L)
(f : Λ →ₗ[k] Λ)
:
Λ →ₗ[k] Λ
The character-χ part of a one-cochain.
Instances For
theorem
MultiplicativeBasisDeformations.LatGrading.cpr1_hom
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
(χ : L)
(f : Λ →ₗ[k] Λ)
{α : L}
{a : Λ}
(ha : W.IsHom α a)
:
theorem
MultiplicativeBasisDeformations.LatGrading.cpr2_hom
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
(χ : L)
(φ : Λ →ₗ[k] Λ →ₗ[k] Λ)
{α β : L}
{a b : Λ}
(ha : W.IsHom α a)
(hb : W.IsHom β b)
:
theorem
MultiplicativeBasisDeformations.LatGrading.char₂_cpr2
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
(χ : L)
(φ : Λ →ₗ[k] Λ →ₗ[k] Λ)
:
theorem
MultiplicativeBasisDeformations.LatGrading.cpr2_of_char₂
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
{χ : L}
{φ : Λ →ₗ[k] Λ →ₗ[k] Λ}
(h : W.Char₂ χ φ)
:
W.cpr2 χ φ = φ
def
MultiplicativeBasisDeformations.LatGrading.chars
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
:
Finset L
The characters which can occur.
Instances For
theorem
MultiplicativeBasisDeformations.LatGrading.sum_cpr2
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
(φ : Λ →ₗ[k] Λ →ₗ[k] Λ)
:
A two-cochain is the sum of its character parts.
theorem
MultiplicativeBasisDeformations.LatGrading.proj_isHomLen
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
{G : LenGrading k Λ}
(compat : ∀ (d : ℕ) (l : L) (x : Λ), (G.proj d) ((W.proj l) x) = (W.proj l) ((G.proj d) x))
{d : ℕ}
{l : L}
{x : Λ}
(hx : G.IsHom d x)
:
theorem
MultiplicativeBasisDeformations.LatGrading.hasDeg₂_cpr2
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
{G : LenGrading k Λ}
(compat : ∀ (d : ℕ) (l : L) (x : Λ), (G.proj d) ((W.proj l) x) = (W.proj l) ((G.proj d) x))
{q : ℕ}
{φ : Λ →ₗ[k] Λ →ₗ[k] Λ}
(hφ : G.HasDeg₂ q φ)
(χ : L)
:
theorem
MultiplicativeBasisDeformations.LatGrading.hasDeg₁_cpr1
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
{G : LenGrading k Λ}
(compat : ∀ (d : ℕ) (l : L) (x : Λ), (G.proj d) ((W.proj l) x) = (W.proj l) ((G.proj d) x))
{q : ℕ}
{f : Λ →ₗ[k] Λ}
(hf : G.HasDeg₁ q f)
(χ : L)
:
theorem
MultiplicativeBasisDeformations.LatGrading.isCocycle₂_cpr2
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
{φ : Λ →ₗ[k] Λ →ₗ[k] Λ}
(hφ : LenGrading.IsCocycle₂ φ)
(χ : L)
:
LenGrading.IsCocycle₂ (W.cpr2 χ φ)
theorem
MultiplicativeBasisDeformations.LatGrading.cobdry_cpr1
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
(f : Λ →ₗ[k] Λ)
(χ : L)
:
LenGrading.cobdry k (W.cpr1 χ f) = W.cpr2 χ (LenGrading.cobdry k f)
theorem
MultiplicativeBasisDeformations.LatGrading.isRel₂_cpr2
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
{G : LenGrading k Λ}
(V : G.Vertices)
(he0 : ∀ (i : Fin V.n), W.IsHom 0 (V.e i))
{φ : Λ →ₗ[k] Λ →ₗ[k] Λ}
(hφ : LenGrading.IsRel₂ V φ)
(χ : L)
:
LenGrading.IsRel₂ V (W.cpr2 χ φ)
def
MultiplicativeBasisDeformations.LenGrading.innerDer
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
(u : Λ)
:
Λ →ₗ[k] Λ
The inner derivation a ↦ u a − a u.
Instances For
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.exists_rel_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)
:
Relative coboundaries. A normalized relative cocycle which is the coboundary of a
one-cochain of degree q is the coboundary of a normalized relative one-cochain of degree
q.
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}
{φ : Λ →ₗ[k] Λ →ₗ[k] Λ}
(hφ : IsRel₂ V φ)
(t : k)
:
IsRel₂ V (t • φ)
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₂.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.cobdry_zero
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
:
cobdry k 0 = 0
theorem
MultiplicativeBasisDeformations.LenGrading.hasDeg₁_sum
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
{q : ℕ}
{ι : Type u_1}
(s : Finset ι)
{f : ι → Λ →ₗ[k] Λ}
(h : ∀ i ∈ s, G.HasDeg₁ q (f i))
:
G.HasDeg₁ q (∑ i ∈ s, f i)
theorem
MultiplicativeBasisDeformations.LenGrading.span_of_char
{k : Type u}
[Field k]
{Λ : Type v}
[Ring Λ]
[Algebra k Λ]
{G : LenGrading k Λ}
(V : G.Vertices)
{L : Type}
[AddCommGroup L]
[DecidableEq L]
(W : LatGrading k Λ L)
(compat : ∀ (d : ℕ) (l : L) (x : Λ), (G.proj d) ((W.proj l) x) = (W.proj l) ((G.proj d) x))
(he0 : ∀ (i : Fin V.n), W.IsHom 0 (V.e i))
{n : ℕ}
{μ : Fin n → Λ →ₗ[k] Λ →ₗ[k] Λ}
{qd : Fin n → ℕ}
(hμrel : ∀ (i : Fin n), IsRel₂ V (μ i))
(h :
∀ (q : ℕ),
0 < q →
∀ (χ : L) (φ : Λ →ₗ[k] Λ →ₗ[k] Λ),
IsRel₂ V φ →
G.HasDeg₂ q φ →
IsCocycle₂ φ →
W.Char₂ χ φ →
∃ (c : Fin n → k) (f : Λ →ₗ[k] Λ),
G.HasDeg₁ q f ∧ φ = ∑ i : Fin n with qd i = q, c i • μ i + cobdry k f)
(q : ℕ)
:
The spanning hypothesis of Theorem 7.7 from its character parts.