Graded covering categories and Lemma 4.7

Definition 4.5 (def:graded-covering-category, scalar-normalization.tex): for an algebra graded by a group 𝒢, with chosen primitive idempotents of identity degree, the graded covering category has objects (x, g) and morphisms B(x, y)_{g⁻¹h} from (x, g) to (y, h).

We work with a family F : ι → C in a k-linear category whose Hom spaces are 𝒢-graded compatibly with composition (HomGrading); the algebra is B = (Alg F)ᵒᵖ. A finite full subcategory of the graded covering category, with objects s p = (x_p, g_p), has the category algebra cov s: the subalgebra of (Alg (F ∘ x))ᵒᵖ of the matrices with (p, q)-entry in degree g_p⁻¹ g_q.

Lemma 4.7 (lem:homogeneous-projection, lines 305–320): "Projection π : B' → H onto the indicated homogeneous components is an H-bimodule retraction. Indeed, for p ∈ H(i,j), q ∈ H(l,m) and b ∈ B'(j,l), cancellation of the degrees of p and q in the grading group gives π(pbq) = p π(b) q. Lemma 4.6 therefore applies with C = D = H." (isRepresentationFinite_cov).

structure MultiplicativeBasisDeformations.CatAlg.HomGrading {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} (F : ι → 𝒞) (G : Type) [Group G] [DecidableEq G] : Type w

A grading of the Hom spaces of a family by a group, compatible with composition, with identities in degree one.

• proj : G → (x y : ι) → (F x ⟶ F y) →ₗ[k] F x ⟶ F y
• proj_proj (g h : G) (x y : ι) (f : F x ⟶ F y) : (self.proj g x y) ((self.proj h x y) f) = if h = g then (self.proj h x y) f else 0
• sum (x y : ι) (f : F x ⟶ F y) : ∃ (s : Finset G), f = ∑ g ∈ s, (self.proj g x y) f
• proj_comp (g a b : G) (x y z : ι) (f : F x ⟶ F y) (f' : F y ⟶ F z) : (self.proj g x z) (CategoryTheory.CategoryStruct.comp ((self.proj a x y) f) ((self.proj b y z) f')) = if a * b = g then CategoryTheory.CategoryStruct.comp ((self.proj a x y) f) ((self.proj b y z) f') else 0
• proj_id (g : G) (x : ι) : (self.proj g x x) (CategoryTheory.CategoryStruct.id (F x)) = if 1 = g then CategoryTheory.CategoryStruct.id (F x) else 0

def MultiplicativeBasisDeformations.CatAlg.HomGrading.IsHom {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] (D : HomGrading F G) (g : G) {x y : ι} (f : F x ⟶ F y) : Prop

A homogeneous morphism of degree g.

theorem MultiplicativeBasisDeformations.CatAlg.HomGrading.isHom_proj {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] (D : HomGrading F G) (g : G) {x y : ι} (f : F x ⟶ F y) : D.IsHom g ((D.proj g x y) f)

theorem MultiplicativeBasisDeformations.CatAlg.HomGrading.proj_of_isHom {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] (D : HomGrading F G) {g h : G} {x y : ι} {f : F x ⟶ F y} (hf : D.IsHom h f) : (D.proj g x y) f = if h = g then f else 0

theorem MultiplicativeBasisDeformations.CatAlg.HomGrading.isHom_zero {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] (D : HomGrading F G) (g : G) {x y : ι} : D.IsHom g 0

theorem MultiplicativeBasisDeformations.CatAlg.HomGrading.isHom_add {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] (D : HomGrading F G) {g : G} {x y : ι} {f f' : F x ⟶ F y} (hf : D.IsHom g f) (hf' : D.IsHom g f') : D.IsHom g (f + f')

theorem MultiplicativeBasisDeformations.CatAlg.HomGrading.isHom_smul {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] (D : HomGrading F G) {g : G} {x y : ι} (c : k) {f : F x ⟶ F y} (hf : D.IsHom g f) : D.IsHom g (c • f)

theorem MultiplicativeBasisDeformations.CatAlg.HomGrading.isHom_sum {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] (D : HomGrading F G) {g : G} {x y : ι} {κ : Type u_1} (s : Finset κ) {f : κ → (F x ⟶ F y)} (hf : ∀ i ∈ s, D.IsHom g (f i)) : D.IsHom g (∑ i ∈ s, f i)

theorem MultiplicativeBasisDeformations.CatAlg.HomGrading.proj_comp_of_isHom {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] (D : HomGrading F G) {g a b : G} {x y z : ι} {f : F x ⟶ F y} {f' : F y ⟶ F z} (hf : D.IsHom a f) (hf' : D.IsHom b f') : (D.proj g x z) (CategoryTheory.CategoryStruct.comp f f') = if a * b = g then CategoryTheory.CategoryStruct.comp f f' else 0

theorem MultiplicativeBasisDeformations.CatAlg.HomGrading.isHom_comp {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] (D : HomGrading F G) {a b : G} {x y z : ι} {f : F x ⟶ F y} {f' : F y ⟶ F z} (hf : D.IsHom a f) (hf' : D.IsHom b f') : D.IsHom (a * b) (CategoryTheory.CategoryStruct.comp f f')

theorem MultiplicativeBasisDeformations.CatAlg.HomGrading.isHom_id {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] (D : HomGrading F G) (x : ι) : D.IsHom 1 (CategoryTheory.CategoryStruct.id (F x))

theorem MultiplicativeBasisDeformations.CatAlg.HomGrading.proj_sandwich {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] (D : HomGrading F G) {g a b : G} {x y z t : ι} {f : F x ⟶ F y} {f' : F z ⟶ F t} (hf : D.IsHom a f) (hf' : D.IsHom b f') (m : F y ⟶ F z) : (D.proj g x t) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp m f')) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp ((D.proj (a⁻¹ * g * b⁻¹) y z) m) f')

Cancellation of degrees: π(p b q) = p π(b) q for homogeneous p, q.

The covering subalgebras

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.CatAlg.lab {ι G κ : Type} (s : κ → ι × G) : κ → ι

The labels of a finite set of objects of the graded covering category.

def MultiplicativeBasisDeformations.CatAlg.cov {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] (D : HomGrading F G) {κ : Type} [Fintype κ] [DecidableEq κ] (s : κ → ι × G) : Subalgebra k (Alg (F ∘ lab s))ᵐᵒᵖ

The category algebra of a finite full subcategory of the graded covering category: entries (p, q) of degree g_p⁻¹ g_q.

def MultiplicativeBasisDeformations.CatAlg.covProj {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] (D : HomGrading F G) {κ : Type} [Fintype κ] [DecidableEq κ] (s : κ → ι × G) : (Alg (F ∘ lab s))ᵐᵒᵖ →ₗ[k] ↥(cov D s)

The projection onto the homogeneous entries.

theorem MultiplicativeBasisDeformations.CatAlg.covProj_of_mem {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] (D : HomGrading F G) {κ : Type} [Fintype κ] [DecidableEq κ] (s : κ → ι × G) (c : ↥(cov D s)) : (covProj D s) ↑c = c

theorem MultiplicativeBasisDeformations.CatAlg.covProj_bimod {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] (D : HomGrading F G) {κ : Type} [Fintype κ] [DecidableEq κ] (s : κ → ι × G) (c c' : ↥(cov D s)) (b : (Alg (F ∘ lab s))ᵐᵒᵖ) : (covProj D s) (↑c * b * ↑c') = c * (covProj D s) b * c'

theorem MultiplicativeBasisDeformations.CatAlg.isRepresentationFinite_cov {k : Type u} [Field k] {𝒞 : Type v} [CategoryTheory.Category.{w, v} 𝒞] [CategoryTheory.Preadditive 𝒞] [CategoryTheory.Linear k 𝒞] {ι : Type} [Fintype ι] [DecidableEq ι] {F : ι → 𝒞} {G : Type} [Group G] [DecidableEq G] (D : HomGrading F G) {κ : Type} [Fintype κ] [DecidableEq κ] (s : κ → ι × G) [∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] (hF : IsRepresentationFinite k (Alg F)ᵐᵒᵖ) : IsRepresentationFinite k ↥(cov D s)

Lemma 4.7 (lem:homogeneous-projection): every finite full subcategory of the graded covering category of a representation-finite graded algebra is representation-finite.