Full idempotents: Morita equivalence for representation-finiteness

For Lemma 4.7 (lem:homogeneous-projection, scalar-normalization.tex): "Repeated labels give matrix multiplicities, and the distinct labels give an idempotent corner of B. Thus B' is representation-finite by Morita equivalence and Lemma 3.1(1)."

The Morita equivalence used is the one of a full idempotent e (AeA = A): every right A-module N is the coinduced module Hom_C(Ae, Ne) of its C = eAe-module Ne (theta_bijective). Hence if eAe is representation-finite, so is A (isRepresentationFinite_of_full). Repeated labels are handled by placing them, together with the distinct labels, in one category algebra in which the distinct labels form a full idempotent (CategoryAlgebraCorners.lean).

theorem MultiplicativeBasisDeformations.exists_sum_eq_one {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} (hfull : ∀ (a : A), a ∈ Submodule.span k {x : A | ∃ (p : A) (q : A), x = p * e * q}) : ∃ (m : ℕ) (p : Fin m → A) (q : Fin m → A), ∑ i : Fin m, p i * e * q i = 1

A full idempotent, as a finite sum ∑ pᵢ e qᵢ = 1.

def MultiplicativeBasisDeformations.Coind.resSub {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} (N : RightModuleCat A) : Submodule k ↑N

Ne, for a right A-module N.

theorem MultiplicativeBasisDeformations.Coind.mem_resSub {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} {N : RightModuleCat A} {n : ↑N} : n ∈ resSub N ↔ MulOpposite.op e • n = n

theorem MultiplicativeBasisDeformations.Coind.corner_smul_mem {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} {he : IsIdempotentElem e} {N : RightModuleCat A} (c : he.Corner) (n : ↑N) : MulOpposite.op (cornerVal he c) • n ∈ resSub N

@[instance_reducible]

instance MultiplicativeBasisDeformations.Coind.instSMulMulOppositeCornerSubtypeCarrierMemSubmoduleResSub {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} {he : IsIdempotentElem e} (N : RightModuleCat A) : SMul he.Cornerᵐᵒᵖ ↥(resSub N)

theorem MultiplicativeBasisDeformations.Coind.res_smul_val {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} {he : IsIdempotentElem e} {N : RightModuleCat A} (c : he.Cornerᵐᵒᵖ) (n : ↥(resSub N)) : ↑(c • n) = MulOpposite.op (cornerVal he (MulOpposite.unop c)) • ↑n

@[instance_reducible]

instance MultiplicativeBasisDeformations.Coind.instModuleMulOppositeCornerSubtypeCarrierMemSubmoduleResSub {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} {he : IsIdempotentElem e} (N : RightModuleCat A) : Module he.Cornerᵐᵒᵖ ↥(resSub N)

def MultiplicativeBasisDeformations.Coind.res {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} (he : IsIdempotentElem e) (N : RightModuleCat A) : RightModuleCat he.Corner

The restriction N ↦ Ne to the corner.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.Coind.resK (k : Type u) [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} {he : IsIdempotentElem e} (N : RightModuleCat A) : RightModuleCat he.Corner

res with the field explicit.

def MultiplicativeBasisDeformations.Coind.rv {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} {he : IsIdempotentElem e} {N : RightModuleCat A} (m : ↑(resK k N)) : ↑N

The underlying element of N of an element of Ne.

def MultiplicativeBasisDeformations.Coind.rmk {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} {he : IsIdempotentElem e} {N : RightModuleCat A} (n : ↑N) (hn : n ∈ resSub N) : ↑(resK k N)

An element of Ne.

@[simp]

theorem MultiplicativeBasisDeformations.Coind.rv_rmk {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} {he : IsIdempotentElem e} {N : RightModuleCat A} (n : ↑N) (hn : n ∈ resSub N) : rv (rmk n hn) = n

theorem MultiplicativeBasisDeformations.Coind.rv_injective {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} {he : IsIdempotentElem e} {N : RightModuleCat A} : Function.Injective rv

@[simp]

theorem MultiplicativeBasisDeformations.Coind.rv_add {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} {he : IsIdempotentElem e} {N : RightModuleCat A} (m m' : ↑(resK k N)) : rv (m + m') = rv m + rv m'

@[simp]

theorem MultiplicativeBasisDeformations.Coind.rv_smul {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} {he : IsIdempotentElem e} {N : RightModuleCat A} (c : he.Cornerᵐᵒᵖ) (m : ↑(resK k N)) : rv (c • m) = MulOpposite.op (cornerVal he (MulOpposite.unop c)) • rv m

theorem MultiplicativeBasisDeformations.Coind.rv_sum {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} {he : IsIdempotentElem e} {N : RightModuleCat A} {ι : Type u_1} (s : Finset ι) (f : ι → ↑(resK k N)) : rv (∑ i ∈ s, f i) = ∑ i ∈ s, rv (f i)

theorem MultiplicativeBasisDeformations.Coind.smul_mem_res {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} {N : RightModuleCat A} (n : ↑N) (y : ↥leftIdeal) : MulOpposite.op ↑y • n ∈ resSub N

n y ∈ Ne for y ∈ Ae.

def MultiplicativeBasisDeformations.Coind.thetaFun {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} (he : IsIdempotentElem e) (N : RightModuleCat A) (n : ↑N) : Obj he (resK k N)

The comparison map N → Hom_C(Ae, Ne), n ↦ (y ↦ n y).

theorem MultiplicativeBasisDeformations.Coind.thetaFun_apply {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} {he : IsIdempotentElem e} (N : RightModuleCat A) (n : ↑N) (y : ↥leftIdeal) : rv ((thetaFun he N n) y) = MulOpposite.op ↑y • n

def MultiplicativeBasisDeformations.Coind.theta {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} (he : IsIdempotentElem e) (N : RightModuleCat A) : ↑N →ₗ[Aᵐᵒᵖ] Obj he (resK k N)

The comparison map, as a map of right A-modules.

theorem MultiplicativeBasisDeformations.Coind.theta_bijective {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} {he : IsIdempotentElem e} (hfull : ∀ (a : A), a ∈ Submodule.span k {x : A | ∃ (p : A) (q : A), x = p * e * q}) (N : RightModuleCat A) : Function.Bijective ⇑(theta he N)

Morita for a full idempotent: N ≅ Hom_C(Ae, Ne).

def MultiplicativeBasisDeformations.Coind.rvK {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} {he : IsIdempotentElem e} (N : RightModuleCat A) : ↑(resK k N) →ₗ[k] ↑N

Ne → N is k-linear for the module structure through the corner.

theorem MultiplicativeBasisDeformations.Coind.res_finite {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} {he : IsIdempotentElem e} (N : RightModuleCat A) [Module.Finite k ↑N] : Module.Finite k ↑(resK k N)

def MultiplicativeBasisDeformations.Coind.endRingEquivOfIso {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X Y : C} (i : X ≅ Y) : CategoryTheory.End X ≃+* CategoryTheory.End Y

A ring isomorphism of endomorphism rings from an isomorphism.

theorem MultiplicativeBasisDeformations.isRepresentationFinite_of_full {k : Type u} [Field k] {A : Type v} [Ring A] [Algebra k A] {e : A} (he : IsIdempotentElem e) [FiniteDimensional k A] (hfull : ∀ (a : A), a ∈ Submodule.span k {x : A | ∃ (p : A) (q : A), x = p * e * q}) (hC : IsRepresentationFinite k he.Corner) : IsRepresentationFinite k A

Morita for a full idempotent: if AeA = A and eAe is representation-finite, so is A.