Proposition 12.8: the polynomial mesh comparison

deformation-refinements.tex (prop:polynomial-mesh-comparison): "Let m + Σ_{i∈I} t_i μ_i be an associative family satisfying the hypotheses of Proposition 7.9 […], now indexed by I = I₀. There are polynomial lifts of the normalized modules, their morphisms, and their mesh presentations for which the retained mesh coefficients are F_i(t) = a_i t_i, a_i ∈ k^*. After every specialization to k, these modules exhaust the indecomposables of the fibre algebra."

polynomialMeshComparison, for the mesh category C of mesh data whose positive degrees are radical (as for k(Γ_A), IndSkeleton.arHrad). Hypotheses: the family μ_i (FamHyp: internal degrees q_i ≥ 1, normalized, m + Σ_i t_i μ_i associative for all t), of characters χ_i for a mesh weight W, with coordinates χ_i ↦ e_i (part of an integer basis, Proposition 7.5); retained rows R_i of length q_i + 2 and relative weight χ_i whose classes span the cokernels of the mesh derivatives (CokerSpan); no μ_i is a coboundary (its class in HH²(A₀)_{χ_i} is nonzero). Conclusions, for every t : I → k:

• the lifted actions on the evaluated modules and the lifted arrows are polynomial in t;
• the lifted arrows satisfy r_x = Σ_i a_i t_i R_i with a_i ≠ 0, and present the lifted category of the fibre: the realization of kQ is surjective, with kernel (𝔪^{N+1}, r_x − Σ_i a_i t_i R_i);
• the lifted modules exhaust the indecomposable modules of the fibre algebra (Corollary 12.1).

theorem MultiplicativeBasisDeformations.MeshWalk.polynomialMeshComparison {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} {hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y)} [Fintype ↑Q.nonprojective] [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {I : Type} [Fintype I] [DecidableEq I] {μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} {qd : I → ℕ} {Wt : Type} [AddCommGroup Wt] {χ : I → Wt} {coords : Wt →+ I → ℤ} [Infinite k] (H : FamHyp D hfin μ qd) (W : MeshWt Q Wt) (hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)) (hco : ∀ (i : I), coords (χ i) = Pi.single i 1) (J : D.InjData) (h1 : DegOne D) (hrad : ∀ (x y : V) (d : ℕ), 1 ≤ d → ∀ f ∈ ScalarMeshCategory.degreePart c d x y, f ∈ L.rad x y) (Rw : I → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x) (hlen : ∀ (i : I), (Rw i).snd.length = qd i + 2) (hwt : ∀ (i : I), W.pw (Rw i).snd = W.ν (Rw i).fst + χ i) (hS : ScalarMeshCategory.CokerSpan c (Set.range Rw)) (hnc : ∀ (j : I), ¬∃ (Hc : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ), (∀ (p : ℤ) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), (galgA0 D hfin).gr.IsHom p a → (galgA0 D hfin).gr.IsHom (p + ↑(qd j)) (Hc a)) ∧ μ j = GExt.hcobdry Hc) : ∃ (A : ArrowL H W hχ J h1 hco) (a : I → k) (N : ℕ), (∀ (i : I), a i ≠ 0) ∧ (∀ (X : V), IsPoly fun (t : I → k) => (famAct H W hχ J h1 hco t X).tot) ∧ (∀ {y x : V} (b : y ⟶ x), IsPoly fun (t : I → k) => toLin (twArrow A t b)) ∧ ∀ (t : I → k), (∀ (x : ↑Q.nonprojective), (PathReal.realizeR k (fun {y x : V} => twArrow A t) ↑(Q.tau x) ↑x) (meshRelation c x) = ∑ i : I, (a i * t i) • (PathReal.realizeR k (fun {y x : V} => twArrow A t) ↑(Q.tau x) ↑x) (rowQ Rw i x)) ∧ (∀ {y x : V} (f : FB (famLifts H W hχ J h1 hco t) y ⟶ FB (famLifts H W hχ J h1 hco t) x), ∃ (F : LinearPaths.obj y ⟶ LinearPaths.obj x), (PathReal.realizeR k (fun {y x : V} => twArrow A t) y x) F = f) ∧ (∀ {y x : V} (F : FlatPert.Hm k y x), (PathReal.realizeR k (fun {y x : V} => twArrow A t) y x) F = 0 ↔ F ∈ (FlatPert.idealB (FlatPert.meshPres c) (ftp Rw a t) ⋯ N).I y x) ∧ (∀ (x : V), IsFiniteIndecomposable k (Fib (famAM H t)) (FB (famLifts H W hχ J h1 hco t) x)) ∧ (∀ (x y : V), Nonempty (FB (famLifts H W hχ J h1 hco t) x ≅ FB (famLifts H W hχ J h1 hco t) y) → x = y) ∧ ∀ (M : RightModuleCat (Fib (famAM H t))), IsFiniteIndecomposable k (Fib (famAM H t)) M → ∃ (x : V), Nonempty (M ≅ FB (famLifts H W hχ J h1 hco t) x)

Proposition 12.8 (polynomial mesh comparison).