Thinness of the graded covering category #
Lemma 4.8, first part (lem:lifted-projective-evaluation,
scalar-normalization.tex): "Height gives End_L(x) = k. By
Lemma 4.7, every full subcategory on two objects is representation-finite. It
is directed. Every subspace of its nonidentity morphism space is an ideal. By
Lemma 3.1(1), there are only finitely many such ideals. A space of dimension at
least two would have infinitely many lines, so that morphism space has
dimension at most one."
Height is a homomorphism hgt : G → ℤ such that nonzero homogeneous morphisms
have nonnegative height, and those of height zero are scalar multiples of
identities in degree one (HeightData).
theorem
MultiplicativeBasisDeformations.finrank_le_one_of_finite_submodules
{k : Type u}
[Field k]
[Infinite k]
{V : Type v}
[AddCommGroup V]
[Module k V]
(P : Submodule k V)
(hfin : {W : Submodule k V | W ≤ P}.Finite)
:
Module.finrank k ↥P ≤ 1
Over an infinite field, a finite-dimensional space with finitely many subspaces has dimension at most one.
def
MultiplicativeBasisDeformations.CatAlg.HomGrading.part
{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 : ι)
:
Submodule k (F x ⟶ F y)
The degree-g part of C(F x, F y).
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.HomGrading.mem_part_iff
{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}
:
structure
MultiplicativeBasisDeformations.CatAlg.HeightData
{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)
:
Height data for a grading.
- hgt : G → ℤ
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.HeightData.hgt_one
{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)
:
H.hgt 1 = 0
theorem
MultiplicativeBasisDeformations.CatAlg.HeightData.hgt_inv
{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)
(g : G)
:
theorem
MultiplicativeBasisDeformations.CatAlg.HeightData.scalar_one
{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)
{x : ι}
{f : F x ⟶ F x}
(hf : D.IsHom 1 f)
:
∃ (c : k), f = c • CategoryTheory.CategoryStruct.id (F x)
Endomorphisms of degree one are scalars.
theorem
MultiplicativeBasisDeformations.CatAlg.HeightData.back_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}
(H : HeightData D)
{g : G}
{x y : ι}
(hxy : ¬(x = y ∧ g = 1))
{f : F x ⟶ F y}
(hf : D.IsHom g f)
(hf0 : f ≠ 0)
{f' : F y ⟶ F x}
(hf' : D.IsHom g⁻¹ f')
:
f' = 0
Directedness: no nonzero morphisms back.
The two-object subcategory #
def
MultiplicativeBasisDeformations.CatAlg.two
{ι G : Type}
[Group G]
(x y : ι)
(g : G)
:
Bool → ι × G
The objects (x, 1) and (y, g).
Instances For
def
MultiplicativeBasisDeformations.CatAlg.single01
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
{ι : Type}
{F : ι → 𝒞}
{G : Type}
[Group G]
{x y : ι}
{g : G}
(w : F x ⟶ F y)
:
The element with the single entry w from (x, 1) to (y, g).
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.single01_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}
{x y : ι}
{g : G}
{w : F x ⟶ F y}
(hw : D.IsHom g w)
:
def
MultiplicativeBasisDeformations.CatAlg.idealOf
{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 : ι}
{g : G}
(hback : ∀ (a : ↥(cov D (two x y g))), MulOpposite.unop (↑a) true false = 0)
(hdiag0 :
∀ (a : ↥(cov D (two x y g))),
∃ (c : k), MulOpposite.unop (↑a) false false = c • CategoryTheory.CategoryStruct.id ((F ∘ lab (two x y g)) false))
(hdiag1 :
∀ (a : ↥(cov D (two x y g))),
∃ (c : k), MulOpposite.unop (↑a) true true = c • CategoryTheory.CategoryStruct.id ((F ∘ lab (two x y g)) true))
(W : Submodule k (F x ⟶ F y))
:
The ideal of a subspace W of the degree-g part.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.finrank_part_le_one
{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)ᵐᵒᵖ)
(g : G)
(x y : ι)
:
Module.finrank k ↥(D.part g x y) ≤ 1
Thinness (Lemma 4.8, first part): every graded piece has dimension at most one.