Left almost-split monomorphisms for finite-dimensional modules

Finite-dimensional contragredient duality transfers finite projective presentations to finite injective copresentations. Consequently the chosen left almost-split map at a noninjective indecomposable is monic. Its cokernel projection is then the dual Auslander--Reiten map.

theorem MagnitudeConjecture.fgProjective_of_moduleProjective {R : Type u} [Ring R] (X : FGModuleCat R) (h : Module.Projective R ↑X) : CategoryTheory.Projective X

Module projectivity gives categorical projectivity in the finitely generated subcategory.

theorem MagnitudeConjecture.fgModuleCat_projectivePresentation_nonempty {R : Type u} [Ring R] (X : FGModuleCat R) : Nonempty (CategoryTheory.ProjectivePresentation X)

Every finitely generated module has a finite free projective presentation.

theorem MagnitudeConjecture.fgModuleCat_enoughProjectives (R : Type u) [Ring R] : CategoryTheory.EnoughProjectives (FGModuleCat R)

The category of finitely generated modules has enough finitely generated projectives.

theorem MagnitudeConjecture.fgModuleCat_enoughInjectives (k R : Type u) [Field k] [Ring R] [Algebra k R] [FiniteDimensional k R] : CategoryTheory.EnoughInjectives (FGModuleCat R)

Finite-dimensional contragredient duality supplies enough injectives in the category of finitely generated modules.

theorem MagnitudeConjecture.rightAlmostSplit_target_isIndecomposableModule {R : Type u} [Ring R] {E Z : FGModuleCat R} (f : E ⟶ Z) (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule R ↑Z

The target of a right almost-split morphism of finitely generated modules is indecomposable.

theorem MagnitudeConjecture.IsRightAlmostSplit.not_projective_target {C : Type u} [CategoryTheory.Category.{u_1, u} C] {E Z : C} (f : E ⟶ Z) [CategoryTheory.Epi f] (hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit f) : ¬CategoryTheory.Projective Z

An epic right almost-split morphism cannot end at a projective object.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.noninjectiveLeftAlmostSplit_mono {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : { x : Fin S.n // ¬CategoryTheory.Injective (S.fgObj x) }) : CategoryTheory.Mono (S.minimalLeftAlmostSplitAt ↑x).map

At a noninjective selected module, the chosen minimal left almost-split map is monic.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.noninjectiveLeftCokernel_rightAlmostSplit {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : { x : Fin S.n // ¬CategoryTheory.Injective (S.fgObj x) }) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (CategoryTheory.Limits.cokernel.π (S.minimalLeftAlmostSplitAt ↑x).map)

The cokernel projection of the chosen noninjective left almost-split map is right almost split.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.leftAlmostSplit_cokernel_π_isRightMinimal_obj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x : Fin S.n} {E : FinitelyGeneratedCategory A} (f : S.fgObj x ⟶ E) [CategoryTheory.Mono f] (hf : QuotientSubmoduleEquidistribution.IsLeftAlmostSplit f) (hq : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (CategoryTheory.Limits.cokernel.π f)) : QuotientSubmoduleEquidistribution.IsRightMinimal (CategoryTheory.Limits.cokernel.π f)

At a selected indecomposable source, the cokernel projection of a left-almost-split monomorphism is right minimal.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.noninjectiveLeftCokernel_rightMinimal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : { x : Fin S.n // ¬CategoryTheory.Injective (S.fgObj x) }) : QuotientSubmoduleEquidistribution.IsRightMinimal (CategoryTheory.Limits.cokernel.π (S.minimalLeftAlmostSplitAt ↑x).map)

The chosen noninjective left cokernel projection is right minimal.