Counting simple modules by indecomposable projectives

Taking the simple top gives a bijection between the projective labels and the simple labels of a complete finite indecomposable right-module family. Consequently, the projective count used by the magnitude calculation equals the literal number of simple-module isomorphism classes.

The bijection works over any field. Algebraic closedness is unnecessary.

@[reducible, inline]

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

Labels whose representatives are simple right modules. Completeness and absence of repeated isomorphism classes make their cardinality the simple count.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.simpleCount {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : ℕ

The literal number of simple-module classes in the family.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_simpleLabel_top_iso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.ProjectiveLabel) : ∃ (i : S.SimpleLabel), Nonempty (S.projectiveSimpleTop p ≅ S.fgObj ↑i)

The simple top of each projective occurs in the complete family.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.simpleTopLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.ProjectiveLabel) : S.SimpleLabel

The label of the simple top of a projective representative.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.simpleTopLabelIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.ProjectiveLabel) : S.projectiveSimpleTop p ≅ S.fgObj ↑(S.simpleTopLabel p)

The chosen identification of a projective's top with its simple representative.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.simpleTopLabel_injective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Function.Injective S.simpleTopLabel

Distinct indecomposable projectives have nonisomorphic simple tops.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.simpleTopDesc {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (p : S.ProjectiveLabel) (i : S.SimpleLabel) (f : S.fgObj p.label ⟶ S.fgObj ↑i) : S.projectiveSimpleTop p ⟶ S.fgObj ↑i

A map from a projective to a simple module descends to its simple top.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveSimpleTopProjection_desc {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (p : S.ProjectiveLabel) (i : S.SimpleLabel) (f : S.fgObj p.label ⟶ S.fgObj ↑i) : CategoryTheory.CategoryStruct.comp (S.projectiveSimpleTopProjection p) (S.simpleTopDesc p i f) = f

Descent recovers the original map after the top projection.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.simpleTopLabel_surjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Function.Surjective S.simpleTopLabel

Every simple representative is the top of an indecomposable projective.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.projectiveLabelEquivSimpleLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.ProjectiveLabel ≃ S.SimpleLabel

Taking the top identifies projective classes with simple classes.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.simpleCount_eq_card_projectiveLabel {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.simpleCount = Fintype.card S.ProjectiveLabel

The simple count equals the number of indecomposable projectives.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.simpleCount_eq_projectiveCount {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : ↑S.simpleCount = ARCount.projectiveCount fun (i : Fin S.n) => CategoryTheory.Projective (S.fgObj i)

The literal simple count is the integer projective count used in the magnitude formula.