Restricting Π of a star to a substar

periodic-mesh-calculations.tex: "Removing the outer vertex of the long E₈ arm at every repetition coordinate gives exactly this mesh category by (5.2)." On Π this is the identification of Π(Δ) modulo the deleted vertices with Π(Δ') of the retained substar Δ': paths through deleted vertices vanish, a relation at a deleted vertex consists of such paths, and a relation at a retained vertex loses exactly its terms through deleted neighbours.

For arm lengths L' ≤ L the star of L' embeds in that of L (ιv). The restriction res sends a path inside the image to its preimage and other paths to zero; it maps the ideal of Π(Δ) with the outside deleted into the ideal of Π(Δ') (res_mem). Hence nonzero paths of Π(Δ') stay nonzero.

def MultiplicativeBasisDeformations.Substar.ιv {t : ℕ} {L L' : Fin t → ℕ} (hle : ∀ (i : Fin t), L' i ≤ L i) (x : StarV L') : StarV L

The embedding of the smaller star.

theorem MultiplicativeBasisDeformations.Substar.ιv_injective {t : ℕ} {L L' : Fin t → ℕ} (hle : ∀ (i : Fin t), L' i ≤ L i) : Function.Injective (ιv hle)

theorem MultiplicativeBasisDeformations.Substar.depth_ιv {t : ℕ} {L L' : Fin t → ℕ} (hle : ∀ (i : Fin t), L' i ≤ L i) (x : StarV L') : starDepth (ιv hle x) = starDepth x

theorem MultiplicativeBasisDeformations.Substar.adj_ιv {t : ℕ} {L L' : Fin t → ℕ} (hle : ∀ (i : Fin t), L' i ≤ L i) (x y : StarV L') : starAdj (ιv hle x) (ιv hle y) ↔ starAdj x y

theorem MultiplicativeBasisDeformations.Substar.sgn_ιv {t : ℕ} {L L' : Fin t → ℕ} (hle : ∀ (i : Fin t), L' i ≤ L i) {k : Type u} [Field k] (x y : StarV L') : (starTree L).sgn k (ιv hle x) (ιv hle y) = (starTree L').sgn k x y

def MultiplicativeBasisDeformations.Substar.ιq {t : ℕ} {L L' : Fin t → ℕ} (hle : ∀ (i : Fin t), L' i ≤ L i) : (starTree L').Dbl ⥤q (starTree L).Dbl

The embedding of doubled quivers.

theorem MultiplicativeBasisDeformations.Substar.vertices_mapPath {t : ℕ} {L L' : Fin t → ℕ} (hle : ∀ (i : Fin t), L' i ≤ L i) {v w : (starTree L').Dbl} (q : Quiver.Path v w) : ((ιq hle).mapPath q).vertices = List.map (ιv hle) q.vertices

theorem MultiplicativeBasisDeformations.Substar.mapPath_injective {t : ℕ} {L L' : Fin t → ℕ} (hle : ∀ (i : Fin t), L' i ≤ L i) {v w : (starTree L').Dbl} (q₁ q₂ : Quiver.Path v w) : (ιq hle).mapPath q₁ = (ιq hle).mapPath q₂ → q₁ = q₂

theorem MultiplicativeBasisDeformations.Substar.exists_lift {t : ℕ} {L L' : Fin t → ℕ} (hle : ∀ (i : Fin t), L' i ≤ L i) {v : (starTree L').Dbl} {z : (starTree L).Dbl} (q : Quiver.Path ((ιq hle).obj v) z) : (∀ x ∈ q.vertices, x ∈ Set.range (ιv hle)) → ∃ (w : (starTree L').Dbl) (q' : Quiver.Path v w) (_ : (ιq hle).obj w = z), (ιq hle).mapPath q' ≍ q

Paths inside the image lift.

noncomputable def MultiplicativeBasisDeformations.Substar.res {t : ℕ} {L L' : Fin t → ℕ} (hle : ∀ (i : Fin t), L' i ≤ L i) {k : Type u} [Field k] (v w : (starTree L').Dbl) : (LinearPaths.obj ((ιq hle).obj v) ⟶ LinearPaths.obj ((ιq hle).obj w)) →ₗ[k] LinearPaths.obj v ⟶ LinearPaths.obj w

The restriction to the substar.

theorem MultiplicativeBasisDeformations.Substar.res_mapPath {t : ℕ} {L L' : Fin t → ℕ} (hle : ∀ (i : Fin t), L' i ≤ L i) {k : Type u} [Field k] {v w : (starTree L').Dbl} (q' : Quiver.Path v w) : (res hle v w) (LinearPaths.path ((ιq hle).mapPath q')) = LinearPaths.path q'

theorem MultiplicativeBasisDeformations.Substar.res_out {t : ℕ} {L L' : Fin t → ℕ} (hle : ∀ (i : Fin t), L' i ≤ L i) {k : Type u} [Field k] {v w : (starTree L').Dbl} (q : Quiver.Path ((ιq hle).obj v) ((ιq hle).obj w)) (h : ∃ x ∈ q.vertices, x ∉ Set.range (ιv hle)) : (res hle v w) (LinearPaths.path q) = 0

theorem MultiplicativeBasisDeformations.Substar.mem_comp_left {V : Type u_1} [Quiver V] {a b c : V} (p : Quiver.Path a b) (q : Quiver.Path b c) {x : V} (hx : x ∈ p.vertices) : x ∈ (p.comp q).vertices

theorem MultiplicativeBasisDeformations.Substar.mem_comp_right {V : Type u_1} [Quiver V] {a b c : V} (p : Quiver.Path a b) (q : Quiver.Path b c) {x : V} (hx : x ∈ q.vertices) : x ∈ (p.comp q).vertices

def MultiplicativeBasisDeformations.Substar.Out {t : ℕ} {L L' : Fin t → ℕ} (hle : ∀ (i : Fin t), L' i ≤ L i) : Set (starTree L).Dbl

The vertices outside the substar.

theorem MultiplicativeBasisDeformations.Substar.mem_range_iff {t : ℕ} {L L' : Fin t → ℕ} (hle : ∀ (i : Fin t), L' i ≤ L i) (x : (starTree L).Dbl) : x ∈ Set.range (ιv hle) ↔ x ∉ Out hle

theorem MultiplicativeBasisDeformations.Substar.rel_expand {t : ℕ} {L : Fin t → ℕ} {k : Type u} [Field k] {x y u : (starTree L).Dbl} (p : Quiver.Path x u) (p' : Quiver.Path u y) : CategoryTheory.CategoryStruct.comp (LinearPaths.path p) (CategoryTheory.CategoryStruct.comp ((starTree L).preprojRel k u) (LinearPaths.path p')) = ∑ e : (z : (starTree L).Dbl) × (u ⟶ z), ↑((starTree L).sgn k u e.fst) • LinearPaths.path ((p.comp (e.snd.toPath.comp (have this := { down := ⋯ }; this).toPath)).comp p')

The relation of Π(Δ) in path context, expanded.

theorem MultiplicativeBasisDeformations.Substar.res_rel {t : ℕ} {L L' : Fin t → ℕ} (hle : ∀ (i : Fin t), L' i ≤ L i) {k : Type u} [Field k] {v w : (starTree L').Dbl} {i : (starTree L).Dbl} (p : Quiver.Path ((ιq hle).obj v) i) (p' : Quiver.Path i ((ιq hle).obj w)) : (res hle v w) (CategoryTheory.CategoryStruct.comp (LinearPaths.path p) (CategoryTheory.CategoryStruct.comp ((starTree L).preprojRel k i) (LinearPaths.path p'))) ∈ (starTree L').Id k v w

theorem MultiplicativeBasisDeformations.Substar.res_mem {t : ℕ} {L L' : Fin t → ℕ} (hle : ∀ (i : Fin t), L' i ≤ L i) {k : Type u} [Field k] {v w : (starTree L').Dbl} {f : LinearPaths.obj ((ιq hle).obj v) ⟶ LinearPaths.obj ((ιq hle).obj w)} (hf : f ∈ (((starTree L).preproj k).del (Out hle)).ideal (LinearPaths.obj ((ιq hle).obj v)) (LinearPaths.obj ((ιq hle).obj w))) : (res hle v w) f ∈ (starTree L').Id k v w

Restriction maps the ideal with the outside deleted into the ideal of the substar.

theorem MultiplicativeBasisDeformations.Substar.not_mem_del {t : ℕ} {L L' : Fin t → ℕ} (hle : ∀ (i : Fin t), L' i ≤ L i) {k : Type u} [Field k] {v w : (starTree L').Dbl} (p : Quiver.Path v w) (hp : LinearPaths.path p ∉ (starTree L').Id k v w) : LinearPaths.path ((ιq hle).mapPath p) ∉ (((starTree L).preproj k).del (Out hle)).ideal (LinearPaths.obj ((ιq hle).obj v)) (LinearPaths.obj ((ιq hle).obj w))

Nonvanishing passes from the substar.