Lemma 4.6: split representation transfer

lem:split-representation-transfer (scalar-normalization.tex): let C ⊆ B be a unital inclusion of finite-dimensional algebras, q : C ↠ D a quotient and π : B → D a C-bimodule map with π|_C = q. If B is representation-finite, so is D.

The source proves that a right D-module M, inflated to C, is a summand of (M ⊗_C B)|_C (map m ↦ m ⊗ 1, retraction m ⊗ b ↦ m π(b)). We use the adjoint form: M is a summand of Hom_C(B, M)|_C, with map m ↦ (b ↦ m π(b)) and retraction φ ↦ φ(1); the rest of the argument (decomposition over the finitely many indecomposable B-modules, exchange, inflation fully faithful) is the source's.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.inclOp {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] (C : Subalgebra k B) : (↥C)ᵐᵒᵖ →+* Bᵐᵒᵖ

The inclusion Cᵐᵒᵖ → Bᵐᵒᵖ.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.qOp {k : Type u} [Field k] {B D : Type v} [Ring B] [Algebra k B] [Ring D] [Algebra k D] (C : Subalgebra k B) (q : ↥C →ₐ[k] D) : (↥C)ᵐᵒᵖ →+* Dᵐᵒᵖ

The quotient Cᵐᵒᵖ → Dᵐᵒᵖ.

theorem MultiplicativeBasisDeformations.pi_mul_right {k : Type u} [Field k] {B D : Type v} [Ring B] [Algebra k B] [Ring D] [Algebra k D] {C : Subalgebra k B} {q : ↥C →ₐ[k] D} (π : B →ₗ[k] D) (hbimod : ∀ (c c' : ↥C) (b : B), π (↑c * b * ↑c') = q c * π b * q c') (b : B) (c : ↥C) : π (b * ↑c) = π b * q c

theorem MultiplicativeBasisDeformations.pi_mul_left {k : Type u} [Field k] {B D : Type v} [Ring B] [Algebra k B] [Ring D] [Algebra k D] {C : Subalgebra k B} {q : ↥C →ₐ[k] D} (π : B →ₗ[k] D) (hbimod : ∀ (c c' : ↥C) (b : B), π (↑c * b * ↑c') = q c * π b * q c') (c : ↥C) (b : B) : π (↑c * b) = q c * π b

def MultiplicativeBasisDeformations.SplitCoind.RC {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] (_C : Subalgebra k B) : Type v

B as a right C-module.

@[instance_reducible]

instance MultiplicativeBasisDeformations.SplitCoind.instAddCommGroupRC {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] {C : Subalgebra k B} : AddCommGroup (RC C)

def MultiplicativeBasisDeformations.SplitCoind.toRC {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] {C : Subalgebra k B} : B ≃+ RC C

The identification B = RC.

@[instance_reducible]

instance MultiplicativeBasisDeformations.SplitCoind.instModuleMulOppositeSubtypeMemSubalgebraRC {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] {C : Subalgebra k B} : Module (↥C)ᵐᵒᵖ (RC C)

theorem MultiplicativeBasisDeformations.SplitCoind.smul_def {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] {C : Subalgebra k B} (c : (↥C)ᵐᵒᵖ) (x : B) : c • toRC x = toRC (x * ↑(MulOpposite.unop c))

def MultiplicativeBasisDeformations.SplitCoind.lmul {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] {C : Subalgebra k B} (b : B) : RC C →ₗ[(↥C)ᵐᵒᵖ] RC C

Left multiplication by b on RC.

def MultiplicativeBasisDeformations.SplitCoind.Obj {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] (C : Subalgebra k B) (V : ModuleCat (↥C)ᵐᵒᵖ) : Type v

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

@[instance_reducible]

instance MultiplicativeBasisDeformations.SplitCoind.instAddCommGroupObj {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] {C : Subalgebra k B} (V : ModuleCat (↥C)ᵐᵒᵖ) : AddCommGroup (Obj C V)

@[instance_reducible]

instance MultiplicativeBasisDeformations.SplitCoind.instFunLikeObjRCCarrierMulOppositeSubtypeMemSubalgebra {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] {C : Subalgebra k B} (V : ModuleCat (↥C)ᵐᵒᵖ) : FunLike (Obj C V) (RC C) ↑V

instance MultiplicativeBasisDeformations.SplitCoind.instLinearMapClassObjMulOppositeSubtypeMemSubalgebraRCCarrier {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] {C : Subalgebra k B} (V : ModuleCat (↥C)ᵐᵒᵖ) : LinearMapClass (Obj C V) (↥C)ᵐᵒᵖ (RC C) ↑V

theorem MultiplicativeBasisDeformations.SplitCoind.Obj.ext {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] {C : Subalgebra k B} {V : ModuleCat (↥C)ᵐᵒᵖ} {φ ψ : Obj C V} (h : ∀ (x : RC C), φ x = ψ x) : φ = ψ

theorem MultiplicativeBasisDeformations.SplitCoind.Obj.ext_iff {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] {C : Subalgebra k B} {V : ModuleCat (↥C)ᵐᵒᵖ} {φ ψ : Obj C V} : φ = ψ ↔ ∀ (x : RC C), φ x = ψ x

@[instance_reducible]

instance MultiplicativeBasisDeformations.SplitCoind.instSMulMulOppositeObj {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] {C : Subalgebra k B} (V : ModuleCat (↥C)ᵐᵒᵖ) : SMul Bᵐᵒᵖ (Obj C V)

theorem MultiplicativeBasisDeformations.SplitCoind.smul_apply' {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] {C : Subalgebra k B} {V : ModuleCat (↥C)ᵐᵒᵖ} (b : Bᵐᵒᵖ) (φ : Obj C V) (x : B) : (b • φ) (toRC x) = φ (toRC (MulOpposite.unop b * x))

@[instance_reducible]

instance MultiplicativeBasisDeformations.SplitCoind.instModuleMulOppositeObj {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] {C : Subalgebra k B} (V : ModuleCat (↥C)ᵐᵒᵖ) : Module Bᵐᵒᵖ (Obj C V)

def MultiplicativeBasisDeformations.SplitCoind.coind {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] {C : Subalgebra k B} (V : ModuleCat (↥C)ᵐᵒᵖ) : ModuleCat Bᵐᵒᵖ

The coinduced right B-module.

def MultiplicativeBasisDeformations.SplitCoind.evalK {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] {C : Subalgebra k B} (V : ModuleCat (↥C)ᵐᵒᵖ) : ↑(coind V) →ₗ[k] B →ₗ[k] ↑V

Evaluation of Hom_C(B, V) on B, a k-linear injection into Hom_k(B, V).

theorem MultiplicativeBasisDeformations.SplitCoind.evalK_injective {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] {C : Subalgebra k B} (V : ModuleCat (↥C)ᵐᵒᵖ) : Function.Injective ⇑(evalK V)

theorem MultiplicativeBasisDeformations.SplitCoind.coind_finite {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] {C : Subalgebra k B} [FiniteDimensional k B] (V : ModuleCat (↥C)ᵐᵒᵖ) [Module.Finite k ↑V] : Module.Finite k ↑(coind V)

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.SplitCoind.Infl {k : Type u} [Field k] {B D : Type v} [Ring B] [Algebra k B] [Ring D] [Algebra k D] {C : Subalgebra k B} (q : ↥C →ₐ[k] D) (M : ModuleCat Dᵐᵒᵖ) : ModuleCat (↥C)ᵐᵒᵖ

Inflation of a right D-module to C.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.SplitCoind.Res {k : Type u} [Field k] {B : Type v} [Ring B] [Algebra k B] (C : Subalgebra k B) (N : ModuleCat Bᵐᵒᵖ) : ModuleCat (↥C)ᵐᵒᵖ

Restriction of a right B-module to C.

def MultiplicativeBasisDeformations.SplitCoind.gm {k : Type u} [Field k] {B D : Type v} [Ring B] [Algebra k B] [Ring D] [Algebra k D] {C : Subalgebra k B} {q : ↥C →ₐ[k] D} (π : B →ₗ[k] D) (hbimod : ∀ (c c' : ↥C) (b : B), π (↑c * b * ↑c') = q c * π b * q c') (M : ModuleCat Dᵐᵒᵖ) (m : ↑M) : Obj C (Infl q M)

ψ_m : b ↦ m π(b).

theorem MultiplicativeBasisDeformations.SplitCoind.gm_apply {k : Type u} [Field k] {B D : Type v} [Ring B] [Algebra k B] [Ring D] [Algebra k D] {C : Subalgebra k B} {q : ↥C →ₐ[k] D} (π : B →ₗ[k] D) (hbimod : ∀ (c c' : ↥C) (b : B), π (↑c * b * ↑c') = q c * π b * q c') (M : ModuleCat Dᵐᵒᵖ) (m : ↑M) (x : B) : (gm π hbimod M m) (toRC x) = MulOpposite.op (π x) • m

noncomputable def MultiplicativeBasisDeformations.SplitCoind.jmap {k : Type u} [Field k] {B D : Type v} [Ring B] [Algebra k B] [Ring D] [Algebra k D] {C : Subalgebra k B} {q : ↥C →ₐ[k] D} (π : B →ₗ[k] D) (hbimod : ∀ (c c' : ↥C) (b : B), π (↑c * b * ↑c') = q c * π b * q c') (M : ModuleCat Dᵐᵒᵖ) : Infl q M ⟶ Res C (coind (Infl q M))

The split mono M → Hom_C(B, M)|_C.

noncomputable def MultiplicativeBasisDeformations.SplitCoind.rmap {k : Type u} [Field k] {B D : Type v} [Ring B] [Algebra k B] [Ring D] [Algebra k D] {C : Subalgebra k B} {q : ↥C →ₐ[k] D} (M : ModuleCat Dᵐᵒᵖ) : Res C (coind (Infl q M)) ⟶ Infl q M

The retraction φ ↦ φ(1).

theorem MultiplicativeBasisDeformations.SplitCoind.jmap_rmap {k : Type u} [Field k] {B D : Type v} [Ring B] [Algebra k B] [Ring D] [Algebra k D] {C : Subalgebra k B} {q : ↥C →ₐ[k] D} (π : B →ₗ[k] D) (hbimod : ∀ (c c' : ↥C) (b : B), π (↑c * b * ↑c') = q c * π b * q c') (hπ : ∀ (c : ↥C), π ↑c = q c) (M : ModuleCat Dᵐᵒᵖ) : CategoryTheory.CategoryStruct.comp (jmap π hbimod M) (rmap M) = CategoryTheory.CategoryStruct.id (Infl q M)

theorem MultiplicativeBasisDeformations.finite_restrict {k : Type u} [Field k] {R S : Type v} [Ring R] [Ring S] [Algebra k R] [Algebra k S] (φ : R →+* S) (hφ : ∀ (c : k), φ ((algebraMap k R) c) = (algebraMap k S) c) (M : ModuleCat S) [Module.Finite k ↑M] : Module.Finite k ↑((ModuleCat.restrictScalars φ).obj M)

Restriction of scalars along a k-algebra map preserves finite dimension over k.

theorem MultiplicativeBasisDeformations.restrict_full {R S : Type v} [Ring R] [Ring S] (φ : R →+* S) (hφ : Function.Surjective ⇑φ) : (ModuleCat.restrictScalars φ).Full

Restriction of scalars along a surjective ring map is full.

theorem MultiplicativeBasisDeformations.not_isZero_of_local {𝒞 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒞] [CategoryTheory.Preadditive 𝒞] {X : 𝒞} [IsLocalRing (CategoryTheory.End X)] : ¬CategoryTheory.Limits.IsZero X

theorem MultiplicativeBasisDeformations.splitRepresentationTransfer_of {k : Type u} [Field k] {B D : Type v} [Ring B] [Algebra k B] [Ring D] [Algebra k D] {C : Subalgebra k B} {q : ↥C →ₐ[k] D} (π : B →ₗ[k] D) (hbimod : ∀ (c c' : ↥C) (b : B), π (↑c * b * ↑c') = q c * π b * q c') [FiniteDimensional k B] [FiniteDimensional k D] (hq : Function.Surjective ⇑q) (hπ : ∀ (c : ↥C), π ↑c = q c) (hB : IsRepresentationFinite k B) : IsRepresentationFinite k D

Lemma 4.6 (lem:split-representation-transfer).