Polynomial lifts of the evaluated modules (Proposition 12.8, first part)

deformation-refinements.tex: for the family m + Σ_i t_i μ_i, "keep the underlying modules M_i ⊗ K and their vertex actions fixed", and lift the actions degree by degree, with the choices made separately in each degree and weight; all entries are polynomials.

Here: the fibre at t is the algebra Fib (famMul t) with its length filtration (famPF), split by the identity (famSplit); its deformation terms are [q = 0]·m + Σ_{q_i = q} t_i μ_i (famSplit_μ). The lifted actions at t = 1 are chosen with relative weights in the monoid of the χ_i (exists_actFam_cone), and their twists are lifts for every fibre (famLifts), which are polynomial in t and specialize to the chosen lifts at t = 1.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.famMul {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) {I : Type} [Fintype I] (μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ) (t : I → k) : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ

The family m + Σ_i t_i μ_i.

structure MultiplicativeBasisDeformations.MeshWalk.FamHyp {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)) {I : Type} [Fintype I] (μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ) (qd : I → ℕ) : Prop

The hypotheses on the family: positive internal degrees, normalized, associative for every value of the parameters.

• q_pos (i : I) : 1 ≤ qd i
• deg (i : I) : GExt.HDeg (galgA0 D hfin) (μ i) ↑(qd i)
• one_left (i : I) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) : ((μ i) 1) a = 0
• one_right (i : I) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ) : ((μ i) a) 1 = 0
• assoc (t : I → k) (a b c : (CatAlg.Alg D.F0)ᵐᵒᵖ) : ((famMul D μ t) (((famMul D μ t) a) b)) c = ((famMul D μ t) a) (((famMul D μ t) b) c)

theorem MultiplicativeBasisDeformations.MeshWalk.famMul_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} [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)ᵐᵒᵖ} (t : I → k) (a b : (CatAlg.Alg D.F0)ᵐᵒᵖ) : ((famMul D μ t) a) b = a * b + ∑ i : I, t i • ((μ i) a) b

noncomputable def MultiplicativeBasisDeformations.MeshWalk.famAM {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)} [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 → ℕ} (H : FamHyp D hfin μ qd) (t : I → k) : AssocMul k (CatAlg.Alg D.F0)ᵐᵒᵖ

The fibre product as an associative product.

theorem MultiplicativeBasisDeformations.MeshWalk.len_isHom_of_hdeg {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)} [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 → ℕ} {i : I} (h : GExt.HDeg (galgA0 D hfin) (μ i) ↑(qd i)) {d e : ℕ} {a b : (CatAlg.Alg D.F0)ᵐᵒᵖ} (ha : (lenA0 D hfin).IsHom d a) (hb : (lenA0 D hfin).IsHom e b) : (lenA0 D hfin).IsHom (d + e + qd i) (((μ i) a) b)

theorem MultiplicativeBasisDeformations.MeshWalk.famHdef {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)} [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 → ℕ} (H : FamHyp D hfin μ qd) (t : I → k) (d e : ℕ) (a b : (CatAlg.Alg D.F0)ᵐᵒᵖ) : (lenA0 D hfin).IsHom d a → (lenA0 D hfin).IsHom e b → (lenA0 D hfin).Ge (d + e + 1) (((famAM H t).mm a) b - a * b)

noncomputable def MultiplicativeBasisDeformations.MeshWalk.famPF {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)} [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 → ℕ} (H : FamHyp D hfin μ qd) (t : I → k) : PosFiltration (lenA0 D hfin) (Fib (famAM H t))

The fibre at t as a positive filtered deformation of A₀.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.famSplit {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)} [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 → ℕ} (H : FamHyp D hfin μ qd) (t : I → k) : (famPF H t).Split

The identity splitting of a fibre.

theorem MultiplicativeBasisDeformations.MeshWalk.famSplit_star {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)} [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 → ℕ} (H : FamHyp D hfin μ qd) (t : I → k) (a b : (CatAlg.Alg D.F0)ᵐᵒᵖ) : ((famSplit H t).star a) b = ((famMul D μ t) a) b

noncomputable def MultiplicativeBasisDeformations.MeshWalk.famμ {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} {I : Type} [Fintype I] (μ : I → (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ) (qd : I → ℕ) (t : I → k) (q : ℕ) : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ

The degree-q term of the fibre product: [q = 0]·m + Σ_{q_i = q} t_i μ_i.

theorem MultiplicativeBasisDeformations.MeshWalk.lenBil_ext {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {f g : (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ} (h : ∀ (d e : ℕ) (a b : (CatAlg.Alg D.F0)ᵐᵒᵖ), (lenA0 D hfin).IsHom d a → (lenA0 D hfin).IsHom e b → (f a) b = (g a) b) : f = g

Bilinear maps on A₀ agreeing on homogeneous elements agree.

theorem MultiplicativeBasisDeformations.MeshWalk.famSplit_μ {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)} [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 → ℕ} (H : FamHyp D hfin μ qd) (t : I → k) (q : ℕ) : (famSplit H t).μ q = famμ μ qd t q

Weights

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.MeshWalk.cone {I Wt : Type} [AddCommGroup Wt] (χ : I → Wt) : AddSubmonoid Wt

The monoid spanned by the characters χ_i.

theorem MultiplicativeBasisDeformations.MeshWalk.cone_nonneg {I : Type} [Fintype I] [DecidableEq I] {Wt : Type} [AddCommGroup Wt] {χ : I → Wt} {coords : Wt →+ I → ℤ} (hco : ∀ (i : I), coords (χ i) = Pi.single i 1) (γ : Wt) : γ ∈ cone χ → ∀ (i : I), 0 ≤ coords γ i

theorem MultiplicativeBasisDeformations.MeshWalk.cone_eq_sum {I : Type} [Fintype I] [DecidableEq I] {Wt : Type} [AddCommGroup Wt] {χ : I → Wt} {coords : Wt →+ I → ℤ} (hco : ∀ (i : I), coords (χ i) = Pi.single i 1) (γ : Wt) : γ ∈ cone χ → γ = ∑ i : I, (coords γ i).toNat • χ i

theorem MultiplicativeBasisDeformations.MeshWalk.cone_pointed {I : Type} [Fintype I] [DecidableEq I] {Wt : Type} [AddCommGroup Wt] {χ : I → Wt} {coords : Wt →+ I → ℤ} (hco : ∀ (i : I), coords (χ i) = Pi.single i 1) (γ : Wt) : γ ∈ cone χ → ∀ δ ∈ cone χ, γ + δ = 0 → γ = 0

theorem MultiplicativeBasisDeformations.MeshWalk.χ_ne_zero {I : Type} [Fintype I] [DecidableEq I] {Wt : Type} [AddCommGroup Wt] {χ : I → Wt} {coords : Wt →+ I → ℤ} (hco : ∀ (i : I), coords (χ i) = Pi.single i 1) (i : I) : χ i ≠ 0

theorem MultiplicativeBasisDeformations.MeshWalk.ch_χ {k : Type u} [Field k] {I : Type} [Fintype I] [DecidableEq I] {Wt : Type} [AddCommGroup Wt] {χ : I → Wt} {coords : Wt →+ I → ℤ} (hco : ∀ (i : I), coords (χ i) = Pi.single i 1) (t : I → k) (i : I) : MGr.ch coords t (χ i) = t i

theorem MultiplicativeBasisDeformations.MeshWalk.ch_zero' {k : Type u} [Field k] {I : Type} [Fintype I] [DecidableEq I] {Wt : Type} [AddCommGroup Wt] {coords : Wt →+ I → ℤ} (t : I → k) : MGr.ch coords t 0 = 1

theorem MultiplicativeBasisDeformations.MeshWalk.wtCompat {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)) [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {Wt : Type} [AddCommGroup Wt] (W : MeshWt Q Wt) (X : V) : GExt.WtCompat (gmodEv D hfin X) (grA0 W hfin D) (grEv W hfin D X)

The weight gradings of A₀ and of the evaluated modules are compatible.

theorem MultiplicativeBasisDeformations.MeshWalk.sum_smul_proj_hom {k : Type u} [Field k] {Wt : Type} [AddCommGroup Wt] {N : Type u_1} [AddCommGroup N] [Module k N] (G : MGr k Wt N) (f : Wt → k) {γ : Wt} {x : N} (hx : G.IsHom γ x) : ∑ δ ∈ G.supp, f δ • (G.proj δ) x = f γ • x

A weighted sum of the components of a homogeneous element.

theorem MultiplicativeBasisDeformations.MeshWalk.famμ_cone {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)} [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] (W : MeshWt Q Wt) {χ : I → Wt} (hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)) (q : ℕ) : MGr.ConeBil 0 (famμ μ qd 1 q)

The deformation terms have relative weights in the cone.

theorem MultiplicativeBasisDeformations.MeshWalk.famμ_bottom {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)} [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] (W : MeshWt Q Wt) {χ : I → Wt} {coords : Wt →+ I → ℤ} (hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)) (hco : ∀ (i : I), coords (χ i) = Pi.single i 1) (q : ℕ) (hq : 1 ≤ q) (α β : Wt) (a b : (CatAlg.Alg D.F0)ᵐᵒᵖ) : (grA0 W hfin D).IsHom α a → (grA0 W hfin D).IsHom β b → ((grA0 W hfin D).proj (α + β)) (((famμ μ qd 1 q) a) b) = 0

The positive-degree deformation terms have no relative weight 0.

theorem MultiplicativeBasisDeformations.MeshWalk.twb_famμ {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)} [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] (W : MeshWt Q Wt) {χ : I → Wt} {coords : Wt →+ I → ℤ} (hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)) (hco : ∀ (i : I), coords (χ i) = Pi.single i 1) (t : I → k) (q : ℕ) : MGr.twb coords (grA0 W hfin D) (grA0 W hfin D) (grA0 W hfin D) t 0 (famμ μ qd 1 q) = famμ μ qd t q

Twisting the fibre at 1 gives the fibre at t.

Lifted actions

theorem MultiplicativeBasisDeformations.MeshWalk.isShift_twb {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {I : Type} [Fintype I] [DecidableEq I] {Wt : Type} [AddCommGroup Wt] (W : MeshWt Q Wt) {coords : Wt →+ I → ℤ} {X : V} (t : I → k) {n : ℤ} {φ : CatAlg.Rep D.F0 (meshFam Q c X) →ₗ[k] (CatAlg.Alg D.F0)ᵐᵒᵖ →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c X)} (hφ : GExt.IsShift (gmodEv D hfin X) n φ) : GExt.IsShift (gmodEv D hfin X) n (MGr.twb coords (grEv W hfin D X) (grA0 W hfin D) (grEv W hfin D X) t 0 φ)

theorem MultiplicativeBasisDeformations.MeshWalk.twb_act {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)} [hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)] {I : Type} [Fintype I] [DecidableEq I] {Wt : Type} [AddCommGroup Wt] (W : MeshWt Q Wt) {coords : Wt →+ I → ℤ} (X : V) (t : I → k) : MGr.twb coords (grEv W hfin D X) (grA0 W hfin D) (grEv W hfin D X) t 0 (gmodEv D hfin X).act = (gmodEv D hfin X).act

theorem MultiplicativeBasisDeformations.MeshWalk.exists_actFam_one {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)} [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 → ℕ} (H : FamHyp D hfin μ qd) {Wt : Type} [AddCommGroup Wt] (W : MeshWt Q Wt) {χ : I → Wt} {coords : Wt →+ I → ℤ} (hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)) (J : D.InjData) (h1 : DegOne D) (hco : ∀ (i : I), coords (χ i) = Pi.single i 1) (X : V) : ∃ (A : GExt.ActFam ((famSplit H 1).posDef ⋯) (gmodEv D hfin X)), (∀ (n : ℕ), MGr.ConeBil 0 (A.ν n)) ∧ ∀ (n : ℕ), 1 ≤ n → ∀ (β α : Wt) (m : CatAlg.Rep D.F0 (meshFam Q c X)) (a : (CatAlg.Alg D.F0)ᵐᵒᵖ), (grEv W hfin D X).IsHom β m → (grA0 W hfin D).IsHom α a → ((grEv W hfin D X).proj (β + α)) (((A.ν n) m) a) = 0

Homogeneous lifted actions at t = 1, without corrections of relative weight 0.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.act1 {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)} [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 → ℕ} (H : FamHyp D hfin μ qd) {Wt : Type} [AddCommGroup Wt] (W : MeshWt Q Wt) {χ : I → Wt} {coords : Wt →+ I → ℤ} (hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)) (J : D.InjData) (h1 : DegOne D) (hco : ∀ (i : I), coords (χ i) = Pi.single i 1) (X : V) : GExt.ActFam ((famSplit H 1).posDef ⋯) (gmodEv D hfin X)

The chosen homogeneous lifted action at t = 1.

theorem MultiplicativeBasisDeformations.MeshWalk.act1_cone {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)} [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 → ℕ} (H : FamHyp D hfin μ qd) {Wt : Type} [AddCommGroup Wt] (W : MeshWt Q Wt) {χ : I → Wt} {coords : Wt →+ I → ℤ} (hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)) (J : D.InjData) (h1 : DegOne D) (hco : ∀ (i : I), coords (χ i) = Pi.single i 1) (X : V) (n : ℕ) : MGr.ConeBil 0 ((act1 H W hχ J h1 hco X).ν n)

theorem MultiplicativeBasisDeformations.MeshWalk.act1_bottom {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)} [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 → ℕ} (H : FamHyp D hfin μ qd) {Wt : Type} [AddCommGroup Wt] (W : MeshWt Q Wt) {χ : I → Wt} {coords : Wt →+ I → ℤ} (hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)) (J : D.InjData) (h1 : DegOne D) (hco : ∀ (i : I), coords (χ i) = Pi.single i 1) (X : V) (n : ℕ) (hn : 1 ≤ n) {β α : Wt} {m : CatAlg.Rep D.F0 (meshFam Q c X)} {a : (CatAlg.Alg D.F0)ᵐᵒᵖ} (hm : (grEv W hfin D X).IsHom β m) (ha : (grA0 W hfin D).IsHom α a) : ((grEv W hfin D X).proj (β + α)) ((((act1 H W hχ J h1 hco X).ν n) m) a) = 0

noncomputable def MultiplicativeBasisDeformations.MeshWalk.famAct {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)} [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 → ℕ} (H : FamHyp D hfin μ qd) {Wt : Type} [AddCommGroup Wt] (W : MeshWt Q Wt) {χ : I → Wt} {coords : Wt →+ I → ℤ} (hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)) (J : D.InjData) (h1 : DegOne D) (hco : ∀ (i : I), coords (χ i) = Pi.single i 1) [Infinite k] (t : I → k) (X : V) : GExt.ActFam ((famSplit H t).posDef ⋯) (gmodEv D hfin X)

The twisted lifted action at the fibre t.

noncomputable def MultiplicativeBasisDeformations.MeshWalk.famLifts {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)} [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 → ℕ} (H : FamHyp D hfin μ qd) {Wt : Type} [AddCommGroup Wt] (W : MeshWt Q Wt) {χ : I → Wt} {coords : Wt →+ I → ℤ} (hχ : ∀ (i : I), HasChar W hfin D (χ i) (μ i)) (J : D.InjData) (h1 : DegOne D) (hco : ∀ (i : I), coords (χ i) = Pi.single i 1) [Infinite k] (t : I → k) : Lifts D hfin (famPF H t)

Polynomial lifts of the evaluated modules: filtered lifts for every fibre.