Representation-finite algebras: bounded modules and two-sided ideals

Lemma 3.1(1), first part (projective-rays.tex): "The annihilator of the right module A/I is I. Finite representation type gives only finitely many isomorphism classes of modules of dimension at most dim_k A."

theorem MultiplicativeBasisDeformations.exists_labels_iso {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (hA : IsRepresentationFinite k A) : ∃ (N : ℕ) (X : Fin N → RightModuleCat A), (∀ (i : Fin N), IsFiniteIndecomposable k A (X i)) ∧ ∀ (M : RightModuleCat A), Module.Finite k ↑M → ∃ (n : ℕ) (l : Fin n → Fin N), n ≤ Module.finrank k ↑M ∧ Nonempty (M ≅ ⨁ fun (j : Fin n) => X (l j))

Every finite-dimensional right module over a representation-finite algebra is a biproduct of at most dim M modules from the finite list.

def MultiplicativeBasisDeformations.TwoSidedIdeal.toRightSub {A : Type v} [Ring A] (I : TwoSidedIdeal A) : Submodule Aᵐᵒᵖ A

A two-sided ideal as a right submodule of A_A.

def MultiplicativeBasisDeformations.quotModule {A : Type v} [Ring A] (I : TwoSidedIdeal A) : RightModuleCat A

The right module A/I.

def MultiplicativeBasisDeformations.quotMk {A : Type v} [Ring A] (I : TwoSidedIdeal A) (x : A) : ↑(quotModule I)

The class of x in A/I.

theorem MultiplicativeBasisDeformations.quotMk_surjective {A : Type v} [Ring A] (I : TwoSidedIdeal A) : Function.Surjective (quotMk I)

theorem MultiplicativeBasisDeformations.smul_quotMk {A : Type v} [Ring A] (I : TwoSidedIdeal A) (a x : A) : MulOpposite.op a • quotMk I x = quotMk I (x * a)

theorem MultiplicativeBasisDeformations.quotMk_eq_zero {A : Type v} [Ring A] (I : TwoSidedIdeal A) (x : A) : quotMk I x = 0 ↔ x ∈ I

theorem MultiplicativeBasisDeformations.mem_iff_annihilates {A : Type v} [Ring A] (I : TwoSidedIdeal A) (a : A) : a ∈ I ↔ ∀ (m : ↑(quotModule I)), MulOpposite.op a • m = 0

The annihilator of A/I is I.

theorem MultiplicativeBasisDeformations.eq_of_iso {A : Type v} [Ring A] (I J : TwoSidedIdeal A) (e : quotModule I ≅ quotModule J) : I = J

theorem MultiplicativeBasisDeformations.quotModule_finite {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (I : TwoSidedIdeal A) : Module.Finite k ↑(quotModule I) ∧ Module.finrank k ↑(quotModule I) ≤ Module.finrank k A

theorem MultiplicativeBasisDeformations.finite_twoSidedIdeals_of {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] [FiniteDimensional k A] (hA : IsRepresentationFinite k A) : Set.univ.Finite

Lemma 3.1(1), first part: a representation-finite algebra has finitely many two-sided ideals.