The ray table of A₀

Setting 8.4 (local-ray-geometry.tex) for A₀: "A₀ = kP … identified with kP by Proposition 4.14. We use its normed homogeneous ray basis." The basis of Proposition 4.14 (basisA0) consists of one vector on each nonzero deck-homogeneous piece A₀(x, y)_g; its multiplication table is the ray table P (A0Tab), with the weight [x, y, g] ∈ W(P) of Definition 7.1 (cls) and the degree given by the length mesh weight. Rays with the same endpoints and the same weight are equal, since both lie in one length degree and the length pieces of a corner are lines (lines, Lemma 3.7 for A₀). By Theorem 4.? A₀ is representation-finite, so the table carries Setting 8.4 (A0Sys).

The basis vector of the piece (x, y, g) lies in the corner e_y A₀ e_x of the opposite algebra, so the table has source y and target x.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.deckV {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 : D.PV) : Deck Q v₀ → (D.F0 x ⟶ D.F0 y)

The chosen deck-homogeneous vectors of Proposition 4.14.

theorem MultiplicativeBasisDeformations.MeshWalk.deckV_mem {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 : D.PV) (g : Deck Q v₀) : deckV D v₀ hF x y g ∈ (D0 Q c v₀ D).part g x y

theorem MultiplicativeBasisDeformations.MeshWalk.deckV_span {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 : D.PV) (g : Deck Q v₀) (f : D.F0 x ⟶ D.F0 y) (hf : f ∈ (D0 Q c v₀ D).part g x y) : ∃ (c_1 : k), f = c_1 • deckV D v₀ hF x y g

theorem MultiplicativeBasisDeformations.MeshWalk.deckV_ne {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 : D.PV) (g : Deck Q v₀) (h : (D0 Q c v₀ D).part g x y ≠ ⊥) : deckV D v₀ hF x y g ≠ 0

theorem MultiplicativeBasisDeformations.MeshWalk.deckV_id {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) : deckV D v₀ hF x x 1 = CategoryTheory.CategoryStruct.id (D.F0 x)

theorem MultiplicativeBasisDeformations.MeshWalk.deckV_mul {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₀) : CategoryTheory.CategoryStruct.comp (deckV D v₀ hF x y g) (deckV D v₀ hF y z h) = 0 ∨ CategoryTheory.CategoryStruct.comp (deckV D v₀ hF x y g) (deckV D v₀ hF y z h) = deckV D v₀ hF x z (g * h)

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.RayA0 {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) : Type

The rays of A₀: the nonzero deck-homogeneous pieces.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.basisR {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)ᵐᵒᵖ) : Module.Basis (RayA0 D v₀) k (CatAlg.Alg D.F0)ᵐᵒᵖ

The normed homogeneous ray basis of A₀ (Proposition 4.14).

instance MultiplicativeBasisDeformations.MeshWalk.instFiniteRayA0 {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) : Finite (RayA0 D v₀)

theorem MultiplicativeBasisDeformations.MeshWalk.idTo_ne_zero' {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)] (x : D.PV) : CategoryTheory.CategoryStruct.id (D.F0 x) ≠ 0

noncomputable def MultiplicativeBasisDeformations.MeshWalk.eR {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) : RayA0 D v₀

The identity piece of a vertex.

theorem MultiplicativeBasisDeformations.MeshWalk.basisR_eR {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) : (basisR D v₀ hF) (eR D v₀ hF x) = MulOpposite.op (CatAlg.unitM x x (CategoryTheory.CategoryStruct.id (D.F0 x)))

theorem MultiplicativeBasisDeformations.MeshWalk.basisR_apply {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)ᵐᵒᵖ) (t : RayA0 D v₀) : (basisR D v₀ hF) t = MulOpposite.op (CatAlg.unitM (↑t).1 (↑t).2.1 (deckV D v₀ hF (↑t).1 (↑t).2.1 (↑t).2.2))

theorem MultiplicativeBasisDeformations.MeshWalk.basisR_mult {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)ᵐᵒᵖ) : IsMultiplicativeBasis (basisR D v₀ hF)

theorem MultiplicativeBasisDeformations.MeshWalk.basisR_complete {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)ᵐᵒᵖ) : CompleteOrthogonalIdempotents fun (x : D.PV) => (basisR D v₀ hF) (eR D v₀ hF x)

def MultiplicativeBasisDeformations.MeshWalk.srcR {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) (t : RayA0 D v₀) : D.PV

Source of a ray of A₀ (the opposite convention).

def MultiplicativeBasisDeformations.MeshWalk.tgtR {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) (t : RayA0 D v₀) : D.PV

Target of a ray of A₀.

theorem MultiplicativeBasisDeformations.MeshWalk.basisR_corner {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)ᵐᵒᵖ) (t : RayA0 D v₀) : (basisR D v₀ hF) (eR D v₀ hF (srcR D v₀ t)) * (basisR D v₀ hF) t * (basisR D v₀ hF) (eR D v₀ hF (tgtR D v₀ t)) = (basisR D v₀ hF) t

theorem MultiplicativeBasisDeformations.MeshWalk.srcR_eR {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) : srcR D v₀ (eR D v₀ hF x) = x

theorem MultiplicativeBasisDeformations.MeshWalk.tgtR_eR {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) : tgtR D v₀ (eR D v₀ hF x) = x

@[instance_reducible]

noncomputable instance MultiplicativeBasisDeformations.MeshWalk.instFintypeRayA0 {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) : Fintype (RayA0 D v₀)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.A0Mult {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)ᵐᵒᵖ) : RaySys.Mult D.PV (RayA0 D v₀)

The multiplication table of A₀.

Idempotents and length grading of A₀

theorem MultiplicativeBasisDeformations.MeshWalk.hfinObj {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} [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)] (x y : V) : FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.FpA0 {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)ᵐᵒᵖ) : PrimitiveIdempotents (CatAlg.Alg D.F0)ᵐᵒᵖ

The vertex idempotents of A₀ as primitive idempotents.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.idxA0 {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)ᵐᵒᵖ) : D.PV ≃ Fin (FpA0 D v₀ hF).m

Vertices as indices of the idempotents of A₀.

theorem MultiplicativeBasisDeformations.MeshWalk.FpA0_e {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) : (FpA0 D v₀ hF).e ((idxA0 D v₀ hF) x) = MulOpposite.op (CatAlg.unitM x x (CategoryTheory.CategoryStruct.id (D.F0 x)))

theorem MultiplicativeBasisDeformations.MeshWalk.FpA0_he0 {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)ᵐᵒᵖ) (i : Fin (FpA0 D v₀ hF).m) : (lenA0 D ⋯).IsHom 0 ((FpA0 D v₀ hF).e i)

theorem MultiplicativeBasisDeformations.MeshWalk.FpA0_hcorner0 {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)ᵐᵒᵖ) (i : Fin (FpA0 D v₀ hF).m) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) (ha : a ∈ (FpA0 D v₀ hF).corner i i) (h0 : (lenA0 D ⋯).IsHom 0 a) : ∃ (t : k), a = t • (FpA0 D v₀ hF).e i

theorem MultiplicativeBasisDeformations.MeshWalk.basisR_mem_corner {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)ᵐᵒᵖ) (t : RayA0 D v₀) : (basisR D v₀ hF) t ∈ (FpA0 D v₀ hF).corner ((idxA0 D v₀ hF) (srcR D v₀ t)) ((idxA0 D v₀ hF) (tgtR D v₀ t))

Weights and degrees

def MultiplicativeBasisDeformations.MeshWalk.lenW {V : Type} [Quiver V] {Q : TranslationQuiver V} : MeshWt Q ℤ

The length mesh weight: every arrow has weight one.

theorem MultiplicativeBasisDeformations.MeshWalk.lenW_pw {V : Type} [Quiver V] [Fintype V] [DecidableEq V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] [hone : ∀ (x y : V), Subsingleton (x ⟶ y)] [(x y : V) → Fintype (x ⟶ y)] {y x : V} (p : Quiver.Path y x) : lenW.pw p = ↑p.length

theorem MultiplicativeBasisDeformations.MeshWalk.deg_cls_path {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) {x y : D.PV} {g : Deck Q v₀} (h : NZ Q c v₀ D (x, y, g)) {p : Quiver.Path ↑x ↑y} (hp : (degW Q v₀).deg p = g) : (MeshWt.res c D lenW) (cls Q c v₀ D (x, y, g)) = ↑p.length

theorem MultiplicativeBasisDeformations.MeshWalk.basisR_isHom {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 : D.PV} {g : Deck Q v₀} (h : NZ Q c v₀ D (x, y, g)) {p : Quiver.Path ↑x ↑y} (hp : (degW Q v₀).deg p = g) : (lenA0 D ⋯).IsHom p.length ((basisR D v₀ hF) ⟨(x, y, g), h⟩)

Products of rays

theorem MultiplicativeBasisDeformations.MeshWalk.basisR_mul_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) [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)ᵐᵒᵖ) {r s t : RayA0 D v₀} (h : (basisR D v₀ hF) r * (basisR D v₀ hF) s = (basisR D v₀ hF) t) : ∃ (hm : (↑s).2.1 = (↑r).1), CategoryTheory.CategoryStruct.comp (deckV D v₀ hF (↑s).1 (↑s).2.1 (↑s).2.2) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (deckV D v₀ hF (↑r).1 (↑r).2.1 (↑r).2.2)) ≠ 0 ∧ ↑t = ((↑s).1, (↑r).2.1, (↑s).2.2 * (↑r).2.2)

A nonzero product of rays of A₀ is the composite piece.

theorem MultiplicativeBasisDeformations.MeshWalk.A0Mult_mul_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) [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)ᵐᵒᵖ) {r s t : RayA0 D v₀} (h : (A0Mult D v₀ hF).mul r s = some t) : (basisR D v₀ hF) r * (basisR D v₀ hF) s = (basisR D v₀ hF) t

theorem MultiplicativeBasisDeformations.MeshWalk.cls_mul_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} {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)ᵐᵒᵖ) {r s t : RayA0 D v₀} (h : (A0Mult D v₀ hF).mul r s = some t) : cls Q c v₀ D ↑t = cls Q c v₀ D ↑r + cls Q c v₀ D ↑s

noncomputable def MultiplicativeBasisDeformations.MeshWalk.wtR {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) (t : RayA0 D v₀) : WP Q c v₀ D

The weight of a ray of A₀ in W(P).

noncomputable def MultiplicativeBasisDeformations.MeshWalk.degR {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) : WP Q c v₀ D →+ ℤ

The length degree on W(P).

theorem MultiplicativeBasisDeformations.MeshWalk.degR_wtR_path {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) {t : RayA0 D v₀} {p : Quiver.Path ↑(↑t).1 ↑(↑t).2.1} (hp : (degW Q v₀).deg p = (↑t).2.2) : (degR D v₀) (wtR D v₀ t) = ↑p.length

theorem MultiplicativeBasisDeformations.MeshWalk.degR_pos {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)ᵐᵒᵖ) (t : RayA0 D v₀) (h : t ≠ eR D v₀ hF (srcR D v₀ t)) : 0 < (degR D v₀) (wtR D v₀ t)

theorem MultiplicativeBasisDeformations.MeshWalk.degR_nonneg {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)ᵐᵒᵖ) (t : RayA0 D v₀) : 0 ≤ (degR D v₀) (wtR D v₀ t)

theorem MultiplicativeBasisDeformations.MeshWalk.sepR_deg {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)ᵐᵒᵖ) (r s : RayA0 D v₀) (h1 : srcR D v₀ r = srcR D v₀ s) (h2 : tgtR D v₀ r = tgtR D v₀ s) (hw : (degR D v₀) (wtR D v₀ r) = (degR D v₀) (wtR D v₀ s)) : r = s

Rays of A₀ with the same endpoints and weight are equal (one line per length degree in each corner).

theorem MultiplicativeBasisDeformations.MeshWalk.sepR {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)ᵐᵒᵖ) (r s : RayA0 D v₀) (h1 : srcR D v₀ r = srcR D v₀ s) (h2 : tgtR D v₀ r = tgtR D v₀ s) (hw : wtR D v₀ r = wtR D v₀ s) : r = s

noncomputable def MultiplicativeBasisDeformations.MeshWalk.A0Tab {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)ᵐᵒᵖ) : RaySys.Tab D.PV (RayA0 D v₀) (WP Q c v₀ D)

The ray table P = ray A₀ with weights in W(P).

noncomputable def MultiplicativeBasisDeformations.MeshWalk.thetaA0 {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)ᵐᵒᵖ) : ↥((A0Tab D v₀ hF).Lin k) ≃ₐ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ

kP ≅ A₀ (Proposition 4.14).

theorem MultiplicativeBasisDeformations.MeshWalk.thetaA0_b {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)ᵐᵒᵖ) (t : RayA0 D v₀) : (thetaA0 D v₀ hF) ((A0Tab D v₀ hF).b k t) = (basisR D v₀ hF) t

theorem MultiplicativeBasisDeformations.MeshWalk.A0Tab_isRepresentationFinite {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)ᵐᵒᵖ) : IsRepresentationFinite k ↥((A0Tab D v₀ hF).Lin k)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.A0Sys {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)ᵐᵒᵖ) : RaySys.Sys D.PV (RayA0 D v₀) (WP Q c v₀ D)

Setting 8.4 for A₀.

Other weight lattices

Any mesh weight Wt with values in L, with a homomorphism dg : L → ℤ recovering the length, gives ray weights Wt.res [x, y, g] making the same table a ray table with weights in L.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.wtLat {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) {L' : Type} [AddCommGroup L'] (Wt : MeshWt Q L') (t : RayA0 D v₀) : L'

The ray weights in L'.

theorem MultiplicativeBasisDeformations.MeshWalk.dg_wtLat {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) {L' : Type} [AddCommGroup L'] (Wt : MeshWt Q L') (dg : L' →+ ℤ) (hdg : dg.comp (MeshWt.res c D Wt) = MeshWt.res c D lenW) (t : RayA0 D v₀) : dg (wtLat D v₀ Wt t) = (degR D v₀) (wtR D v₀ t)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.A0TabL {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)ᵐᵒᵖ) {L' : Type} [AddCommGroup L'] (Wt : MeshWt Q L') (dg : L' →+ ℤ) (hdg : dg.comp (MeshWt.res c D Wt) = MeshWt.res c D lenW) : RaySys.Tab D.PV (RayA0 D v₀) L'

The ray table of A₀ with weights in L'.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.thetaA0L {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)ᵐᵒᵖ) {L' : Type} [AddCommGroup L'] (Wt : MeshWt Q L') (dg : L' →+ ℤ) (hdg : dg.comp (MeshWt.res c D Wt) = MeshWt.res c D lenW) : ↥((A0TabL D v₀ hF Wt dg hdg).Lin k) ≃ₐ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ

kP ≅ A₀ for the table with weights in L'.

theorem MultiplicativeBasisDeformations.MeshWalk.thetaA0L_b {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)ᵐᵒᵖ) {L' : Type} [AddCommGroup L'] (Wt : MeshWt Q L') (dg : L' →+ ℤ) (hdg : dg.comp (MeshWt.res c D Wt) = MeshWt.res c D lenW) (t : RayA0 D v₀) : (thetaA0L D v₀ hF Wt dg hdg) ((A0TabL D v₀ hF Wt dg hdg).b k t) = (basisR D v₀ hF) t

theorem MultiplicativeBasisDeformations.MeshWalk.A0TabL_isRepresentationFinite {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)ᵐᵒᵖ) {L' : Type} [AddCommGroup L'] (Wt : MeshWt Q L') (dg : L' →+ ℤ) (hdg : dg.comp (MeshWt.res c D Wt) = MeshWt.res c D lenW) : IsRepresentationFinite k ↥((A0TabL D v₀ hF Wt dg hdg).Lin k)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.A0SysL {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)ᵐᵒᵖ) {L' : Type} [AddCommGroup L'] (Wt : MeshWt Q L') (dg : L' →+ ℤ) (hdg : dg.comp (MeshWt.res c D Wt) = MeshWt.res c D lenW) : RaySys.Sys D.PV (RayA0 D v₀) L'

Setting 8.4 for A₀ with weights in L'.