Biserial canonical projectives of a finite category algebra

The canonical projector attached to an object of a finite linear category is primitive when that object's endomorphism ring is local. The direct coordinate-thin biserial induction therefore applies to its principal right ideal.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.finiteCategoryBiserialAlgebraFiniteDimensional {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : FiniteDimensional k (algebra hP)

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.finiteCategoryBiserialAlgebraOppositeIsNoetherian {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) : IsNoetherianRing (algebra hP)ᵐᵒᵖ

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.canonicalRightIdeal_isBiserial_of_allIndecomposablesCoordinateThin {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (Hthin : RightModule.AllIndecomposablesCoordinateThin (canonicalProjector hP)) (X : C) : IsBiserialModule (algebra hP)ᵐᵒᵖ ↑(RightModule.rightIdealFGObj (canonicalProjector hP X))

If all indecomposable modules over a finite category algebra are thin in the canonical coordinates, then every canonical principal right projective is biserial.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.representedCovariantRepresentable_isBiserial_of_allIndecomposablesCoordinateThin {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (Hthin : RightModule.AllIndecomposablesCoordinateThin (canonicalProjector hP)) (X : C) : IsBiserialModule (algebra hP)ᵐᵒᵖ ↑((representedFGFunctor hP).obj ((finiteDimensionalLinearCoyonedaFunctor hP).obj (Opposite.op X)))

Under the finite-category projective-generator equivalence, every covariant representable is biserial when all indecomposable algebra modules are thin in the canonical coordinates.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.canonicalRightIdeal_isBiserialObject_of_allIndecomposablesCoordinateThin {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (Hthin : RightModule.AllIndecomposablesCoordinateThin (canonicalProjector hP)) (X : C) : IsBiserialObject (RightModule.rightIdealFGObj (canonicalProjector hP X))

A canonical principal right projective is intrinsically biserial in the finitely generated module category.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.representedCovariantRepresentable_isBiserialObject_of_allIndecomposablesCoordinateThin {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (Hthin : RightModule.AllIndecomposablesCoordinateThin (canonicalProjector hP)) (X : C) : IsBiserialObject ((representedFGFunctor hP).obj ((finiteDimensionalLinearCoyonedaFunctor hP).obj (Opposite.op X)))

The represented covariant representable is intrinsically biserial in the finitely generated module category.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.covariantRepresentable_isBiserialObject_of_allIndecomposablesCoordinateThin {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (Hthin : RightModule.AllIndecomposablesCoordinateThin (canonicalProjector hP)) (X : C) : IsBiserialObject ((finiteDimensionalLinearCoyonedaFunctor hP).obj (Opposite.op X))

Every covariant representable of the finite linear category is intrinsically biserial when all indecomposable modules over its category algebra are thin in the canonical coordinates.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.canonicalRightIdeal_isBiserialObject_of_covariantRepresentable {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hP : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (X : C) (hX : IsBiserialObject ((finiteDimensionalLinearCoyonedaFunctor hP).obj (Opposite.op X))) : IsBiserialObject (RightModule.rightIdealFGObj (canonicalProjector hP X))

Intrinsic biseriality of a covariant representable transports to its canonical principal right ideal in the finite category algebra.