Retained mesh coefficients at t = 1 (Proposition 12.8, mesh presentations) #
deformation-refinements.tex: "Lift the arrows using these bases. In each path degree
q ≥ 3, decompose their current mesh errors into the image of the original derivative and the
span of the retained p_i of that degree. The chosen splitting removes the image part by an arrow
correction of degree q − 1. […] these corrections do not change earlier coefficients, so the
procedure is triangular and finite. It produces polynomials F_i(t) in the mesh relations."
At the fibre t = 1: lifted arrows (ArrowL) are realized on paths (pathR); their realizations
have the expected order, leading term, weights in the cone and bottom part (pathR_props).
Weight and degree projections commute #
theorem
MultiplicativeBasisDeformations.MeshWalk.evProj_zproj
{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)]
{Wt : Type}
[AddCommGroup Wt]
(W : MeshWt Q Wt)
[Infinite k]
(X : V)
(γ : Wt)
(d : ℤ)
(v : CatAlg.Rep D.F0 (meshFam Q c X))
:
theorem
MultiplicativeBasisDeformations.MeshWalk.pr_zcomp
{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)]
{Wt : Type}
[AddCommGroup Wt]
(W : MeshWt Q Wt)
[Infinite k]
{y x : V}
(δ : Wt)
(r : ℤ)
(u : CatAlg.Rep D.F0 (meshFam Q c y) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x))
:
Weight parts commute with degree components.
Lifted arrows and their realizations on paths #
structure
MultiplicativeBasisDeformations.MeshWalk.ArrowL
{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]
:
Type u
Lifted arrows at t = 1: order 1, leading term the arrow, relative weights in the cone,
bottom part the arrow.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.toLin_pathR_cons
{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)
{x y z : V}
(p : Quiver.Path x y)
(a : y ⟶ z)
:
toLin (PathReal.pathR (fun {y x : V} => A.g) (p.cons a)) = toLin (A.g a) ∘ₗ toLin (PathReal.pathR (fun {y x : V} => A.g) p)
theorem
MultiplicativeBasisDeformations.MeshWalk.pathR_props
{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)
{y x : V}
(p : Quiver.Path y x)
:
GExt.OrderGe (gmodEv D hfin y) (gmodEv D hfin x) (↑p.length) (toLin (PathReal.pathR (fun {y x : V} => A.g) p)) ∧ (gmodEv D hfin y).gr.comp (gmodEv D hfin x).gr (↑p.length) (toLin (PathReal.pathR (fun {y x : V} => A.g) p)) = rs D (ScalarMeshCategory.pathMor c p) ∧ MGr.ConeLin (W.pw p) (toLin (PathReal.pathR (fun {y x : V} => A.g) p)) ∧ MGr.clin ⊥ (grEv W hfin D y) (grEv W hfin D x) (W.pw p) (toLin (PathReal.pathR (fun {y x : V} => A.g) p)) = rs D (ScalarMeshCategory.pathMor c p)
The realization of a path: order, leading term, cone and bottom part.
Orders and leading terms #
theorem
MultiplicativeBasisDeformations.MeshWalk.orderGe_succ_of_comp
{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)]
[Infinite k]
{y x : V}
{r : ℤ}
{u : CatAlg.Rep D.F0 (meshFam Q c y) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x)}
(hu : GExt.OrderGe (gmodEv D hfin y) (gmodEv D hfin x) r u)
(h0 : (gmodEv D hfin y).gr.comp (gmodEv D hfin x).gr r u = 0)
:
GExt.OrderGe (gmodEv D hfin y) (gmodEv D hfin x) (r + 1) u
theorem
MultiplicativeBasisDeformations.MeshWalk.OrderGe.sub'
{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)]
[Infinite k]
{y x : V}
{r : ℤ}
{u v : CatAlg.Rep D.F0 (meshFam Q c y) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x)}
(hu : GExt.OrderGe (gmodEv D hfin y) (gmodEv D hfin x) r u)
(hv : GExt.OrderGe (gmodEv D hfin y) (gmodEv D hfin x) r v)
:
GExt.OrderGe (gmodEv D hfin y) (gmodEv D hfin x) r (u - v)
theorem
MultiplicativeBasisDeformations.MeshWalk.comp_eq_zero_of_orderGe
{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)]
[Infinite k]
{y x : V}
{r s : ℤ}
{u : CatAlg.Rep D.F0 (meshFam Q c y) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x)}
(hu : GExt.OrderGe (gmodEv D hfin y) (gmodEv D hfin x) r u)
(hs : s < r)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.OrderGe.sum'
{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)]
[Infinite k]
{y x : V}
{r : ℤ}
{ι : Type u_1}
(s : Finset ι)
{u : ι → CatAlg.Rep D.F0 (meshFam Q c y) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x)}
(hu : ∀ i ∈ s, GExt.OrderGe (gmodEv D hfin y) (gmodEv D hfin x) r (u i))
:
GExt.OrderGe (gmodEv D hfin y) (gmodEv D hfin x) r (∑ i ∈ s, u i)
theorem
MultiplicativeBasisDeformations.MeshWalk.comp_sum'
{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)]
[Infinite k]
{y x : V}
{r : ℤ}
{ι : Type u_1}
(s : Finset ι)
(u : ι → CatAlg.Rep D.F0 (meshFam Q c y) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x))
:
Realizing homogeneous morphisms of kQ #
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.WPs
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
{Wt : Type}
[AddCommGroup Wt]
(W : MeshWt Q Wt)
(γ : Wt)
(d : ℕ)
(y x : V)
:
Submodule k (LinearPaths.obj y ⟶ LinearPaths.obj x)
The span of the paths of length d and weight γ.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.realize_props
{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)
{y x : V}
{γ : Wt}
{d : ℕ}
{F : LinearPaths.obj y ⟶ LinearPaths.obj x}
(hF : F ∈ WPs W γ d y x)
:
GExt.OrderGe (gmodEv D hfin y) (gmodEv D hfin x) (↑d) (toLin ((PathReal.realizeR k (fun {y x : V} => A.g) y x) F)) ∧ (gmodEv D hfin y).gr.comp (gmodEv D hfin x).gr (↑d) (toLin ((PathReal.realizeR k (fun {y x : V} => A.g) y x) F)) = rs D (img F) ∧ MGr.ConeLin γ (toLin ((PathReal.realizeR k (fun {y x : V} => A.g) y x) F)) ∧ MGr.clin ⊥ (grEv W hfin D y) (grEv W hfin D x) γ (toLin ((PathReal.realizeR k (fun {y x : V} => A.g) y x) F)) = rs D (img F)
theorem
MultiplicativeBasisDeformations.MeshWalk.pathR_sub
{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 A' : ArrowL H W hχ J h1 hco)
{m : ℕ}
(hm : 1 ≤ m)
(hAA : ∀ {y x : V} (a : y ⟶ x), GExt.OrderGe (gmodEv D hfin y) (gmodEv D hfin x) (↑m) (toLin (A'.g a - A.g a)))
{y x : V}
(p : Quiver.Path y x)
:
GExt.OrderGe (gmodEv D hfin y) (gmodEv D hfin x) (↑p.length + ↑m - 1)
(toLin (PathReal.pathR (fun {y x : V} => A'.g) p - PathReal.pathR (fun {y x : V} => A.g) p))
theorem
MultiplicativeBasisDeformations.MeshWalk.realize_sub
{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 A' : ArrowL H W hχ J h1 hco)
{m : ℕ}
(hm : 1 ≤ m)
(hAA : ∀ {y x : V} (a : y ⟶ x), GExt.OrderGe (gmodEv D hfin y) (gmodEv D hfin x) (↑m) (toLin (A'.g a - A.g a)))
{y x : V}
{γ : Wt}
{d : ℕ}
{F : LinearPaths.obj y ⟶ LinearPaths.obj x}
(hF : F ∈ WPs W γ d y x)
:
GExt.OrderGe (gmodEv D hfin y) (gmodEv D hfin x) (↑d + ↑m - 1)
(toLin ((PathReal.realizeR k (fun {y x : V} => A'.g) y x) F - (PathReal.realizeR k (fun {y x : V} => A.g) y x) F))
The mesh errors relative to the retained rows #
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.rowQ
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[DecidableEq V]
{Q : TranslationQuiver V}
{I : Type}
(Rw : I → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x)
(i : I)
(x : ↑Q.nonprojective)
:
LinearPaths.obj ↑(Q.tau x) ⟶ LinearPaths.obj ↑x
The retained row R_i, as a family in kQ.
Instances For
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.errE
{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]
(Rw : I → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x)
(A : ArrowL H W hχ J h1 hco)
(lam : I → k)
(x : ↑Q.nonprojective)
:
The mesh error relative to the retained rows r_x − Σ_i λ_i R_i, realized.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.meshRelation_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}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
(x : ↑Q.nonprojective)
:
meshRelation c x ∈ WPs W (W.ν x) 2 ↑(Q.tau x) ↑x
theorem
MultiplicativeBasisDeformations.MeshWalk.rowQ_mem
{k : Type u}
[Field k]
{V : Type}
[Quiver V]
[Fintype V]
[DecidableEq V]
{Q : TranslationQuiver V}
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
[Fintype ↑Q.nonprojective]
{I : Type}
[Fintype I]
[DecidableEq I]
{qd : I → ℕ}
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{χ : I → Wt}
{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)
(i : I)
(x : ↑Q.nonprojective)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.img_rowQ
{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}
[Fintype ↑Q.nonprojective]
[hfd : ∀ (x y : V), FiniteDimensional k (meshFam Q c x ⟶ meshFam Q c y)]
{I : Type}
[Fintype I]
[DecidableEq I]
{Rw : I → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x}
(i : I)
(x : ↑Q.nonprojective)
:
img (rowQ Rw i x) = ScalarMeshCategory.row c (Rw i).fst (Rw i).snd x
theorem
MultiplicativeBasisDeformations.MeshWalk.errE_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]
{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)
(x : ↑Q.nonprojective)
:
The errors have relative weights in the cone, with no bottom part.
Weight decomposition of the leading terms #
theorem
MultiplicativeBasisDeformations.MeshWalk.pr_eq_clin_bot
{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)]
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
{y x : V}
(ρ : Wt)
(f : CatAlg.Rep D.F0 (meshFam Q c y) →ₗ[k] CatAlg.Rep D.F0 (meshFam Q c x))
:
theorem
MultiplicativeBasisDeformations.MeshWalk.lead_wπ_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}
{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)
{r : ℕ}
(x : ↑Q.nonprojective)
{ε : ScalarMeshCategory.obj c ↑(Q.tau x) ⟶ ScalarMeshCategory.obj c ↑x}
(hε : (gmodEv D hfin ↑(Q.tau x)).gr.comp (gmodEv D hfin ↑x).gr (↑r) (toLin (errE Rw A lam x)) = rs D ε)
(γ : Wt)
(hγ : ¬(γ ∈ cone χ ∧ γ ≠ 0))
:
The leading term of an error has weights in ν x + (C ∖ 0).
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.relWts
{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}
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
[Fintype ↑Q.nonprojective]
{Wt : Type}
[AddCommGroup Wt]
(W : MeshWt Q Wt)
:
Finset Wt
The finite set of relative weights that can occur.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.eq_sum_relWts
{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}
{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)]
{Wt : Type}
[AddCommGroup Wt]
{W : MeshWt Q Wt}
(x : ↑Q.nonprojective)
(f : ScalarMeshCategory.obj c ↑(Q.tau x) ⟶ ScalarMeshCategory.obj c ↑x)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.realize_meshRelation
{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)
(x : ↑Q.nonprojective)
:
(PathReal.realizeR k (fun {y x : V} => A.g) ↑(Q.tau x) ↑x) (meshRelation c x) = ∑ a : (y : V) × (y ⟶ ↑x),
↑(c x a.fst a.snd) • CategoryTheory.CategoryStruct.comp (A.g ((Q.mate x a.fst) a.snd)) (A.g a.snd)
The retained-row coefficients of a family realize the rows.
The correction step #
theorem
MultiplicativeBasisDeformations.MeshWalk.exists_correction
{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)
(hS : ScalarMeshCategory.CokerSpan c (Set.range Rw))
(A : ArrowL H W hχ J h1 hco)
(lam : I → k)
{m : ℕ}
(hm : 2 ≤ m)
(hE :
∀ (x : ↑Q.nonprojective),
GExt.OrderGe (gmodEv D hfin ↑(Q.tau x)) (gmodEv D hfin ↑x) (↑(m + 1)) (toLin (errE Rw A lam x)))
:
∃ (A' : ArrowL H W hχ J h1 hco) (lam' : I → k),
∀ (x : ↑Q.nonprojective),
GExt.OrderGe (gmodEv D hfin ↑(Q.tau x)) (gmodEv D hfin ↑x) (↑(m + 2)) (toLin (errE Rw A' lam' x))
The correction step: if the errors relative to the retained rows have order m + 1
(m ≥ 2), a correction of the lifted arrows in degree m with homogeneous components of
relative weights in C ∖ 0, and of the retained coefficients in degree m + 1, raises it to
m + 2.
The normal form at t = 1 #
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.arrowL0
{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]
:
ArrowL H W hχ J h1 hco
The initial lifted arrows.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.exists_errE_order
{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)
(hS : ScalarMeshCategory.CokerSpan c (Set.range Rw))
(n : ℕ)
:
∃ (A : ArrowL H W hχ J h1 hco) (lam : I → k),
∀ (x : ↑Q.nonprojective),
GExt.OrderGe (gmodEv D hfin ↑(Q.tau x)) (gmodEv D hfin ↑x) (↑(n + 3)) (toLin (errE Rw A lam x))
Successive corrections: errors of order n + 3.
theorem
MultiplicativeBasisDeformations.MeshWalk.exists_normalForm_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)}
[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)
(hS : ScalarMeshCategory.CokerSpan c (Set.range Rw))
:
∃ (A : ArrowL H W hχ J h1 hco) (lam : I → k), ∀ (x : ↑Q.nonprojective), errE Rw A lam x = 0
The normal form at t = 1: lifted arrows satisfying r_x = Σ_i λ_i R_i exactly in the
lifted category.