Weighted decomposition of mesh errors (toward Proposition 12.8) #
deformation-refinements.tex: "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", with the choices made "separately in each degree and weight".
The retained tuples are rows R_i = (x_i, w_i) whose classes span the cokernels of the mesh
derivatives (CokerSpan). Every mesh family of degree m + 1 is D f + Σ_i c_i R_i
(exists_span); if it has relative weight γ, then f can be taken of relative weight γ and
only the rows of weight γ occur (exists_span_wt), since the weight projections commute with
D (wπ_meshDerivative).
theorem
MultiplicativeBasisDeformations.MeshWalk.mem_span_rows
{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]
{m : ℕ}
(g : ScalarMeshCategory.MeshFamily c)
(hg : ∀ (x : ↑Q.nonprojective), g x ∈ ScalarMeshCategory.degreePart c (m + 1) ↑(Q.tau x) ↑x)
:
g ∈ Submodule.span k
{e : ScalarMeshCategory.MeshFamily c | ∃ (x : ↑Q.nonprojective) (w : Quiver.Path ↑(Q.tau x) ↑x), w.length = m + 1 ∧ e = ScalarMeshCategory.row c x w}
theorem
MultiplicativeBasisDeformations.MeshWalk.exists_span
{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]
{I : Type}
[Fintype I]
[DecidableEq I]
{Rw : I → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x}
(hS : ScalarMeshCategory.CokerSpan c (Set.range Rw))
{m : ℕ}
(hm : 2 ≤ m)
(g : ScalarMeshCategory.MeshFamily c)
(hg : ∀ (x : ↑Q.nonprojective), g x ∈ ScalarMeshCategory.degreePart c (m + 1) ↑(Q.tau x) ↑x)
:
∃ f ∈ ScalarMeshCategory.familiesDeg c m,
∃ (cc : I → k),
(∀ (i : I), cc i ≠ 0 → (Rw i).snd.length = m + 1) ∧ g = ScalarMeshCategory.meshDerivative c f + ∑ i : I, cc i • ScalarMeshCategory.row c (Rw i).fst (Rw i).snd
Mesh errors modulo the image of D are combinations of the retained rows.
Weights #
theorem
MultiplicativeBasisDeformations.MeshWalk.wπ_meshDerivative
{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]
{Wt : Type}
[AddCommGroup Wt]
(W : MeshWt Q Wt)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
(γ : Wt)
(f : ScalarMeshCategory.ArrowFamily c)
(x : ↑Q.nonprojective)
:
(wπ c W (W.ν x + γ) ↑(Q.tau x) ↑x) (ScalarMeshCategory.meshDerivative c f x) = ScalarMeshCategory.meshDerivative c
(fun (a : (x : V) × (y : V) × (x ⟶ y)) => (wπ c W (W.w a.snd.snd + γ) a.fst a.snd.fst) (f a)) x
The weight projections commute with the mesh derivative.
theorem
MultiplicativeBasisDeformations.MeshWalk.exists_span_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}
[Fintype ↑Q.nonprojective]
{I : Type}
[Fintype I]
[DecidableEq I]
{Rw : I → (x : ↑Q.nonprojective) × Quiver.Path ↑(Q.tau x) ↑x}
{Wt : Type}
[AddCommGroup Wt]
(W : MeshWt Q Wt)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{χ : I → Wt}
(hS : ScalarMeshCategory.CokerSpan c (Set.range Rw))
(hwt : ∀ (i : I), W.pw (Rw i).snd = W.ν (Rw i).fst + χ i)
{m : ℕ}
(hm : 2 ≤ m)
(γ : Wt)
(g : ScalarMeshCategory.MeshFamily c)
(hg : ∀ (x : ↑Q.nonprojective), g x ∈ ScalarMeshCategory.degreePart c (m + 1) ↑(Q.tau x) ↑x)
(hgw : ∀ (x : ↑Q.nonprojective), g x ∈ wP c W (W.ν x + γ) ↑(Q.tau x) ↑x)
:
∃ (f : ScalarMeshCategory.ArrowFamily c),
(∀ (a : (x : V) × (y : V) × (x ⟶ y)),
f a ∈ ScalarMeshCategory.degreePart c m a.fst a.snd.fst ∧ f a ∈ wP c W (W.w a.snd.snd + γ) a.fst a.snd.fst) ∧ ∃ (cc : I → k),
(∀ (i : I), cc i ≠ 0 → (Rw i).snd.length = m + 1 ∧ χ i = γ) ∧ g = ScalarMeshCategory.meshDerivative c f + ∑ i : I, cc i • ScalarMeshCategory.row c (Rw i).fst (Rw i).snd
Weighted decomposition of a homogeneous mesh error.