Representation-finiteness of algebra quotients

Restriction along a quotient map realizes quotient modules as the full exact subcategory annihilated by the quotient ideal. In particular, representation-finiteness descends to every two-sided quotient. We also record the small algebra-equivalence transport needed to return from left modules over the quotient of an opposite algebra to right modules.

The proofs are adapted from CartanDeterminant.Algebra.RepresentationFinite and CartanDeterminant.Algebra.RepresentationFiniteIdeals at homological-conjectures commit 916afb44; the unrelated ideal-lattice and representation-infinite applications are omitted.

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

A finite-dimensional indecomposable left module.

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

Finiteness of the isomorphism classes of finite-dimensional indecomposable left modules.

theorem MagnitudeConjecture.LeftModule.indecomposable_functor_obj_iff {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type v} [CategoryTheory.Category.{w, v} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasBinaryBiproducts D] (E : C ≌ D) [E.functor.Additive] [E.inverse.Additive] (X : C) : CategoryTheory.Indecomposable (E.functor.obj X) ↔ CategoryTheory.Indecomposable X

An additive equivalence preserves and reflects indecomposability.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.LeftModule.moduleEquivalenceOfAlgEquiv {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {B : Type v} [Ring B] [Algebra k B] (f : A ≃ₐ[k] B) : ModuleCat A ≌ ModuleCat B

The module-category equivalence induced by an algebra equivalence.

def MagnitudeConjecture.LeftModule.moduleEquivalenceOfAlgEquivObjLinearEquiv {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {B : Type v} [Ring B] [Algebra k B] (f : A ≃ₐ[k] B) (M : ModuleCat A) : ↑M ≃ₗ[k] ↑((moduleEquivalenceOfAlgEquiv f).functor.obj M)

The underlying k-linear equivalence from a module to its image under the equivalence induced by an algebra equivalence.

noncomputable def MagnitudeConjecture.LeftModule.fgModuleEquivalenceOfAlgEquiv {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {B : Type v} [Ring B] [Algebra k B] [Module.Finite k A] [Module.Finite k B] (f : A ≃ₐ[k] B) : FGModuleCat A ≌ FGModuleCat B

An algebra equivalence induces an equivalence between the literal categories of finitely generated modules. Finite-dimensionality of the two algebras over k supplies finite generation after each restriction of scalars.

instance MagnitudeConjecture.LeftModule.fgModuleEquivalenceOfAlgEquivFunctorAdditive {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {B : Type v} [Ring B] [Algebra k B] [Module.Finite k A] [Module.Finite k B] (f : A ≃ₐ[k] B) : (fgModuleEquivalenceOfAlgEquiv f).functor.Additive

instance MagnitudeConjecture.LeftModule.fgModuleEquivalenceOfAlgEquivInverseAdditive {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {B : Type v} [Ring B] [Algebra k B] [Module.Finite k A] [Module.Finite k B] (f : A ≃ₐ[k] B) : (fgModuleEquivalenceOfAlgEquiv f).inverse.Additive

instance MagnitudeConjecture.LeftModule.fgModuleEquivalenceOfAlgEquivFunctorLinear {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {B : Type v} [Ring B] [Algebra k B] [Module.Finite k A] [Module.Finite k B] (f : A ≃ₐ[k] B) : CategoryTheory.Functor.Linear k (fgModuleEquivalenceOfAlgEquiv f).functor

Restriction along an algebra equivalence is linear over the common ground field.

instance MagnitudeConjecture.LeftModule.fgModuleEquivalenceOfAlgEquivInverseLinear {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {B : Type v} [Ring B] [Algebra k B] [Module.Finite k A] [Module.Finite k B] (f : A ≃ₐ[k] B) : CategoryTheory.Functor.Linear k (fgModuleEquivalenceOfAlgEquiv f).inverse

The inverse restriction equivalence is linear over the common ground field.

theorem MagnitudeConjecture.LeftModule.IsRepresentationFinite.of_algEquiv {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {B : Type v} [Ring B] [Algebra k B] (hA : IsRepresentationFinite k A) (f : A ≃ₐ[k] B) : IsRepresentationFinite k B

Representation-finiteness is preserved by an algebra equivalence.

theorem MagnitudeConjecture.LeftModule.fgModule_indecomposable_iff_obj {R : Type v} [Ring R] [IsNoetherianRing R] (M : FGModuleCat R) : CategoryTheory.Indecomposable M ↔ CategoryTheory.Indecomposable M.obj

Indecomposability in the literal finitely generated module category is equivalent to indecomposability of the underlying module.

def MagnitudeConjecture.LeftModule.quotientRestrictLinearEquiv {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (I : TwoSidedIdeal A) (M : ModuleCat (A ⧸ TwoSidedIdeal.asIdeal I)) : ↑M ≃ₗ[k] ↑((ModuleCat.restrictScalars (Ideal.Quotient.mk (TwoSidedIdeal.asIdeal I))).obj M)

Restriction along a quotient map preserves the underlying k-vector space.

noncomputable def MagnitudeConjecture.LeftModule.quotientRestrictLift {A : Type v} [Ring A] (I : TwoSidedIdeal A) {M N : ModuleCat (A ⧸ TwoSidedIdeal.asIdeal I)} (g : (ModuleCat.restrictScalars (Ideal.Quotient.mk (TwoSidedIdeal.asIdeal I))).obj M ⟶ (ModuleCat.restrictScalars (Ideal.Quotient.mk (TwoSidedIdeal.asIdeal I))).obj N) : M ⟶ N

A map between quotient modules which is linear after restriction is already linear over the quotient, because the quotient map is surjective.

noncomputable def MagnitudeConjecture.LeftModule.quotientRestrictIso {A : Type v} [Ring A] (I : TwoSidedIdeal A) {M N : ModuleCat (A ⧸ TwoSidedIdeal.asIdeal I)} (e : (ModuleCat.restrictScalars (Ideal.Quotient.mk (TwoSidedIdeal.asIdeal I))).obj M ≅ (ModuleCat.restrictScalars (Ideal.Quotient.mk (TwoSidedIdeal.asIdeal I))).obj N) : M ≅ N

An isomorphism between restricted quotient modules lifts uniquely to an isomorphism over the quotient.

@[simp]

theorem MagnitudeConjecture.LeftModule.quotientRestrictIso_hom_apply {A : Type v} [Ring A] (I : TwoSidedIdeal A) {M N : ModuleCat (A ⧸ TwoSidedIdeal.asIdeal I)} (e : (ModuleCat.restrictScalars (Ideal.Quotient.mk (TwoSidedIdeal.asIdeal I))).obj M ≅ (ModuleCat.restrictScalars (Ideal.Quotient.mk (TwoSidedIdeal.asIdeal I))).obj N) (m : ↑M) : (CategoryTheory.ConcreteCategory.hom (quotientRestrictIso I e).hom) m = (CategoryTheory.ConcreteCategory.hom e.hom) m

theorem MagnitudeConjecture.LeftModule.quotientRestrict_indecomposable {A : Type v} [Ring A] (I : TwoSidedIdeal A) (M : ModuleCat (A ⧸ TwoSidedIdeal.asIdeal I)) (hM : CategoryTheory.Indecomposable M) : CategoryTheory.Indecomposable ((ModuleCat.restrictScalars (Ideal.Quotient.mk (TwoSidedIdeal.asIdeal I))).obj M)

Restriction along a quotient map preserves indecomposability.

theorem MagnitudeConjecture.LeftModule.IsRepresentationFinite.quotient {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] (hA : IsRepresentationFinite k A) (I : TwoSidedIdeal A) : IsRepresentationFinite k (A ⧸ TwoSidedIdeal.asIdeal I)

Representation-finiteness descends to every two-sided algebra quotient.