The characteristic-two decomposition of HH²(A₀)_{>0} (Proposition 7.6)

weights-and-parameters.tex: "Proposition 6.1 and the distinct characters χ_i now give the asserted decomposition and the one-dimensionality of every nonzero summand, with I₀ the set of i for which HH²(A₀)_{χ_i} ≠ 0."

Here: S is a set of rows spanning the derivative cokernels, with distinct relative weights relW R = w(p_R) − ν_{v_R}. A cocycle of positive degree and character χ is a coboundary unless χ = relW R for a row R ∈ S; and if a cocycle μ_i of character relW R has nonzero class, every cocycle of that character is a multiple of μ_i up to a coboundary, in the same internal degree (char_part). With the character decomposition this gives the spanning hypothesis of Theorem 7.7 (span_A0).

def MultiplicativeBasisDeformations.MeshWalk.rowWt {V : Type} [Quiver V] {Q : TranslationQuiver V} {M : Type} [AddCommGroup M] (W : MeshWt Q M) (R : (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) : M

The relative weight of a row.

theorem MultiplicativeBasisDeformations.MeshWalk.mem_rowsOf {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {M : Type} [AddCommGroup M] (W : MeshWt Q M) [Fintype ↑Q.nonprojective] {χ : M} {S : ScalarMeshCategory.RowSet Q} {R : (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x} : R ∈ rowsOf W χ S ↔ R ∈ S ∧ rowWt W R = χ

theorem MultiplicativeBasisDeformations.MeshWalk.mem_rowSpan_le_single {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] [Fintype ↑Q.nonprojective] {m : ℕ} {T : ScalarMeshCategory.RowSet Q} {R₀ : (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x} (hT : T ⊆ {R₀}) {v : ScalarMeshCategory.Coker c m} (hv : v ∈ ScalarMeshCategory.rowSpan c m T) : v = 0 ∨ R₀.snd.length = m + 1 ∧ ∃ (a : k), v = a • ScalarMeshCategory.rowClass c m R₀.fst R₀.snd

A vector in the span of at most one row.

Bridging the two cochain formalisms

theorem MultiplicativeBasisDeformations.MeshWalk.hDeg_of_hasDeg₂ {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] [Fintype ↑Q.nonprojective] {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (h : (lenA0 D hfin).HasDeg₂ q μ) : GExt.HDeg (galgA0 D hfin) μ ↑q

theorem MultiplicativeBasisDeformations.MeshWalk.hasDeg₁_of {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] [Fintype ↑Q.nonprojective] {q : ℕ} {H : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (h : ∀ (p : ℤ) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), (galgA0 D hfin).gr.IsHom p a → (galgA0 D hfin).gr.IsHom (p + ↑q) (H a)) : (lenA0 D hfin).HasDeg₁ q H

theorem MultiplicativeBasisDeformations.MeshWalk.hcobdry_eq {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] [Fintype ↑Q.nonprojective] (H : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ) : GExt.hcobdry H = LenGrading.cobdry k H

theorem MultiplicativeBasisDeformations.MeshWalk.cobdry_of_Ψc {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] [Fintype ↑Q.nonprojective] (J : D.InjData) (h1 : DegOne D) {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (hμ : LenGrading.IsCocycle₂ μ) (hμd : (lenA0 D hfin).HasDeg₂ q μ) (Ld : LiftData D hfin q μ) (h : Ψc Ld = 0) : ∃ (H : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ), (lenA0 D hfin).HasDeg₁ q H ∧ μ = LenGrading.cobdry k H

Proposition 7.6, injectivity, in the cochain formalism of Theorem 7.8.

theorem MultiplicativeBasisDeformations.MeshWalk.exists_liftData' {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] [Fintype ↑Q.nonprojective] (J : D.InjData) (h1 : DegOne D) {q : ℕ} {μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (hμ : LenGrading.IsCocycle₂ μ) (hμd : (lenA0 D hfin).HasDeg₂ q μ) : Nonempty (LiftData D hfin q μ)

Characters with a spanning row

theorem MultiplicativeBasisDeformations.MeshWalk.char_part {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] [Fintype ↑Q.nonprojective] (J : D.InjData) (h1 : DegOne D) {S : ScalarMeshCategory.RowSet Q} (hS : ScalarMeshCategory.CokerSpan c S) (hdist : ∀ R ∈ S, ∀ R' ∈ S, rowWt W R = rowWt W R' → R = R') (V✝ : (lenA0 D hfin).Vertices) {n : ℕ} (μ : Fin n → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ) (qd : Fin n → ℕ) (R : Fin n → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) (hRS : ∀ (i : Fin n), R i ∈ S) (hμc : ∀ (i : Fin n), LenGrading.IsCocycle₂ (μ i)) (hμd : ∀ (i : Fin n), (lenA0 D hfin).HasDeg₂ (qd i) (μ i)) (hqpos : ∀ (i : Fin n), 0 < qd i) (hμχ : ∀ (i : Fin n), (latA0 W hfin D).Char₂ (rowWt W (R i)) (μ i)) (hμnz : ∀ (i : Fin n), ¬∃ (H : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ), (lenA0 D hfin).HasDeg₁ (qd i) H ∧ μ i = LenGrading.cobdry k H) (hcover : ∀ R' ∈ S, (∃ (i : Fin n), R i = R') ∨ ∀ (q : ℕ), 0 < q → ∀ (φ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ), LenGrading.IsRel₂ V✝ φ → (lenA0 D hfin).HasDeg₂ q φ → LenGrading.IsCocycle₂ φ → (latA0 W hfin D).Char₂ (rowWt W R') φ → ∃ (H : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ), (lenA0 D hfin).HasDeg₁ q H ∧ φ = LenGrading.cobdry k H) (q : ℕ) (hq : 0 < q) (χ : M) (φ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ) (hφr : LenGrading.IsRel₂ V✝ φ) (hφd : (lenA0 D hfin).HasDeg₂ q φ) (hφc : LenGrading.IsCocycle₂ φ) (hφχ : (latA0 W hfin D).Char₂ χ φ) : ∃ (cf : Fin n → k) (f : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ), (lenA0 D hfin).HasDeg₁ q f ∧ φ = ∑ i : Fin n with qd i = q, cf i • μ i + LenGrading.cobdry k f

One character part.

theorem MultiplicativeBasisDeformations.MeshWalk.compat_A0 {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] [Fintype ↑Q.nonprojective] (d : ℕ) (l : M) (x : (CatAlg.Alg D.F0)ᵐᵒᵖ) : ((lenA0 D hfin).proj d) (((latA0 W hfin D).proj l) x) = ((latA0 W hfin D).proj l) (((lenA0 D hfin).proj d) x)

The weight and length gradings of A₀ commute.

theorem MultiplicativeBasisDeformations.MeshWalk.span_A0 {k : Type u} [Field k] {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] {c : MeshCoefficients k Q} {M : Type} [AddCommGroup M] (W : MeshWt Q M) (hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)) {L : CatAlg.LocalFamily (meshFam Q c)} {D : CatAlg.MeshData (meshFam Q c) L} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] [Fintype ↑Q.nonprojective] (J : D.InjData) (h1 : DegOne D) {S : ScalarMeshCategory.RowSet Q} (hS : ScalarMeshCategory.CokerSpan c S) (hdist : ∀ R ∈ S, ∀ R' ∈ S, rowWt W R = rowWt W R' → R = R') (V✝ : (lenA0 D hfin).Vertices) (he0 : ∀ (i : Fin V✝.n), (latA0 W hfin D).IsHom 0 (V✝.e i)) {n : ℕ} (μ : Fin n → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ) (qd : Fin n → ℕ) (R : Fin n → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) (hRS : ∀ (i : Fin n), R i ∈ S) (hμrel : ∀ (i : Fin n), LenGrading.IsRel₂ V✝ (μ i)) (hμc : ∀ (i : Fin n), LenGrading.IsCocycle₂ (μ i)) (hμd : ∀ (i : Fin n), (lenA0 D hfin).HasDeg₂ (qd i) (μ i)) (hqpos : ∀ (i : Fin n), 0 < qd i) (hμχ : ∀ (i : Fin n), (latA0 W hfin D).Char₂ (rowWt W (R i)) (μ i)) (hμnz : ∀ (i : Fin n), ¬∃ (H : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ), (lenA0 D hfin).HasDeg₁ (qd i) H ∧ μ i = LenGrading.cobdry k H) (hcover : ∀ R' ∈ S, (∃ (i : Fin n), R i = R') ∨ ∀ (q : ℕ), 0 < q → ∀ (φ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ), LenGrading.IsRel₂ V✝ φ → (lenA0 D hfin).HasDeg₂ q φ → LenGrading.IsCocycle₂ φ → (latA0 W hfin D).Char₂ (rowWt W R') φ → ∃ (H : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ), (lenA0 D hfin).HasDeg₁ q H ∧ φ = LenGrading.cobdry k H) (q : ℕ) : 0 < q → ∀ (φ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ), LenGrading.IsRel₂ V✝ φ → (lenA0 D hfin).HasDeg₂ q φ → LenGrading.IsCocycle₂ φ → ∃ (cf : Fin n → k) (f : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ), LenGrading.IsRel₁ V✝ f ∧ (lenA0 D hfin).HasDeg₁ q f ∧ φ = ∑ i : Fin n with qd i = q, cf i • μ i + LenGrading.cobdry k f

Proposition 7.6, the decomposition, in the form of the spanning hypothesis of Theorem 7.7: chosen cocycles μ_i of the characters of the spanning rows, with nonzero classes, span the positive-degree Hochschild cohomology of A₀ when every other spanning row has zero cohomology in its character.