Independent vocabulary for the magnitude theorem

These definitions use only Mathlib. They describe finite representation type, the inverse Hom-matrix sum, simple modules, and special biserial presentations in the Morita class. Connections to the proof library belong in separate modules.

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

One representative of each finite-dimensional indecomposable right module. Existence of such a family expresses finite representation type.

• size : ℕ
• obj : Fin self.size → ModuleCat Aᵐᵒᵖ
• finite (i : Fin self.size) : Module.Finite k ↑(self.obj i)
• indecomposable (i : Fin self.size) : CategoryTheory.Indecomposable (self.obj i)
• distinct {i j : Fin self.size} : Nonempty (self.obj i ≅ self.obj j) → i = j
• complete (M : ModuleCat Aᵐᵒᵖ) : Module.Finite k ↑M → CategoryTheory.Indecomposable M → ∃ (i : Fin self.size), Nonempty (M ≅ self.obj i)

noncomputable def MagnitudeConjecture.Statement.homMatrix (k A : Type u) [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) : Matrix (Fin S.size) (Fin S.size) ℚ

The Hom-dimension matrix, with rational coefficients.

noncomputable def MagnitudeConjecture.Statement.magnitude (k A : Type u) [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) : ℚ

The sum of the entries of the inverse Hom-dimension matrix. Nonsingularity is asserted separately in the full statement below.

noncomputable def MagnitudeConjecture.Statement.simpleCount (k A : Type u) [Field k] [Ring A] [Algebra k A] (S : IndecomposableFamily k A) : ℕ

The number of isomorphism classes of simple right modules, counted inside the complete family; simplicity is Mathlib's module-theoretic notion.

noncomputable def MagnitudeConjecture.Statement.QuiverPresentation.representable (k Q : Type u) [Field k] [Quiver Q] (i : Q) : CategoryTheory.Functor (CategoryTheory.Paths Q) (ModuleCat k)

The representation freely generated at a vertex: its component at j has a basis consisting of the paths from i to j.

theorem MagnitudeConjecture.Statement.QuiverPresentation.representable_map_single (k Q : Type u) [Field k] [Quiver Q] (i : Q) {a b : Q} (p : Quiver.Path a b) (q : Quiver.Path i a) (c : k) : (CategoryTheory.ConcreteCategory.hom ((representable k Q i).map p)) (Finsupp.single q c) = Finsupp.single (q.comp p) c

Paths act by concatenation on the free representation.

@[reducible, inline]

abbrev MagnitudeConjecture.Statement.QuiverPresentation.FreeCategory (k Q : Type u) [Field k] [Quiver Q] : Type u

The free linear path category, in the reversed orientation supplied by covariant representables. Its objects are exactly the vertices of Q.

noncomputable def MagnitudeConjecture.Statement.QuiverPresentation.coefficients (k Q : Type u) [Field k] [Quiver Q] {X Y : FreeCategory k Q} (f : X ⟶ Y) : Quiver.Path (have this := Y; this) (have this := X; this) →₀ k

The coefficient vector of a morphism, obtained by evaluating at the stationary path.

noncomputable def MagnitudeConjecture.Statement.QuiverPresentation.pathHom (k Q : Type u) [Field k] [Quiver Q] {x y : Q} (p : Quiver.Path x y) : (have this := y; this) ⟶ have this := x; this

Prepending a path gives the corresponding morphism of representables.

noncomputable def MagnitudeConjecture.Statement.QuiverPresentation.ideal {k Q : Type u} [Field k] [Quiver Q] (R : (X Y : FreeCategory k Q) → Set (X ⟶ Y)) (X Y : FreeCategory k Q) : Submodule k (X ⟶ Y)

The two-sided linear ideal generated by the stated relations.

theorem MagnitudeConjecture.Statement.QuiverPresentation.precomp {k Q : Type u} [Field k] [Quiver Q] (R : (X Y : FreeCategory k Q) → Set (X ⟶ Y)) {X Y Z : FreeCategory k Q} (f : X ⟶ Y) {g : Y ⟶ Z} (hg : g ∈ ideal R Y Z) : CategoryTheory.CategoryStruct.comp f g ∈ ideal R X Z

The generated ideal is closed under precomposition.

theorem MagnitudeConjecture.Statement.QuiverPresentation.postcomp {k Q : Type u} [Field k] [Quiver Q] (R : (X Y : FreeCategory k Q) → Set (X ⟶ Y)) {X Y Z : FreeCategory k Q} {f : X ⟶ Y} (g : Y ⟶ Z) (hf : f ∈ ideal R X Y) : CategoryTheory.CategoryStruct.comp f g ∈ ideal R X Z

The generated ideal is closed under postcomposition.

def MagnitudeConjecture.Statement.QuiverPresentation.rel {k Q : Type u} [Field k] [Quiver Q] (R : (X Y : FreeCategory k Q) → Set (X ⟶ Y)) : HomRel (FreeCategory k Q)

Equality modulo the relation ideal.

instance MagnitudeConjecture.Statement.QuiverPresentation.instCongruenceFreeCategoryRel {k Q : Type u} [Field k] [Quiver Q] (R : (X Y : FreeCategory k Q) → Set (X ⟶ Y)) : CategoryTheory.Congruence (rel R)

theorem MagnitudeConjecture.Statement.QuiverPresentation.add_compatible {k Q : Type u} [Field k] [Quiver Q] (R : (X Y : FreeCategory k Q) → Set (X ⟶ Y)) {X Y : FreeCategory k Q} (f₁ f₂ g₁ g₂ : X ⟶ Y) (hf : rel R f₁ f₂) (hg : rel R g₁ g₂) : rel R (f₁ + g₁) (f₂ + g₂)

Addition respects equality modulo the generated ideal.

@[reducible, inline]

abbrev MagnitudeConjecture.Statement.QuiverPresentation.QuotientCategory {k Q : Type u} [Field k] [Quiver Q] (R : (X Y : FreeCategory k Q) → Set (X ⟶ Y)) : Type u

The bound-quiver category obtained by imposing the relations.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.Statement.QuiverPresentation.instPreadditiveQuotientCategory {k Q : Type u} [Field k] [Quiver Q] (R : (X Y : FreeCategory k Q) → Set (X ⟶ Y)) : CategoryTheory.Preadditive (QuotientCategory R)

instance MagnitudeConjecture.Statement.QuiverPresentation.instAdditiveFreeCategoryQuotientRelFunctor {k Q : Type u} [Field k] [Quiver Q] (R : (X Y : FreeCategory k Q) → Set (X ⟶ Y)) : (CategoryTheory.Quotient.functor (rel R)).Additive

@[instance_reducible]

noncomputable instance MagnitudeConjecture.Statement.QuiverPresentation.instLinearQuotientCategory {k Q : Type u} [Field k] [Quiver Q] (R : (X Y : FreeCategory k Q) → Set (X ⟶ Y)) : CategoryTheory.Linear k (QuotientCategory R)

noncomputable def MagnitudeConjecture.Statement.QuiverPresentation.pathMap {k Q : Type u} [Field k] [Quiver Q] (R : (X Y : FreeCategory k Q) → Set (X ⟶ Y)) {x y : Q} (p : Quiver.Path x y) : (CategoryTheory.Quotient.functor (rel R)).obj (have this := y; this) ⟶ (CategoryTheory.Quotient.functor (rel R)).obj (have this := x; this)

The image of a path in the relation quotient.

def MagnitudeConjecture.Statement.QuiverPresentation.IsLinearModule {k : Type u} [Field k] (C : Type u) [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : CategoryTheory.ObjectProperty (CategoryTheory.Functor C (ModuleCat k))

Covariant linear modules over a linear category.

@[reducible, inline]

abbrev MagnitudeConjecture.Statement.QuiverPresentation.LinearModules {k : Type u} [Field k] (C : Type u) [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : Type (u + 1)

def MagnitudeConjecture.Statement.QuiverPresentation.IsFiniteModule {k : Type u} [Field k] (C : Type u) [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : CategoryTheory.ObjectProperty (LinearModules C)

Finite-dimensional modules with finite object support.

@[reducible, inline]

abbrev MagnitudeConjecture.Statement.QuiverPresentation.FiniteModules {k : Type u} [Field k] (C : Type u) [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] : Type (u + 1)

def MagnitudeConjecture.Statement.QuiverPresentation.finiteRepresentable {k : Type u} [Field k] (C : Type u) [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (h : ∀ (X Y : C), FiniteDimensional k (X ⟶ Y)) (X : C) : FiniteModules C

A covariant representable, as a finite-dimensional linear module.

structure MagnitudeConjecture.Statement.QuiverPresentation.CategoryAlgebra {k : Type u} [Field k] (C : Type u) [CategoryTheory.Category.{u, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (h : ∀ (X Y : C), FiniteDimensional k (X ⟶ Y)) (B : Type u) [Ring B] [Algebra k B] : Type (u + 1)

The category algebra is the endomorphism algebra of the direct sum of its representable modules. The bicone records that finite direct sum by its universal property, independently of any choice of a library construction.

• generator : CategoryTheory.Limits.Bicone (finiteRepresentable C h)
• isBilimit : self.generator.IsBilimit
• algebraEquiv : B ≃ₐ[k] CategoryTheory.End self.generator.pt

structure MagnitudeConjecture.Statement.QuiverPresentation.Presentation {k Q : Type u} [Field k] [Quiver Q] [Fintype Q] (B : Type u) [Ring B] [Algebra k B] : Type (u + 1)

An admissible bound-quiver presentation with the special-biserial arrow bounds. The ideal conditions are exactly J^N ⊆ I ⊆ J², where J is the arrow ideal. Morphisms reverse path direction; both incoming and outgoing conditions are imposed, so the convention is symmetric.

• relations (X Y : FreeCategory k Q) : Set (X ⟶ Y)
• no_short_relations (X Y : FreeCategory k Q) (f : X ⟶ Y) : f ∈ ideal self.relations X Y → ∀ (p : Quiver.Path (have this := Y; this) (have this := X; this)), p.length < 2 → (coefficients k Q f) p = 0
• long_paths_vanish : ∃ (N : ℕ), 2 ≤ N ∧ ∀ {x y : Q} (p : Quiver.Path x y), N ≤ p.length → pathHom k Q p ∈ ideal self.relations y x
• finiteHom (X Y : QuotientCategory self.relations) : FiniteDimensional k (X ⟶ Y)
• algebra : CategoryAlgebra (QuotientCategory self.relations) ⋯ B
• outgoing_le_two (x : Q) : Nat.card ((y : Q) × (x ⟶ y)) ≤ 2
• incoming_le_two (y : Q) : Nat.card ((x : Q) × (x ⟶ y)) ≤ 2
• successor_le_one {x y : Q} (a : x ⟶ y) : Nat.card { b : (z : Q) × (y ⟶ z) // CategoryTheory.CategoryStruct.comp (pathMap self.relations b.snd.toPath) (pathMap self.relations a.toPath) ≠ 0 } ≤ 1
• predecessor_le_one {x y : Q} (a : x ⟶ y) : Nat.card { b : (z : Q) × (z ⟶ x) // CategoryTheory.CategoryStruct.comp (pathMap self.relations a.toPath) (pathMap self.relations b.snd.toPath) ≠ 0 } ≤ 1

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

A finite-dimensional special biserial algebra in the Morita class of A. This includes nonbasic A and uses k-linear Morita equivalence.

• Carrier : Type u
• ring : Ring self.Carrier
• algebra : Algebra k self.Carrier
• finiteDimensional : FiniteDimensional k self.Carrier
• morita : MoritaEquivalence k A self.Carrier
• Vertex : Type u
• vertices : Fintype self.Vertex
• quiver : Quiver self.Vertex
• arrows (i j : self.Vertex) : Fintype (i ⟶ j)
• presentation : QuiverPresentation.Presentation self.Carrier

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

Special biseriality with the paper's convention for nonbasic algebras.

def MagnitudeConjecture.Statement.MainClaim (k A : Type u) [Field k] [Ring A] [Algebra k A] [IsAlgClosed k] [FiniteDimensional k A] : Prop

The full magnitude assertion: for every complete finite indecomposable family, the Hom matrix is invertible and magnitude is at least the simple count, with equality exactly in the special biserial case.

This definition specifies the proposition; its proof is supplied separately.