Corollary 10.5 with the residual characters in W(P)

cor:zero-supported-coverage (integral-deformations.tex): "Assume the smaller-table lifting hypothesis of Theorem 9.1. Then every nonzero line HH²(A₀)_{χ_i}, with i ∈ I₀, has a nonzero representative supported on composable pairs (r, s) with rs = 0 and r * s ≠ 0 […]. Its value at such a pair lies in the line U_{r*s}."

The statement of Char2A0.Cor105 and its proof (Cor105A0.lean) for an arbitrary mesh weight W with values in a lattice and a degree map (Cor105G, IStarG, cor105G_of_IStar; the characters are only required to be primitive), and the instance for A₀ of a basic connected representation-finite algebra in characteristic two with the characters in L = W(P) (IndSkeleton.zeroSupportedCoverage_WP): Proposition 10.3 for this weight by the generic MeshWalk.istar with the prime-field table, and primitivity from the integer basis of Proposition 7.5.

def MultiplicativeBasisDeformations.MeshWalk.Cor105G {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) [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) {Lt : Type} [AddCommGroup Lt] (W : MeshWt Q Lt) (dg : Lt →+ ℤ) (hdg : dg.comp (MeshWt.res c D W) = MeshWt.res c D lenW) {ι : Type} (Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) : Prop

Corollary 10.5 for A₀ with characters rowWt W (Rw i).

def MultiplicativeBasisDeformations.MeshWalk.IStarG {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) [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) {Lt : Type} [AddCommGroup Lt] (W : MeshWt Q Lt) (dg : Lt →+ ℤ) (hdg : dg.comp (MeshWt.res c D W) = MeshWt.res c D lenW) {ι : Type} [CharP k 2] (Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) : Prop

Proposition 10.3 for A₀ in coefficients, for the rows Rw.

theorem MultiplicativeBasisDeformations.MeshWalk.cor105G_of_IStar {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) [IsAlgClosed k] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] (v₀ : V) (hF : IsRepresentationFinite k (CatAlg.Alg D.F0)ᵐᵒᵖ) {Lt : Type} [AddCommGroup Lt] (W : MeshWt Q Lt) (dg : Lt →+ ℤ) (hdg : dg.comp (MeshWt.res c D W) = MeshWt.res c D lenW) {ι : Type} [Fintype ι] [DecidableEq ι] [CharP k 2] (Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) (hprimR : ∀ (i : ι), RaySys.Sys.Prim (rowWt W (Rw i))) (hLB : LiftBelow k (Fintype.card (RayA0 D v₀))) (hI : IStarG D v₀ hF W dg hdg Rw) : Cor105G D v₀ hF W dg hdg Rw

Corollary 10.5 for A₀ given Proposition 10.3 and the induction hypothesis.

theorem MultiplicativeBasisDeformations.IndSkeleton.zeroSupportedCoverage_WP {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) [CharP k 2] (hbasic : IsBasicAlgebra A) (hconn : IsConnectedRing A) (v₀ : S.ARVertex) (hLB : LiftBelow k (Module.finrank k A)) : have hF := ⋯; have dg := MeshWalk.MeshWt.res (S.arCoefficients b) (S.arMeshData b) MeshWalk.lenW; ∃ (m : ℕ) (Rw : Fin m → (x : ↑S.arTranslationQuiver.nonprojective) × Quiver.Path ↑(S.arTranslationQuiver.tau x) ↑x) (Wu : MeshWalk.MeshWt S.arTranslationQuiver (MeshWalk.WP S.arTranslationQuiver (S.arCoefficients b) v₀ (S.arMeshData b))) (hdg : dg.comp (MeshWalk.MeshWt.res (S.arCoefficients b) (S.arMeshData b) Wu) = MeshWalk.MeshWt.res (S.arCoefficients b) (S.arMeshData b) MeshWalk.lenW), MeshWalk.MeshWt.res (S.arCoefficients b) (S.arMeshData b) Wu = AddMonoidHom.id (MeshWalk.WP S.arTranslationQuiver (S.arCoefficients b) v₀ (S.arMeshData b)) ∧ Function.Injective Rw ∧ (∀ (i : Fin m), ↑(Rw i).fst ∈ S.arTranslationQuiver.periodic) ∧ (∀ (i j : Fin m), ↑(Rw j).fst ∈ S.arTranslationQuiver.component ↑(Rw i).fst → i = j) ∧ ScalarMeshCategory.CokerSpan (S.arCoefficients b) (Set.range Rw) ∧ MeshWalk.Cor105G (S.arMeshData b) v₀ hF Wu dg hdg Rw

Corollary 10.5 (cor:zero-supported-coverage) with the residual characters in W(P): for a basic connected representation-finite algebra in characteristic two, under the smaller-table lifting hypothesis of Theorem 9.1 (LiftBelow), for the rows of Proposition 6.1 and the universal mesh weight, every row with a nonzero class in HH²(A₀)_{χ_i} (i ∈ I₀) has a non-coboundary representative supported on the pairs with zero product and nonzero stem product, with values in the stem lines (Cor105G).