Cokernels of arrows in a string category algebra

For a displayed arrow a : x ⟶ y, Butler--Ringel's module V(a) is the quotient of the represented projective at y by the submodule generated by a. This file packages that quotient literally and records its first local properties: the arrow-generated submodule lies in the projective radical, so the quotient retains the simple top and is indecomposable.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelAlgebraFiniteDimensional {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.arrowCokernelAlgebraOppositeIsNoetherian {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ᵐᵒᵖ

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelSubmodule {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) : Submodule P.quotientCategoryAlgebraᵐᵒᵖ ↑(P.representedVertexModule y)

The submodule of the represented target projective generated by a displayed arrow.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelFGObj {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) : FGModuleCat P.quotientCategoryAlgebraᵐᵒᵖ

Butler--Ringel's arrow-indexed module V(a), retained in the finitely generated module category.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelProjection {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 y) →ₗ[P.quotientCategoryAlgebraᵐᵒᵖ] ↑(P.arrowCokernelFGObj a)

The canonical projection from the represented target projective to V(a).

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.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) : P.representedVertexModule y ⟶ P.arrowCokernelFGObj a

The canonical projection onto V(a), bundled in the finitely generated module category.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelSubmodule_le_jacobson {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.arrowCokernelSubmodule a ≤ Module.jacobson P.quotientCategoryAlgebraᵐᵒᵖ ↑(P.representedVertexModule y)

An arrow-generated submodule is one summand of the represented projective's radical.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelSubmodule_ne_bot {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.arrowCokernelSubmodule a ≠ ⊥

The branch killed in V(a) is nonzero.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexModule_top_isSimple {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) (y : Q) : IsSimpleModule P.quotientCategoryAlgebraᵐᵒᵖ (↑(P.representedVertexModule y) ⧸ Module.jacobson P.quotientCategoryAlgebraᵐᵒᵖ ↑(P.representedVertexModule y))

The represented target projective has simple top.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelSubmodule_ne_top {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.arrowCokernelSubmodule a ≠ ⊤

The branch killed in V(a) is a proper submodule of its represented projective.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelFGObj_top_isSimple {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) : IsSimpleModule P.quotientCategoryAlgebraᵐᵒᵖ (↑(P.arrowCokernelFGObj a) ⧸ Module.jacobson P.quotientCategoryAlgebraᵐᵒᵖ ↑(P.arrowCokernelFGObj a))

Quotienting a represented projective by one arrow-generated branch preserves its simple top.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelProjection_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 ⇑(P.arrowCokernelProjection a)

The canonical projection onto V(a) is surjective.

instance MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelProjectionHom_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.arrowCokernelProjectionHom a)

The bundled canonical projection onto V(a) is epic.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelProjection_ker {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.arrowCokernelProjection a).ker = P.arrowCokernelSubmodule a

The kernel of the canonical projection onto V(a) is precisely the arrow-generated branch.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelProjectionHom_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.arrowCokernelProjectionHom a ≠ 0

The canonical projection onto V(a) is nonzero.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelProjectionHom_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.arrowCokernelProjectionHom a)

The canonical projective epimorphism onto V(a) is right minimal.

noncomputable def MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelMinimalProjectivePresentation {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 (P.arrowCokernelFGObj a)

The represented target projective and its canonical quotient map form the minimal projective presentation of V(a).

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelFGObj_nontrivial {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) : Nontrivial ↑(P.arrowCokernelFGObj a)

Every arrow-indexed cokernel V(a) is nonzero.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelFGObj_indecomposable {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.Indecomposable (P.arrowCokernelFGObj a)

Every arrow-indexed cokernel V(a) is indecomposable.

theorem MagnitudeConjecture.BoundQuiver.StringPresentation.arrowCokernelFGObj_not_projective {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.Projective (P.arrowCokernelFGObj a)

An arrow-indexed cokernel V(a) is not projective. Otherwise its canonical quotient would split, decomposing the indecomposable represented target projective into the nonzero arrow range and a nonzero complement.