Local vertex endomorphism rings of string quotients

At a displayed vertex of an admissible monomial bound-quiver quotient, the surviving loops form a basis. Splitting off the trivial loop writes every endomorphism as a scalar identity plus a positive-length tail. Path length is additive under multiplication, while admissibility kills every sufficiently long path, so the positive tail is nilpotent. Consequently the vertex endomorphism ring is local.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.quotientVertexEndLinearEquiv {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) : (obj P.relations y ⟶ obj P.relations y) ≃ₗ[k] CategoryTheory.End (obj P.relations y)

Regard a vertex endomorphism in the quotient category as an element of its endomorphism ring.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.quotientVertexEndBasis {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) : Module.Basis (SurvivingPath P.relations y y) k (CategoryTheory.End (obj P.relations y))

The surviving-loop basis, regarded as a basis of the vertex endomorphism ring.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientVertexEndBasis_apply {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) (p : SurvivingPath P.relations y y) : (P.quotientVertexEndBasis y) p = CategoryTheory.End.of (pathMap P.relations ↑p)

def MagnitudeConjecture.BoundQuiver.StringPresentation.nilSurvivingLoop {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) : SurvivingPath P.relations y y

The surviving trivial loop at a displayed vertex.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientVertexEndBasis_nilSurvivingLoop {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) : (P.quotientVertexEndBasis y) (P.nilSurvivingLoop y) = 1

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.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) (y : Q) (n : ℕ) : Submodule k (CategoryTheory.End (obj P.relations y))

The subspace spanned by surviving loops of length at least n.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientVertexEndBasis_mem_lengthTail {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) (n : ℕ) (p : SurvivingPath P.relations y y) (hp : n ≤ (↑p).length) : (P.quotientVertexEndBasis y) p ∈ P.quotientVertexEndLengthTail y n

A surviving-loop basis vector lies in every tail below its length.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientVertexEndLengthTail_zero_eq_top {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) : P.quotientVertexEndLengthTail y 0 = ⊤

The length-zero tail is the whole vertex endomorphism ring.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientVertexEndLengthTail_eq_bot_of_forall_lt {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) (n : ℕ) (hn : ∀ (p : SurvivingPath P.relations y y), (↑p).length < n) : P.quotientVertexEndLengthTail y n = ⊥

If no surviving loop reaches length n, then the nth tail is zero.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.exists_quotientVertexEndLengthTail_eq_bot {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) : ∃ (n : ℕ), P.quotientVertexEndLengthTail y n = ⊥

Admissibility makes one sufficiently deep surviving-loop tail zero.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.mul_mem_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) (y : Q) {i j : ℕ} {f g : CategoryTheory.End (obj P.relations y)} (hf : f ∈ P.quotientVertexEndLengthTail y i) (hg : g ∈ P.quotientVertexEndLengthTail y j) : f * g ∈ P.quotientVertexEndLengthTail y (i + j)

Multiplication adds lower bounds on the lengths of surviving loops.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.exists_eq_smul_one_add_mem_quotientVertexEndLengthTail_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) (y : Q) (f : CategoryTheory.End (obj P.relations y)) : ∃ (c : k), ∃ r ∈ P.quotientVertexEndLengthTail y 1, f = c • 1 + r

Every vertex endomorphism is a scalar identity plus a positive-length tail.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.isNilpotent_of_mem_quotientVertexEndLengthTail_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) (y : Q) (r : CategoryTheory.End (obj P.relations y)) (hr : r ∈ P.quotientVertexEndLengthTail y 1) : IsNilpotent r

Positive-length vertex endomorphisms are nilpotent.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientVertexEnd_nontrivial {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) : Nontrivial (CategoryTheory.End (obj P.relations y))

The endomorphism ring of a displayed quotient vertex is nontrivial, witnessed by the surviving trivial path.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientVertexEnd_isLocalRing {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) : IsLocalRing (CategoryTheory.End (obj P.relations y))

Every displayed vertex of an admissible monomial bound-quiver quotient has a local endomorphism ring.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.quotientEnd_isLocalRing {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 : Category P.relations) : IsLocalRing (CategoryTheory.End X)

Every object of the quotient category is represented by a displayed vertex, so all of its endomorphism rings are local.