The graded first-arrow sequence of Π(Δ) #
periodic-mesh-calculations.tex (proof of the bound by the U_d): "The
first-arrow presentation of each simple gives, as in (A.1), an exact sequence
e_iΠ⟨2⟩ → ⊕_{j∼i} e_jΠ⟨1⟩ → e_iΠ → S_i → 0. Exactness at the middle term is
proved as for (A.1)."
We fix the endpoint j and the degree. Write h_i(d) = dim e_i Π_d e_j. The
middle exactness (exact_star, proved for Proposition 4.1) and the grading of
the ideal give ∑_{l∼i} h_l(d+1) ≤ h_i(d+2) + h_i(d) and
∑_{l∼i} h_l(0) ≤ h_i(1); these are the inequalities κ ≥ 0 of UBound.
@[reducible, inline]
noncomputable abbrev
MultiplicativeBasisDeformations.OrientedTree.Id
{D : Type v}
(T : OrientedTree D)
[Fintype D]
[DecidableRel T.orient]
(k : Type u)
[Field k]
(x y : T.Dbl)
:
Submodule k (LinearPaths.obj x ⟶ LinearPaths.obj y)
The ideal of Π(Δ) between two vertices.
Instances For
theorem
MultiplicativeBasisDeformations.OrientedTree.ofStar_pre
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableEq D]
[DecidableRel T.orient]
{k : Type u}
[Field k]
{i l j : T.Dbl}
(a : i ⟶ l)
(F : T.Sp k l)
:
(RelSystem.ofStar j) ((pre a) F) = CategoryTheory.CategoryStruct.comp (LinearPaths.arrow a) ((RelSystem.ofStar j) F)
theorem
MultiplicativeBasisDeformations.OrientedTree.ofStar_mem_Id
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableEq D]
[DecidableRel T.orient]
{k : Type u}
[Field k]
{i j : T.Dbl}
{F : T.Sp k i}
(hF : F ∈ T.Ist k i)
:
(RelSystem.ofStar j) F ∈ T.Id k i j
theorem
MultiplicativeBasisDeformations.OrientedTree.toStar_mem_Ist
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableEq D]
[DecidableRel T.orient]
{k : Type u}
[Field k]
{i j : T.Dbl}
{f : LinearPaths.obj i ⟶ LinearPaths.obj j}
(hf : f ∈ T.Id k i j)
:
(RelSystem.toStar j) f ∈ T.Ist k i
theorem
MultiplicativeBasisDeformations.OrientedTree.exact_hom
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableEq D]
[DecidableRel T.orient]
{k : Type u}
[Field k]
{i j : T.Dbl}
(w : (e : T.OutArrow i) → LinearPaths.obj e.fst ⟶ LinearPaths.obj j)
(hw : ∑ e : T.OutArrow i, CategoryTheory.CategoryStruct.comp (LinearPaths.arrow e.snd) (w e) ∈ T.Id k i j)
:
∃ (W : LinearPaths.obj i ⟶ LinearPaths.obj j),
∀ (e : T.OutArrow i),
w e - ↑(T.sgn k i e.fst) • CategoryTheory.CategoryStruct.comp (LinearPaths.arrow (rev e)) W ∈ T.Id k e.fst j
Middle exactness with a fixed endpoint.
Degree projections #
theorem
MultiplicativeBasisDeformations.OrientedTree.proj_arrow_comp
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableEq D]
[DecidableRel T.orient]
{k : Type u}
[Field k]
{i l j : T.Dbl}
(a : i ⟶ l)
(d : ℕ)
(F : LinearPaths.obj l ⟶ LinearPaths.obj j)
:
(LinearPaths.proj (d + 1) i j) (CategoryTheory.CategoryStruct.comp (LinearPaths.arrow a) F) = CategoryTheory.CategoryStruct.comp (LinearPaths.arrow a) ((LinearPaths.proj d l j) F)
theorem
MultiplicativeBasisDeformations.OrientedTree.proj_zero_arrow_comp
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableEq D]
[DecidableRel T.orient]
{k : Type u}
[Field k]
{i l j : T.Dbl}
(a : i ⟶ l)
(F : LinearPaths.obj l ⟶ LinearPaths.obj j)
:
(LinearPaths.proj 0 i j) (CategoryTheory.CategoryStruct.comp (LinearPaths.arrow a) F) = 0
theorem
MultiplicativeBasisDeformations.OrientedTree.proj_mem_Id
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableEq D]
[DecidableRel T.orient]
{k : Type u}
[Field k]
{x y : T.Dbl}
(d : ℕ)
{f : LinearPaths.obj x ⟶ LinearPaths.obj y}
(hf : f ∈ T.Id k x y)
:
(LinearPaths.proj d x y) f ∈ T.Id k x y
The ideal of Π(Δ) is graded.
The graded pieces e_i Π_d e_j #
noncomputable def
MultiplicativeBasisDeformations.OrientedTree.Wsp
{D : Type v}
(T : OrientedTree D)
[Fintype D]
[DecidableRel T.orient]
(k : Type u)
[Field k]
(i j : T.Dbl)
(d : ℕ)
:
Submodule k ((LinearPaths.obj i ⟶ LinearPaths.obj j) ⧸ T.Id k i j)
e_i Π_d e_j, inside kQ(i, j) modulo the ideal.
Instances For
instance
MultiplicativeBasisDeformations.OrientedTree.fd_degreePart
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableEq D]
[DecidableRel T.orient]
{k : Type u}
[Field k]
(i j : T.Dbl)
(d : ℕ)
:
FiniteDimensional k ↥(LinearPaths.degreePart d i j)
instance
MultiplicativeBasisDeformations.OrientedTree.instFiniteDimensionalSubtypeQuotientHomLinearPathsDblObjSubmoduleIdMemWsp
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableEq D]
[DecidableRel T.orient]
{k : Type u}
[Field k]
(i j : T.Dbl)
(d : ℕ)
:
FiniteDimensional k ↥(T.Wsp k i j d)
noncomputable def
MultiplicativeBasisDeformations.OrientedTree.lcomp
{D : Type v}
{T : OrientedTree D}
{k : Type u}
[Field k]
{i l : T.Dbl}
(a : i ⟶ l)
(j : T.Dbl)
:
(LinearPaths.obj l ⟶ LinearPaths.obj j) →ₗ[k] LinearPaths.obj i ⟶ LinearPaths.obj j
Prefixing an arrow, on kQ(·, j).
Instances For
noncomputable def
MultiplicativeBasisDeformations.OrientedTree.lq
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableRel T.orient]
{k : Type u}
[Field k]
{i l : T.Dbl}
(a : i ⟶ l)
(j : T.Dbl)
:
(LinearPaths.obj l ⟶ LinearPaths.obj j) ⧸ T.Id k l j →ₗ[k] (LinearPaths.obj i ⟶ LinearPaths.obj j) ⧸ T.Id k i j
Prefixing an arrow, on e_l Π e_j → e_i Π e_j.
Instances For
theorem
MultiplicativeBasisDeformations.OrientedTree.lq_mkQ
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableEq D]
[DecidableRel T.orient]
{k : Type u}
[Field k]
{i l j : T.Dbl}
(a : i ⟶ l)
(f : LinearPaths.obj l ⟶ LinearPaths.obj j)
:
(lq a j) ((T.Id k l j).mkQ f) = (T.Id k i j).mkQ (CategoryTheory.CategoryStruct.comp (LinearPaths.arrow a) f)
theorem
MultiplicativeBasisDeformations.OrientedTree.lq_mem
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableEq D]
[DecidableRel T.orient]
{k : Type u}
[Field k]
{i l j : T.Dbl}
(a : i ⟶ l)
(d : ℕ)
{x : (LinearPaths.obj l ⟶ LinearPaths.obj j) ⧸ T.Id k l j}
(hx : x ∈ T.Wsp k l j d)
:
noncomputable def
MultiplicativeBasisDeformations.OrientedTree.G'
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableEq D]
[DecidableRel T.orient]
{k : Type u}
[Field k]
(i j : T.Dbl)
(d : ℕ)
:
⊕_{l∼i} e_l Π_d e_j → e_i Π_{d+1} e_j.
Instances For
noncomputable def
MultiplicativeBasisDeformations.OrientedTree.F'
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableEq D]
[DecidableRel T.orient]
{k : Type u}
[Field k]
(i j : T.Dbl)
(d : ℕ)
:
e_i Π_d e_j → ⊕_{l∼i} e_l Π_{d+1} e_j, with the signs of the relation.
Instances For
theorem
MultiplicativeBasisDeformations.OrientedTree.exists_rep
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableEq D]
[DecidableRel T.orient]
{k : Type u}
[Field k]
{l j : T.Dbl}
{d : ℕ}
(x : ↥(T.Wsp k l j d))
:
∃ w ∈ LinearPaths.degreePart d l j, (T.Id k l j).mkQ w = ↑x
theorem
MultiplicativeBasisDeformations.OrientedTree.ker_G'_le
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableEq D]
[DecidableRel T.orient]
{k : Type u}
[Field k]
(i j : T.Dbl)
(d : ℕ)
:
Middle exactness in each degree.
theorem
MultiplicativeBasisDeformations.OrientedTree.G'_zero_injective
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableEq D]
[DecidableRel T.orient]
{k : Type u}
[Field k]
(i j : T.Dbl)
:
Function.Injective ⇑(G' i j 0)
theorem
MultiplicativeBasisDeformations.OrientedTree.sum_finrank_le
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableEq D]
[DecidableRel T.orient]
{k : Type u}
[Field k]
(i j : T.Dbl)
(d : ℕ)
:
The dimension inequalities ∑_{l∼i} h_l(d+1) ≤ h_i(d+2) + h_i(d).
theorem
MultiplicativeBasisDeformations.OrientedTree.sum_finrank_le_zero
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableEq D]
[DecidableRel T.orient]
{k : Type u}
[Field k]
(i j : T.Dbl)
:
theorem
MultiplicativeBasisDeformations.OrientedTree.one_le_finrank_nil
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableEq D]
[DecidableRel T.orient]
{k : Type u}
[Field k]
(j : T.Dbl)
:
1 ≤ Module.finrank k ↥(T.Wsp k j j 0)
theorem
MultiplicativeBasisDeformations.OrientedTree.exists_path_of_finrank
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableEq D]
[DecidableRel T.orient]
{k : Type u}
[Field k]
{i j : T.Dbl}
{d : ℕ}
(h : 1 ≤ Module.finrank k ↥(T.Wsp k i j d))
:
∃ (p : Quiver.Path i j), p.length = d ∧ LinearPaths.path p ∉ T.Id k i j
A nonzero graded piece contains a path outside the ideal.
noncomputable def
MultiplicativeBasisDeformations.OrientedTree.adjM
{D : Type v}
(T : OrientedTree D)
:
The adjacency matrix of Δ.
Instances For
theorem
MultiplicativeBasisDeformations.OrientedTree.sum_outArrow
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableEq D]
[DecidableRel T.orient]
(i : T.Dbl)
(f : T.Dbl → ℤ)
:
theorem
MultiplicativeBasisDeformations.OrientedTree.U_le_finrank
{D : Type v}
{T : OrientedTree D}
[Fintype D]
[DecidableEq D]
[DecidableRel T.orient]
{k : Type u}
[Field k]
(j : T.Dbl)
(N : ℕ)
(hU : ∀ d ≤ N, ∀ (a b : T.Dbl), 0 ≤ UBound.U T.adjM d a b)
(i : T.Dbl)
:
The lower bound (dim e_i Π_N e_j)_{ij} ≥ U_N when U_0, …, U_N ≥ 0
(periodic-mesh-calculations.tex).