The polynomial mesh relations (Proposition 12.8, F_i(t) = a_i t_i) #
deformation-refinements.tex: "Give t_i total weight −χ_i […] The choices above, made
separately in each weight, make F_j homogeneous of coefficient weight χ_j. […]
Lemma 12.7 therefore gives F_j = a_j t_j."
The lifted arrows at t = 1 (with the normal form r_x = Σ_i λ_i R_i) are twisted to every
fibre (twArrow): the twist of a component of relative weight γ is multiplied by t^{coords γ}.
The twisted arrows are morphisms of the lifted modules of the fibre t, realize every path by the
twist of its realization (toLin_pathR_tw), and satisfy r_x = Σ_i λ_i t_i R_i (tw_relation):
the retained coefficients are F_i(t) = λ_i t_i.
The lifted actions at the fibre t #
theorem
MultiplicativeBasisDeformations.MeshWalk.famAct_tot
{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 → ℕ}
(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)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.famLifts_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)}
[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 → ℕ}
{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)
(m : CatAlg.Rep D.F0 (meshFam Q c X))
(b : Fib (famAM H t))
:
theorem
MultiplicativeBasisDeformations.MeshWalk.act1_tot_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)}
[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 → ℕ}
{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]
(X : V)
:
MGr.ConeBil 0 (act1 H W hχ J h1 hco X).tot
theorem
MultiplicativeBasisDeformations.MeshWalk.toLin_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)}
[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 → ℕ}
{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]
{y x : V}
(f : FB (Ls1 H W hχ J h1 hco) y ⟶ FB (Ls1 H W hχ J h1 hco) x)
(m : CatAlg.Rep D.F0 (meshFam Q c y))
(a : (CatAlg.Alg D.F0)ᵐᵒᵖ)
:
Twisted arrows #
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.twArrow
{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 → ℕ}
{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]
(A : ArrowL H W hχ J h1 hco)
(t : I → k)
{y x : V}
(a : y ⟶ x)
:
The twisted lifted arrow at the fibre t.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.toLin_twArrow
{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 → ℕ}
{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]
(A : ArrowL H W hχ J h1 hco)
(t : I → k)
{y x : V}
(a : y ⟶ x)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.toLin_pathR_tw
{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 → ℕ}
{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]
(A : ArrowL H W hχ J h1 hco)
(t : I → k)
{y x : V}
(p : Quiver.Path y x)
:
toLin (PathReal.pathR (fun {y x : V} => twArrow A t) p) = MGr.twl coords (grEv W hfin D y) (grEv W hfin D x) t (W.pw p) (toLin (PathReal.pathR (fun {y x : V} => A.g) p))
Twisted arrows realize paths by the twists of the realizations.
theorem
MultiplicativeBasisDeformations.MeshWalk.toLin_realize_tw
{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 → ℕ}
{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]
(A : ArrowL H W hχ J h1 hco)
(t : I → k)
{y x : V}
{γ : Wt}
{d : ℕ}
{F : LinearPaths.obj y ⟶ LinearPaths.obj x}
(hF : F ∈ WPs W γ d y x)
:
toLin ((PathReal.realizeR k (fun {y x : V} => twArrow A t) y x) F) = MGr.twl coords (grEv W hfin D y) (grEv W hfin D x) t γ (toLin ((PathReal.realizeR k (fun {y x : V} => A.g) y x) F))
theorem
MultiplicativeBasisDeformations.MeshWalk.tw_relation
{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 → ℕ}
{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]
{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)
(A : ArrowL H W hχ J h1 hco)
(lam : I → k)
(hA : ∀ (x : ↑Q.nonprojective), errE Rw A lam x = 0)
(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, (lam i * t i) • (PathReal.realizeR k (fun {y x : V} => twArrow A t) ↑(Q.tau x) ↑x) (rowQ Rw i x)
The polynomial mesh relations: r_x = Σ_i λ_i t_i R_i at every fibre.