Classification of string-arrow cokernels

For a displayed arrow a : x ⟶ y, the quotient V(a) has the literal two-step minimal projective presentation

P(x) ⟶ P(y) ⟶ V(a).

Uniqueness of minimal projective covers therefore turns an isomorphism V(a) ≅ V(b) into an invertible square between the two represented arrow maps. Passing back through the fully faithful category-algebra realization and reducing modulo paths of length at least two recovers the displayed arrow. Thus the Butler--Ringel modules V(a) are pairwise nonisomorphic.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowClassificationAlgebraFiniteDimensional {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) : FiniteDimensional k P.quotientCategoryAlgebra

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowClassificationAlgebraOppositeIsNoetherian {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) : IsNoetherianRing P.quotientCategoryAlgebraᵐᵒᵖ

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowHom {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : P.representedVertexModule x ⟶ P.representedVertexModule y

The represented projective morphism induced by a displayed arrow.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowHom_hom {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : ModuleCat.Hom.hom (P.representedArrowHom a).hom = P.representedArrowLinearMap a

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowHom_comp_arrowCokernelProjectionHom {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : CategoryTheory.CategoryStruct.comp (P.representedArrowHom a) (P.arrowCokernelProjectionHom a) = 0

The represented arrow map is killed by the canonical projection onto its cokernel.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelKernelCoverHom {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : P.representedVertexModule x ⟶ CategoryTheory.Limits.kernel (P.arrowCokernelProjectionHom a)

The arrow map, corestricted to the categorical kernel of its cokernel projection.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelKernelCoverHom_comp_kernel_ι {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : CategoryTheory.CategoryStruct.comp (P.arrowCokernelKernelCoverHom a) (CategoryTheory.Limits.kernel.ι (P.arrowCokernelProjectionHom a)) = P.representedArrowHom a

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelKernelCoverHom_comp_kernel_ι_assoc {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) {Z : FGModuleCat (CoveringHom.finiteCategoryProjectiveGenerator.algebra ⋯)ᵐᵒᵖ} (h : P.representedVertexModule y ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.arrowCokernelKernelCoverHom a) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (P.arrowCokernelProjectionHom a)) h) = CategoryTheory.CategoryStruct.comp (P.representedArrowHom a) h

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelKernelCoverHom_surjective {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : Function.Surjective ⇑(ModuleCat.Hom.hom (P.arrowCokernelKernelCoverHom a).hom)

The represented source projective surjects onto the kernel of the canonical projection onto V(a).

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedArrowHom_ne_zero {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : P.representedArrowHom a ≠ 0

The represented morphism of a displayed arrow is nonzero.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelKernelCoverHom_ne_zero {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : P.arrowCokernelKernelCoverHom a ≠ 0

The induced cover of the kernel is nonzero.

instance MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelKernelCoverHom_epi {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : CategoryTheory.Epi (P.arrowCokernelKernelCoverHom a)

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelKernelCoverHom_isRightMinimal {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : QuotientSubmoduleEquidistribution.IsRightMinimal (P.arrowCokernelKernelCoverHom a)

The represented source projective is the projective cover of the first syzygy of V(a).

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelKernelMinimalProjectivePresentation {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : MinimalProjectivePresentation (CategoryTheory.Limits.kernel (P.arrowCokernelProjectionHom a))

The minimal projective cover of the first syzygy of V(a).

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelTwoStepMinimalProjectivePresentation {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : TwoStepMinimalProjectivePresentation (P.arrowCokernelFGObj a)

The literal two-step minimal projective presentation P(x) ⟶ P(y) ⟶ V(a).

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelTwoStepMinimalProjectivePresentation_differential {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a : x ⟶ y) : (P.arrowCokernelTwoStepMinimalProjectivePresentation a).differential = P.representedArrowHom a

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrow_eq_of_representedArrow_iso_square {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) {x y : Q} (a b : x ⟶ y) (ex : P.representedVertexModule x ≅ P.representedVertexModule x) (ey : P.representedVertexModule y ≅ P.representedVertexModule y) (hcomm : CategoryTheory.CategoryStruct.comp ex.hom (P.representedArrowHom b) = CategoryTheory.CategoryStruct.comp (P.representedArrowHom a) ey.hom) : a = b

An invertible commuting square between represented arrow maps determines the displayed arrow.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.BoundQuiver.StringPresentation.displayedArrowCokernelFGObj {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (a : DisplayedArrow Q) : FGModuleCat P.quotientCategoryAlgebraᵐᵒᵖ

Butler--Ringel's module attached to a displayed arrow.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.displayedArrow_eq_of_arrowCokernel_iso {k A Q : Type u} [Field k] [Ring A] [Algebra k A] [Fintype Q] [Quiver Q] [(x y : Q) → Fintype (x ⟶ y)] (P : StringPresentation k A Q) (a b : DisplayedArrow Q) (e : P.displayedArrowCokernelFGObj a ≅ P.displayedArrowCokernelFGObj b) : a = b

Distinct displayed arrows have nonisomorphic Butler--Ringel cokernels.