The dimension inequality for Π(Δ)

Proof of Proposition 4.1, Step 2 (periodic-mesh-calculations.tex): "For each vertex i of Δ, put P_i = e_i Π(Δ), n_i = dim_k P_i ... There is an exact sequence P_i → ⊕_{j∼i} P_j → P_i → S_i → 0. The map onto rad P_i prefixes outgoing arrows. To identify its kernel, express a relation among the prefixed paths in the free path algebra as a sum of contextual defining relations. A nonempty initial context gives zero in the coefficient module after its first arrow. An empty initial context gives a right multiple of the single relation at i. These are exactly the images of the first map. ... dimensions give 2n_i - ∑_{j∼i} n_j = 1 + dim K_i > 0."

We work with S i, the formal combinations of all paths starting at i, and its subspace I i spanned by the contextual relations starting at i, so that P_i = S i / I i. Only the inequality ∑_{j∼i} n_j ≤ 2 n_i - 1 is used later.

This file: first-arrow decompositions of paths.

theorem Quiver.Path.nil_or_first {V : Type v} [Quiver V] {i v : V} (u : Path i v) : (∃ (h : i = v), u = h ▸ nil) ∨ ∃ (j : V) (a : i ⟶ j) (u' : Path j v), u = a.toPath.comp u'

A path is empty or begins with an arrow.

theorem Quiver.Path.toPath_comp_vertices {V : Type v} [Quiver V] {i j v : V} (a : i ⟶ j) (u : Path j v) : (a.toPath.comp u).vertices = i :: u.vertices

theorem Quiver.Path.toPath_comp_inj {V : Type v} [Quiver V] {i j j' v : V} (a : i ⟶ j) (a' : i ⟶ j') (u : Path j v) (u' : Path j' v) (h : a.toPath.comp u = a'.toPath.comp u') : ⟨j, (a, u)⟩ = ⟨j', (a', u')⟩

The first arrow and the rest are determined by the path.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.OrientedTree.Sp {D : Type v} (T : OrientedTree D) (k : Type u) [Field k] (i : T.Dbl) : Type (max u v)

Formal combinations of the paths of Δ̄ starting at i.

@[instance_reducible]

noncomputable instance MultiplicativeBasisDeformations.OrientedTree.instAddCommGroupSp {D : Type v} (T : OrientedTree D) (k : Type u) [Field k] (i : T.Dbl) : AddCommGroup (T.Sp k i)

noncomputable def MultiplicativeBasisDeformations.OrientedTree.Ist {D : Type v} (T : OrientedTree D) (k : Type u) [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] (i : T.Dbl) : Submodule k (T.Sp k i)

The contextual relations of Π(Δ) starting at i; P_i = Sp i / Ist i.

noncomputable def MultiplicativeBasisDeformations.OrientedTree.pre {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] {i j : T.Dbl} (a : i ⟶ j) : T.Sp k j →ₗ[k] T.Sp k i

Prefixing an arrow a : i → j.

theorem MultiplicativeBasisDeformations.OrientedTree.pre_toStar {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] {i j : T.Dbl} (a : i ⟶ j) {Y : T.Dbl} (f : LinearPaths.obj j ⟶ LinearPaths.obj Y) : (pre a) ((RelSystem.toStar Y) f) = (RelSystem.toStar Y) (CategoryTheory.CategoryStruct.comp (LinearPaths.arrow a) f)

theorem MultiplicativeBasisDeformations.OrientedTree.pre_mem {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] {i j : T.Dbl} (a : i ⟶ j) {F : T.Sp k j} (hF : F ∈ T.Ist k j) : (pre a) F ∈ T.Ist k i

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.OrientedTree.OutArrow {D : Type v} (T : OrientedTree D) (i : T.Dbl) : Type v

An arrow out of i, with its target.

def MultiplicativeBasisDeformations.OrientedTree.rev {D : Type v} {T : OrientedTree D} {i : T.Dbl} (e : T.OutArrow i) : e.fst ⟶ i

The reverse of an arrow.

noncomputable def MultiplicativeBasisDeformations.OrientedTree.strip {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] {i : T.Dbl} (e : T.OutArrow i) : T.Sp k i →ₗ[k] T.Sp k e.fst

Removing the first arrow e: a left inverse of pre e.2.

theorem MultiplicativeBasisDeformations.OrientedTree.strip_pre_single {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] {i : T.Dbl} (e e' : T.OutArrow i) (p : Quiver.PathStar e'.fst) (c : k) : (strip e) ((pre e'.snd) fun₀ | p => c) = if h : e' = e then h ▸ fun₀ | p => c else 0

theorem MultiplicativeBasisDeformations.OrientedTree.strip_pre {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] {i : T.Dbl} (e e' : T.OutArrow i) (X : T.Sp k e'.fst) : (strip e) ((pre e'.snd) X) = if h : e' = e then h ▸ X else 0

noncomputable def MultiplicativeBasisDeformations.OrientedTree.gmap {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [Fintype D] (i : T.Dbl) : ((e : T.OutArrow i) → T.Sp k e.fst) →ₗ[k] T.Sp k i

Prefixing the outgoing arrows: ⊕_{j∼i} P_j → P_i, on formal paths.

theorem MultiplicativeBasisDeformations.OrientedTree.strip_gmap {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] {i : T.Dbl} (e : T.OutArrow i) (X : (e : T.OutArrow i) → T.Sp k e.fst) : (strip e) ((gmap i) X) = X e

theorem MultiplicativeBasisDeformations.OrientedTree.gmap_injective {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] (i : T.Dbl) : Function.Injective ⇑(gmap i)

theorem MultiplicativeBasisDeformations.OrientedTree.gmap_single {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] {i : T.Dbl} (e : T.OutArrow i) (x : T.Sp k e.fst) : (gmap i) (Pi.single e x) = (pre e.snd) x

noncomputable def MultiplicativeBasisDeformations.OrientedTree.fmap {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] (i : T.Dbl) : T.Sp k i →ₗ[k] (e : T.OutArrow i) → T.Sp k e.fst

Prefixing the reversed arrows, with the signs of the relation: P_i → ⊕_{j∼i} P_j.

theorem MultiplicativeBasisDeformations.OrientedTree.gmap_fmap_toStar {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] {i Y : T.Dbl} (f : LinearPaths.obj i ⟶ LinearPaths.obj Y) : (gmap i) ((fmap i) ((RelSystem.toStar Y) f)) = (RelSystem.toStar Y) (CategoryTheory.CategoryStruct.comp (T.preprojRel k i) f)

theorem MultiplicativeBasisDeformations.OrientedTree.path_nil_cast {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] {a b : T.Dbl} (h : a = b) : LinearPaths.path (h ▸ Quiver.Path.nil) = CategoryTheory.eqToHom ⋯

theorem MultiplicativeBasisDeformations.OrientedTree.eqToHom_preprojRel {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] {a b : T.Dbl} (h : a = b) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((T.preproj k).rel b) = CategoryTheory.CategoryStruct.comp (T.preprojRel k a) (CategoryTheory.eqToHom ⋯)

theorem MultiplicativeBasisDeformations.OrientedTree.exists_decomp {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] {i Y : T.Dbl} {f : LinearPaths.obj i ⟶ LinearPaths.obj Y} (hf : f ∈ (T.preproj k).ideal (LinearPaths.obj i) (LinearPaths.obj Y)) : ∃ (W : T.Sp k i) (R : (e : T.OutArrow i) → T.Sp k e.fst), (∀ (e : T.OutArrow i), R e ∈ T.Ist k e.fst) ∧ (RelSystem.toStar Y) f = (gmap i) ((fmap i) W) + (gmap i) R

First-arrow decomposition of the relations: a relation starting at i is a right multiple of ρ_i (empty initial context) plus prefixed relations (nonempty initial context).

theorem MultiplicativeBasisDeformations.OrientedTree.exists_decomp_Ist {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] {i : T.Dbl} {F : T.Sp k i} (hF : F ∈ T.Ist k i) : ∃ (W : T.Sp k i) (R : (e : T.OutArrow i) → T.Sp k e.fst), (∀ (e : T.OutArrow i), R e ∈ T.Ist k e.fst) ∧ F = (gmap i) ((fmap i) W) + (gmap i) R

theorem MultiplicativeBasisDeformations.OrientedTree.exact_star {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] {i : T.Dbl} (H : (e : T.OutArrow i) → T.Sp k e.fst) (hH : (gmap i) H ∈ T.Ist k i) : ∃ (W : T.Sp k i) (R : (e : T.OutArrow i) → T.Sp k e.fst), (∀ (e : T.OutArrow i), R e ∈ T.Ist k e.fst) ∧ H = (fmap i) W + R

Exactness at the middle term, on formal paths.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.OrientedTree.Pq {D : Type v} (T : OrientedTree D) (k : Type u) [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] (i : T.Dbl) : Type (max (max v u) u v)

P_i = e_i Π(Δ).

noncomputable def MultiplicativeBasisDeformations.OrientedTree.gbar {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] (i : T.Dbl) : ((e : T.OutArrow i) → T.Pq k e.fst) →ₗ[k] T.Pq k i

⊕_{j∼i} P_j → P_i.

noncomputable def MultiplicativeBasisDeformations.OrientedTree.fbar {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] (i : T.Dbl) : T.Pq k i →ₗ[k] (e : T.OutArrow i) → T.Pq k e.fst

P_i → ⊕_{j∼i} P_j.

theorem MultiplicativeBasisDeformations.OrientedTree.gbar_mk {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] {i : T.Dbl} (H : (e : T.OutArrow i) → T.Sp k e.fst) : ((gbar i) fun (e : T.OutArrow i) => Submodule.Quotient.mk (H e)) = Submodule.Quotient.mk ((gmap i) H)

theorem MultiplicativeBasisDeformations.OrientedTree.fbar_mk {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] {i : T.Dbl} (W : T.Sp k i) : (fbar i) (Submodule.Quotient.mk W) = fun (e : T.OutArrow i) => Submodule.Quotient.mk ((fmap i) W e)

theorem MultiplicativeBasisDeformations.OrientedTree.ker_gbar_le {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] (i : T.Dbl) : (gbar i).ker ≤ (fbar i).range

Exactness of P_i → ⊕_{j∼i} P_j → P_i at the middle term (one inclusion, the one used).

noncomputable def MultiplicativeBasisDeformations.OrientedTree.psi0 {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] (i : T.Dbl) : T.Sp k i →ₗ[k] k

The coefficient of the paths of length zero.

theorem MultiplicativeBasisDeformations.OrientedTree.psi0_toStar_path {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] {i Y : T.Dbl} (p : Quiver.Path i Y) : (psi0 i) ((RelSystem.toStar Y) (LinearPaths.path p)) = if p.length = 0 then 1 else 0

theorem MultiplicativeBasisDeformations.OrientedTree.psi0_ideal {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] {i Y : T.Dbl} {f : LinearPaths.obj i ⟶ LinearPaths.obj Y} (hf : f ∈ (T.preproj k).ideal (LinearPaths.obj i) (LinearPaths.obj Y)) : (psi0 i) ((RelSystem.toStar Y) f) = 0

theorem MultiplicativeBasisDeformations.OrientedTree.Ist_le_ker_psi0 {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] (i : T.Dbl) : T.Ist k i ≤ (psi0 i).ker

theorem MultiplicativeBasisDeformations.OrientedTree.psi0_pre {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] {i j : T.Dbl} (a : i ⟶ j) (X : T.Sp k j) : (psi0 i) ((pre a) X) = 0

theorem MultiplicativeBasisDeformations.OrientedTree.finite_short_paths {D : Type v} {T : OrientedTree D} [DecidableRel T.orient] [Fintype D] [DecidableEq D] (i : T.Dbl) (N : ℕ) : Finite { e : Quiver.PathStar i // e.snd.length < N }

theorem MultiplicativeBasisDeformations.OrientedTree.finiteDimensional_Pq {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] (N : ℕ) (hN : ∀ (v Y : T.Dbl) (P : Quiver.Path v Y), N ≤ P.length → LinearPaths.path P ∈ (T.preproj k).ideal (LinearPaths.obj v) (LinearPaths.obj Y)) (i : T.Dbl) : FiniteDimensional k (T.Pq k i)

With long paths vanishing, P_i is finite-dimensional.

theorem MultiplicativeBasisDeformations.OrientedTree.sum_finrank_add_one_le {D : Type v} {T : OrientedTree D} {k : Type u} [Field k] [DecidableRel T.orient] [Fintype D] [DecidableEq D] (N : ℕ) (hN : ∀ (v Y : T.Dbl) (P : Quiver.Path v Y), N ≤ P.length → LinearPaths.path P ∈ (T.preproj k).ideal (LinearPaths.obj v) (LinearPaths.obj Y)) (i : T.Dbl) : ∑ e : T.OutArrow i, Module.finrank k (T.Pq k e.fst) + 1 ≤ 2 * Module.finrank k (T.Pq k i)

The dimension inequality ∑_{j∼i} n_j ≤ 2 n_i - 1 (periodic-mesh-calculations.tex).