Weight lifting for the ray table of A₀

Proposition 8.3(3) for P = ray A₀ (local-ray-geometry.tex: "For the present P = ray A₀, freeness already follows directly from Proposition 7.2"): an additive weight of P modulo two factors through W(P) ⊗ 𝔽₂; since W(P) is free (WP_free), it lifts to an integer additive weight (A0Mult_lift2).

theorem MultiplicativeBasisDeformations.MeshWalk.A0Mult_of_comp {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)ᵐᵒᵖ) {x y z : D.PV} {g h : Deck Q v₀} {f : D.F0 x ⟶ D.F0 y} {f' : D.F0 y ⟶ D.F0 z} (hf : f ∈ (D0 Q c v₀ D).part g x y) (hf' : f' ∈ (D0 Q c v₀ D).part h y z) (hff : CategoryTheory.CategoryStruct.comp f f' ≠ 0) : ∃ (h1 : NZ Q c v₀ D (x, y, g)) (h2 : NZ Q c v₀ D (y, z, h)) (h3 : NZ Q c v₀ D (x, z, g * h)), (A0Mult D v₀ hF).mul ⟨(y, z, h), h2⟩ ⟨(x, y, g), h1⟩ = some ⟨(x, z, g * h), h3⟩

A nonzero composite of deck pieces is a product of rays of A₀.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.wPiece {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) (v₀ : V) (w : RayA0 D v₀ → ZMod 2) (t : Piece Q c v₀ D) : ZMod 2

The additive weight on pieces induced by a weight of the rays.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.wbar {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)ᵐᵒᵖ) (w : RayA0 D v₀ → ZMod 2) (hw : ∀ (r s t : RayA0 D v₀), (A0Mult D v₀ hF).mul r s = some t → w t = w r + w s) : WP Q c v₀ D →+ ZMod 2

An additive weight modulo two factors through W(P).

theorem MultiplicativeBasisDeformations.MeshWalk.wbar_cls {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)ᵐᵒᵖ) (w : RayA0 D v₀ → ZMod 2) (hw : ∀ (r s t : RayA0 D v₀), (A0Mult D v₀ hF).mul r s = some t → w t = w r + w s) (t : RayA0 D v₀) : (wbar D v₀ hF w hw) (cls Q c v₀ D ↑t) = w t

theorem MultiplicativeBasisDeformations.MeshWalk.A0Mult_lift2 {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)ᵐᵒᵖ) (x₀ : D.PV) (hconn : A0Conn Q c v₀ D x₀) : (A0Mult D v₀ hF).Lift2

Weight lifting for the ray table of a connected A₀ (Proposition 7.2(1)).

theorem MultiplicativeBasisDeformations.MeshWalk.A0Conn_of_conn {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)ᵐᵒᵖ) (hc : (A0Mult D v₀ hF).Conn) (x₀ : D.PV) : A0Conn Q c v₀ D x₀

Connectivity of the table of A₀ is connectivity of A₀.