Simple tops and positive coordinate vectors

For each selected indecomposable projective, its radical quotient has the corresponding standard basis vector as its projective-Hom dimension vector. Finite biproducts of these quotients will therefore realize arbitrary nonnegative integral coordinate vectors in the weak-positivity argument.

theorem MagnitudeConjecture.RightModule.fgModule_simple_of_isSimpleModule {R : Type u} [Ring R] [IsNoetherianRing R] (X : FGModuleCat R) [IsSimpleModule R ↑X] : CategoryTheory.Simple X

A simple module carried by FGModuleCat is a simple object of the finitely generated module category.

theorem MagnitudeConjecture.RightModule.fgModule_isSimpleModule_of_simple {R : Type u} [Ring R] [IsNoetherianRing R] (X : FGModuleCat R) [CategoryTheory.Simple X] : IsSimpleModule R ↑X

Conversely, a simple object of the finitely generated module category is a simple module. Noetherianity is used only to bundle an arbitrary submodule as a finitely generated test object.

theorem MagnitudeConjecture.RightModule.fgModule_simple_iff_isSimpleModule {R : Type u} [Ring R] [IsNoetherianRing R] (X : FGModuleCat R) : CategoryTheory.Simple X ↔ IsSimpleModule R ↑X

Simplicity in FGModuleCat is exactly module-theoretic simplicity.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.radicalQuotientFGObj {B : Type u} [Ring B] (P : FGModuleCat Bᵐᵒᵖ) : FGModuleCat Bᵐᵒᵖ

The quotient of a finite module by its module Jacobson radical.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.radicalQuotientFGObjProjection {B : Type u} [Ring B] (P : FGModuleCat Bᵐᵒᵖ) : P ⟶ radicalQuotientFGObj P

The quotient map to the module-Jacobson-radical quotient.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveSimpleTop {k B : Type u} [Field k] [Ring B] [Algebra k B] (S : FiniteIndecomposableSkeleton k B) (p : S.ProjectiveLabel) : FGModuleCat Bᵐᵒᵖ

The radical quotient of a selected indecomposable projective.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveSimpleTopProjection {k B : Type u} [Field k] [Ring B] [Algebra k B] (S : FiniteIndecomposableSkeleton k B) (p : S.ProjectiveLabel) : S.fgObj p.label ⟶ S.projectiveSimpleTop p

The canonical projection from a selected projective to its radical quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveSimpleTopProjection_epi {k B : Type u} [Field k] [Ring B] [Algebra k B] (S : FiniteIndecomposableSkeleton k B) (p : S.ProjectiveLabel) : CategoryTheory.Epi (S.projectiveSimpleTopProjection p)

The canonical projection to the radical quotient is epic.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveSimpleTopProjection_ne_zero {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k B) (p : S.ProjectiveLabel) : S.projectiveSimpleTopProjection p ≠ 0

The canonical projection to the radical quotient is nonzero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveSimpleTop_isSimpleModule {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k B) (p : S.ProjectiveLabel) : IsSimpleModule Bᵐᵒᵖ ↑(S.projectiveSimpleTop p)

The radical quotient of a selected indecomposable projective is a simple module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.hom_projectiveSimpleTop_eq_zero {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k B) (p q : S.ProjectiveLabel) (hpq : q ≠ p) (f : S.fgObj q.label ⟶ S.projectiveSimpleTop p) : f = 0

A distinct selected indecomposable projective has no map to the simple top belonging to p.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finrank_hom_projectiveSimpleTop_self_eq_one {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k B) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (p : S.ProjectiveLabel) : Module.finrank k (S.fgObj p.label ⟶ S.projectiveSimpleTop p) = 1

The projective indexed by p maps one-dimensionally to its simple top.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveHomVectorFGObj_projectiveSimpleTop {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k B) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (p : S.ProjectiveLabel) : S.projectiveHomVectorFGObj (S.projectiveSimpleTop p) = Pi.single p 1

The radical quotient of p has the standard basis vector at p as its projective-Hom dimension vector.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveHomVectorFGObj_biprod {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k B) (X Y : FGModuleCat Bᵐᵒᵖ) : S.projectiveHomVectorFGObj (X ⊞ Y) = S.projectiveHomVectorFGObj X + S.projectiveHomVectorFGObj Y

Projective-Hom vectors are additive on binary biproducts.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveHomVectorFGObj_middle_eq_add {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k B) {Q : CategoryTheory.ShortComplex (FGModuleCat Bᵐᵒᵖ)} (hQ : Q.ShortExact) : S.projectiveHomVectorFGObj Q.X₂ = S.projectiveHomVectorFGObj Q.X₁ + S.projectiveHomVectorFGObj Q.X₃

Projective-Hom vectors are additive across a short exact sequence.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveVectorRealization {k B : Type u} [Field k] [Ring B] [Algebra k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k B) (v : S.ProjectiveLabel → ℕ) : FGModuleCat Bᵐᵒᵖ

A finite biproduct of simple tops realizing the prescribed natural projective-coordinate multiplicities.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveHomVectorFGObj_projectiveVectorRealization {k B : Type u} [Field k] [Ring B] [Algebra k B] [FiniteDimensional k B] [IsNoetherianRing Bᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k B) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (v : S.ProjectiveLabel → ℕ) : S.projectiveHomVectorFGObj (S.projectiveVectorRealization v) = fun (p : S.ProjectiveLabel) => ↑(v p)

Every nonnegative integral vector is the projective-Hom dimension vector of the corresponding finite biproduct of simple tops.