Restricting Π of a tree to a full subtree

The argument of SubstarRestriction for any embedding f : Δ' → Δ of oriented trees that preserves and reflects adjacency and orientation: the restriction res maps the ideal of Π(Δ) with the outside of the image deleted into the ideal of Π(Δ') (res_mem), so nonzero paths of Π(Δ') stay nonzero (not_mem_del). We use it for intervals in the middle of a path (Appendix B, odd quotients of even A: "retain the first (r+1)/2 levels").

theorem MultiplicativeBasisDeformations.TreeEmbed.sgn_f {D : Type u_1} {D' : Type u_2} [Fintype D] [DecidableEq D] [Fintype D'] [DecidableEq D'] (T : OrientedTree D) (T' : OrientedTree D') [DecidableRel T.orient] [DecidableRel T'.orient] (f : D' → D) (hor : ∀ (x y : D'), T.orient (f x) (f y) ↔ T'.orient x y) {k : Type u} [Field k] (x y : D') : T.sgn k (f x) (f y) = T'.sgn k x y

def MultiplicativeBasisDeformations.TreeEmbed.ιq {D : Type u_1} {D' : Type u_2} (T : OrientedTree D) (T' : OrientedTree D') (f : D' → D) (hadj : ∀ (x y : D'), T.G.Adj (f x) (f y) ↔ T'.G.Adj x y) : T'.Dbl ⥤q T.Dbl

The embedding of doubled quivers.

theorem MultiplicativeBasisDeformations.TreeEmbed.vertices_mapPath {D : Type u_1} {D' : Type u_2} [Fintype D] [DecidableEq D] [Fintype D'] [DecidableEq D'] (T : OrientedTree D) (T' : OrientedTree D') [DecidableRel T.orient] [DecidableRel T'.orient] (f : D' → D) (hadj : ∀ (x y : D'), T.G.Adj (f x) (f y) ↔ T'.G.Adj x y) {v w : T'.Dbl} (q : Quiver.Path v w) : ((ιq T T' f hadj).mapPath q).vertices = List.map f q.vertices

theorem MultiplicativeBasisDeformations.TreeEmbed.mapPath_injective {D : Type u_1} {D' : Type u_2} [Fintype D] [DecidableEq D] [Fintype D'] [DecidableEq D'] (T : OrientedTree D) (T' : OrientedTree D') [DecidableRel T.orient] [DecidableRel T'.orient] (f : D' → D) (hf : Function.Injective f) (hadj : ∀ (x y : D'), T.G.Adj (f x) (f y) ↔ T'.G.Adj x y) {v w : T'.Dbl} (q₁ q₂ : Quiver.Path v w) : (ιq T T' f hadj).mapPath q₁ = (ιq T T' f hadj).mapPath q₂ → q₁ = q₂

theorem MultiplicativeBasisDeformations.TreeEmbed.exists_lift {D : Type u_1} {D' : Type u_2} [Fintype D] [DecidableEq D] [Fintype D'] [DecidableEq D'] (T : OrientedTree D) (T' : OrientedTree D') [DecidableRel T.orient] [DecidableRel T'.orient] (f : D' → D) (hadj : ∀ (x y : D'), T.G.Adj (f x) (f y) ↔ T'.G.Adj x y) {v : T'.Dbl} {z : T.Dbl} (q : Quiver.Path ((ιq T T' f hadj).obj v) z) : (∀ x ∈ q.vertices, x ∈ Set.range f) → ∃ (w : T'.Dbl) (q' : Quiver.Path v w) (_ : (ιq T T' f hadj).obj w = z), (ιq T T' f hadj).mapPath q' ≍ q

Paths inside the image lift.

noncomputable def MultiplicativeBasisDeformations.TreeEmbed.res {D : Type u_1} {D' : Type u_2} (T : OrientedTree D) (T' : OrientedTree D') (f : D' → D) (hadj : ∀ (x y : D'), T.G.Adj (f x) (f y) ↔ T'.G.Adj x y) {k : Type u} [Field k] (v w : T'.Dbl) : (LinearPaths.obj ((ιq T T' f hadj).obj v) ⟶ LinearPaths.obj ((ιq T T' f hadj).obj w)) →ₗ[k] LinearPaths.obj v ⟶ LinearPaths.obj w

The restriction to the substar.

theorem MultiplicativeBasisDeformations.TreeEmbed.res_mapPath {D : Type u_1} {D' : Type u_2} [Fintype D] [DecidableEq D] [Fintype D'] [DecidableEq D'] (T : OrientedTree D) (T' : OrientedTree D') [DecidableRel T.orient] [DecidableRel T'.orient] (f : D' → D) (hf : Function.Injective f) (hadj : ∀ (x y : D'), T.G.Adj (f x) (f y) ↔ T'.G.Adj x y) {k : Type u} [Field k] {v w : T'.Dbl} (q' : Quiver.Path v w) : (res T T' f hadj v w) (LinearPaths.path ((ιq T T' f hadj).mapPath q')) = LinearPaths.path q'

theorem MultiplicativeBasisDeformations.TreeEmbed.res_out {D : Type u_1} {D' : Type u_2} [Fintype D] [DecidableEq D] [Fintype D'] [DecidableEq D'] (T : OrientedTree D) (T' : OrientedTree D') [DecidableRel T.orient] [DecidableRel T'.orient] (f : D' → D) (hadj : ∀ (x y : D'), T.G.Adj (f x) (f y) ↔ T'.G.Adj x y) {k : Type u} [Field k] {v w : T'.Dbl} (q : Quiver.Path ((ιq T T' f hadj).obj v) ((ιq T T' f hadj).obj w)) (h : ∃ x ∈ q.vertices, x ∉ Set.range f) : (res T T' f hadj v w) (LinearPaths.path q) = 0

theorem MultiplicativeBasisDeformations.TreeEmbed.mem_comp_left {V : Type u_3} [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.TreeEmbed.mem_comp_right {V : Type u_3} [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.TreeEmbed.Out {D : Type u_1} {D' : Type u_2} (T : OrientedTree D) (T' : OrientedTree D') (f : D' → D) (hadj : ∀ (x y : D'), T.G.Adj (f x) (f y) ↔ T'.G.Adj x y) : Set T.Dbl

The vertices outside the substar.

theorem MultiplicativeBasisDeformations.TreeEmbed.mem_range_iff {D : Type u_1} {D' : Type u_2} [Fintype D] [DecidableEq D] [Fintype D'] [DecidableEq D'] (T : OrientedTree D) (T' : OrientedTree D') [DecidableRel T.orient] [DecidableRel T'.orient] (f : D' → D) (hadj : ∀ (x y : D'), T.G.Adj (f x) (f y) ↔ T'.G.Adj x y) (x : T.Dbl) : x ∈ Set.range f ↔ x ∉ Out T T' f hadj

theorem MultiplicativeBasisDeformations.TreeEmbed.rel_expand {D : Type u_1} [Fintype D] [DecidableEq D] (T : OrientedTree D) [DecidableRel T.orient] {k : Type u} [Field k] {x y u : T.Dbl} (p : Quiver.Path x u) (p' : Quiver.Path u y) : CategoryTheory.CategoryStruct.comp (LinearPaths.path p) (CategoryTheory.CategoryStruct.comp (T.preprojRel k u) (LinearPaths.path p')) = ∑ e : (z : T.Dbl) × (u ⟶ z), ↑(T.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.TreeEmbed.res_rel {D : Type u_1} {D' : Type u_2} [Fintype D] [DecidableEq D] [Fintype D'] [DecidableEq D'] (T : OrientedTree D) (T' : OrientedTree D') [DecidableRel T.orient] [DecidableRel T'.orient] (f : D' → D) (hf : Function.Injective f) (hadj : ∀ (x y : D'), T.G.Adj (f x) (f y) ↔ T'.G.Adj x y) (hor : ∀ (x y : D'), T.orient (f x) (f y) ↔ T'.orient x y) {k : Type u} [Field k] {v w : T'.Dbl} {i : T.Dbl} (p : Quiver.Path ((ιq T T' f hadj).obj v) i) (p' : Quiver.Path i ((ιq T T' f hadj).obj w)) : (res T T' f hadj v w) (CategoryTheory.CategoryStruct.comp (LinearPaths.path p) (CategoryTheory.CategoryStruct.comp (T.preprojRel k i) (LinearPaths.path p'))) ∈ T'.Id k v w

theorem MultiplicativeBasisDeformations.TreeEmbed.res_mem {D : Type u_1} {D' : Type u_2} [Fintype D] [DecidableEq D] [Fintype D'] [DecidableEq D'] (T : OrientedTree D) (T' : OrientedTree D') [DecidableRel T.orient] [DecidableRel T'.orient] (f : D' → D) (hf : Function.Injective f) (hadj : ∀ (x y : D'), T.G.Adj (f x) (f y) ↔ T'.G.Adj x y) (hor : ∀ (x y : D'), T.orient (f x) (f y) ↔ T'.orient x y) {k : Type u} [Field k] {v w : T'.Dbl} {φ : LinearPaths.obj ((ιq T T' f hadj).obj v) ⟶ LinearPaths.obj ((ιq T T' f hadj).obj w)} (hφ : φ ∈ ((T.preproj k).del (Out T T' f hadj)).ideal (LinearPaths.obj ((ιq T T' f hadj).obj v)) (LinearPaths.obj ((ιq T T' f hadj).obj w))) : (res T T' f hadj v w) φ ∈ T'.Id k v w

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

theorem MultiplicativeBasisDeformations.TreeEmbed.not_mem_del {D : Type u_1} {D' : Type u_2} [Fintype D] [DecidableEq D] [Fintype D'] [DecidableEq D'] (T : OrientedTree D) (T' : OrientedTree D') [DecidableRel T.orient] [DecidableRel T'.orient] (f : D' → D) (hf : Function.Injective f) (hadj : ∀ (x y : D'), T.G.Adj (f x) (f y) ↔ T'.G.Adj x y) (hor : ∀ (x y : D'), T.orient (f x) (f y) ↔ T'.orient x y) {k : Type u} [Field k] {v w : T'.Dbl} (p : Quiver.Path v w) (hp : LinearPaths.path p ∉ T'.Id k v w) : LinearPaths.path ((ιq T T' f hadj).mapPath p) ∉ ((T.preproj k).del (Out T T' f hadj)).ideal (LinearPaths.obj ((ιq T T' f hadj).obj v)) (LinearPaths.obj ((ιq T T' f hadj).obj w))

Nonvanishing passes from the substar.