Basicness of admissible bound-quiver algebras

The positive path-length filtration survives an arbitrary admissible relation quotient; no monomial hypothesis is needed. Its positive part is nilpotent, every vertex endomorphism is a scalar plus a positive term, and maps between distinct displayed vertices are positive. Consequently the displayed vertex endomorphism rings are local and the quotient category is skeletal.

noncomputable def MagnitudeConjecture.BoundQuiver.relationQuotientObjectEquiv {k Q : Type u} [Field k] [Quiver Q] (R : RelationFamily k Q) : Category R ≃ Q

The objects of any relation quotient are exactly its displayed quiver vertices.

noncomputable def MagnitudeConjecture.BoundQuiver.IsAdmissible.quotientHomLengthTail {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (_hR : IsAdmissible R) (X Y : LinearPathCategory.Category k Q) (n : ℕ) : Submodule k (LinearPathCategory.HomogeneousQuotient.obj R X ⟶ LinearPathCategory.HomogeneousQuotient.obj R Y)

The image of the free path-length tail in a quotient Hom space.

theorem MagnitudeConjecture.BoundQuiver.IsAdmissible.quotientHomLengthTail_zero_eq_top {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R : RelationFamily k Q} (hR : IsAdmissible R) (X Y : LinearPathCategory.Category k Q) : hR.quotientHomLengthTail X Y 0 = ⊤

The zeroth quotient path tail is the full Hom space.

theorem MagnitudeConjecture.BoundQuiver.IsAdmissible.quotientHomLengthTail_antitone {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R : RelationFamily k Q} (hR : IsAdmissible R) (X Y : LinearPathCategory.Category k Q) {m n : ℕ} (hmn : m ≤ n) : hR.quotientHomLengthTail X Y n ≤ hR.quotientHomLengthTail X Y m

Raising the cutoff shrinks the quotient path-length tail.

theorem MagnitudeConjecture.BoundQuiver.IsAdmissible.comp_mem_quotientHomLengthTail {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R : RelationFamily k Q} (hR : IsAdmissible R) {X Y Z : LinearPathCategory.Category k Q} {i j : ℕ} {f : LinearPathCategory.HomogeneousQuotient.obj R X ⟶ LinearPathCategory.HomogeneousQuotient.obj R Y} {g : LinearPathCategory.HomogeneousQuotient.obj R Y ⟶ LinearPathCategory.HomogeneousQuotient.obj R Z} (hf : f ∈ hR.quotientHomLengthTail X Y i) (hg : g ∈ hR.quotientHomLengthTail Y Z j) : CategoryTheory.CategoryStruct.comp f g ∈ hR.quotientHomLengthTail X Z (i + j)

Composition adds lower bounds in the quotient path filtration.

theorem MagnitudeConjecture.BoundQuiver.IsAdmissible.exists_quotientHomLengthTail_eq_bot {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R : RelationFamily k Q} (hR : IsAdmissible R) (X Y : LinearPathCategory.Category k Q) : ∃ (n : ℕ), hR.quotientHomLengthTail X Y n = ⊥

The admissibility cutoff makes a sufficiently deep quotient tail zero.

theorem MagnitudeConjecture.BoundQuiver.IsAdmissible.quotientHomLengthTail_one_eq_top_of_vertex_ne {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R : RelationFamily k Q} (hR : IsAdmissible R) {X Y : LinearPathCategory.Category k Q} (hXY : LinearPathCategory.vertex Y ≠ LinearPathCategory.vertex X) : hR.quotientHomLengthTail X Y 1 = ⊤

Every map between distinct displayed vertices belongs to the positive quotient path tail.

theorem MagnitudeConjecture.BoundQuiver.IsAdmissible.exists_eq_smul_one_add_mem_quotientHomLengthTail_one {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R : RelationFamily k Q} (hR : IsAdmissible R) (X : LinearPathCategory.Category k Q) (f : CategoryTheory.End (LinearPathCategory.HomogeneousQuotient.obj R X)) : ∃ (c : k) (r : CategoryTheory.End (LinearPathCategory.HomogeneousQuotient.obj R X)), r.asHom ∈ hR.quotientHomLengthTail X X 1 ∧ f = c • 1 + r

Every quotient vertex endomorphism is a scalar identity plus an element of the positive path tail.

theorem MagnitudeConjecture.BoundQuiver.IsAdmissible.isNilpotent_of_mem_quotientHomLengthTail_one {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R : RelationFamily k Q} (hR : IsAdmissible R) (X : LinearPathCategory.Category k Q) (r : CategoryTheory.End (LinearPathCategory.HomogeneousQuotient.obj R X)) (hr : r.asHom ∈ hR.quotientHomLengthTail X X 1) : IsNilpotent r

Positive-tail vertex endomorphisms are nilpotent.

theorem MagnitudeConjecture.BoundQuiver.IsAdmissible.quotientVertexEnd_nontrivial {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R : RelationFamily k Q} (hR : IsAdmissible R) (X : LinearPathCategory.Category k Q) : Nontrivial (CategoryTheory.End (LinearPathCategory.HomogeneousQuotient.obj R X))

The quotient identity at a displayed vertex is nonzero.

theorem MagnitudeConjecture.BoundQuiver.IsAdmissible.quotientVertexEnd_isLocalRing {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R : RelationFamily k Q} (hR : IsAdmissible R) (X : LinearPathCategory.Category k Q) : IsLocalRing (CategoryTheory.End (LinearPathCategory.HomogeneousQuotient.obj R X))

Every displayed vertex has a local endomorphism ring.

theorem MagnitudeConjecture.BoundQuiver.IsAdmissible.quotientEnd_isLocalRing {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R : RelationFamily k Q} (hR : IsAdmissible R) (Y : Category R) : IsLocalRing (CategoryTheory.End Y)

Every quotient object is represented by a displayed vertex, so every endomorphism ring is local.

theorem MagnitudeConjecture.BoundQuiver.IsAdmissible.eq_of_quotientVertex_iso {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R : RelationFamily k Q} (hR : IsAdmissible R) {x y : Q} (e : obj R x ≅ obj R y) : x = y

Isomorphic displayed quotient vertices are equal.

theorem MagnitudeConjecture.BoundQuiver.IsAdmissible.quotientCategory_skeletal {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R : RelationFamily k Q} (hR : IsAdmissible R) : CategoryTheory.Skeletal (Category R)

The quotient category of an admissible relation family is skeletal.