Multiplicative bases

MultiplicativeBasisDeformations.Foundations.RepresentationTransfer

Lemma 8.9: representation transfer along a functor with a bimodule retraction #

local-ray-geometry.tex (lem:representation-transfer): "Let F : S → B be a functor between finite categories. Let B_F be the category with the objects of S and morphisms B_F(x, y) = B(Fx, Fy), so that F gives a functor S → B_F, which we assume injective on morphisms. Suppose that there is an S-bimodule map π : B_F → S retracting this inclusion. If B is representation-finite, then so is S."

Finite k-linear categories are given by finite families of objects (CatAlg.Alg): S by FS : ι → 𝒮 and B by FB : κ → ℬ; the functor is a k-linear functor G : 𝒮 ⥤ ℬ with G (FS i) = FB (σ i). B_F is the family G ∘ FS = FB ∘ σ, representation-finite by repeated labels (isRepresentationFinite_comp: an idempotent corner of a Morita equivalent algebra); G embeds S into B_F (funcAlgHom), and Lemma 4.6 (splitRepresentationTransfer_of) applies to the retraction (representationTransfer).

source
def MultiplicativeBasisDeformations.CatAlg.funcAlg {𝒮 : Type v} [CategoryTheory.Category.{w, v} 𝒮] {ℬ : Type v'} [CategoryTheory.Category.{w, v'} ℬ] {ι : Type} (FS : ι → 𝒮) (G : CategoryTheory.Functor 𝒮 ℬ) (a : Alg FS) :
Alg fun (i : ι) => G.obj (FS i)

G on category algebras: (a_{xy}) ↦ (G a_{xy}).

Instances For
    source
    theorem MultiplicativeBasisDeformations.CatAlg.funcAlg_apply {𝒮 : Type v} [CategoryTheory.Category.{w, v} 𝒮] [CategoryTheory.Preadditive 𝒮] {ℬ : Type v'} [CategoryTheory.Category.{w, v'} ℬ] [CategoryTheory.Preadditive ℬ] {ι : Type} [Fintype ι] [DecidableEq ι] (FS : ι → 𝒮) (G : CategoryTheory.Functor 𝒮 ℬ) [G.Additive] (a : Alg FS) (x y : ι) :
    funcAlg FS G a x y = G.map (a x y)
    source
    theorem MultiplicativeBasisDeformations.CatAlg.funcMap_idTo {𝒮 : Type v} [CategoryTheory.Category.{w, v} 𝒮] [CategoryTheory.Preadditive 𝒮] {ℬ : Type v'} [CategoryTheory.Category.{w, v'} ℬ] [CategoryTheory.Preadditive ℬ] {ι : Type} [Fintype ι] [DecidableEq ι] (FS : ι → 𝒮) (G : CategoryTheory.Functor 𝒮 ℬ) [G.Additive] (x y : ι) :
    G.map (idTo x y) = idTo x y
    source
    def MultiplicativeBasisDeformations.CatAlg.funcAlgHom {k : Type u} [Field k] {𝒮 : Type v} [CategoryTheory.Category.{w, v} 𝒮] [CategoryTheory.Preadditive 𝒮] [CategoryTheory.Linear k 𝒮] {ℬ : Type v'} [CategoryTheory.Category.{w, v'} ℬ] [CategoryTheory.Preadditive ℬ] [CategoryTheory.Linear k ℬ] {ι : Type} [Fintype ι] [DecidableEq ι] (FS : ι → 𝒮) (G : CategoryTheory.Functor 𝒮 ℬ) [G.Additive] [CategoryTheory.Functor.Linear k G] :
    Alg FS →ₐ[k] Alg fun (i : ι) => G.obj (FS i)

    G as an algebra map kS → kB_F.

    Instances For
      source
      theorem MultiplicativeBasisDeformations.CatAlg.funcAlgHom_injective {k : Type u} [Field k] {𝒮 : Type v} [CategoryTheory.Category.{w, v} 𝒮] [CategoryTheory.Preadditive 𝒮] [CategoryTheory.Linear k 𝒮] {ℬ : Type v'} [CategoryTheory.Category.{w, v'} ℬ] [CategoryTheory.Preadditive ℬ] [CategoryTheory.Linear k ℬ] {ι : Type} [Fintype ι] [DecidableEq ι] (FS : ι → 𝒮) (G : CategoryTheory.Functor 𝒮 ℬ) [G.Additive] [CategoryTheory.Functor.Linear k G] (hinj : ∀ (X Y : 𝒮), Function.Injective G.map) :
      Function.Injective ⇑(funcAlgHom FS G)
      source
      def MultiplicativeBasisDeformations.CatAlg.funcRet {k : Type u} [Field k] {𝒮 : Type v} [CategoryTheory.Category.{w, v} 𝒮] [CategoryTheory.Preadditive 𝒮] [CategoryTheory.Linear k 𝒮] {ℬ : Type v'} [CategoryTheory.Category.{w, v'} ℬ] [CategoryTheory.Preadditive ℬ] [CategoryTheory.Linear k ℬ] {ι : Type} [Fintype ι] [DecidableEq ι] (FS : ι → 𝒮) (G : CategoryTheory.Functor 𝒮 ℬ) (π : (x y : ι) → (G.obj (FS x) ⟶ G.obj (FS y)) →ₗ[k] FS x ⟶ FS y) :
      (Alg fun (i : ι) => G.obj (FS i)) →ₗ[k] Alg FS

      The retraction on category algebras.

      Instances For
        source
        theorem MultiplicativeBasisDeformations.CatAlg.funcRet_mul_left {k : Type u} [Field k] {𝒮 : Type v} [CategoryTheory.Category.{w, v} 𝒮] [CategoryTheory.Preadditive 𝒮] [CategoryTheory.Linear k 𝒮] {ℬ : Type v'} [CategoryTheory.Category.{w, v'} ℬ] [CategoryTheory.Preadditive ℬ] [CategoryTheory.Linear k ℬ] {ι : Type} [Fintype ι] [DecidableEq ι] (FS : ι → 𝒮) (G : CategoryTheory.Functor 𝒮 ℬ) [G.Additive] [CategoryTheory.Functor.Linear k G] (π : (x y : ι) → (G.obj (FS x) ⟶ G.obj (FS y)) →ₗ[k] FS x ⟶ FS y) (hl : ∀ (x y z : ι) (f : FS x ⟶ FS y) (b : G.obj (FS y) ⟶ G.obj (FS z)), (π x z) (CategoryTheory.CategoryStruct.comp (G.map f) b) = CategoryTheory.CategoryStruct.comp f ((π y z) b)) (a : Alg FS) (b : Alg fun (i : ι) => G.obj (FS i)) :
        (funcRet FS G π) ((funcAlgHom FS G) a * b) = a * (funcRet FS G π) b
        source
        theorem MultiplicativeBasisDeformations.CatAlg.funcRet_mul_right {k : Type u} [Field k] {𝒮 : Type v} [CategoryTheory.Category.{w, v} 𝒮] [CategoryTheory.Preadditive 𝒮] [CategoryTheory.Linear k 𝒮] {ℬ : Type v'} [CategoryTheory.Category.{w, v'} ℬ] [CategoryTheory.Preadditive ℬ] [CategoryTheory.Linear k ℬ] {ι : Type} [Fintype ι] [DecidableEq ι] (FS : ι → 𝒮) (G : CategoryTheory.Functor 𝒮 ℬ) [G.Additive] [CategoryTheory.Functor.Linear k G] (π : (x y : ι) → (G.obj (FS x) ⟶ G.obj (FS y)) →ₗ[k] FS x ⟶ FS y) (hr : ∀ (x y z : ι) (b : G.obj (FS x) ⟶ G.obj (FS y)) (f : FS y ⟶ FS z), (π x z) (CategoryTheory.CategoryStruct.comp b (G.map f)) = CategoryTheory.CategoryStruct.comp ((π x y) b) f) (b : Alg fun (i : ι) => G.obj (FS i)) (a : Alg FS) :
        (funcRet FS G π) (b * (funcAlgHom FS G) a) = (funcRet FS G π) b * a
        source
        theorem MultiplicativeBasisDeformations.CatAlg.representationTransfer {k : Type u} [Field k] {𝒮 : Type v} [CategoryTheory.Category.{w, v} 𝒮] [CategoryTheory.Preadditive 𝒮] [CategoryTheory.Linear k 𝒮] {ℬ : Type v'} [CategoryTheory.Category.{w, v'} ℬ] [CategoryTheory.Preadditive ℬ] [CategoryTheory.Linear k ℬ] {ι κ : Type} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (FS : ι → 𝒮) (G : CategoryTheory.Functor 𝒮 ℬ) [G.Additive] [CategoryTheory.Functor.Linear k G] (π : (x y : ι) → (G.obj (FS x) ⟶ G.obj (FS y)) →ₗ[k] FS x ⟶ FS y) (FB : κ → ℬ) [∀ (x y : ι), FiniteDimensional k (FS x ⟶ FS y)] [∀ (x y : κ), FiniteDimensional k (FB x ⟶ FB y)] (σ : ι → κ) (hσ : ∀ (i : ι), G.obj (FS i) = FB (σ i)) (hinj : ∀ (X Y : 𝒮), Function.Injective G.map) (hret : ∀ (x y : ι) (f : FS x ⟶ FS y), (π x y) (G.map f) = f) (hl : ∀ (x y z : ι) (f : FS x ⟶ FS y) (b : G.obj (FS y) ⟶ G.obj (FS z)), (π x z) (CategoryTheory.CategoryStruct.comp (G.map f) b) = CategoryTheory.CategoryStruct.comp f ((π y z) b)) (hr : ∀ (x y z : ι) (b : G.obj (FS x) ⟶ G.obj (FS y)) (f : FS y ⟶ FS z), (π x z) (CategoryTheory.CategoryStruct.comp b (G.map f)) = CategoryTheory.CategoryStruct.comp ((π x y) b) f) (hB : IsRepresentationFinite k (Alg FB)ᵐᵒᵖ) :
        IsRepresentationFinite k (Alg FS)ᵐᵒᵖ

        Lemma 8.9 (lem:representation-transfer): for a k-linear functor G : 𝒮 ⥤ ℬ carrying the objects FS i of the finite category S to objects FB (σ i) of the finite category B, injective on morphisms, with an S-bimodule retraction π : B_F → S: if B is representation-finite, so is S.