Both sides of a finite category algebra from thin indecomposables

@[instance_reducible]

def MagnitudeConjecture.CoveringHom.twoSidedBiserialOpFintype {C : Type} [Fintype C] : Fintype Cᵒᵖ

theorem MagnitudeConjecture.CoveringHom.pointwiseThin_of_opposite_indecomposables_pointwiseThin {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] (hthin : ∀ (M : FiniteDimensionalModuleCategory k), CategoryTheory.Indecomposable M → IsPointwiseThin M.obj.obj) (M : FiniteDimensionalModuleCategory k) (hM : CategoryTheory.Indecomposable M) : IsPointwiseThin M.obj.obj

Coefficient duality gives thinness in the other variance.

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

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

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

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

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

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

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.canonicalLeftIdeal_isBiserialObject_of_opposite_pointwiseThin {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hOp : ∀ (X : Cᵒᵖ), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (hthin : ∀ (M : FiniteDimensionalModuleCategory k), CategoryTheory.Indecomposable M → IsPointwiseThin M.obj.obj) (X : Cᵒᵖ) : IsBiserialObject (RightModule.leftIdealFGObj (canonicalProjector hOp X))

Thinness in the opposite functor category makes canonical left ideals biserial by coefficient duality and the opposite-algebra identification.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.primitiveProjectivePresentation_isBiserial_of_opposite_pointwiseThin {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hOp : ∀ (X : Cᵒᵖ), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (hlocalOp : ∀ (X : Cᵒᵖ), IsLocalRing (CategoryTheory.End X)) (hskel : CategoryTheory.Skeletal Cᵒᵖ) (hthin : ∀ (M : FiniteDimensionalModuleCategory k), CategoryTheory.Indecomposable M → IsPointwiseThin M.obj.obj) (S : RightModule.FiniteIndecomposableSkeleton k (algebra hOp)) : (primitiveProjectivePresentation hOp hlocalOp S hskel).IsBiserial

The complete primitive-projective presentation is biserial on both sides when all indecomposable opposite-category modules are thin.

theorem MagnitudeConjecture.CoveringHom.finiteCategoryProjectiveGenerator.admitsSpecialBiserialPresentation_of_opposite_pointwiseThin {k : Type u} [Field k] {C : Type} [CategoryTheory.Category.{u, 0} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [Fintype C] (hC : ∀ (X : C), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) (hOp : ∀ (X : Cᵒᵖ), IsFiniteDimensionalModule k (linearCoyonedaLinearModule X)) [IsAlgClosed k] (hlocal : ∀ (X : C), IsLocalRing (CategoryTheory.End X)) (hlocalOp : ∀ (X : Cᵒᵖ), IsLocalRing (CategoryTheory.End X)) (hskel : CategoryTheory.Skeletal Cᵒᵖ) (hthin : ∀ (M : FiniteDimensionalModuleCategory k), CategoryTheory.Indecomposable M → IsPointwiseThin M.obj.obj) (S : RightModule.FiniteIndecomposableSkeleton k (algebra hOp)) : BoundQuiver.AdmitsSpecialBiserialPresentation k (algebra hOp)

The resulting category algebra has a literal special-biserial presentation.