Extending a mesh weight from one periodic component (Proposition 7.5) #
A mesh weight on a periodic component T of Q extends to a mesh weight on Q which
agrees with it on the edges inside T and vanishes on the edges inside every other periodic
component (exists_ext_wt). The values on the unmatched edges of the collapse of Lemma 4.2
are prescribed (the given weight inside T, zero elsewhere), and the matched edges are
solved from their triangles (Morse.zval); the triangles which solve edges inside a
periodic component lie in that component.
def
MultiplicativeBasisDeformations.MeshWalk.EdIn
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
(T : Set V)
:
An edge of K inside a set of vertices.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.MeshWt.w_congr
{M : Type}
[AddCommGroup M]
{V' : Type}
[Quiver V']
[∀ (x y : V'), Subsingleton (x ⟶ y)]
{Q' : TranslationQuiver V'}
(W : MeshWt Q' M)
{a b a' b' : V'}
(e : a ⟶ b)
(e' : a' ⟶ b')
(ha : a = a')
(hb : b = b')
:
theorem
MultiplicativeBasisDeformations.MeshWalk.mem_comp_of_arrow
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[Fintype V]
[DecidableEq V]
[∀ (x y : V), Subsingleton (x ⟶ y)]
[(x y : V) → Fintype (x ⟶ y)]
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{r y x : V}
(hx : x ∈ Q.component r)
(hy : y ∈ Q.periodic)
(a : y ⟶ x)
:
y ∈ Q.component r
theorem
MultiplicativeBasisDeformations.MeshWalk.edIn_tri
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[Fintype V]
[DecidableEq V]
[∀ (x y : V), Subsingleton (x ⟶ y)]
[(x y : V) → Fintype (x ⟶ y)]
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{k : Type u_1}
[Field k]
(c : MeshCoefficients k Q)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{r : V}
(t : Tri Q)
(h : EdIn (Q.component r) ((meshTris Q).edge t ((meshMatching (meshDepth c hfin)).m t)))
(j : Fin 3)
:
The triangles solving edges inside a periodic component lie in it.
def
MultiplicativeBasisDeformations.MeshWalk.ofZ
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
(z : Ed Q → ℤ)
(hz : ∀ (t : Tri Q), z (Sum.inl t.mateArr) + z (Sum.inl t.arr) = z (Sum.inr t.fst))
:
MeshWt Q ℤ
The mesh weight of an integer cocycle on K.
Instances For
noncomputable def
MultiplicativeBasisDeformations.MeshWalk.gT
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
(r : V)
(WT : MeshWt (TranslationQuiver.restrict ⋯) ℤ)
:
Ed Q → ℤ
The values of a weight of the component of r on the edges of K.
Instances For
theorem
MultiplicativeBasisDeformations.MeshWalk.gT_tri
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[Fintype V]
[DecidableEq V]
[∀ (x y : V), Subsingleton (x ⟶ y)]
[(x y : V) → Fintype (x ⟶ y)]
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
(r : V)
(WT : MeshWt (TranslationQuiver.restrict ⋯) ℤ)
(t : Tri Q)
(ht : ∀ (j : Fin 3), EdIn (Q.component r) ((meshTris Q).edge t j))
:
theorem
MultiplicativeBasisDeformations.MeshWalk.edIn_disjoint
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[Fintype V]
[DecidableEq V]
[∀ (x y : V), Subsingleton (x ⟶ y)]
[(x y : V) → Fintype (x ⟶ y)]
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{r r' : V}
(hne : Q.component r' ≠ Q.component r)
{e : Ed Q}
(h : EdIn (Q.component r') e)
:
theorem
MultiplicativeBasisDeformations.MeshWalk.exists_ext_wt
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[Fintype V]
[DecidableEq V]
[∀ (x y : V), Subsingleton (x ⟶ y)]
[(x y : V) → Fintype (x ⟶ y)]
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{k : Type u_1}
[Field k]
(c : MeshCoefficients k Q)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
(r : V)
(WT : MeshWt (TranslationQuiver.restrict ⋯) ℤ)
:
∃ (W : MeshWt Q ℤ),
(∀ {y x : V} (a : y ⟶ x) (hy : y ∈ Q.component r) (hx : x ∈ Q.component r),
W.w a = WT.w
(have this := a;
this)) ∧ (∀ (x : ↑Q.nonprojective) (hx : ↑x ∈ Q.component r), W.ν x = WT.ν ⟨FullSub.mk (↑x) hx, ⋯⟩) ∧ ∀ (r' : V),
Q.component r' ≠ Q.component r →
(∀ {y x : V} (a : y ⟶ x), y ∈ Q.component r' → x ∈ Q.component r' → W.w a = 0) ∧ ∀ (x : ↑Q.nonprojective), ↑x ∈ Q.component r' → W.ν x = 0
Extension of a mesh weight of a periodic component.
theorem
MultiplicativeBasisDeformations.MeshWalk.edIn_mono
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[Fintype V]
[DecidableEq V]
[∀ (x y : V), Subsingleton (x ⟶ y)]
[(x y : V) → Fintype (x ⟶ y)]
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{T T' : Set V}
(h : T ⊆ T')
{e : Ed Q}
(he : EdIn T e)
:
EdIn T' e
theorem
MultiplicativeBasisDeformations.MeshWalk.edIn_tri_periodic
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[Fintype V]
[DecidableEq V]
[∀ (x y : V), Subsingleton (x ⟶ y)]
[(x y : V) → Fintype (x ⟶ y)]
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{k : Type u_1}
[Field k]
(c : MeshCoefficients k Q)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
(t : Tri Q)
(h : EdIn Q.periodic ((meshTris Q).edge t ((meshMatching (meshDepth c hfin)).m t)))
(j : Fin 3)
:
The triangles solving edges inside the periodic vertices lie inside them.
theorem
MultiplicativeBasisDeformations.MeshWalk.periodicWeightExtension
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[Fintype V]
[DecidableEq V]
[∀ (x y : V), Subsingleton (x ⟶ y)]
[(x y : V) → Fintype (x ⟶ y)]
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{k : Type u_1}
[Field k]
(c : MeshCoefficients k Q)
(hfin : ∀ (x y : V), FiniteDimensional k (ScalarMeshCategory.obj c x ⟶ ScalarMeshCategory.obj c y))
{G : Type u_2}
[AddCommGroup G]
(w : Ed Q → G)
(hw :
∀ (t : Tri Q),
(∀ (j : Fin 3), EdIn Q.periodic ((meshTris Q).edge t j)) →
w (Sum.inl t.mateArr) + w (Sum.inl t.arr) = w (Sum.inr t.fst))
:
Lemma 4.3 (lem:periodic-weight-extension): every closed edge weight, with values in
an abelian group, on the union of the periodic subcomplexes extends to a closed edge weight on
K. Closed means that the triangle relations hold; the extension solves the edges matched by
the collapse of Lemma 4.2 from their triangles (Morse.zval), with the prescribed values on
the unmatched periodic edges and zero on the other unmatched edges.
Weights of included paths #
theorem
MultiplicativeBasisDeformations.MeshWalk.pw_incl_of
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[Fintype V]
[DecidableEq V]
[∀ (x y : V), Subsingleton (x ⟶ y)]
[(x y : V) → Fintype (x ⟶ y)]
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{S : Set V}
(hS : Q.IsTauClosed S)
(W : MeshWt Q ℤ)
(WT : MeshWt (TranslationQuiver.restrict hS) ℤ)
(hw :
∀ {a b : FullSub S} (e : a ⟶ b),
W.w
(have this := e;
this) = WT.w e)
{a b : FullSub S}
(p : Quiver.Path a b)
:
W.pw ((FullSub.incl S).mapPath p) = WT.pw p
theorem
MultiplicativeBasisDeformations.MeshWalk.pw_incl_zero
{V : Type}
[Quiver V]
{Q : TranslationQuiver V}
[Fintype V]
[DecidableEq V]
[∀ (x y : V), Subsingleton (x ⟶ y)]
[(x y : V) → Fintype (x ⟶ y)]
[(x : V) → Fintype ((y : V) × (y ⟶ x))]
{S : Set V}
(W : MeshWt Q ℤ)
(hw :
∀ {a b : FullSub S} (e : a ⟶ b),
W.w
(have this := e;
this) = 0)
{a b : FullSub S}
(p : Quiver.Path a b)
:
W.pw ((FullSub.incl S).mapPath p) = 0