Skeletality of a string bound-quiver quotient

The positive-length path filtration is closed under composition. A morphism between distinct displayed vertices lies in its first step, whereas the identity does not. Thus two distinct displayed vertices cannot become isomorphic in the quotient category.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.quotientHomLengthTail {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (x y : Q) (n : ℕ) : Submodule k (obj P.relations y ⟶ obj P.relations x)

The subspace of a quotient Hom space spanned by surviving paths of length at least n. The endpoint order follows the quotient category's contravariant path convention.

def MagnitudeConjecture.BoundQuiver.StringPresentation.survivingArrowPath {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : SurvivingPath P.relations x y

A displayed arrow, regarded as a surviving path of length one.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.survivingArrowPath_length {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : (↑(P.survivingArrowPath a)).length = 1

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.survivingPathBasis_survivingArrowPath {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : (survivingPathBasis P.relations ⋯ x y) (P.survivingArrowPath a) = arrowMap P.relations a

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.survivingPathBasis_mem_quotientHomLengthTail {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (x y : Q) (n : ℕ) (p : SurvivingPath P.relations x y) (hp : n ≤ (↑p).length) : (survivingPathBasis P.relations ⋯ x y) p ∈ P.quotientHomLengthTail x y n

A surviving-path basis vector belongs to every Hom tail below its path length.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientHomLengthTail_one_eq_top_of_ne {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (hxy : x ≠ y) : P.quotientHomLengthTail x y 1 = ⊤

Between distinct displayed vertices, every quotient morphism has positive path length.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientHomLengthTail_antitone {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (x y : Q) {m n : ℕ} (hmn : m ≤ n) : P.quotientHomLengthTail x y n ≤ P.quotientHomLengthTail x y m

The quotient Hom path filtration is decreasing.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.comp_mem_quotientHomLengthTail {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y z : Q} {i j : ℕ} {f : obj P.relations y ⟶ obj P.relations x} {g : obj P.relations z ⟶ obj P.relations y} (hf : f ∈ P.quotientHomLengthTail x y i) (hg : g ∈ P.quotientHomLengthTail y z j) : CategoryTheory.CategoryStruct.comp g f ∈ P.quotientHomLengthTail x z (i + j)

Composition adds lower bounds in the quotient Hom path filtration.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.smul_arrowMap_sub_smul_arrowMap_not_mem_lengthTail_two {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} {a b : x ⟶ y} (hab : a ≠ b) {c d : k} (hc : c ≠ 0) : c • arrowMap P.relations a - d • arrowMap P.relations b ∉ P.quotientHomLengthTail x y 2

Two distinct displayed arrows remain linearly distinct modulo the length-two path tail.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientHomLengthTail_self_eq_quotientVertexEndLengthTail {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (x : Q) (n : ℕ) : P.quotientHomLengthTail x x n = P.quotientVertexEndLengthTail x n

On an endomorphism space, the Hom path tail is the previously defined endomorphism-ring path tail.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientIdentity_not_mem_quotientHomLengthTail_one {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (x : Q) : CategoryTheory.CategoryStruct.id (obj P.relations x) ∉ P.quotientHomLengthTail x x 1

The identity of a displayed quotient vertex does not have positive path length.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.scalar_ne_zero_of_isIso_of_eq_smul_one_add_tail {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (y : Q) (f : CategoryTheory.End (obj P.relations y)) [CategoryTheory.IsIso f] {c : k} {r : CategoryTheory.End (obj P.relations y)} (hr : r ∈ P.quotientVertexEndLengthTail y 1) (hfr : f = c • 1 + r) : c ≠ 0

The scalar part of an invertible vertex endomorphism is nonzero.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrow_eq_of_iso_square {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a b : x ⟶ y) (ex : obj P.relations x ≅ obj P.relations x) (ey : obj P.relations y ≅ obj P.relations y) (hcomm : CategoryTheory.CategoryStruct.comp (arrowMap P.relations a) ex.hom = CategoryTheory.CategoryStruct.comp ey.hom (arrowMap P.relations b)) : a = b

A commuting square with invertible vertex endomorphisms cannot identify two distinct displayed arrows.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.eq_of_quotientVertex_iso {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (e : obj P.relations x ≅ obj P.relations y) : x = y

Isomorphic displayed vertices of a string quotient are equal.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientCategory_skeletal {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) : CategoryTheory.Skeletal (Category P.relations)

The quotient category of a string presentation is skeletal.