Proposition 12.5: weights, and I₀ = I #
deformation-refinements.tex: "Giving ε internal degree −q and the opposite weight
makes the corner deformation homogeneous of the required degree and weight. […] In
characteristic two, each residual line k[p_i] of Proposition 6.1 has weight χ_i and is now
in the image, so HH²(A₀)_{χ_i} ≠ 0 and I₀ = I."
For a mesh weight W, the weight-χ part of a category cocycle (CatCocycle.wproj) is again a
cocycle of the same internal degree; its mesh value is the relative weight-χ part of the
original one, and its corner μ has character χ (catMu_hasChar). Hence every correction
tuple of relative weight χ is Ψ[μ] for a cocycle μ of character χ
(Ψc_surjective_char), and a row with nonzero cokernel class gives a cocycle of the row's
character which is not a coboundary (exists_not_cobdry): I ⊆ I₀. The inclusion I₀ ⊆ I is
Proposition 7.6 (Ψc_mem_rowSpan_char).
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.CatCocycle.wφ
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
[(x y : V) → Fintype (x ⟶ y)]
{Q : TranslationQuiver V}
{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))
{q : ℕ}
(Φ : CatCocycle c q)
(χ : M)
{X Y Z : V}
(f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y)
(g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z)
:
ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Z
The weight-χ part of a category cocycle.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.CatCocycle.wφ_hom
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
[(x y : V) → Fintype (x ⟶ y)]
[(x y : V) → DecidableEq (x ⟶ y)]
{Q : TranslationQuiver V}
{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))
{q : ℕ}
(Φ : CatCocycle c q)
(χ : M)
{X Y Z : V}
{α β : M}
{f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y}
{g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z}
(hf : f ∈ wP c W α X Y)
(hg : g ∈ wP c W β Y Z)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.CatCocycle.wφ_add_left
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
[(x y : V) → Fintype (x ⟶ y)]
[(x y : V) → DecidableEq (x ⟶ y)]
{Q : TranslationQuiver V}
{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))
{q : ℕ}
(Φ : CatCocycle c q)
(χ : M)
{X Y Z : V}
(f f' : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y)
(g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.CatCocycle.wφ_add_right
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
[(x y : V) → Fintype (x ⟶ y)]
[(x y : V) → DecidableEq (x ⟶ y)]
{Q : TranslationQuiver V}
{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))
{q : ℕ}
(Φ : CatCocycle c q)
(χ : M)
{X Y Z : V}
(f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y)
(g g' : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.CatCocycle.wφ_smul_left
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
[(x y : V) → Fintype (x ⟶ y)]
[(x y : V) → DecidableEq (x ⟶ y)]
{Q : TranslationQuiver V}
{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))
{q : ℕ}
(Φ : CatCocycle c q)
(χ : M)
{X Y Z : V}
(t : k)
(f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y)
(g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.CatCocycle.wφ_smul_right
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
[(x y : V) → Fintype (x ⟶ y)]
[(x y : V) → DecidableEq (x ⟶ y)]
{Q : TranslationQuiver V}
{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))
{q : ℕ}
(Φ : CatCocycle c q)
(χ : M)
{X Y Z : V}
(t : k)
(f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y)
(g : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.CatCocycle.eq_zero_of_whom
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
[(x y : V) → Fintype (x ⟶ y)]
[(x y : V) → DecidableEq (x ⟶ y)]
{Q : TranslationQuiver V}
{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))
{X Y : V}
{N : Type u_1}
[AddCommGroup N]
(F : (ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y) →+ N)
(h : ∀ (α : M), ∀ f ∈ wP c W α X Y, F f = 0)
(f : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y)
:
F f = 0
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.CatCocycle.wExpr
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
[(x y : V) → Fintype (x ⟶ y)]
{Q : TranslationQuiver V}
{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))
{q : ℕ}
(Φ : CatCocycle c q)
(χ : M)
{V₀ X Y Z : V}
(f : ScalarMeshCategory.obj c V₀ ⟶ ScalarMeshCategory.obj c X)
(g : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y)
(h : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z)
:
ScalarMeshCategory.obj c V₀ ⟶ ScalarMeshCategory.obj c Z
The cocycle expression of the weight part.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.CatCocycle.wExpr_hom
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
[(x y : V) → Fintype (x ⟶ y)]
[(x y : V) → DecidableEq (x ⟶ y)]
{Q : TranslationQuiver V}
{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))
{q : ℕ}
(Φ : CatCocycle c q)
(χ : M)
{V₀ X Y Z : V}
{a b d : M}
{f : ScalarMeshCategory.obj c V₀ ⟶ ScalarMeshCategory.obj c X}
{g : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y}
{h : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z}
(hf : f ∈ wP c W a V₀ X)
(hg : g ∈ wP c W b X Y)
(hh : h ∈ wP c W d Y Z)
:
wExpr W hfin Φ χ f g h = 0
theorem
MultiplicativeBasisDeformations.MeshWalk.CatCocycle.wExpr_eq_zero
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
[(x y : V) → Fintype (x ⟶ y)]
[(x y : V) → DecidableEq (x ⟶ y)]
{Q : TranslationQuiver V}
{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))
{q : ℕ}
(Φ : CatCocycle c q)
(χ : M)
{V₀ X Y Z : V}
(f : ScalarMeshCategory.obj c V₀ ⟶ ScalarMeshCategory.obj c X)
(g : ScalarMeshCategory.obj c X ⟶ ScalarMeshCategory.obj c Y)
(h : ScalarMeshCategory.obj c Y ⟶ ScalarMeshCategory.obj c Z)
:
wExpr W hfin Φ χ f g h = 0
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.CatCocycle.wproj
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
[(x y : V) → Fintype (x ⟶ y)]
[(x y : V) → DecidableEq (x ⟶ y)]
{Q : TranslationQuiver V}
{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))
{q : ℕ}
(Φ : CatCocycle c q)
(χ : M)
:
CatCocycle c q
The weight-χ part of a category cocycle, of the same internal degree.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.CatCocycle.meshVal_wproj
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
[(x y : V) → Fintype (x ⟶ y)]
[(x y : V) → DecidableEq (x ⟶ y)]
{Q : TranslationQuiver V}
{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))
{q : ℕ}
(Φ : CatCocycle c q)
(χ : M)
(x : ↑Q.nonprojective)
:
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.CatCocycle.zero
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[(x y : V) → Fintype (x ⟶ y)]
{Q : TranslationQuiver V}
{c : MeshCoefficients k Q}
{q : ℕ}
:
CatCocycle c q
The zero cocycle.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.CatCocycle.meshVal_zero
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
[(x y : V) → Fintype (x ⟶ y)]
[(x y : V) → DecidableEq (x ⟶ y)]
{Q : TranslationQuiver V}
{c : MeshCoefficients k Q}
{q : ℕ}
:
theorem
MultiplicativeBasisDeformations.MeshWalk.catMu_hasChar
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
[(x y : V) → Fintype (x ⟶ y)]
[(x y : V) → DecidableEq (x ⟶ y)]
{Q : TranslationQuiver V}
{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)]
{q : ℕ}
(Φ : CatCocycle c q)
(χ : M)
:
HasChar W hfin D χ (catMu D (CatCocycle.wproj W hfin Φ χ))
theorem
MultiplicativeBasisDeformations.MeshWalk.catMu_zero
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
[(x y : V) → Fintype (x ⟶ y)]
[(x y : V) → DecidableEq (x ⟶ y)]
{Q : TranslationQuiver V}
{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)]
{q : ℕ}
:
catMu D CatCocycle.zero = 0
theorem
MultiplicativeBasisDeformations.MeshWalk.Ψc_cast
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
[(x y : V) → Fintype (x ⟶ y)]
[(x y : V) → DecidableEq (x ⟶ y)]
{Q : TranslationQuiver V}
{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)]
{q : ℕ}
{μ μ' : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ}
(e : μ = μ')
(Ld : LiftData D hfin q μ)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.Ψc_surjective_char
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
[(x y : V) → Fintype (x ⟶ y)]
[(x y : V) → DecidableEq (x ⟶ y)]
{Q : TranslationQuiver V}
{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)]
(hres :
∀ (w x : V),
Function.Injective
⇑(FlatPert.relMap (FlatPert.meshPres c) (FlatPert.idealC (FlatPert.meshPres c)) (FlatPert.meshPres c).r w x) ∧ (FlatPert.alpha (FlatPert.idealC (FlatPert.meshPres c)) w x).ker ≤ (FlatPert.relMap (FlatPert.meshPres c) (FlatPert.idealC (FlatPert.meshPres c)) (FlatPert.meshPres c).r w
x).range)
{q : ℕ}
(hq : 1 ≤ q)
(χ : M)
(z : ScalarMeshCategory.MeshFamily c)
(hz : ∀ (x : ↑Q.nonprojective), z x ∈ ScalarMeshCategory.degreePart c (q + 2) ↑(Q.tau x) ↑x)
(hzw : ∀ (x : ↑Q.nonprojective), z x ∈ wP c W (W.ν x + χ) ↑(Q.tau x) ↑x)
:
∃ (μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ) (_ : GExt.IsHCocycle μ) (_ :
GExt.HDeg (galgA0 D hfin) μ ↑q) (_ : HasChar W hfin D χ μ) (Ld : LiftData D hfin q μ), Ψc Ld = Submodule.Quotient.mk z
Proposition 12.5 with weights: a correction tuple of relative weight χ is Ψ[μ] for a
cocycle μ of character χ.
theorem
MultiplicativeBasisDeformations.MeshWalk.exists_not_cobdry
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
[(x y : V) → Fintype (x ⟶ y)]
[(x y : V) → DecidableEq (x ⟶ y)]
{Q : TranslationQuiver V}
{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)]
(J : D.InjData)
(h1 : DegOne D)
(hres :
∀ (w x : V),
Function.Injective
⇑(FlatPert.relMap (FlatPert.meshPres c) (FlatPert.idealC (FlatPert.meshPres c)) (FlatPert.meshPres c).r w x) ∧ (FlatPert.alpha (FlatPert.idealC (FlatPert.meshPres c)) w x).ker ≤ (FlatPert.relMap (FlatPert.meshPres c) (FlatPert.idealC (FlatPert.meshPres c)) (FlatPert.meshPres c).r w
x).range)
{q : ℕ}
(hq : 1 ≤ q)
(x : ↑Q.nonprojective)
(p : Quiver.Path ↑(Q.tau x) ↑x)
(hp : p.length = q + 2)
(hne : ScalarMeshCategory.rowClass c (q + 1) x p ≠ 0)
:
∃ (μ : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ) (_ : GExt.IsHCocycle μ) (_ :
GExt.HDeg (galgA0 D hfin) μ ↑q) (_ : HasChar W hfin D (W.pw p - W.ν x) μ) (Ld : LiftData D hfin q μ),
Ψc Ld = ScalarMeshCategory.rowClass c (q + 1) x p ∧ ¬∃ (H : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ),
(∀ (p : ℤ) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), (galgA0 D hfin).gr.IsHom p a → (galgA0 D hfin).gr.IsHom (p + ↑q) (H a)) ∧ μ = GExt.hcobdry H
I ⊆ I₀ (deformation-refinements.tex): a row p : τx → x of length
q + 2 ≥ 3 whose class in coker D_{q+1} is nonzero gives a Hochschild cocycle of A₀ of
internal degree q and of the row's character χ = w(p) − ν_x which is not a coboundary of
degree q, with Ψ[μ] = [p].
theorem
MultiplicativeBasisDeformations.IndSkeleton.exists_not_cobdry_ar
{k A : Type w}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : IndSkeleton k A)
(b : S.ArrowBases)
{M : Type}
[AddCommGroup M]
(W : MeshWalk.MeshWt S.arTranslationQuiver M)
{q : ℕ}
(hq : 1 ≤ q)
(x : ↑S.arTranslationQuiver.nonprojective)
(p : Quiver.Path ↑(S.arTranslationQuiver.tau x) ↑x)
(hp : p.length = q + 2)
(hne : ScalarMeshCategory.rowClass (S.arCoefficients b) (q + 1) x p ≠ 0)
:
∃ (μ :
(CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ)
(_ : GExt.IsHCocycle μ) (_ : GExt.HDeg (MeshWalk.galgA0 (S.arMeshData b) ⋯) μ ↑q) (_ :
MeshWalk.HasChar W ⋯ (S.arMeshData b) (W.pw p - W.ν x) μ) (Ld : MeshWalk.LiftData (S.arMeshData b) ⋯ q μ),
MeshWalk.Ψc Ld = ScalarMeshCategory.rowClass (S.arCoefficients b) (q + 1) x p ∧ ¬∃ (H : (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ),
(∀ (p : ℤ) (a : (CatAlg.Alg (S.arMeshData b).F0)ᵐᵒᵖ),
(MeshWalk.galgA0 (S.arMeshData b) ⋯).gr.IsHom p a →
(MeshWalk.galgA0 (S.arMeshData b) ⋯).gr.IsHom (p + ↑q) (H a)) ∧ μ = GExt.hcobdry H
I ⊆ I₀ for A₀ (Proposition 12.5, deformation-refinements.tex): a row of
Γ_A of length q + 2 ≥ 3 with nonzero cokernel class gives a non-trivial Hochschild class of
A₀ of the row's character.