Lemma 4.10: the support poset of a thin module #
lem:thin-module-incidence (scalar-normalization.tex): "Let T be a
finite directed category, and let M be a covariant or contravariant k-linear
functor from T to vector spaces with dim M(y) ≤ 1 for every object y. Let
R be the category obtained from T by passing to the quotient by the
annihilator of M and discarding the objects y with M(y) = 0. Then R is
the incidence category of a finite poset. If T is representation-finite,
then so is R."
For M = T(s, -) (a source, covariant) and M = T(-, t) (a sink,
contravariant) in the graded covering category, the passage to R is the
surjective algebra map from the category algebra of the support (Lemma 4.7) to
the incidence algebra, sending a morphism to its action on M
(qSrc, qSnk). Hence the incidence algebra is representation-finite
(Lemma 4.6 applied to the quotient).
theorem
MultiplicativeBasisDeformations.incidence_finiteDimensional
{k : Type u}
[Field k]
{P : Type u_1}
[PartialOrder P]
[Fintype P]
[DecidableEq P]
[LocallyFiniteOrder P]
:
FiniteDimensional k (IncidenceAlgebra k P)
The incidence algebra of a finite poset is finite-dimensional.
Sources #
@[reducible, inline]
abbrev
MultiplicativeBasisDeformations.CatAlg.labSrc
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(s : CovObj D)
(P : Finset (CovObj D))
(fv : (y : CovObj D) → s ⟶ y)
:
Thin.SupP s P fv → ι × G
The objects of the support, as objects of the graded covering category.
Instances For
def
MultiplicativeBasisDeformations.CatAlg.entry
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(s : CovObj D)
(P : Finset (CovObj D))
(fv : (y : CovObj D) → s ⟶ y)
(a : ↥(cov D (labSrc s P fv)))
(y z : Thin.SupP s P fv)
:
↑y ⟶ ↑z
An entry of an element of the covering algebra of the support, as a morphism of the graded covering category.
Instances For
noncomputable def
MultiplicativeBasisDeformations.CatAlg.qSrcFun
{k : Type u}
[Field k]
[Infinite k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(H : HeightData D)
[∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(hF : IsRepresentationFinite k (Alg F)ᵐᵒᵖ)
(s : CovObj D)
(P : Finset (CovObj D))
(fv : (y : CovObj D) → s ⟶ y)
(a : ↥(cov D (labSrc s P fv)))
:
The action on M = T(s, -).
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.entry_add
{k : Type u}
[Field k]
[Infinite k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, 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)]
(s : CovObj D)
(P : Finset (CovObj D))
(fv : (y : CovObj D) → s ⟶ y)
(a b : ↥(cov D (labSrc s P fv)))
(y z : Thin.SupP s P fv)
:
theorem
MultiplicativeBasisDeformations.CatAlg.entry_smul
{k : Type u}
[Field k]
[Infinite k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, 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)]
(s : CovObj D)
(P : Finset (CovObj D))
(fv : (y : CovObj D) → s ⟶ y)
(c : k)
(a : ↥(cov D (labSrc s P fv)))
(y z : Thin.SupP s P fv)
:
theorem
MultiplicativeBasisDeformations.CatAlg.entry_mul
{k : Type u}
[Field k]
[Infinite k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, 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)]
(s : CovObj D)
(P : Finset (CovObj D))
(fv : (y : CovObj D) → s ⟶ y)
(a b : ↥(cov D (labSrc s P fv)))
(y w : Thin.SupP s P fv)
:
theorem
MultiplicativeBasisDeformations.CatAlg.entry_one
{k : Type u}
[Field k]
[Infinite k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, 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)]
(s : CovObj D)
(P : Finset (CovObj D))
(fv : (y : CovObj D) → s ⟶ y)
(y z : Thin.SupP s P fv)
:
entry s P fv 1 y z = if h : y = z then CategoryTheory.eqToHom ⋯ else 0
theorem
MultiplicativeBasisDeformations.CatAlg.coef_entry_eq_zero
{k : Type u}
[Field k]
[Infinite k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, 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)]
{s : CovObj D}
{P : Finset (CovObj D)}
{fv : (y : CovObj D) → s ⟶ y}
{y z : Thin.SupP s P fv}
(h : ¬Thin.supLe y z)
(a : ↥(cov D (labSrc s P fv)))
:
CategoryTheory.CategoryStruct.comp (fv ↑y) (entry s P fv a y z) = 0
theorem
MultiplicativeBasisDeformations.CatAlg.supRepFinite_src
{k : Type u}
[Field k]
[Infinite k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(H : HeightData D)
[∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(hF : IsRepresentationFinite k (Alg F)ᵐᵒᵖ)
(s : CovObj D)
(P : Finset (CovObj D))
(fv : (y : CovObj D) → s ⟶ y)
(hfv : ∀ y ∈ P, fv y ≠ 0)
:
Thin.SupRepFinite ⋯ hfv
Lemma 4.10 for a source: the incidence algebra of the dual support poset
is representation-finite, through the algebra map given by the action on
T(s, -).
Sinks #
@[reducible, inline]
abbrev
MultiplicativeBasisDeformations.CatAlg.labSnk
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(t : CovObj D)
(P : Finset (CovObj D)ᵒᵖ)
(fv : (Y : (CovObj D)ᵒᵖ) → Opposite.op t ⟶ Y)
:
Thin.SupP (Opposite.op t) P fv → ι × G
The objects of the support of T(-, t).
Instances For
def
MultiplicativeBasisDeformations.CatAlg.entryK
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(t : CovObj D)
(P : Finset (CovObj D)ᵒᵖ)
(fv : (Y : (CovObj D)ᵒᵖ) → Opposite.op t ⟶ Y)
(a : ↥(cov D (labSnk t P fv)))
(Y Z : Thin.SupP (Opposite.op t) P fv)
:
Opposite.unop ↑Y ⟶ Opposite.unop ↑Z
An entry of an element of the covering algebra.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.entryK_add
{k : Type u}
[Field k]
[Infinite k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, 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)]
(t : CovObj D)
(P : Finset (CovObj D)ᵒᵖ)
(fv : (Y : (CovObj D)ᵒᵖ) → Opposite.op t ⟶ Y)
(a b : ↥(cov D (labSnk t P fv)))
(Y Z : Thin.SupP (Opposite.op t) P fv)
:
theorem
MultiplicativeBasisDeformations.CatAlg.entryK_smul
{k : Type u}
[Field k]
[Infinite k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, 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)]
(t : CovObj D)
(P : Finset (CovObj D)ᵒᵖ)
(fv : (Y : (CovObj D)ᵒᵖ) → Opposite.op t ⟶ Y)
(c : k)
(a : ↥(cov D (labSnk t P fv)))
(Y Z : Thin.SupP (Opposite.op t) P fv)
:
theorem
MultiplicativeBasisDeformations.CatAlg.entryK_mul
{k : Type u}
[Field k]
[Infinite k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, 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)]
(t : CovObj D)
(P : Finset (CovObj D)ᵒᵖ)
(fv : (Y : (CovObj D)ᵒᵖ) → Opposite.op t ⟶ Y)
(a b : ↥(cov D (labSnk t P fv)))
(Y W : Thin.SupP (Opposite.op t) P fv)
:
theorem
MultiplicativeBasisDeformations.CatAlg.entryK_one
{k : Type u}
[Field k]
[Infinite k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, 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)]
(t : CovObj D)
(P : Finset (CovObj D)ᵒᵖ)
(fv : (Y : (CovObj D)ᵒᵖ) → Opposite.op t ⟶ Y)
(Y Z : Thin.SupP (Opposite.op t) P fv)
:
entryK t P fv 1 Y Z = if h : Y = Z then CategoryTheory.eqToHom ⋯ else 0
def
MultiplicativeBasisDeformations.CatAlg.φK
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(t : CovObj D)
(P : Finset (CovObj D)ᵒᵖ)
(fv : (Y : (CovObj D)ᵒᵖ) → Opposite.op t ⟶ Y)
(Y : Thin.SupP (Opposite.op t) P fv)
:
Opposite.unop ↑Y ⟶ t
The map φ_Y : Y → t.
Instances For
noncomputable def
MultiplicativeBasisDeformations.CatAlg.qSnkFun
{k : Type u}
[Field k]
[Infinite k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(H : HeightData D)
[∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(hF : IsRepresentationFinite k (Alg F)ᵐᵒᵖ)
(t : CovObj D)
(P : Finset (CovObj D)ᵒᵖ)
(fv : (Y : (CovObj D)ᵒᵖ) → Opposite.op t ⟶ Y)
(a : ↥(cov D (labSnk t P fv)))
:
The action on M = T(-, t).
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.φK_ne
{k : Type u}
[Field k]
[Infinite k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, 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)]
(t : CovObj D)
(P : Finset (CovObj D)ᵒᵖ)
(fv : (Y : (CovObj D)ᵒᵖ) → Opposite.op t ⟶ Y)
(hfv : ∀ Y ∈ P, fv Y ≠ 0)
(Y : Thin.SupP (Opposite.op t) P fv)
:
φK t P fv Y ≠ 0
theorem
MultiplicativeBasisDeformations.CatAlg.le_of_comp_ne
{k : Type u}
[Field k]
[Infinite k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, 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)]
{t : CovObj D}
{P : Finset (CovObj D)ᵒᵖ}
{fv : (Y : (CovObj D)ᵒᵖ) → Opposite.op t ⟶ Y}
{Y Z : Thin.SupP (Opposite.op t) P fv}
(h : Opposite.unop ↑Z ⟶ Opposite.unop ↑Y)
(hne : CategoryTheory.CategoryStruct.comp h (φK t P fv Y) ≠ 0)
:
Thin.supLe Y Z
theorem
MultiplicativeBasisDeformations.CatAlg.comp_ne_of_le
{k : Type u}
[Field k]
[Infinite k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, 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)]
{t : CovObj D}
{P : Finset (CovObj D)ᵒᵖ}
{fv : (Y : (CovObj D)ᵒᵖ) → Opposite.op t ⟶ Y}
{Y Z : Thin.SupP (Opposite.op t) P fv}
(g : ↑Y ⟶ ↑Z)
(hg : CategoryTheory.CategoryStruct.comp (fv ↑Y) g ≠ 0)
:
CategoryTheory.CategoryStruct.comp g.unop (φK t P fv Y) ≠ 0
theorem
MultiplicativeBasisDeformations.CatAlg.supRepFinite_snk
{k : Type u}
[Field k]
[Infinite k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(H : HeightData D)
[∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(hF : IsRepresentationFinite k (Alg F)ᵐᵒᵖ)
(t : CovObj D)
(P : Finset (CovObj D)ᵒᵖ)
(fv : (Y : (CovObj D)ᵒᵖ) → Opposite.op t ⟶ Y)
(hfv : ∀ Y ∈ P, fv Y ≠ 0)
:
Thin.SupRepFinite ⋯ hfv
Lemma 4.10 for a sink: the incidence algebra of the support poset of
T(-, t) (as a source of the opposite category) is representation-finite.
theorem
MultiplicativeBasisDeformations.CatAlg.cov_exists_multBasis
{k : Type u}
[Field k]
[Infinite k]
{𝒞 : Type v}
[CategoryTheory.Category.{u, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{G : Type}
[Group G]
[DecidableEq G]
{D : HomGrading F G}
(H : HeightData D)
[∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(hF : IsRepresentationFinite k (Alg F)ᵐᵒᵖ)
[Countable G]
:
∃ (β : (o o' : CovObj D) → o ⟶ o'), Thin.MultBasis Set.univ β
Lemma 4.12 for the graded covering category: it has a multiplicative basis.