Exhaustive families of graded simple modules

A family is exhaustive up to internal shifts when every simple finite graded module is isomorphic to a shift of a member. This property is used both to classify simple modules and to construct their classes in the graded Grothendieck group.

Exhaustive families of graded simples

def TauCeti.IsExhaustiveGradedSimpleFamily {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} (S : I → (gradedFiniteModules 𝒜).FullSubcategory) : Prop

A family of finite graded modules is an exhaustive family of graded simples up to shift if every finite graded module which is a simple object of the graded module category is isomorphic to an internal shift (S i){d} of a member of the family.

theorem TauCeti.isExhaustiveGradedSimpleFamily_iff {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} (S : I → (gradedFiniteModules 𝒜).FullSubcategory) : IsExhaustiveGradedSimpleFamily S ↔ ∀ (M : (gradedFiniteModules 𝒜).FullSubcategory), CategoryTheory.Simple M.obj → ∃ (i : I) (d : ℤ), Nonempty (M.obj ≅ (S i).obj.shiftObj d)

Characterization of IsExhaustiveGradedSimpleFamily, for importing modules, to which the body of the definition is not exposed.

theorem TauCeti.IsExhaustiveGradedSimpleFamily.exists_iso_of_concentrated {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} (S : I → (gradedFiniteModules 𝒜).FullSubcategory) (hS : IsExhaustiveGradedSimpleFamily S) (hSzero : ∀ (i : I) (p : ℤ), p ≠ 0 → (S i).obj.grading.piece ℤ p = ⊥) (N : (gradedFiniteModules 𝒜).FullSubcategory) (hNsimple : CategoryTheory.Simple N.obj) (hNzero : ∀ (p : ℤ), p ≠ 0 → N.obj.grading.piece ℤ p = ⊥) : ∃ (i : I), Nonempty (N.obj ≅ (S i).obj)

An exhaustive family up to shift is exhaustive without shifts among simple modules concentrated in degree zero, provided the chosen representatives are also concentrated in degree zero.

theorem TauCeti.IsExhaustiveGradedSimpleFamily.prop_on_pairs {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {I : Type uI} [Module.Finite k A] {S : I → (gradedFiniteModules 𝒜).FullSubcategory} (hS : IsExhaustiveGradedSimpleFamily S) (P : GradedModuleCat 𝒜 → GradedModuleCat 𝒜 → Prop) (hiso : ∀ {X X' Y Y' : GradedModuleCat 𝒜}, P X Y → ∀ (a : X ≅ X') (a : Y ≅ Y'), P X' Y') (hshift : ∀ {X Y : GradedModuleCat 𝒜}, P X Y → ∀ (d : ℤ), P (X.shiftObj d) Y) (hshiftRight : ∀ {X Y : GradedModuleCat 𝒜}, P X Y → ∀ (d : ℤ), P X (Y.shiftObj d)) (hleft : ∀ (Y : GradedModuleCat 𝒜), (∀ (T : GradedModuleCat 𝒜), Module.Finite k T.carrier → CategoryTheory.Simple T → P T Y) → ∀ (X : GradedModuleCat 𝒜), Module.Finite k X.carrier → P X Y) (hright : ∀ (X : GradedModuleCat 𝒜), (∀ (T : GradedModuleCat 𝒜), Module.Finite k T.carrier → CategoryTheory.Simple T → P X T) → ∀ (Y : GradedModuleCat 𝒜), Module.Finite k Y.carrier → P X Y) (h : ∀ (i j : I), P (S i).obj (S j).obj) {X Y : GradedModuleCat 𝒜} (hX : gradedFiniteModules 𝒜 X) (hY : gradedFiniteModules 𝒜 Y) : P X Y

A property of pairs which is invariant under isomorphisms and internal shifts and can be tested on finite-dimensional simples in either variable is detected on an exhaustive family of simples up to shift.