String bound-quiver presentations

This file records the string-algebra convention used in the frozen manuscript. A relation ideal is monomial when, in every Hom space of the free linear path category, it is spanned by the individual paths killed by the quotient. Thus the nonzero images of paths form a basis of the quotient Hom space, and products of basis vectors are either zero or another basis vector.

A string presentation is a special-biserial presentation with this monomial condition. The bundled existence predicate retains the literal displayed quiver, while the transport lemmas show that only the presented algebra up to algebra equivalence matters.

@[reducible, inline]

abbrev MagnitudeConjecture.BoundQuiver.SurvivingPath {k Q : Type u} [Field k] [Quiver Q] (R : RelationFamily k Q) (x y : Q) : Type u

A path whose image in the relation quotient is nonzero.

def MagnitudeConjecture.BoundQuiver.IsMonomial {k Q : Type u} [Field k] [Quiver Q] (R : RelationFamily k Q) : Prop

A relation ideal is monomial when each of its Hom subspaces is the span of the individual paths killed by the quotient. This is the directly usable linear-category form of saying that the ideal is generated by paths.

theorem MagnitudeConjecture.BoundQuiver.pathMap_eq_zero_iff_mem_relationIdeal {k Q : Type u} [Field k] [Quiver Q] (R : RelationFamily k Q) {x y : Q} (p : Quiver.Path x y) : pathMap R p = 0 ↔ LinearPathCategory.pathHom p ∈ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k R (LinearPathCategory.obj k Q y) (LinearPathCategory.obj k Q x)

A path dies in the quotient exactly when its linearized path belongs to the generated relation ideal.

theorem MagnitudeConjecture.BoundQuiver.survivingPathFiniteOfAdmissible {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) : Finite (SurvivingPath R x y)

Admissibility bounds the lengths of all surviving paths, so the path basis of every quotient Hom space is finite.

theorem MagnitudeConjecture.BoundQuiver.survivingPathMap_linearIndependent {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsMonomial R) (x y : Q) : LinearIndependent k fun (p : SurvivingPath R x y) => pathMap R ↑p

In a monomial quotient, distinct surviving paths have linearly independent images.

theorem MagnitudeConjecture.BoundQuiver.span_survivingPathMap_eq_top {k Q : Type u} [Field k] [Quiver Q] (R : RelationFamily k Q) (x y : Q) : Submodule.span k (Set.range fun (p : SurvivingPath R x y) => pathMap R ↑p) = ⊤

The nonzero path images span the corresponding Hom space in every bound-quiver quotient.

noncomputable def MagnitudeConjecture.BoundQuiver.survivingPathBasis {k Q : Type u} [Field k] [Quiver Q] (R : RelationFamily k Q) (hR : IsMonomial R) (x y : Q) : Module.Basis (SurvivingPath R x y) k (obj R y ⟶ obj R x)

The surviving paths form the canonical path basis of each Hom space in a monomial bound-quiver quotient.

@[simp]

theorem MagnitudeConjecture.BoundQuiver.survivingPathBasis_apply {k Q : Type u} [Field k] [Quiver Q] (R : RelationFamily k Q) (hR : IsMonomial R) (x y : Q) (p : SurvivingPath R x y) : (survivingPathBasis R hR x y) p = pathMap R ↑p

theorem MagnitudeConjecture.BoundQuiver.finrank_quotientHom_eq_natCard_survivingPath {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (R : RelationFamily k Q) (hadm : IsAdmissible R) (hmono : IsMonomial R) (x y : Q) : Module.finrank k (obj R y ⟶ obj R x) = Nat.card (SurvivingPath R x y)

In an admissible monomial quotient, the Hom-space dimension counts the surviving paths with the specified endpoints.

theorem MagnitudeConjecture.BoundQuiver.survivingPathMap_comp_eq_zero_or_eq {k Q : Type u} [Field k] [Quiver Q] (R : RelationFamily k Q) {x y z : Q} (p : SurvivingPath R x y) (q : SurvivingPath R y z) : CategoryTheory.CategoryStruct.comp (pathMap R ↑q) (pathMap R ↑p) = 0 ∨ ∃ (r : SurvivingPath R x z), CategoryTheory.CategoryStruct.comp (pathMap R ↑q) (pathMap R ↑p) = pathMap R ↑r

Products of surviving-path basis vectors are either zero or another surviving-path basis vector.

structure MagnitudeConjecture.BoundQuiver.StringPresentation (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.SpecialBiserialPresentation k A Q : Type u

A string presentation is a special-biserial presentation whose relation ideal is monomial.

• 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
• monomial : IsMonomial self.relations

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

Transport a string presentation across an algebra equivalence.

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

A universe-local finite quiver carrying a string presentation of the given algebra.

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

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

The algebra admits a literal string bound-quiver presentation.

def MagnitudeConjecture.BoundQuiver.StringModel.toSpecialBiserialModel {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] (M : StringModel k A) : SpecialBiserialModel k A

Forget the monomial condition from a bundled string model.

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

Transport a bundled string model across an algebra equivalence.

theorem MagnitudeConjecture.BoundQuiver.admitsSpecialBiserialPresentation_of_admitsStringPresentation {k : Type u} [Field k] {A : Type u} [Ring A] [Algebra k A] (h : AdmitsStringPresentation k A) : AdmitsSpecialBiserialPresentation k A

Every string presentation is, after forgetting monomiality, a special-biserial presentation.

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

Admitting a string presentation is invariant under algebra equivalence.