Indecomposable skeletons of arbitrary ideal quotients

For a two-sided ideal I, the indecomposable right modules over the literal quotient A/I are indexed by the ambient finite-skeleton labels annihilated by I. This is the ideal-independent skeleton layer used by socle rejection.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.IdealQuotientLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (I : TwoSidedIdeal A) : Type

Ambient indecomposable labels annihilated by I.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.idealQuotientLabelFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (I : TwoSidedIdeal A) : Fintype (S.IdealQuotientLabel I)

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.idealQuotientLabelObj {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (I : TwoSidedIdeal A) (x : S.IdealQuotientLabel I) : IdealQuotientSubcategory I

A surviving ambient label as an object of the annihilated full subcategory.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.idealQuotientFGObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (I : TwoSidedIdeal A) (x : S.IdealQuotientLabel I) : FinitelyGeneratedCategory (idealQuotientAlgebra I)

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

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.idealQuotientSubcategory_indecomposable_iff_ambient {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) [CategoryTheory.Limits.HasBinaryBiproducts (IdealQuotientSubcategory I)] (M : IdealQuotientSubcategory I) : CategoryTheory.Indecomposable M ↔ CategoryTheory.Indecomposable M.obj

Indecomposability in the annihilated full subcategory is exactly ambient indecomposability.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.idealQuotientSubcategory_simple_iff_ambient {A : Type u} [Ring A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) (M : IdealQuotientSubcategory I) : CategoryTheory.Simple M ↔ CategoryTheory.Simple M.obj

For an annihilated module, simplicity in the full quotient subcategory is exactly simplicity in the ambient module category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.idealQuotientFGObj_simple_iff_ambient {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (I : TwoSidedIdeal A) (M : IdealQuotientSubcategory I) : CategoryTheory.Simple ((idealQuotientEquivalence I).functor.obj M) ↔ CategoryTheory.Simple M.obj

Simplicity of a literal quotient module is exactly ambient simplicity of its inflated annihilated module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.idealQuotientFGObj_indecomposable {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (I : TwoSidedIdeal A) [IsNoetherianRing (idealQuotientAlgebra I)ᵐᵒᵖ] (x : S.IdealQuotientLabel I) : QuotientSubmoduleEquidistribution.Foundation.IsIndecomposableModule (idealQuotientAlgebra I)ᵐᵒᵖ ↑(S.idealQuotientFGObj I x)

Every displayed quotient representative is indecomposable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.idealQuotientFGObj_skeletal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (I : TwoSidedIdeal A) {x y : S.IdealQuotientLabel I} (h : Nonempty (S.idealQuotientFGObj I x ≅ S.idealQuotientFGObj I y)) : x = y

The displayed quotient representatives have no isomorphic duplicates.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.idealQuotientFGObj_complete {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (I : TwoSidedIdeal A) [IsNoetherianRing (idealQuotientAlgebra I)ᵐᵒᵖ] (X : FinitelyGeneratedCategory (idealQuotientAlgebra I)) (hX : CategoryTheory.Indecomposable X) : ∃ (x : S.IdealQuotientLabel I), Nonempty (X ≅ S.idealQuotientFGObj I x)

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

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.idealQuotientFGObj_decomposition {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (I : TwoSidedIdeal A) [IsNoetherianRing (idealQuotientAlgebra I)ᵐᵒᵖ] (X : FinitelyGeneratedCategory (idealQuotientAlgebra I)) : ∃ (n : ℕ) (label : Fin n → S.IdealQuotientLabel I), Nonempty (X ≅ ⨁ fun (i : Fin n) => S.idealQuotientFGObj I (label i))

Every quotient module decomposes over the displayed surviving label family.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.idealQuotientAlmostSplitSkeleton {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (I : TwoSidedIdeal A) [IsNoetherianRing (idealQuotientAlgebra I)ᵐᵒᵖ] : QuotientSubmoduleEquidistribution.IndecomposableSkeleton (idealQuotientAlgebra I)ᵐᵒᵖ (S.IdealQuotientLabel I)

The indecomposable skeleton of the literal quotient A/I, with labels identified with the annihilated ambient labels.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.idealQuotientFiniteLabelEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (I : TwoSidedIdeal A) : Fin (Nat.card (S.IdealQuotientLabel I)) ≃ S.IdealQuotientLabel I

The single reindexing from the intrinsic surviving-label type to the finite-ordinal shape used by FiniteIndecomposableSkeleton.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.idealQuotientFiniteIndecomposableSkeleton {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (I : TwoSidedIdeal A) [IsNoetherianRing (idealQuotientAlgebra I)ᵐᵒᵖ] : FiniteIndecomposableSkeleton k (idealQuotientAlgebra I)

The complete duplicate-free finite skeleton of the literal ideal quotient, retaining the intrinsic surviving labels through idealQuotientFiniteLabelEquiv.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.idealQuotientFiniteFGObjIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (I : TwoSidedIdeal A) [IsNoetherianRing (idealQuotientAlgebra I)ᵐᵒᵖ] (j : Fin (S.idealQuotientFiniteIndecomposableSkeleton I).n) : (S.idealQuotientFiniteIndecomposableSkeleton I).fgObj j ≅ S.idealQuotientFGObj I ((S.idealQuotientFiniteLabelEquiv I) j)

The finite-ordinal quotient representative is canonically the intrinsic surviving-label representative from which it was constructed.