Representation-finite algebras and finite right-module skeletons

Finitely generated right A-modules are represented using Mathlib's left module category over Aᵐᵒᵖ. Representation-finiteness is the finiteness of the isomorphism classes of finite-dimensional indecomposable right modules.

The skeleton construction is adapted from CartanDeterminant.Algebra.RepresentationFinite and CartanDeterminant.RepresentationTheory.FiniteIndecomposableSkeleton at homological-conjectures commit eade4e75, with the module side made explicit and the unrelated Auslander-algebra layer omitted.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.Category (A : Type v) [Ring A] : Type (v + 1)

Mathlib model for right A-modules: left modules over Aᵐᵒᵖ.

def MagnitudeConjecture.RightModule.IsFiniteIndecomposable (k : Type u) [Field k] (A : Type v) [Ring A] [Algebra k A] (M : Category A) : Prop

A finite-dimensional indecomposable right A-module.

def MagnitudeConjecture.RightModule.IsRepresentationFinite (k : Type u) [Field k] (A : Type v) [Ring A] [Algebra k A] : Prop

There are finitely many isomorphism classes of finite-dimensional indecomposable right A-modules. The witnessing family may contain repetitions.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FinitelyGeneratedCategory (A : Type v) [Ring A] : Type (v + 1)

Mathlib's literal category of finitely generated right A-modules.

def MagnitudeConjecture.RightModule.IsRepresentationFiniteFinitelyGenerated (A : Type v) [Ring A] : Prop

Representation-finiteness stated literally on finitely generated right modules. Indecomposability is tested after the fully faithful inclusion into the ambient module category.

theorem MagnitudeConjecture.RightModule.finite_over_field_of_finitelyGenerated (k : Type u) [Field k] (A : Type v) [Ring A] [Algebra k A] [FiniteDimensional k A] (M : FinitelyGeneratedCategory A) : Module.Finite k ↑M

A finitely generated right module over a finite-dimensional algebra is finite-dimensional over the coefficient field.

def MagnitudeConjecture.RightModule.finitelyGeneratedOfFiniteDimensional (k : Type u) [Field k] (A : Type v) [Ring A] [Algebra k A] (M : Category A) [Module.Finite k ↑M] : FinitelyGeneratedCategory A

A finite-dimensional right module is finitely generated over Aᵐᵒᵖ.

theorem MagnitudeConjecture.RightModule.isRepresentationFinite_iff_finitelyGenerated (k : Type u) [Field k] (A : Type v) [Ring A] [Algebra k A] [FiniteDimensional k A] : IsRepresentationFinite k A ↔ IsRepresentationFiniteFinitelyGenerated A

For a finite-dimensional algebra, the finite-dimensional and literally finitely generated formulations of right representation-finiteness agree.

structure MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton (k : Type u) [Field k] (A : Type v) [Ring A] [Algebra k A] : Type (v + 1)

A finite skeleton of the finite-dimensional indecomposable right A-modules.

• n : ℕ
• obj : Fin self.n → Category A
• obj_finite (i : Fin self.n) : Module.Finite k ↑(self.obj i)
• obj_indecomposable (i : Fin self.n) : CategoryTheory.Indecomposable (self.obj i)
• eq_of_iso {i j : Fin self.n} : Nonempty (self.obj i ≅ self.obj j) → i = j
• complete (M : Category A) : IsFiniteIndecomposable k A M → ∃ (i : Fin self.n), Nonempty (M ≅ self.obj i)

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.moduleIsoSetoid {A : Type v} [Ring A] {σ : Type u_1} (X : σ → Category A) : Setoid σ

Isomorphism of modules in a family is an equivalence relation on its index type.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.exists_of_isRepresentationFinite {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (hA : IsRepresentationFinite k A) : Nonempty (FiniteIndecomposableSkeleton k A)

Representation-finiteness supplies an actual finite skeleton with no repeated isomorphism classes.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.obj_decomposition {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) [FiniteDimensional k A] (M : Category A) [Module.Finite k ↑M] : ∃ (n : ℕ) (label : Fin n → Fin S.n), Nonempty (M ≅ ⨁ fun (i : Fin n) => S.obj (label i))

Every finite-dimensional right module is a finite biproduct of objects from the chosen duplicate-free indecomposable skeleton.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgObj {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) : FinitelyGeneratedCategory A

A chosen finite-dimensional skeleton object, bundled as a finitely generated right module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.indecomposable_iff_obj {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (M : FinitelyGeneratedCategory A) : CategoryTheory.Indecomposable M ↔ CategoryTheory.Indecomposable M.obj

Indecomposability of a finitely generated right module is detected by the fully faithful inclusion into all right modules.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgObj_indecomposable {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (i : Fin S.n) : CategoryTheory.Indecomposable (S.fgObj i)

A chosen skeleton object remains indecomposable when bundled as a finitely generated right module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgObj_complete {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (M : FinitelyGeneratedCategory A) (hM : CategoryTheory.Indecomposable M) : ∃ (i : Fin S.n), Nonempty (M ≅ S.fgObj i)

The chosen finitely generated skeleton contains every indecomposable finitely generated right module.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgObj_skeletal {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) {i j : Fin S.n} (h : Nonempty (S.fgObj i ≅ S.fgObj j)) : i = j

The chosen finitely generated skeleton has no repeated isomorphism classes.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.oppositeIsNoetherian {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] : IsNoetherianRing Aᵐᵒᵖ

The opposite of a finite-dimensional algebra is Noetherian, so its finitely generated module category is abelian and idempotent-complete. This is a named value rather than a global instance because the coefficient field is not determined by the target ring.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgObj_decomposition {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (M : FinitelyGeneratedCategory A) : ∃ (n : ℕ) (label : Fin n → Fin S.n), Nonempty (M ≅ ⨁ fun (i : Fin n) => S.fgObj (label i))

Every finitely generated right module over a finite-dimensional algebra is a finite biproduct of the chosen skeleton objects, now inside the literal finitely generated module category.

@[reducible, inline]

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

The full category on the chosen finite right-module skeleton.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.categoryFintype {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : Fintype S.IndecCategory

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.inclusion {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor S.IndecCategory (Category A)

The fully faithful inclusion of the finite indecomposable skeleton into the right-module category.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.inclusion_additive {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : S.inclusion.Additive

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.inclusion_linear {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor.Linear k S.inclusion

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.indecCategory_obj_finite {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) : Module.Finite k ↑(S.inclusion.obj i)

Every chosen skeleton object is finite-dimensional over k.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.indecCategory_obj_indecomposable {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (i : S.IndecCategory) : CategoryTheory.Indecomposable (S.inclusion.obj i)

Every chosen skeleton object is indecomposable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.moduleCat_hom_finite {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (M N : Category A) [Module.Finite k ↑M] [Module.Finite k ↑N] : Module.Finite k (M ⟶ N)

Hom spaces between finite-dimensional right modules are finite-dimensional over the coefficient field.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.fgModuleCatHomFinite {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (M N : FinitelyGeneratedCategory A) : Module.Finite k (M ⟶ N)

Hom spaces in the literal category of finitely generated right modules are finite-dimensional over the coefficient field.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.indecCategoryHomFinite {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (i j : S.IndecCategory) : Module.Finite k (i ⟶ j)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.indecCategory_eq_of_iso {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) {i j : S.IndecCategory} (h : Nonempty (i ≅ j)) : i = j

Isomorphic objects of the chosen right-module skeleton have equal labels.