A label-aligned indecomposable skeleton of the primitive quotient

The indecomposable right modules over A / AeA are indexed literally by the ambient skeleton labels annihilated by AeA. This file realizes those labels inside the quotient module category and supplies the complete donor skeleton needed to form intrinsic irreducible-Hom spaces. No quotient-only relabeling is introduced.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientFGObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) (x : S.PrimitiveQuotientLabel D) : FinitelyGeneratedCategory (primitiveQuotientAlgebra e)

A surviving ambient label, realized as a finitely generated module over the literal primitive quotient.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientSubcategory_indecomposable_iff_ambient {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] {e : A} [CategoryTheory.Limits.HasBinaryBiproducts (PrimitiveQuotientSubcategory e)] (M : PrimitiveQuotientSubcategory e) : CategoryTheory.Indecomposable M ↔ CategoryTheory.Indecomposable M.obj

Indecomposability in the annihilated full subcategory is exactly indecomposability in the ambient finitely generated module category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientFGObj_indecomposable {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) [IsNoetherianRing (primitiveQuotientAlgebra e)ᵐᵒᵖ] (x : S.PrimitiveQuotientLabel D) : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule (primitiveQuotientAlgebra e)ᵐᵒᵖ ↑(S.primitiveQuotientFGObj D x)

Every literal quotient representative is indecomposable in the module-theoretic sense used by the almost-split API.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientFGObj_skeletal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) {x y : S.PrimitiveQuotientLabel D} (h : Nonempty (S.primitiveQuotientFGObj D x ≅ S.primitiveQuotientFGObj D y)) : x = y

The literal quotient representatives contain no isomorphic duplicates.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientFGObj_complete {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) [IsNoetherianRing (primitiveQuotientAlgebra e)ᵐᵒᵖ] (X : FinitelyGeneratedCategory (primitiveQuotientAlgebra e)) (hX : CategoryTheory.Indecomposable X) : ∃ (x : S.PrimitiveQuotientLabel D), Nonempty (X ≅ S.primitiveQuotientFGObj D x)

Every indecomposable quotient module is represented by a unique surviving ambient label.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientFGObj_decomposition {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) [IsNoetherianRing (primitiveQuotientAlgebra e)ᵐᵒᵖ] (X : FinitelyGeneratedCategory (primitiveQuotientAlgebra e)) : ∃ (n : ℕ) (label : Fin n → S.PrimitiveQuotientLabel D), Nonempty (X ≅ ⨁ fun (i : Fin n) => S.primitiveQuotientFGObj D (label i))

Every quotient module decomposes over the literal surviving label family.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.primitiveQuotientAlmostSplitSkeleton {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {e : A} (D : PrimitiveIdempotentData e) [IsNoetherianRing (primitiveQuotientAlgebra e)ᵐᵒᵖ] : QuotientSubmoduleEquidistribution.IndecomposableSkeleton (primitiveQuotientAlgebra e)ᵐᵒᵖ (S.PrimitiveQuotientLabel D)

The indecomposable skeleton of the primitive quotient whose labels are literally the surviving labels of the ambient skeleton.