Corollary 10.5 for A₀, given Proposition 10.3

cor:zero-supported-coverage (integral-deformations.tex) for the ray system of A₀ with the dual weights (Char2A0.Cor105): the hypotheses of Theorem 9.1(3) come from the induction hypothesis of Proposition 8.3 through Lemma 9.2 (hWl_of_liftBelow), and the only remaining input is Proposition 10.3 in coefficients (IStar).

theorem MultiplicativeBasisDeformations.RaySys.Sys.hWl_of_liftBelow {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (hLB : LiftBelow k (Fintype.card R)) (w : R → ZMod 2) : (∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → w t = w r + w s) → ∃ (ω : R → ℤ), (∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → ω t = ω r + ω s) ∧ ∀ (r : R), S.TB χ r → ↑(ω r) = w r

The lifting hypothesis of Theorem 9.1(3) from the induction hypothesis (Lemma 9.2).

theorem MultiplicativeBasisDeformations.RaySys.Sys.integralPartialLifting {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (hLB : LiftBelow k (Fintype.card R)) {d : R → ZMod 2} (hd : S.IsSol χ d) : ∃ (D : R → ℤ), S.IsSol χ D ∧ ∀ (r : R), ↑(D r) = d r

Theorem 9.1 (thm:integral-partial-lifting): if the lifting assertion of Proposition 8.2 holds for every table with representation-finite linearization and fewer than dim A₀ rays, every solution modulo two of the Leibniz equations lifts to an integer solution (and hence to ℤ/4).

theorem MultiplicativeBasisDeformations.RaySys.Sys.hVx_of {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] {Λ : Type u} [Ring Λ] [Algebra k Λ] (Θ : ↥(S.P.Lin k) ≃ₐ[k] Λ) {G : LenGrading k Λ} (Vx : G.Vertices) (h : ∀ (i : Fin Vx.n), ∃ (x : V), Vx.e i = Θ (S.P.b k (S.P.e x))) (x : V) : ∃ (i : Fin Vx.n), Vx.e i = Θ (S.P.b k (S.P.e x))

Every vertex idempotent occurs among the vertices of a grading.

def MultiplicativeBasisDeformations.MeshWalk.IStarA0 {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)ᵐᵒᵖ) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWt Q ℤ) [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.cor105_of_IStarA0 {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)ᵐᵒᵖ) {ι : Type} [Fintype ι] [DecidableEq ι] (Wd : ι → MeshWt Q ℤ) [CharP k 2] (Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) (hWd : ∀ (i j : ι), rowWt (Wd i) (Rw j) = if j = i then 1 else 0) (hLB : LiftBelow k (Fintype.card (RayA0 D v₀))) (hI : IStarA0 D v₀ hF Wd Rw) : Cor105 D v₀ hF Wd Rw

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

def MultiplicativeBasisDeformations.IndSkeleton.IStarAR {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] : Prop

Proposition 10.3 for the algebra A₀ of A, for every choice of rows and dual weights.

theorem MultiplicativeBasisDeformations.IndSkeleton.cor105AR_of_IStar {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) (hLB : LiftBelow k (Module.finrank k A)) (hI : S.IStarAR b) : S.Cor105AR b

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

def MultiplicativeBasisDeformations.IStarHyp (k : Type u) [Field k] [IsAlgClosed k] [CharP k 2] : Prop

Proposition 10.3 for every basic representation-finite algebra (in coefficients).

theorem MultiplicativeBasisDeformations.cor105Hyp_of_IStar (k : Type u) [Field k] [IsAlgClosed k] [CharP k 2] (hI : IStarHyp k) : Cor105Hyp k

Corollary 10.5 under the induction hypothesis, given Proposition 10.3.