Deleting vertices along a covering

Appendix A, periodic-mesh-calculations.tex: "Paths lift uniquely from a chosen start. Contextual mesh relations lift to contextual mesh relations … The fixed-start lifting of paths and relations preserves nonvanishing", and "Delete all lifts of the two outer vertices of the long arms … (5.2) identifies the object quotient with the D₄ mesh category of the same period."

The object quotient C(Q)/[D] is kQ modulo the mesh ideal plus the paths through D (oqFunctor_map_eq_zero_iff). We add the identities of the deleted vertices to a relation system (RelSystem.del), lift relations along a covering from a fixed start (ofStar_liftStar_mem), rescale to signed coefficients, and forget heights into Π(Δ) modulo the deleted vertices.

theorem MultiplicativeBasisDeformations.RelSystem.path_nil' {k : Type u} [Field k] {V : Type v} [Quiver V] (x : V) : LinearPaths.path Quiver.Path.nil = CategoryTheory.CategoryStruct.id (LinearPaths.obj x)

noncomputable def MultiplicativeBasisDeformations.RelSystem.del {k : Type u} [Field k] {V : Type v} [Quiver V] (R : RelSystem k V) (D : Set V) : RelSystem k V

The relations together with the identities of the vertices of D.

theorem MultiplicativeBasisDeformations.RelSystem.ideal_le_del {k : Type u} [Field k] {V : Type v} [Quiver V] (R : RelSystem k V) (D : Set V) {X Y : V} : R.ideal (LinearPaths.obj X) (LinearPaths.obj Y) ≤ (R.del D).ideal (LinearPaths.obj X) (LinearPaths.obj Y)

theorem MultiplicativeBasisDeformations.RelSystem.path_comp_mem_del {k : Type u} [Field k] {V : Type v} [Quiver V] (R : RelSystem k V) (D : Set V) {X d Y : V} (hd : d ∈ D) (p : Quiver.Path X d) (q : Quiver.Path d Y) : LinearPaths.path (p.comp q) ∈ (R.del D).ideal (LinearPaths.obj X) (LinearPaths.obj Y)

theorem MultiplicativeBasisDeformations.RelSystem.through_le_del {k : Type u} [Field k] {V : Type v} [Quiver V] (R : RelSystem k V) (D : Set V) {X Y : V} : through k D X Y ≤ (R.del D).ideal (LinearPaths.obj X) (LinearPaths.obj Y)

theorem MultiplicativeBasisDeformations.RelSystem.del_induction {k : Type u} [Field k] {V : Type v} [Quiver V] (R : RelSystem k V) (D : Set V) {X Y : V} {P : (LinearPaths.obj X ⟶ LinearPaths.obj Y) → Prop} (h0 : P 0) (hadd : ∀ (f g : LinearPaths.obj X ⟶ LinearPaths.obj Y), P f → P g → P (f + g)) (hsmul : ∀ (c : k) (f : LinearPaths.obj X ⟶ LinearPaths.obj Y), P f → P (c • f)) (hgen : ∀ (i : R.I) (p : Quiver.Path X (R.s i)) (p' : Quiver.Path (R.t i) Y), P (CategoryTheory.CategoryStruct.comp (LinearPaths.path p) (CategoryTheory.CategoryStruct.comp (R.rel i) (LinearPaths.path p')))) (hdel : ∀ d ∈ D, ∀ (p : Quiver.Path X d) (p' : Quiver.Path d Y), P (CategoryTheory.CategoryStruct.comp (LinearPaths.path p) (LinearPaths.path p'))) {f : LinearPaths.obj X ⟶ LinearPaths.obj Y} (hf : f ∈ (R.del D).ideal (LinearPaths.obj X) (LinearPaths.obj Y)) : P f

Induction over the ideal of a deletion.

theorem MultiplicativeBasisDeformations.RelSystem.lift_condition_del {k : Type u} [Field k] {V : Type v} [Quiver V] {W : Type v'} [Quiver W] (φ : W ⥤q V) (RW : RelSystem k W) (RV : RelSystem k V) (DW : Set W) (DV : Set V) (hD : ∀ (Z : W), φ.obj Z ∈ DV → Z ∈ DW) (hrel : ∀ (Z : W) (i' : RV.I) (h : RV.s i' = φ.obj Z), ∃ (i : RW.I) (hs : RW.s i = Z) (ht : RV.t i' = φ.obj (RW.t i)), (LinearPaths.mapPaths φ (RW.s i) (RW.t i)) (RW.rel i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (RV.rel i') (CategoryTheory.eqToHom ⋯))) (Z : W) (i' : (RV.del DV).I) (h : (RV.del DV).s i' = φ.obj Z) : ∃ (i : (RW.del DW).I) (hs : (RW.del DW).s i = Z) (ht : (RV.del DV).t i' = φ.obj ((RW.del DW).t i)), (LinearPaths.mapPaths φ ((RW.del DW).s i) ((RW.del DW).t i)) ((RW.del DW).rel i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((RV.del DV).rel i') (CategoryTheory.eqToHom ⋯))

Relations of a deletion lift along a covering, if the relations do and the deleted vertices of the cover contain the preimages of those of the base.

theorem MultiplicativeBasisDeformations.RelSystem.ofStar_liftStar_mem {k : Type u} [Field k] {V : Type v} [Quiver V] {W : Type v'} [Quiver W] (φ : W ⥤q V) (hφ : φ.IsCovering) (RW : RelSystem k W) (RV : RelSystem k V) (hL : ∀ (X : W) (i' : RV.I) (p : Quiver.Path (φ.obj X) (RV.s i')) {y : V} (p' : Quiver.Path (RV.t i') y), ∃ (Y : W) (e : φ.obj Y = y), ∃ g ∈ RW.ideal (LinearPaths.obj X) (LinearPaths.obj Y), (LinearPaths.mapPaths φ X Y) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (LinearPaths.path p) (CategoryTheory.CategoryStruct.comp (RV.rel i') (LinearPaths.path p'))) (CategoryTheory.eqToHom ⋯)) {X : W} {y : V} {F : LinearPaths.obj (φ.obj X) ⟶ LinearPaths.obj y} (hF : F ∈ RV.ideal (LinearPaths.obj (φ.obj X)) (LinearPaths.obj y)) (Y : W) : (ofStar Y) ((liftStar φ hφ X) ((toStar y) F)) ∈ RW.ideal (LinearPaths.obj X) (LinearPaths.obj Y)

Fixed-start lifting of relations: every target component of the lift of an element of the base ideal lies in the ideal of the cover.

theorem MultiplicativeBasisDeformations.RelSystem.liftStar_single {k : Type u} [Field k] {V : Type v} [Quiver V] {W : Type v'} [Quiver W] (φ : W ⥤q V) (hφ : φ.IsCovering) {X Y : W} (P : Quiver.Path X Y) : ((liftStar φ hφ X) fun₀ | ⟨φ.obj Y, φ.mapPath P⟩ => 1) = fun₀ | ⟨Y, P⟩ => 1

theorem MultiplicativeBasisDeformations.RelSystem.components {k : Type u} [Field k] {V : Type v} [Quiver V] {W : Type v'} [Quiver W] (φ : W ⥤q V) (hφ : φ.IsCovering) {X E : W} (hXE : X ≠ E) (hE : φ.obj E = φ.obj X) (P : Quiver.Path X E) (a b : k) : (ofStar E) ((liftStar φ hφ X) ((toStar (φ.obj X)) (a • CategoryTheory.CategoryStruct.id (LinearPaths.obj (φ.obj X)) + b • LinearPaths.path (Quiver.Path.cast ⋯ hE (φ.mapPath P))))) = b • LinearPaths.path P ∧ (ofStar X) ((liftStar φ hφ X) ((toStar (φ.obj X)) (a • CategoryTheory.CategoryStruct.id (LinearPaths.obj (φ.obj X)) + b • LinearPaths.path (Quiver.Path.cast ⋯ hE (φ.mapPath P))))) = a • CategoryTheory.CategoryStruct.id (LinearPaths.obj X)

The two components of the lift of a 𝟙 + b (φ P) for a path P : X → E whose image is closed.

theorem MultiplicativeBasisDeformations.gaugeMap_mem_del {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (c c' : MeshCoefficients k Q) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c' x y a = η x * c x y a * μ ((Q.mate x y) a) * μ a) (D : Set V) {X Y : V} {f : LinearPaths.obj X ⟶ LinearPaths.obj Y} (hf : f ∈ ((RelSystem.mesh c).del D).ideal (LinearPaths.obj X) (LinearPaths.obj Y)) : (gaugeMap (fun {x y : V} => μ) X Y) f ∈ ((RelSystem.mesh c').del D).ideal (LinearPaths.obj X) (LinearPaths.obj Y)

A gauge transformation maps the ideal of a deletion of the mesh relations of c into that of c'.

theorem MultiplicativeBasisDeformations.path_mem_del_of_gauge {k : Type u} [Field k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (μ : {x y : V} → (x ⟶ y) → kˣ) (η : ↑Q.nonprojective → kˣ) (c c' : MeshCoefficients k Q) (h : ∀ (x : ↑Q.nonprojective) (y : V) (a : y ⟶ ↑x), c' x y a = η x * c x y a * μ ((Q.mate x y) a) * μ a) (D : Set V) {X Y : V} (P : Quiver.Path X Y) (hP : LinearPaths.path P ∈ ((RelSystem.mesh c).del D).ideal (LinearPaths.obj X) (LinearPaths.obj Y)) : LinearPaths.path P ∈ ((RelSystem.mesh c').del D).ideal (LinearPaths.obj X) (LinearPaths.obj Y)

A single path lies in the deletion ideal of c' if it lies in that of c.

theorem MultiplicativeBasisDeformations.OrientedTree.forget_mem_preproj_del {D : Type v} (T : OrientedTree D) [Fintype D] [DecidableEq D] [DecidableRel T.orient] {k : Type u} [Field k] (DZ : Set T.ZVert) (Del : Set T.Dbl) (hD : ∀ Z ∈ DZ, T.toDbl Z.v ∈ Del) {X Y : T.ZVert} {f : LinearPaths.obj X ⟶ LinearPaths.obj Y} (hf : f ∈ ((RelSystem.mesh (T.zSigned k)).del DZ).ideal (LinearPaths.obj X) (LinearPaths.obj Y)) : (LinearPaths.mapPaths T.forget X Y) f ∈ ((T.preproj k).del Del).ideal (LinearPaths.obj (T.forget.obj X)) (LinearPaths.obj (T.forget.obj Y))

Forgetting heights maps the signed mesh ideal with deleted vertices into the ideal of Π(Δ) with deleted vertices.

theorem MultiplicativeBasisDeformations.OrientedTree.lift_del {D : Type v} (T : OrientedTree D) [Fintype D] [DecidableEq D] [DecidableRel T.orient] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [Field k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (hπ : π.IsCovering) (hτ : ∀ (Y : T.ZVert), π.obj (T.ztau Y) = hQ.tauE (π.obj Y)) (Dset : Set V) (X : T.ZVert) (i' : ((RelSystem.mesh c).del Dset).I) (p : Quiver.Path (π.obj X) (((RelSystem.mesh c).del Dset).s i')) {y : V} (p' : Quiver.Path (((RelSystem.mesh c).del Dset).t i') y) : ∃ (Y : T.ZVert) (e : π.obj Y = y), ∃ g ∈ ((RelSystem.mesh (T.pullCoeff hQ π c)).del {Z : T.ZVert | π.obj Z ∈ Dset}).ideal (LinearPaths.obj X) (LinearPaths.obj Y), (LinearPaths.mapPaths π X Y) g = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (LinearPaths.path p) (CategoryTheory.CategoryStruct.comp (((RelSystem.mesh c).del Dset).rel i') (LinearPaths.path p'))) (CategoryTheory.eqToHom ⋯)

Mesh relations with deleted vertices lift along π from a fixed start.

theorem MultiplicativeBasisDeformations.OrientedTree.transfer_del {D : Type v} (T : OrientedTree D) [Fintype D] [DecidableEq D] [DecidableRel T.orient] {V : Type v'} [Quiver V] [∀ (x y : V), Subsingleton (x ⟶ y)] {Q : TranslationQuiver V} (hQ : Q.IsStable) (π : T.ZVert ⥤q V) {k : Type u} [Field k] [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (hπ : π.IsCovering) (hτ : ∀ (Y : T.ZVert), π.obj (T.ztau Y) = hQ.tauE (π.obj Y)) (Dset : Set V) (Del : Set T.Dbl) (hD : ∀ (Z : T.ZVert), π.obj Z ∈ Dset → T.toDbl Z.v ∈ Del) {X E : T.ZVert} (hXE : X ≠ E) (hE : π.obj E = π.obj X) (P : Quiver.Path X E) (a b : k) (hmem : a • CategoryTheory.CategoryStruct.id (LinearPaths.obj (π.obj X)) + b • LinearPaths.path (Quiver.Path.cast ⋯ hE (π.mapPath P)) ∈ meshIdealSub c (LinearPaths.obj (π.obj X)) (LinearPaths.obj (π.obj X)) ⊔ through k Dset (π.obj X) (π.obj X)) : b • LinearPaths.path (T.forget.mapPath P) ∈ ((T.preproj k).del Del).ideal (LinearPaths.obj (T.forget.obj X)) (LinearPaths.obj (T.forget.obj E)) ∧ a • LinearPaths.path Quiver.Path.nil ∈ ((T.preproj k).del Del).ideal (LinearPaths.obj (T.forget.obj X)) (LinearPaths.obj (T.forget.obj X))

Fixed-start lifting into Π(Δ) modulo deleted vertices. If a 𝟙 + b (π P) vanishes in the object quotient C(Q)/[D] for a path P : X → E with closed image, then b P and a 𝟙 vanish in Π(Δ) modulo the deleted vertices, after forgetting heights.