Path-generated bound-quiver relations

This file supplies the generic linear-algebra step behind monomializing a bound-quiver presentation. If every displayed relation is itself a path, then the generated two-sided Hom ideal is spanned, in every Hom space, by the individual paths which it kills. Thus the presentation is monomial in the sense used by StringBoundQuiver.

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

A relation family is path-valued when every one of its displayed generators is the linearization of a single path.

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

Enlarge a family of linear relations by declaring every path which occurs with nonzero coefficient in a displayed relation to be a relation on its own. Two-sided closure is still taken by generatedHomSubmodule.

theorem MagnitudeConjecture.BoundQuiver.pathSupportHull_isPathRelationFamily {k Q : Type u} [Field k] [Quiver Q] (R : RelationFamily k Q) : IsPathRelationFamily (pathSupportHull R)

The path-support hull is visibly generated by individual paths.

theorem MagnitudeConjecture.BoundQuiver.relation_mem_pathSupportHullIdeal {k Q : Type u} [Field k] [Quiver Q] (R : RelationFamily k Q) {X Y : LinearPathCategory.Category k Q} {r : X ⟶ Y} (hr : r ∈ R X Y) : r ∈ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k (pathSupportHull R) X Y

Every original relation belongs to the ideal generated by its path-support hull.

theorem MagnitudeConjecture.BoundQuiver.relationIdeal_le_pathSupportHullIdeal {k Q : Type u} [Field k] [Quiver Q] (R : RelationFamily k Q) {X Y : LinearPathCategory.Category k Q} : QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k R X Y ≤ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k (pathSupportHull R) X Y

The ideal of the original relations is contained in the ideal of the path-support hull.

theorem MagnitudeConjecture.BoundQuiver.exists_relation_path_factor_of_pathMap_eq_zero {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsPathRelationFamily R) {x y : Q} (p : Quiver.Path x y) (hp : pathMap R p = 0) : ∃ (U : LinearPathCategory.Category k Q) (V : LinearPathCategory.Category k Q) (q : Quiver.Path (LinearPathCategory.vertex V) (LinearPathCategory.vertex U)), LinearPathCategory.pathHom q ∈ R U V ∧ ∃ (a : Quiver.Path (LinearPathCategory.vertex U) y) (b : Quiver.Path x (LinearPathCategory.vertex V)), p = (b.comp q).comp a

If an ideal generated by literal paths kills a basis path, then one of the displayed relation paths occurs as an ordinary subpath.

theorem MagnitudeConjecture.BoundQuiver.isMonomial_of_isPathRelationFamily {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsPathRelationFamily R) : IsMonomial R

A two-sided Hom ideal generated by individual paths is monomial.

theorem MagnitudeConjecture.BoundQuiver.pathSupportHull_isMonomial {k Q : Type u} [Field k] [Quiver Q] (R : RelationFamily k Q) : IsMonomial (pathSupportHull R)

The path-support hull is a monomial relation family.

theorem MagnitudeConjecture.BoundQuiver.pathSupportHull_isAdmissible {k Q : Type u} [Field k] [Quiver Q] {R : RelationFamily k Q} (hR : IsAdmissible R) : IsAdmissible (pathSupportHull R)

Taking the path-support hull preserves admissibility.

theorem MagnitudeConjecture.BoundQuiver.pathMap_pathSupportHull_eq_zero_of_eq_zero {k Q : Type u} [Field k] [Quiver Q] (R : RelationFamily k Q) {x y : Q} {p : Quiver.Path x y} (hp : pathMap R p = 0) : pathMap (pathSupportHull R) p = 0

Every path killed by the original relations is killed after passing to the path-support hull.

noncomputable def MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.pathSupportHullStringPresentation {k Q : Type u} [Field k] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] {A : Type u} [Ring A] [Algebra k A] (P : SpecialBiserialPresentation k A Q) : have hR := ⋯; StringPresentation k (CoveringHom.finiteCategoryProjectiveGenerator.algebra ⋯) Q

A special-biserial presentation has a canonical string-algebra quotient: replace its relation family by the path-support hull. This is the generic presentation-theoretic half of special-biserial socle reduction; identifying the resulting algebra quotient with a particular socle quotient is a separate theorem.