The graded covering category as a thin category

Definition 4.5 (def:graded-covering-category): objects (x, g), morphisms B(x, y)_{g⁻¹h} from (x, g) to (y, h). For a graded family with height data (HomGrading, HeightData) and a representation-finite algebra this is a thin directed k-linear category with a height and finitely many outgoing lines at each object (isThin, hgt_lt, succ_finite).

def MultiplicativeBasisDeformations.CatAlg.CovObj {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) : Type

The objects of the graded covering category.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.CatAlg.CovHom {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} (o o' : CovObj D) : Submodule k (F o.1 ⟶ F o'.1)

The morphism space B(x, y)_{g⁻¹h}.

theorem MultiplicativeBasisDeformations.CatAlg.covHom_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} {o o' o'' : CovObj D} {f : F o.1 ⟶ F o'.1} {g : F o'.1 ⟶ F o''.1} (hf : f ∈ CovHom o o') (hg : g ∈ CovHom o' o'') : CategoryTheory.CategoryStruct.comp f g ∈ CovHom o o''

theorem MultiplicativeBasisDeformations.CatAlg.covHom_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} (o : CovObj D) : CategoryTheory.CategoryStruct.id (F o.1) ∈ CovHom o o

@[instance_reducible]

instance MultiplicativeBasisDeformations.CatAlg.instCategoryCovObj {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} : CategoryTheory.Category.{w, 0} (CovObj D)

@[simp]

theorem MultiplicativeBasisDeformations.CatAlg.cov_comp_val {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} {o o' o'' : CovObj D} (f : o ⟶ o') (g : o' ⟶ o'') : ↑(CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ↑f ↑g

@[simp]

theorem MultiplicativeBasisDeformations.CatAlg.cov_id_val {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} (o : CovObj D) : ↑(CategoryTheory.CategoryStruct.id o) = CategoryTheory.CategoryStruct.id (F o.1)

@[instance_reducible]

instance MultiplicativeBasisDeformations.CatAlg.instPreadditiveCovObj {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} : CategoryTheory.Preadditive (CovObj D)

@[instance_reducible]

instance MultiplicativeBasisDeformations.CatAlg.instLinearCovObj {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} : CategoryTheory.Linear k (CovObj D)

@[simp]

theorem MultiplicativeBasisDeformations.CatAlg.cov_zero_val {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} {o o' : CovObj D} : ↑0 = 0

@[simp]

theorem MultiplicativeBasisDeformations.CatAlg.cov_smul_val {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} {o o' : CovObj D} (c : k) (f : o ⟶ o') : ↑(c • f) = c • ↑f

theorem MultiplicativeBasisDeformations.CatAlg.cov_ne_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} {o o' : CovObj D} {f : o ⟶ o'} : f ≠ 0 ↔ ↑f ≠ 0

theorem MultiplicativeBasisDeformations.CatAlg.isThin {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} (H : HeightData D) [Infinite k] [∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] (hF : IsRepresentationFinite k (Alg F)ᵐᵒᵖ) : Thin.IsThin k (CovObj D)

The graded covering category is thin and directed (Lemma 4.8, first part, with the height).

def MultiplicativeBasisDeformations.CatAlg.hgtC {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} (H : HeightData D) (o : CovObj D) : ℤ

Height of an object.

theorem MultiplicativeBasisDeformations.CatAlg.hgt_lt {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} (H : HeightData D) {o o' : CovObj D} (h : Thin.Rl o o') : hgtC H o < hgtC H o'

theorem MultiplicativeBasisDeformations.CatAlg.finite_degrees {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 y : ι), FiniteDimensional k (F x ⟶ F y)] (x y : ι) : {h : G | D.part h x y ≠ ⊥}.Finite

Only finitely many degrees occur between two labels.

theorem MultiplicativeBasisDeformations.CatAlg.succ_finite {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 y : ι), FiniteDimensional k (F x ⟶ F y)] (o : CovObj D) : {o' : CovObj D | Thin.Rl o o'}.Finite

Finitely many outgoing lines.