Middle-support quotient algebras

For a basic algebra, choose its complete primitive idempotents in the same indexing as the indecomposable projective labels of the right-module skeleton. The support algebra of a module is the quotient which kills the sum of the complementary primitive idempotents. Its module category is the full exact subcategory of modules supported on the chosen vertices, exactly as in Appendix A of the frozen manuscript.

The quotient is constructed on the left-module side over Aᵐᵒᵖ and then opposed back to a right-module algebra. This makes the side convention literal and avoids identifying the support quotient with the generally different corner algebra.

structure MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Type u

A complete primitive-idempotent presentation indexed by the literal indecomposable projective labels of S. The last field fixes the indexing: the right ideal generated by the idempotent at p is represented by p.

• idempotent : S.ProjectiveLabel → A
• complete : CompleteOrthogonalIdempotents self.idempotent
• primitive (p : S.ProjectiveLabel) : PrimitiveIdempotentData (self.idempotent p)
• sourceLabel (p : S.ProjectiveLabel) : S.primitiveSourceProjectiveLabel ⋯ = p

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.primitiveProjectiveIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) : rightIdealFGObj (P.idempotent p) ≅ S.fgObj p.label

The presentation identifies each chosen primitive right ideal with its literal ambient projective label.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.complementaryIdempotent {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) : A

The sum of the primitive idempotents outside the projective support of X.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.complementaryIdempotent_isIdempotentElem {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) : IsIdempotentElem (P.complementaryIdempotent X)

The complementary sum is an idempotent.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.not_mem_projectiveSupport_iff_idempotent_smul_eq_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (p : S.ProjectiveLabel) (M : FinitelyGeneratedCategory A) : p ∉ S.projectiveSupport M ↔ ∀ (m : ↑M), MulOpposite.op (P.idempotent p) • m = 0

A primitive idempotent acts by zero on a module exactly when its projective label is absent from the module's support.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.complementaryIdempotent_smul_eq_zero_of_support_subset {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) (m : ↑M) : MulOpposite.op (P.complementaryIdempotent X) • m = 0

If the projective support of M lies in that of X, then the complementary idempotent of X annihilates M.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportIdeal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) : TwoSidedIdeal Aᵐᵒᵖ

On the left-module side, the support ideal is generated by the opposite of the complementary idempotent.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.op_idempotent_mem_supportIdeal_of_not_mem {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) (p : S.ProjectiveLabel) (hp : p ∉ S.projectiveSupport X) : MulOpposite.op (P.idempotent p) ∈ P.supportIdeal X

Every omitted primitive idempotent belongs to the ideal generated by the complementary idempotent.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.isTorsionBySupportIdeal_of_support_subset {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) : Module.IsTorsionBySet Aᵐᵒᵖ ↑M ↑(TwoSidedIdeal.asIdeal (P.supportIdeal X))

Every module whose support lies in that of X is annihilated by the support ideal.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.LeftSupportQuotient {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) : Type u

The literal quotient ring whose left modules are the right A-modules supported on X.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.SupportAlgebra {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) : Type u

The same support quotient, oriented as a right-module algebra.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.leftSupportQuotientModuleFinite {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) : Module.Finite k (P.LeftSupportQuotient X)

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.leftSupportQuotientNoetherian {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) : IsNoetherianRing (P.LeftSupportQuotient X)

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportAlgebraModuleFinite {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) : Module.Finite k (P.SupportAlgebra X)

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportAlgebraNoetherian {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) : IsNoetherianRing (P.SupportAlgebra X)ᵐᵒᵖ

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportAlgebra_isRepresentationFinite {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (X : FinitelyGeneratedCategory A) : IsRepresentationFinite k (P.SupportAlgebra X)

Representation-finiteness descends from the ambient algebra to the literal support quotient.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportAlgebraSkeleton {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (X : FinitelyGeneratedCategory A) : FiniteIndecomposableSkeleton k (P.SupportAlgebra X)

The duplicate-free finite indecomposable right-module skeleton of the support quotient.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.leftSupportObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) : ModuleCat (P.LeftSupportQuotient X)

A supported ambient right module, regarded literally as a left module over the quotient of Aᵐᵒᵖ.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.SupportedOn {k A : Type u} [Field k] [Ring A] [Algebra k A] {S : FiniteIndecomposableSkeleton k A} (X : FinitelyGeneratedCategory A) : CategoryTheory.ObjectProperty (FinitelyGeneratedCategory A)

The full subcategory of ambient finitely generated right modules whose projective support lies in that of X.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.SupportSubcategory {k A : Type u} [Field k] [Ring A] [Algebra k A] {S : FiniteIndecomposableSkeleton k A} (X : FinitelyGeneratedCategory A) : Type (u + 1)

The manuscript's full subcategory of modules supported on X.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.leftSupportObjLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) : ↑M ≃ₗ[k] ↑(P.leftSupportObj X M hsub)

The quotient-module construction does not change the underlying finite-dimensional k-vector space.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.leftSupportObjRestrictIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) : (ModuleCat.restrictScalars (Ideal.Quotient.mk (TwoSidedIdeal.asIdeal (P.supportIdeal X)))).obj (P.leftSupportObj X M hsub) ≅ M.obj

Restricting the quotient action recovers the original ambient right module, by the identity map on its underlying carrier.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.leftSupportMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X M N : FinitelyGeneratedCategory A) (hM : S.projectiveSupport M ⊆ S.projectiveSupport X) (hN : S.projectiveSupport N ⊆ S.projectiveSupport X) (f : M ⟶ N) : P.leftSupportObj X M hM ⟶ P.leftSupportObj X N hN

Every ambient morphism between modules supported on X is linear over the support quotient. This is the fullness part of the manuscript's "full exact subcategory" assertion.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.leftSupportMap_apply {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X M N : FinitelyGeneratedCategory A) (hM : S.projectiveSupport M ⊆ S.projectiveSupport X) (hN : S.projectiveSupport N ⊆ S.projectiveSupport X) (f : M ⟶ N) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (P.leftSupportMap X M N hM hN f)) m = (CategoryTheory.ConcreteCategory.hom f) m

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.leftSupportFGObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) : FGModuleCat (P.LeftSupportQuotient X)

The quotient object bundled in the finitely generated module category. Finite generation follows from finite-dimensionality over k.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.leftSupportFunctor {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) : CategoryTheory.Functor (SupportSubcategory X) (FGModuleCat (P.LeftSupportQuotient X))

Passage from the supported full subcategory to finitely generated modules over the literal support quotient.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.leftSupportInflateFGObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) (N : FGModuleCat (P.LeftSupportQuotient X)) : FinitelyGeneratedCategory A

Inflate a finitely generated quotient module to an ambient finitely generated right A-module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.projectiveSupport_leftSupportInflateFGObj_subset {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) (N : FGModuleCat (P.LeftSupportQuotient X)) : S.projectiveSupport (P.leftSupportInflateFGObj X N) ⊆ S.projectiveSupport X

Inflation from the support quotient lands in the supported full subcategory.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.leftSupportInflateFunctor {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) : CategoryTheory.Functor (FGModuleCat (P.LeftSupportQuotient X)) (SupportSubcategory X)

Inflation along the quotient map, with its image bundled in the supported full subcategory.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.leftSupportUnitIsoApp {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) (M : SupportSubcategory X) : M ≅ ((P.leftSupportFunctor X).comp (P.leftSupportInflateFunctor X)).obj M

Restricting a supported quotient object returns its original ambient module. This is the unit component of the support equivalence.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.leftSupportCounitIsoApp {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) (N : FGModuleCat (P.LeftSupportQuotient X)) : ((P.leftSupportInflateFunctor X).comp (P.leftSupportFunctor X)).obj N ≅ N

Applying the quotient action to an inflated quotient module returns the original quotient module.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.leftSupportEquivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) : SupportSubcategory X ≌ FGModuleCat (P.LeftSupportQuotient X)

Finitely generated modules over the literal support quotient are equivalent to the full subcategory of ambient modules supported on X.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceMiddleSupportObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : SupportSubcategory (S.minimalRightAlmostSplitAt ↑z).middle

The middle term of a chosen nonprojective right almost-split sequence, as an object of its own supported full subcategory.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceTargetSupportObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : SupportSubcategory (S.minimalRightAlmostSplitAt ↑z).middle

The endpoint of the sequence lies in the middle-support subcategory.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : rightSequenceMiddleSupportObj z ⟶ rightSequenceTargetSupportObj z

The chosen right almost-split map, restricted to the full subcategory supported on its middle term.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportMap_isRightAlmostSplit {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (rightSequenceSupportMap z)

Restriction to the middle-support full subcategory preserves the right almost-split property.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportMap_isRightMinimal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : QuotientSubmoduleEquidistribution.IsRightMinimal (rightSequenceSupportMap z)

The restricted right almost-split map remains right minimal.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceLeftSupportMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : (P.leftSupportEquivalence (S.minimalRightAlmostSplitAt ↑z).middle).functor.obj (rightSequenceMiddleSupportObj z) ⟶ (P.leftSupportEquivalence (S.minimalRightAlmostSplitAt ↑z).middle).functor.obj (rightSequenceTargetSupportObj z)

The supported right almost-split map, transported to finitely generated modules over the literal quotient of Aᵐᵒᵖ.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceLeftSupportMap_isRightAlmostSplit {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (P.rightSequenceLeftSupportMap z)

The transported quotient map is right almost split.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceLeftSupportMap_isRightMinimal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : QuotientSubmoduleEquidistribution.IsRightMinimal (P.rightSequenceLeftSupportMap z)

The transported quotient map is right minimal.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.leftToRightSupportEquivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) : ModuleCat (P.LeftSupportQuotient X) ≌ Category (P.SupportAlgebra X)

Reorientation from left modules over the quotient of Aᵐᵒᵖ to right modules over the support algebra.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.leftToRightSupportFGEquivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) : FGModuleCat (P.LeftSupportQuotient X) ≌ FinitelyGeneratedCategory (P.SupportAlgebra X)

The same reorientation on literal finitely generated module categories.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.leftToRightSupportFGEquivalenceFunctorAdditive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) : (P.leftToRightSupportFGEquivalence X).functor.Additive

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.leftToRightSupportFGEquivalenceInverseAdditive {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) : (P.leftToRightSupportFGEquivalence X).inverse.Additive

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportEquivalence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) : SupportSubcategory X ≌ FinitelyGeneratedCategory (P.SupportAlgebra X)

The paper's supported full subcategory, identified directly with finitely generated right modules over the support algebra.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportFGObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) : FinitelyGeneratedCategory (P.SupportAlgebra X)

A supported ambient module, bundled as a finitely generated right module over the support algebra.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportSubcategory_epi_ambient {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X : FinitelyGeneratedCategory A) {M N : SupportSubcategory X} (f : M ⟶ N) [CategoryTheory.Epi f] : CategoryTheory.Epi f.hom

An epimorphism in the supported full subcategory is an epimorphism in the ambient finitely generated module category. This follows by transporting it to the literal quotient category, where epimorphisms are the surjective module maps; the support functor does not change the underlying function.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportFGObj_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) (hM : CategoryTheory.Projective M) : CategoryTheory.Projective (P.supportFGObj X M hsub)

A projective ambient module supported on X remains projective over the literal support quotient.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportAlgebraMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : (P.supportEquivalence (S.minimalRightAlmostSplitAt ↑z).middle).functor.obj (rightSequenceMiddleSupportObj z) ⟶ (P.supportEquivalence (S.minimalRightAlmostSplitAt ↑z).middle).functor.obj (rightSequenceTargetSupportObj z)

The chosen right almost-split map transported all the way to finitely generated right modules over the support algebra.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportAlgebraMap_isRightAlmostSplit {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (P.rightSequenceSupportAlgebraMap z)

The support-algebra map is right almost split.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportAlgebraMap_isRightMinimal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : QuotientSubmoduleEquidistribution.IsRightMinimal (P.rightSequenceSupportAlgebraMap z)

The support-algebra map is right minimal.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) : Category (P.SupportAlgebra X)

A supported ambient right module, now oriented as a right module over the support algebra.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.leftSupportObjToSupportObjLinearEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) : ↑(P.leftSupportObj X M hsub) ≃ₗ[k] ↑(P.supportObj X M hsub)

Reorientation likewise preserves the underlying k-vector space.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportObj_moduleFinite {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) : Module.Finite k ↑(P.supportObj X M hsub)

A supported ambient finite module remains finite-dimensional over k after passage to the support algebra.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.leftSupportObj_indecomposable {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) (hM : CategoryTheory.Indecomposable M.obj) : CategoryTheory.Indecomposable (P.leftSupportObj X M hsub)

If the ambient supported module is indecomposable, so is the quotient module before reorientation.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportObj_indecomposable {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) (hM : CategoryTheory.Indecomposable M.obj) : CategoryTheory.Indecomposable (P.supportObj X M hsub)

Indecomposability is also preserved after orienting the quotient object as a right module over the support algebra.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportObj_isFiniteIndecomposable {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) (hM : CategoryTheory.Indecomposable M.obj) : IsFiniteIndecomposable k (P.SupportAlgebra X) (P.supportObj X M hsub)

The exact finite-indecomposable package needed to select the corresponding vertex of the support-algebra skeleton.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) (hM : CategoryTheory.Indecomposable M.obj) : Fin (P.supportAlgebraSkeleton hA X).n

The chosen label of a supported indecomposable in the duplicate-free skeleton of the support algebra.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportObjIsoSkeletonObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) (hM : CategoryTheory.Indecomposable M.obj) : P.supportObj X M hsub ≅ (P.supportAlgebraSkeleton hA X).obj (P.supportLabel hA X M hsub hM)

The selected support-algebra label represents the supported module.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.supportFGObjIsoSkeletonFG {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (X M : FinitelyGeneratedCategory A) (hsub : S.projectiveSupport M ⊆ S.projectiveSupport X) (hM : CategoryTheory.Indecomposable M.obj) : P.supportFGObj X M hsub ≅ (P.supportAlgebraSkeleton hA X).fgObj (P.supportLabel hA X M hsub hM)

The selected support-algebra label represents the supported module in the literal finitely generated category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceMiddleSummand_support_subset {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (t : (S.minimalRightAlmostSplitAt ↑z).index.obj) : S.projectiveSupport (S.fgObj ((S.minimalRightAlmostSplitAt ↑z).label t)) ⊆ S.projectiveSupport (S.minimalRightAlmostSplitAt ↑z).middle

Every displayed indecomposable summand of the chosen right almost-split middle term is supported on that middle term.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportTargetLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : Fin (P.supportAlgebraSkeleton hA (S.minimalRightAlmostSplitAt ↑z).middle).n

The support-algebra skeleton label representing the endpoint of the chosen sequence.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportSourceLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : Fin (P.supportAlgebraSkeleton hA (S.minimalRightAlmostSplitAt ↑z).middle).n

The support-algebra skeleton label representing the translated source of the chosen sequence.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportMiddleLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (t : (S.minimalRightAlmostSplitAt ↑z).index.obj) : Fin (P.supportAlgebraSkeleton hA (S.minimalRightAlmostSplitAt ↑z).middle).n

The support-algebra skeleton label representing a displayed middle summand.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportTargetIsoSkeletonFG {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : P.supportFGObj (S.minimalRightAlmostSplitAt ↑z).middle (S.fgObj ↑z) ⋯ ≅ (P.supportAlgebraSkeleton hA (S.minimalRightAlmostSplitAt ↑z).middle).fgObj (P.rightSequenceSupportTargetLabel hA z)

The quotient endpoint is the finitely generated skeleton object at its selected label.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportSourceIsoSkeletonFG {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : P.supportFGObj (S.minimalRightAlmostSplitAt ↑z).middle (S.fgObj (S.rightTranslationLabel z)) ⋯ ≅ (P.supportAlgebraSkeleton hA (S.minimalRightAlmostSplitAt ↑z).middle).fgObj (P.rightSequenceSupportSourceLabel hA z)

The quotient translated source is the finitely generated skeleton object at its selected label.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportMiddleIsoSkeletonFG {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (t : (S.minimalRightAlmostSplitAt ↑z).index.obj) : P.supportFGObj (S.minimalRightAlmostSplitAt ↑z).middle (S.fgObj ((S.minimalRightAlmostSplitAt ↑z).label t)) ⋯ ≅ (P.supportAlgebraSkeleton hA (S.minimalRightAlmostSplitAt ↑z).middle).fgObj (P.rightSequenceSupportMiddleLabel hA z t)

Each displayed quotient middle summand is the finitely generated skeleton object at its selected label.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportSkeletonMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : (P.supportEquivalence (S.minimalRightAlmostSplitAt ↑z).middle).functor.obj (rightSequenceMiddleSupportObj z) ⟶ (P.supportAlgebraSkeleton hA (S.minimalRightAlmostSplitAt ↑z).middle).fgObj (P.rightSequenceSupportTargetLabel hA z)

Postcompose the transported map with the selected endpoint isomorphism, so that it ends at the literal object of the support-algebra skeleton.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportSkeletonMap_isRightAlmostSplit {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (P.rightSequenceSupportSkeletonMap hA z)

The skeleton-targeted support-algebra map remains right almost split.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportSkeletonMap_isRightMinimal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : QuotientSubmoduleEquidistribution.IsRightMinimal (P.rightSequenceSupportSkeletonMap hA z)

The skeleton-targeted support-algebra map remains right minimal.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.PrimitiveProjectivePresentation.rightSequenceSupportMinimalRightAlmostSplitDecomposition {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} (P : S.PrimitiveProjectivePresentation) (hA : IsRepresentationFinite k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : (P.supportAlgebraSkeleton hA (S.minimalRightAlmostSplitAt ↑z).middle).almostSplitSkeleton.MinimalRightAlmostSplitDecomposition (P.rightSequenceSupportTargetLabel hA z)

The actual transported sequence, bundled as a minimal right almost-split decomposition at the selected support-algebra endpoint.