theorem
MagnitudeConjecture.BoundQuiver.SpecialBiserialPresentation.relationSourceRepresentedModule_not_uniserial
{k A Q : Type u}
[Field k]
[Ring A]
[Algebra k A]
[Fintype Q]
[Quiver Q]
[(x y : Q) → Fintype (x ⟶ y)]
(P : SpecialBiserialPresentation k A Q)
{x z : Q}
(r : LinearPathCategory.obj k Q z ⟶ LinearPathCategory.obj k Q x)
(hr : r ∈ P.relations (LinearPathCategory.obj k Q z) (LinearPathCategory.obj k Q x))
(p : P.RelationSurvivingSupport r)
:
theorem
MagnitudeConjecture.submodule_inf_ne_bot_of_injective_indecomposable
{k B : Type u}
[Field k]
[Ring B]
[Algebra k B]
[FiniteDimensional k B]
[IsNoetherianRing Bᵐᵒᵖ]
(I : FGModuleCat Bᵐᵒᵖ)
[CategoryTheory.Injective I]
(hI : CategoryTheory.Indecomposable I)
(U V : Submodule Bᵐᵒᵖ ↑I)
(hU : U ≠ ⊥)
(hV : V ≠ ⊥)
:
U ⊓ V ≠ ⊥
theorem
MagnitudeConjecture.isUniserialModule_of_fgModuleCat_isUniserialObject
{R : Type u}
[Ring R]
[IsNoetherianRing R]
(N : FGModuleCat R)
(hN : IsUniserialObject N)
:
IsUniserialModule R ↑N
Module-theoretic uniseriality is reflected by the finitely generated module category.
theorem
MagnitudeConjecture.RightModule.idealQuotientFGObj_isUniserial_iff_ambient
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(I : TwoSidedIdeal A)
(M : IdealQuotientSubcategory I)
:
IsUniserialModule (idealQuotientAlgebra I)ᵐᵒᵖ ↑((idealQuotientEquivalence I).functor.obj M) ↔ IsUniserialModule Aᵐᵒᵖ ↑M.obj
For a module annihilated by an ideal, uniseriality over the quotient is exactly uniseriality over the ambient algebra.
theorem
MagnitudeConjecture.BoundQuiver.StringPresentation.representedVertexModule_isUniserial_of_injective
{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)
(hInjective : CategoryTheory.Injective (P.representedVertexModule y))
:
theorem
MagnitudeConjecture.BoundQuiver.StringPresentation.projectiveInjectiveIndecomposable_isUniserial
{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)
(M : FGModuleCat P.quotientCategoryAlgebraᵐᵒᵖ)
[CategoryTheory.Projective M]
[CategoryTheory.Injective M]
(hM : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule P.quotientCategoryAlgebraᵐᵒᵖ ↑M)
:
Every indecomposable projective-injective module over the category algebra of a string presentation is uniserial.