Relations along quiver coverings

Proof of Proposition 4.1, Step 1 (periodic-mesh-calculations.tex): "Paths lift uniquely from a chosen start. Contextual mesh relations lift to contextual mesh relations with a common endpoint for all terms. Conversely every upstairs relation projects to one downstairs. The direct sum of the upstairs path spaces from a fixed start, modulo relations, is therefore the corresponding space downstairs."

A relation system on a quiver is a family of morphisms rel i : s i → t i of the linear path category. Its contextual ideal is spanned by the composites q ≫ rel i ≫ q' (RelSystem.ideal). Let φ be a covering of quivers and let relations of the cover map onto relations of the base, every base relation starting at φ X lifting to one starting at X. Then φ preserves and reflects ideal membership (mapPaths_mem_ideal_iff).

structure MultiplicativeBasisDeformations.RelSystem (k : Type u) [CommRing k] (V : Type v) [Quiver V] : Type (max (max u (v + 1)) w)

A family of relations rel i : s i → t i in the linear path category.

• I : Type v
• s : self.I → V
• t : self.I → V
• rel (i : self.I) : LinearPaths.obj (self.s i) ⟶ LinearPaths.obj (self.t i)

def MultiplicativeBasisDeformations.RelSystem.rels {k : Type u} [CommRing k] {V : Type v} [Quiver V] (R : RelSystem k V) (X Y : LinearPaths k V) : Set (X ⟶ Y)

The relations, as a family indexed by their endpoints.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.RelSystem.ideal {k : Type u} [CommRing k] {V : Type v} [Quiver V] (R : RelSystem k V) (X Y : LinearPaths k V) : Submodule k (X ⟶ Y)

The contextual ideal generated by the relations.

theorem MultiplicativeBasisDeformations.RelSystem.comp_rel_comp_mem {k : Type u} [CommRing k] {V : Type v} [Quiver V] (R : RelSystem k V) {X Y : V} (i : R.I) (q : LinearPaths.obj X ⟶ LinearPaths.obj (R.s i)) (q' : LinearPaths.obj (R.t i) ⟶ LinearPaths.obj Y) : CategoryTheory.CategoryStruct.comp q (CategoryTheory.CategoryStruct.comp (R.rel i) q') ∈ R.ideal (LinearPaths.obj X) (LinearPaths.obj Y)

theorem MultiplicativeBasisDeformations.RelSystem.comp_mem_ideal {k : Type u} [CommRing k] {V : Type v} [Quiver V] (R : RelSystem k V) {X Y Z : LinearPaths k V} (f : X ⟶ Y) {g : Y ⟶ Z} (hg : g ∈ R.ideal Y Z) : CategoryTheory.CategoryStruct.comp f g ∈ R.ideal X Z

theorem MultiplicativeBasisDeformations.RelSystem.mem_ideal_comp {k : Type u} [CommRing k] {V : Type v} [Quiver V] (R : RelSystem k V) {X Y Z : LinearPaths k V} {f : X ⟶ Y} (hf : f ∈ R.ideal X Y) (g : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f g ∈ R.ideal X Z

theorem MultiplicativeBasisDeformations.RelSystem.ideal_induction {k : Type u} [CommRing k] {V : Type v} [Quiver V] (R : RelSystem k 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')))) {f : LinearPaths.obj X ⟶ LinearPaths.obj Y} (hf : f ∈ R.ideal (LinearPaths.obj X) (LinearPaths.obj Y)) : P f

Induction principle for the ideal: it suffices to treat path contexts.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.RelSystem.StarSpace {k : Type u} [CommRing k] {V : Type v} [Quiver V] (X : V) : Type (max u v w)

Morphisms from X, all targets at once: finitely supported functions on the paths starting at X.

noncomputable def MultiplicativeBasisDeformations.RelSystem.toStar {k : Type u} [CommRing k] {V : Type v} [Quiver V] {X : V} (Y : V) : (LinearPaths.obj X ⟶ LinearPaths.obj Y) →ₗ[k] StarSpace X

A morphism X → Y, placed among all morphisms from X.

theorem MultiplicativeBasisDeformations.RelSystem.toStar_path {k : Type u} [CommRing k] {V : Type v} [Quiver V] {X Y : V} (p : Quiver.Path X Y) : (toStar Y) (LinearPaths.path p) = fun₀ | ⟨Y, p⟩ => 1

noncomputable def MultiplicativeBasisDeformations.RelSystem.ofStar {k : Type u} [CommRing k] {V : Type v} [Quiver V] {X : V} (Y : V) : StarSpace X →ₗ[k] LinearPaths.obj X ⟶ LinearPaths.obj Y

The component of target Y.

theorem MultiplicativeBasisDeformations.RelSystem.ofStar_toStar {k : Type u} [CommRing k] {V : Type v} [Quiver V] {X Y : V} (f : LinearPaths.obj X ⟶ LinearPaths.obj Y) : (ofStar Y) ((toStar Y) f) = f

theorem MultiplicativeBasisDeformations.RelSystem.ofStar_toStar_ne {k : Type u} [CommRing k] {V : Type v} [Quiver V] {X Y Y' : V} (h : Y' ≠ Y) (f : LinearPaths.obj X ⟶ LinearPaths.obj Y') : (ofStar Y) ((toStar Y') f) = 0

noncomputable def MultiplicativeBasisDeformations.RelSystem.liftStar {k : Type u} [CommRing k] {V : Type v} [Quiver V] {W : Type v'} [Quiver W] (φ : W ⥤q V) (hφ : φ.IsCovering) (X : W) : StarSpace (φ.obj X) →ₗ[k] StarSpace X

Lifting all paths from φ X to paths from X, along a covering.

theorem MultiplicativeBasisDeformations.RelSystem.liftStar_toStar_mapPaths {k : Type u} [CommRing k] {V : Type v} [Quiver V] {W : Type v'} [Quiver W] (φ : W ⥤q V) (hφ : φ.IsCovering) {X Y : W} (f : LinearPaths.obj X ⟶ LinearPaths.obj Y) : (liftStar φ hφ X) ((toStar (φ.obj Y)) ((LinearPaths.mapPaths φ X Y) f)) = (toStar Y) f

theorem MultiplicativeBasisDeformations.RelSystem.mem_ideal_of_mapPaths_mem {k : Type u} [CommRing k] {V : Type v} [Quiver V] {W : Type v'} [Quiver W] (φ : W ⥤q V) (RW : RelSystem k W) (RV : RelSystem k V) (hφ : φ.IsCovering) (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 Y : W} {f : LinearPaths.obj X ⟶ LinearPaths.obj Y} (hf : (LinearPaths.mapPaths φ X Y) f ∈ RV.ideal (LinearPaths.obj (φ.obj X)) (LinearPaths.obj (φ.obj Y))) : f ∈ RW.ideal (LinearPaths.obj X) (LinearPaths.obj Y)

Coverings reflect relations. Let φ be a covering, and let every contextual relation of the base starting at φ X be the image of a contextual relation of the cover starting at X. If the image of f : X → Y lies in the ideal of the base, then f lies in the ideal of the cover.

noncomputable def MultiplicativeBasisDeformations.RelSystem.mesh {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) : RelSystem k V

The mesh relations of a translation quiver, as a relation system.

@[simp]

theorem MultiplicativeBasisDeformations.RelSystem.mesh_rel {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) (x : ↑Q.nonprojective) : (mesh c).rel x = meshRelation c x

theorem MultiplicativeBasisDeformations.RelSystem.mesh_rels {k : Type u} [CommRing k] {V : Type v} [Quiver V] {Q : TranslationQuiver V} [(x : V) → Fintype ((y : V) × (y ⟶ x))] (c : MeshCoefficients k Q) : (mesh c).rels = meshRelations c

theorem MultiplicativeBasisDeformations.RelSystem.mapPaths_mem_ideal {k : Type u} [CommRing k] {V : Type v} [Quiver V] {W : Type v'} [Quiver W] (φ : W ⥤q V) (RW : RelSystem k W) (RV : RelSystem k V) (hP : ∀ {X Y : W} (i : RW.I) (p : Quiver.Path X (RW.s i)) (p' : Quiver.Path (RW.t i) Y), (LinearPaths.mapPaths φ X Y) (CategoryTheory.CategoryStruct.comp (LinearPaths.path p) (CategoryTheory.CategoryStruct.comp (RW.rel i) (LinearPaths.path p'))) ∈ RV.ideal (LinearPaths.obj (φ.obj X)) (LinearPaths.obj (φ.obj Y))) {X Y : W} {f : LinearPaths.obj X ⟶ LinearPaths.obj Y} (hf : f ∈ RW.ideal (LinearPaths.obj X) (LinearPaths.obj Y)) : (LinearPaths.mapPaths φ X Y) f ∈ RV.ideal (LinearPaths.obj (φ.obj X)) (LinearPaths.obj (φ.obj Y))

Images of relations in path context are relations: the ideal is preserved.

theorem MultiplicativeBasisDeformations.RelSystem.exists_lift {V : Type v} [Quiver V] {W : Type v'} [Quiver W] (φ : W ⥤q V) (hφ : φ.IsCovering) (X : W) {y : V} (p : Quiver.Path (φ.obj X) y) : ∃ (Y : W) (e : φ.obj Y = y) (P : Quiver.Path X Y), φ.mapPath P = Quiver.Path.cast ⋯ ⋯ p

Path lifting along a covering.

theorem MultiplicativeBasisDeformations.RelSystem.path_cast {k : Type u} [CommRing k] {V : Type v} [Quiver V] {u u' w w' : V} (hu : u = u') (hw : w = w') (p : Quiver.Path u w) : LinearPaths.path (Quiver.Path.cast hu hw p) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (LinearPaths.path p) (CategoryTheory.eqToHom ⋯))

theorem MultiplicativeBasisDeformations.RelSystem.lift_condition {k : Type u} [CommRing k] {V : Type v} [Quiver V] {W : Type v'} [Quiver W] (φ : W ⥤q V) (hφ : φ.IsCovering) (RW : RelSystem k W) (RV : RelSystem k V) (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 ⋯))) (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 ⋯)

The lifting condition of mem_ideal_of_mapPaths_mem, from the lifting of single relations.