Bound-quiver and special-biserial presentations

This file records the literal bound-quiver convention used in the frozen manuscript. A relation family is admissible when its generated two-sided ideal contains no terms of path length below two and contains every sufficiently long path. A bound-quiver presentation identifies an algebra with the finite category algebra of that quotient. The special-biserial conditions are then imposed on the displayed arrows and their nonzero two-arrow compositions in the quotient.

The free linear category uses the reversed categorical orientation: pathMap p is a morphism from the endpoint of p to its source. The quiver itself, and hence the degree and continuation conditions below, retain the usual path-algebra orientation.

instance MagnitudeConjecture.BoundQuiver.boundedPathsFinite {Q : Type v} [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (n : ℕ) (x y : Q) : Finite (Quiver.Path.BoundedPaths x y n)

Bounded paths in a finite quiver form a finite type, even when the unbounded path type is infinite because the quiver has oriented cycles.

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.RelationFamily (k : Type u) (Q : Type v) [Field k] [Quiver Q] : Type (max v (max u v) w)

A family of relations in the free linear category on Q.

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.Category {k : Type u} {Q : Type v} [Field k] [Quiver Q] (R : RelationFamily k Q) : Type v

The quotient of the free linear path category by a relation family.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.BoundQuiver.categoryFintype {k : Type u} {Q : Type v} [Field k] [Fintype Q] [Quiver Q] (R : RelationFamily k Q) : Fintype (Category R)

A quotient path category has the same finite object set as its displayed quiver.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.BoundQuiver.obj {k : Type u} {Q : Type v} [Field k] [Quiver Q] (R : RelationFamily k Q) (x : Q) : Category R

A quiver vertex as an object of the relation quotient.

noncomputable def MagnitudeConjecture.BoundQuiver.pathMap {k : Type u} {Q : Type v} [Field k] [Quiver Q] (R : RelationFamily k Q) {x y : Q} (p : Quiver.Path x y) : obj R y ⟶ obj R x

The image in the quotient category of a path in the displayed quiver.

noncomputable def MagnitudeConjecture.BoundQuiver.arrowMap {k : Type u} {Q : Type v} [Field k] [Quiver Q] (R : RelationFamily k Q) {x y : Q} (a : x ⟶ y) : obj R y ⟶ obj R x

The image in the quotient category of one displayed quiver arrow.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.pathMap_comp {k : Type u} {Q : Type v} [Field k] [Quiver Q] (R : RelationFamily k Q) {x y z : Q} (p : Quiver.Path x y) (q : Quiver.Path y z) : CategoryTheory.CategoryStruct.comp (pathMap R q) (pathMap R p) = pathMap R (p.comp q)

structure MagnitudeConjecture.BoundQuiver.IsAdmissible {k : Type u} {Q : Type v} [Field k] [Quiver Q] (R : RelationFamily k Q) : Prop

The usual admissibility condition J^N ⊆ I ⊆ J² for a relation ideal in a path algebra, expressed in the free linear path category.

• relationIdeal_le_lengthTail_two (X Y : LinearPathCategory.Category k Q) : QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k R X Y ≤ LinearPathCategory.lengthTail X Y 2
• long_paths_mem : ∃ (N : ℕ), 2 ≤ N ∧ ∀ {x y : Q} (p : Quiver.Path x y), N ≤ p.length → LinearPathCategory.pathHom p ∈ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k R (LinearPathCategory.obj k Q y) (LinearPathCategory.obj k Q x)

theorem MagnitudeConjecture.BoundQuiver.eq_zero_of_mem_lengthComponent_one_of_mem_lengthTail_two {k : Type u} {Q : Type v} [Field k] [Quiver Q] {X Y : LinearPathCategory.Category k Q} {f : X ⟶ Y} (hone : f ∈ LinearPathCategory.lengthComponent X Y 1) (htwo : f ∈ LinearPathCategory.lengthTail X Y 2) : f = 0

Degree one and the tail of degree at least two meet only in zero.

theorem MagnitudeConjecture.BoundQuiver.quotientHomLinearMap_injOn_lengthComponent_one {k : Type u} {Q : Type v} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) (X Y : LinearPathCategory.Category k Q) : Set.InjOn ⇑(LinearPathCategory.HomogeneousQuotient.quotientHomLinearMap R X Y) ↑(LinearPathCategory.lengthComponent X Y 1)

Admissibility makes the quotient map injective on the entire degree-one subspace.

theorem MagnitudeConjecture.BoundQuiver.pathMap_ne_zero_of_length_lt_two {k : Type u} {Q : Type v} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) {x y : Q} (p : Quiver.Path x y) (hp : p.length < 2) : pathMap R p ≠ 0

A path of length below two survives every admissible quotient.

theorem MagnitudeConjecture.BoundQuiver.arrowMap_ne_zero {k : Type u} {Q : Type v} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) {x y : Q} (a : x ⟶ y) : arrowMap R a ≠ 0

In particular, every displayed arrow survives an admissible quotient.

theorem MagnitudeConjecture.BoundQuiver.arrowMap_linearIndependent {k : Type u} {Q : Type v} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) (x y : Q) : LinearIndependent k fun (a : x ⟶ y) => arrowMap R a

The images of parallel displayed arrows remain linearly independent in an admissible quotient.

theorem MagnitudeConjecture.BoundQuiver.span_boundedPathMap_eq_top {k : Type u} {Q : Type v} [Field k] [Quiver Q] {R : RelationFamily k Q} {N : ℕ} (hlong : ∀ {x y : Q} (p : Quiver.Path x y), N ≤ p.length → LinearPathCategory.pathHom p ∈ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k R (LinearPathCategory.obj k Q y) (LinearPathCategory.obj k Q x)) (x y : Q) : Submodule.span k (Set.range fun (p : Quiver.Path.BoundedPaths y x (N - 1)) => pathMap R ↑p) = ⊤

The images of paths shorter than an admissibility cutoff span every Hom space in the quotient.

theorem MagnitudeConjecture.BoundQuiver.quotientHom_finiteDimensional {k : Type u} {Q : Type v} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R : RelationFamily k Q} (hR : IsAdmissible R) (x y : Q) : FiniteDimensional k (obj R x ⟶ obj R y)

Every Hom space of a finite admissible bound-quiver quotient is finite-dimensional.

theorem MagnitudeConjecture.BoundQuiver.finiteRepresentablesOfAdmissible {k : Type u} {Q : Type v} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R : RelationFamily k Q} (hR : IsAdmissible R) (X : Category R) : CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule X)

Admissibility over a finite quiver supplies the finite-dimensional representables needed by the finite category-algebra construction.

theorem MagnitudeConjecture.BoundQuiver.finiteOppositeRepresentablesOfAdmissible {k : Type u} {Q : Type v} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {R : RelationFamily k Q} (hR : IsAdmissible R) (X : (Category R)ᵒᵖ) : CoveringHom.IsFiniteDimensionalModule k (CoveringHom.linearCoyonedaLinearModule X)

Admissibility also supplies finite-dimensional representables on the opposite quotient category. These are the literal projective right modules for the displayed bound quiver.

structure MagnitudeConjecture.BoundQuiver.Presentation (k A Q : Type u) [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] : Type u

A literal finite bound-quiver presentation of A. Finite-dimensionality of the quotient category algebra is derived from admissibility.

• relations : RelationFamily k Q
• admissible : IsAdmissible self.relations
• algebraEquiv : A ≃ₐ[k] CoveringHom.finiteCategoryProjectiveGenerator.algebra ⋯

structure MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation (k A Q : Type u) [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] extends MagnitudeConjecture.BoundQuiver.Presentation k A Q : Type u

A bound-quiver presentation satisfying the two degree bounds and the two unique-nonzero-continuation conditions of the manuscript.

• relations : RelationFamily k Q
• admissible : IsAdmissible self.relations
• algebraEquiv : A ≃ₐ[k] CoveringHom.finiteCategoryProjectiveGenerator.algebra ⋯
• arrows_starting_le_two (x : Q) : Nat.card (Quiver.Star x) ≤ 2
• arrows_ending_le_two (x : Q) : Nat.card (Quiver.Costar x) ≤ 2
• continuation_right_le_one {x y : Q} (a : x ⟶ y) : Nat.card { b : Quiver.Star y // CategoryTheory.CategoryStruct.comp (arrowMap self.relations b.snd) (arrowMap self.relations a) ≠ 0 } ≤ 1
• continuation_left_le_one {x y : Q} (a : x ⟶ y) : Nat.card { c : Quiver.Costar x // CategoryTheory.CategoryStruct.comp (arrowMap self.relations a) (arrowMap self.relations c.snd) ≠ 0 } ≤ 1

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.mapAlgEquiv {k A B : Type u} [Field k] [Ring A] [Algebra k A] [Ring B] [Algebra k B] {Q' : Type u} [Fintype Q'] [Quiver Q'] [(x y : Q') → Fintype (x ⟶ y)] (P : SpecialBiserialPresentation k A Q') (e : B ≃ₐ[k] A) : SpecialBiserialPresentation k B Q'

Transport a special-biserial presentation across an algebra equivalence.

structure MagnitudeConjecture.BoundQuiver.SpecialBiserialModel (k A : Type u) [Field k] [Ring A] [Algebra k A] : Type (u + 1)

A universe-local bundle of a finite quiver and a special-biserial presentation. Bundling the instances makes the existence predicate below a literal proposition rather than an interface with a hidden chosen quiver.

• Vertex : Type u
• vertexFintype : Fintype self.Vertex
• quiver : Quiver self.Vertex
• arrowFintype (x y : self.Vertex) : Fintype (x ⟶ y)
• presentation : SpecialBiserialPresentation k A self.Vertex

def MagnitudeConjecture.BoundQuiver.AdmitsSpecialBiserialPresentation (k A : Type u) [Field k] [Ring A] [Algebra k A] : Prop

A basic algebra admits the manuscript's special-biserial bound-quiver presentation. The final theorem will apply this predicate to a chosen basic algebra of the original algebra.

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialModel.mapAlgEquiv {k A B : Type u} [Field k] [Ring A] [Algebra k A] [Ring B] [Algebra k B] (M : SpecialBiserialModel k A) (e : B ≃ₐ[k] A) : SpecialBiserialModel k B

Transport a bundled special-biserial model across an algebra equivalence.

theorem MagnitudeConjecture.BoundQuiver.admitsSpecialBiserialPresentation_iff_of_algEquiv {k A B : Type u} [Field k] [Ring A] [Algebra k A] [Ring B] [Algebra k B] (e : A ≃ₐ[k] B) : AdmitsSpecialBiserialPresentation k A ↔ AdmitsSpecialBiserialPresentation k B

Admitting a special-biserial bound-quiver presentation is invariant under algebra equivalence.