Idempotent corners of representation-finite algebras

Lemma 3.1(1), second part (projective-rays.tex): for C = eAe, the extension of C-modules to A-modules is fully faithful and preserves finite dimension, indecomposability and isomorphism classes; hence C is representation-finite. The source uses induction V ↦ V ⊗_C eA, whose unit V → (V ⊗_C eA)e is an isomorphism. We use the adjoint form, coinduction V ↦ Hom_C(Ae, V), whose counit Hom_C(Ae, V)e → V is an isomorphism; this avoids tensor products over the noncommutative ring C.

def MultiplicativeBasisDeformations.Coind.leftIdeal {A : Type v} [Ring A] {e : A} : AddSubgroup A

The left ideal Ae.

theorem MultiplicativeBasisDeformations.Coind.mem_leftIdeal {A : Type v} [Ring A] {e x : A} : x ∈ leftIdeal ↔ x * e = x

@[instance_reducible]

instance MultiplicativeBasisDeformations.Coind.instSMulMulOppositeCornerSubtypeMemAddSubgroupLeftIdeal {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} : SMul he.Cornerᵐᵒᵖ ↥leftIdeal

Ae is a right C-module.

@[simp]

theorem MultiplicativeBasisDeformations.Coind.smul_val {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} (c : he.Cornerᵐᵒᵖ) (x : ↥leftIdeal) : ↑(c • x) = ↑x * cornerVal he (MulOpposite.unop c)

@[instance_reducible]

instance MultiplicativeBasisDeformations.Coind.instModuleMulOppositeCornerSubtypeMemAddSubgroupLeftIdeal {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} : Module he.Cornerᵐᵒᵖ ↥leftIdeal

def MultiplicativeBasisDeformations.Coind.lmul {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} (a : A) : ↥leftIdeal →ₗ[he.Cornerᵐᵒᵖ] ↥leftIdeal

Left multiplication by a on Ae.

@[simp]

theorem MultiplicativeBasisDeformations.Coind.lmul_val {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} (a : A) (x : ↥leftIdeal) : ↑((lmul a) x) = a * ↑x

def MultiplicativeBasisDeformations.Coind.Obj {A : Type v} [Ring A] {e : A} (he : IsIdempotentElem e) (V : RightModuleCat he.Corner) : Type v

The carrier Hom_C(Ae, V) of the coinduced module.

@[instance_reducible]

instance MultiplicativeBasisDeformations.Coind.instAddCommGroupObj {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} (V : RightModuleCat he.Corner) : AddCommGroup (Obj he V)

@[instance_reducible]

instance MultiplicativeBasisDeformations.Coind.instFunLikeObjSubtypeMemAddSubgroupLeftIdealCarrierMulOppositeCorner {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} (V : RightModuleCat he.Corner) : FunLike (Obj he V) ↥leftIdeal ↑V

instance MultiplicativeBasisDeformations.Coind.instLinearMapClassObjMulOppositeCornerSubtypeMemAddSubgroupLeftIdealCarrier {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} (V : RightModuleCat he.Corner) : LinearMapClass (Obj he V) he.Cornerᵐᵒᵖ ↥leftIdeal ↑V

@[instance_reducible]

instance MultiplicativeBasisDeformations.Coind.instSMulMulOppositeObj {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} (V : RightModuleCat he.Corner) : SMul Aᵐᵒᵖ (Obj he V)

theorem MultiplicativeBasisDeformations.Coind.smul_apply' {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} {V : RightModuleCat he.Corner} (a : Aᵐᵒᵖ) (φ : Obj he V) (y : ↥leftIdeal) : (a • φ) y = φ ((lmul (MulOpposite.unop a)) y)

theorem MultiplicativeBasisDeformations.Coind.Obj.ext {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} {V : RightModuleCat he.Corner} {φ ψ : Obj he V} (h : ∀ (y : ↥leftIdeal), φ y = ψ y) : φ = ψ

theorem MultiplicativeBasisDeformations.Coind.Obj.ext_iff {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} {V : RightModuleCat he.Corner} {φ ψ : Obj he V} : φ = ψ ↔ ∀ (y : ↥leftIdeal), φ y = ψ y

theorem MultiplicativeBasisDeformations.Coind.add_apply' {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} {V : RightModuleCat he.Corner} (φ ψ : Obj he V) (y : ↥leftIdeal) : (φ + ψ) y = φ y + ψ y

theorem MultiplicativeBasisDeformations.Coind.zero_apply' {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} {V : RightModuleCat he.Corner} (y : ↥leftIdeal) : 0 y = 0

@[instance_reducible]

instance MultiplicativeBasisDeformations.Coind.instModuleMulOppositeObj {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} (V : RightModuleCat he.Corner) : Module Aᵐᵒᵖ (Obj he V)

def MultiplicativeBasisDeformations.Coind.coind {A : Type v} [Ring A] {e : A} (he : IsIdempotentElem e) (V : RightModuleCat he.Corner) : RightModuleCat A

The coinduced right A-module Hom_C(Ae, V).

def MultiplicativeBasisDeformations.Coind.mapObj {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} {V W : RightModuleCat he.Corner} (f : V ⟶ W) : Obj he V →ₗ[Aᵐᵒᵖ] Obj he W

Postcomposition with a map of C-modules.

theorem MultiplicativeBasisDeformations.Coind.mapObj_apply {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} {V W : RightModuleCat he.Corner} (f : V ⟶ W) (φ : Obj he V) (y : ↥leftIdeal) : ((mapObj f) φ) y = (ModuleCat.Hom.hom f) (φ y)

def MultiplicativeBasisDeformations.Coind.functor {A : Type v} [Ring A] {e : A} (he : IsIdempotentElem e) : CategoryTheory.Functor (RightModuleCat he.Corner) (RightModuleCat A)

Coinduction V ↦ Hom_C(Ae, V).

@[instance_reducible]

instance MultiplicativeBasisDeformations.Coind.instFunLikeCarrierMulOppositeObjRightModuleCatCornerFunctorSubtypeMemAddSubgroupLeftIdeal {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} (V : RightModuleCat he.Corner) : FunLike ↑((functor he).obj V) ↥leftIdeal ↑V

instance MultiplicativeBasisDeformations.Coind.instLinearMapClassCarrierMulOppositeObjRightModuleCatCornerFunctorSubtypeMemAddSubgroupLeftIdeal {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} (V : RightModuleCat he.Corner) : LinearMapClass (↑((functor he).obj V)) he.Cornerᵐᵒᵖ ↥leftIdeal ↑V

def MultiplicativeBasisDeformations.Coind.eL {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} : ↥leftIdeal

The generator e ∈ Ae.

theorem MultiplicativeBasisDeformations.Coind.ey_mem {A : Type v} [Ring A] {e : A} (y : ↥leftIdeal) : e * ↑y ∈ Subsemigroup.corner e

def MultiplicativeBasisDeformations.Coind.ey {A : Type v} [Ring A] {e : A} (he : IsIdempotentElem e) (y : ↥leftIdeal) : he.Corner

ey ∈ eAe for y ∈ Ae.

theorem MultiplicativeBasisDeformations.Coind.ey_add {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} (y z : ↥leftIdeal) : ey he (y + z) = ey he y + ey he z

theorem MultiplicativeBasisDeformations.Coind.ey_smul {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} (c : he.Cornerᵐᵒᵖ) (y : ↥leftIdeal) : ey he (c • y) = ey he y * MulOpposite.unop c

theorem MultiplicativeBasisDeformations.Coind.ey_eL {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} : ey he eL = 1

def MultiplicativeBasisDeformations.Coind.psi {A : Type v} [Ring A] {e : A} (he : IsIdempotentElem e) {V : RightModuleCat he.Corner} (v : ↑V) : Obj he V

ψ_v : y ↦ v · (ey).

theorem MultiplicativeBasisDeformations.Coind.psi_apply {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} {V : RightModuleCat he.Corner} (v : ↑V) (y : ↥leftIdeal) : (psi he v) y = MulOpposite.op (ey he y) • v

theorem MultiplicativeBasisDeformations.Coind.psi_eL {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} {V : RightModuleCat he.Corner} (v : ↑V) : (psi he v) eL = v

theorem MultiplicativeBasisDeformations.Coind.smul_ey {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} (y x : ↥leftIdeal) : MulOpposite.op (ey he x) • y = (lmul ↑y) x

y · (ex) = yx in Ae.

theorem MultiplicativeBasisDeformations.Coind.smul_eq_psi {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} {V : RightModuleCat he.Corner} (φ : Obj he V) (y : ↥leftIdeal) : MulOpposite.op ↑y • φ = psi he (φ y)

y · φ = ψ_{φ(y)}.

instance MultiplicativeBasisDeformations.Coind.faithful {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} : (functor he).Faithful

theorem MultiplicativeBasisDeformations.Coind.psi_add {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} {V : RightModuleCat he.Corner} (v w : ↑V) : psi he (v + w) = psi he v + psi he w

theorem MultiplicativeBasisDeformations.Coind.psi_smul {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} {V : RightModuleCat he.Corner} (c : he.Cornerᵐᵒᵖ) (v : ↑V) : psi he (c • v) = MulOpposite.op (cornerVal he (MulOpposite.unop c)) • psi he v

theorem MultiplicativeBasisDeformations.Coind.lmul_eL {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} (y : ↥leftIdeal) : (lmul ↑y) eL = y

theorem MultiplicativeBasisDeformations.Coind.lmul_corner_eL {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} (c : he.Cornerᵐᵒᵖ) : (lmul (cornerVal he (MulOpposite.unop c))) eL = c • eL

instance MultiplicativeBasisDeformations.Coind.full {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} : (functor he).Full

instance MultiplicativeBasisDeformations.Coind.instAdditiveRightModuleCatCornerFunctor {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} : (functor he).Additive

def MultiplicativeBasisDeformations.Coind.xe {A : Type v} [Ring A] {e : A} {he : IsIdempotentElem e} (x : A) : ↥leftIdeal

xe ∈ Ae.

theorem MultiplicativeBasisDeformations.Coind.xe_smul {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} {he : IsIdempotentElem e} (c : k) (x : A) : xe (c • x) = MulOpposite.op ((algebraMap k he.Corner) c) • xe x

def MultiplicativeBasisDeformations.Coind.evalK {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} {he : IsIdempotentElem e} (V : RightModuleCat he.Corner) : ↑(coind he V) →ₗ[k] A →ₗ[k] ↑V

Evaluation of Hom_C(Ae, V) on the elements xe, a k-linear injection into Hom_k(A, V).

theorem MultiplicativeBasisDeformations.Coind.evalK_injective {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} {he : IsIdempotentElem e} (V : RightModuleCat he.Corner) : Function.Injective ⇑(evalK V)

theorem MultiplicativeBasisDeformations.Coind.coind_finite {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} {he : IsIdempotentElem e} [FiniteDimensional k A] (V : RightModuleCat he.Corner) [Module.Finite k ↑V] : Module.Finite k ↑(coind he V)

theorem MultiplicativeBasisDeformations.corner_finite {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} (he : IsIdempotentElem e) [FiniteDimensional k A] : Module.Finite k he.Corner

The corner is finite-dimensional.

theorem MultiplicativeBasisDeformations.corner_isRepresentationFinite_of {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} (he : IsIdempotentElem e) [FiniteDimensional k A] (hA : IsRepresentationFinite k A) : IsRepresentationFinite k he.Corner

Lemma 3.1(1), second part: every idempotent corner of a representation-finite algebra is representation-finite.