Proposition 7.9 on A₀ for characters in any lattice

The setting of FamilyCriterionA0.lean with the dual mesh weights replaced by an arbitrary mesh weight W with values in a lattice Lt and a degree map dg : Lt → ℤ recovering the length (dg ∘ W.res = lenW.res). The characters are the relative row weights rowCharG W Rw i; instead of the dual-weight identities, the hypotheses are that these characters are pairwise distinct and part of an integer basis of Lt (Proposition 7.5 for Lt = W(P)). The definitions and proofs are those of the dual-weight case (SysG, ΘG, VxG, HH2NonzeroG, I0G, famMulG, fibAMG, familyCriterion_G).

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.SysG {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) : RaySys.Sys D.PV (RayA0 D v₀) Lt

The ray system of A₀ with the dual weights.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.MeshWalk.ΘG {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) : ↥((SysG D v₀ hF W dg hdg).P.Lin k) ≃ₐ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ

kP ≅ A₀.

theorem MultiplicativeBasisDeformations.MeshWalk.ΘG_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)ᵐᵒᵖ) {Lt : Type} [AddCommGroup Lt] (W : MeshWt Q Lt) (dg : Lt →+ ℤ) (hdg : dg.comp (MeshWt.res c D W) = MeshWt.res c D lenW) (t : RayA0 D v₀) : (ΘG D v₀ hF W dg hdg) ((SysG D v₀ hF W dg hdg).P.b k t) = (basisR D v₀ hF) t

theorem MultiplicativeBasisDeformations.MeshWalk.SysG_deg_wt {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) (t : RayA0 D v₀) {p : Quiver.Path ↑(↑t).1 ↑(↑t).2.1} (hp : (degW Q v₀).deg p = (↑t).2.2) : (SysG D v₀ hF W dg hdg).P.deg ((SysG D v₀ hF W dg hdg).P.wt t) = ↑p.length

theorem MultiplicativeBasisDeformations.MeshWalk.ΘG_lenHom {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) (t : RayA0 D v₀) : (lenA0 D ⋯).IsHom ((SysG D v₀ hF W dg hdg).P.deg ((SysG D v₀ hF W dg hdg).P.wt t)).toNat ((ΘG D v₀ hF W dg hdg) ((SysG D v₀ hF W dg hdg).P.b k t))

The ray basis is length-homogeneous.

theorem MultiplicativeBasisDeformations.MeshWalk.ΘG_latHom {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) (t : RayA0 D v₀) : (latA0 W ⋯ D).IsHom ((SysG D v₀ hF W dg hdg).P.wt t) ((ΘG D v₀ hF W dg hdg) ((SysG D v₀ hF W dg hdg).P.b k t))

The ray basis is weight-homogeneous.

theorem MultiplicativeBasisDeformations.MeshWalk.FpA0_e_ΘG {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) (i : Fin (FpA0 D v₀ hF).m) : (FpA0 D v₀ hF).e i = (ΘG D v₀ hF W dg hdg) ((SysG D v₀ hF W dg hdg).P.b k ((SysG D v₀ hF W dg hdg).P.e ((Fintype.equivFin D.PV).symm i)))

noncomputable def MultiplicativeBasisDeformations.MeshWalk.VxG {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) : (lenA0 D ⋯).Vertices

The vertex idempotents of A₀ as degree-zero vertices.

theorem MultiplicativeBasisDeformations.MeshWalk.VxG_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)ᵐᵒᵖ) {Lt : Type} [AddCommGroup Lt] (W : MeshWt Q Lt) (dg : Lt →+ ℤ) (hdg : dg.comp (MeshWt.res c D W) = MeshWt.res c D lenW) (i : Fin (VxG D v₀ hF W dg hdg).n) : ∃ (x : D.PV), (VxG D v₀ hF W dg hdg).e i = (ΘG D v₀ hF W dg hdg) ((SysG D v₀ hF W dg hdg).P.b k ((SysG D v₀ hF W dg hdg).P.e x))

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.rowCharG {V : Type} [Quiver V] {Q : TranslationQuiver V} {Lt : Type} [AddCommGroup Lt] (W : MeshWt Q Lt) {ι : Type} (Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) (i : ι) : Lt

The character χ_i of a row of Proposition 6.1.

def MultiplicativeBasisDeformations.MeshWalk.HH2NonzeroG {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) (i : ι) : Prop

A row with a nonzero space HH²(A₀)_{χ_i} in positive internal degree.

@[reducible, inline]

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

The index set I₀.

@[instance_reducible]

noncomputable instance MultiplicativeBasisDeformations.MeshWalk.instFintypeI0G {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 ι] (Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) : Fintype (I0G D v₀ hF W dg hdg Rw)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.famMulG {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 ι] {Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x} (μ : I0G D v₀ hF W dg hdg Rw → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ) (lam : I0G D v₀ hF W dg hdg Rw → k) : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ

The family product m + Σ λ_i μ_i.

theorem MultiplicativeBasisDeformations.MeshWalk.famMulG_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)ᵐᵒᵖ) {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 ι] (Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) (μ : I0G D v₀ hF W dg hdg Rw → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ) (lam : I0G D v₀ hF W dg hdg Rw → k) (a b : (CatAlg.Alg D.F0)ᵐᵒᵖ) : ((famMulG μ lam) a) b = a * b + ∑ i : I0G D v₀ hF W dg hdg Rw, lam i • ((μ i) a) b

theorem MultiplicativeBasisDeformations.MeshWalk.mLam_reindexG {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 ι] (Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) {n : ℕ} (e : Fin n ≃ I0G D v₀ hF W dg hdg Rw) (μ : I0G D v₀ hF W dg hdg Rw → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ) (lam : Fin n → k) (a b : (CatAlg.Alg D.F0)ᵐᵒᵖ) : ((LenGrading.mLam (fun (j : Fin n) => μ (e j)) lam) a) b = ((famMulG μ fun (i : I0G D v₀ hF W dg hdg Rw) => lam (e.symm i)) a) b

noncomputable def MultiplicativeBasisDeformations.MeshWalk.fibAMG {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 ι] {Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x} {μ : I0G D v₀ hF W dg hdg Rw → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (hrel : ∀ (i : I0G D v₀ hF W dg hdg Rw), LenGrading.IsRel₂ (VxG D v₀ hF W dg hdg) (μ i)) (hassoc : ∀ (lam : I0G D v₀ hF W dg hdg Rw → k) (a b z : (CatAlg.Alg D.F0)ᵐᵒᵖ), ((famMulG μ lam) (((famMulG μ lam) a) b)) z = ((famMulG μ lam) a) (((famMulG μ lam) b) z)) (lam : I0G D v₀ hF W dg hdg Rw → k) : AssocMul k (CatAlg.Alg D.F0)ᵐᵒᵖ

A binary or scalar fibre: the family product at lam as an associative unital product.

theorem MultiplicativeBasisDeformations.MeshWalk.familyCriterion_G {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 ι] (Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) (J : D.InjData) (h1 : DegOne D) [Fintype ↑Q.nonprojective] (hχinj : Function.Injective fun (i : ι) => rowCharG W Rw i) (hbasisι : ∃ (κ : Type) (bL : Module.Basis κ ℤ Lt) (jι : ι → κ), Function.Injective jι ∧ ∀ (i : ι), bL (jι i) = rowCharG W Rw i) (hS : ScalarMeshCategory.CokerSpan c (Set.range Rw)) (μ : I0G D v₀ hF W dg hdg Rw → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ) (hrel : ∀ (i : I0G D v₀ hF W dg hdg Rw), LenGrading.IsRel₂ (VxG D v₀ hF W dg hdg) (μ i)) (hchar : ∀ (i : I0G D v₀ hF W dg hdg Rw), (latA0 W ⋯ D).Char₂ (rowCharG W Rw ↑i) (μ i)) (hcoc : ∀ (i : I0G D v₀ hF W dg hdg Rw), LenGrading.IsCocycle₂ (μ i)) (hnz : ∀ (i : I0G D v₀ hF W dg hdg Rw), ¬∃ (f : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ), μ i = LenGrading.cobdry k f) (hassoc : ∀ (lam : I0G D v₀ hF W dg hdg Rw → k) (a b z : (CatAlg.Alg D.F0)ᵐᵒᵖ), ((famMulG μ lam) (((famMulG μ lam) a) b)) z = ((famMulG μ lam) a) (((famMulG μ lam) b) z)) (hfib : ∀ (lam : I0G D v₀ hF W dg hdg Rw → k), (∀ (i : I0G D v₀ hF W dg hdg Rw), lam i = 0 ∨ lam i = 1) → IsNormedMultiplicativeBasis ((basisR D v₀ hF).map (Fib.toΛ (fibAMG hrel hassoc lam)).symm) ∧ ∃ (F : PrimitiveIdempotents (Fib (fibAMG hrel hassoc lam))) (ιF : D.PV ≃ Fin F.m), F.IsRayPres (A0Mult D v₀ hF) ιF fun (r : RayA0 D v₀) => (Fib.toΛ (fibAMG hrel hassoc lam)).symm ((basisR D v₀ hF) r)) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Pf : PosFiltration (lenA0 D ⋯) B) : ∃ (lam : I0G D v₀ hF W dg hdg Rw → k) (_ : ∀ (i : I0G D v₀ hF W dg hdg Rw), lam i = 0 ∨ lam i = 1) (Ψ : (CatAlg.Alg D.F0)ᵐᵒᵖ ≃ₗ[k] B), (∀ (a b : (CatAlg.Alg D.F0)ᵐᵒᵖ), Ψ (((famMulG μ lam) a) b) = Ψ a * Ψ b) ∧ (∀ (d : ℕ), Submodule.map (↑Ψ) ((lenA0 D ⋯).geSub d) = Pf.F d) ∧ IsNormedMultiplicativeBasis ((basisR D v₀ hF).map Ψ) ∧ (∃ (F : PrimitiveIdempotents B) (ιF : D.PV ≃ Fin F.m), F.IsRayPres (A0Mult D v₀ hF) ιF fun (r : RayA0 D v₀) => Ψ ((basisR D v₀ hF) r)) ∧ ∀ (r : RayA0 D v₀), ∃ (t : k), t ≠ 0 ∧ (Pf.σ ((SysG D v₀ hF W dg hdg).P.deg ((SysG D v₀ hF W dg hdg).P.wt r)).toNat) (Ψ ((basisR D v₀ hF) r)) = t • (basisR D v₀ hF) r

Proposition 7.9 on A₀ (prop:family-criterion): for the rows and characters of Proposition 6.1 and any family μ_i, i ∈ I₀, of normalized S-relative cocycles of character χ_i with nonzero classes, whose family product is associative and whose binary fibres have the basis of kP as a normed multiplicative basis with ray category P: every positive filtered deformation B of A₀ is isomorphic to a binary fibre; the transported basis is a normed multiplicative ray basis of B presenting P, and the leading term of the image of each ray vector b_r is a nonzero multiple of b_r.

def MultiplicativeBasisDeformations.MeshWalk.FamilyCriterionStmt {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 ι] (Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) [Fintype ↑Q.nonprojective] {B : Type u} [Ring B] [Algebra k B] (Pf : PosFiltration (lenA0 D ⋯) B) : Prop

The conclusion of Proposition 7.9 on A₀ for a positive filtered deformation B, as a predicate on the data: for every family with the hypotheses (1)–(3), the conclusions hold.

theorem MultiplicativeBasisDeformations.MeshWalk.familyCriterionStmt_G {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 ι] (Rw : ι → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) (J : D.InjData) (h1 : DegOne D) [Fintype ↑Q.nonprojective] (hS : ScalarMeshCategory.CokerSpan c (Set.range Rw)) (hχinj : Function.Injective fun (i : ι) => rowCharG W Rw i) (hbasisι : ∃ (κ : Type) (bL : Module.Basis κ ℤ Lt) (jι : ι → κ), Function.Injective jι ∧ ∀ (i : ι), bL (jι i) = rowCharG W Rw i) {B : Type u} [Ring B] [Algebra k B] [FiniteDimensional k B] (Pf : PosFiltration (lenA0 D ⋯) B) : FamilyCriterionStmt D v₀ hF W dg hdg Rw Pf