Proposition 2.10(2): A₀ is representation-finite #
prop:projective-evaluation(2) (graded-category.tex): evaluation
add C → mod A₀ is an equivalence, so the indecomposable A₀-modules are the
evaluations of the finitely many objects of C.
Every finite-dimensional module is the evaluation of a family
(InjData.essSurj); an indecomposable one has local endomorphism ring and is a
retract of one summand (exchange), which is an evaluation R_x with local
endomorphism ring C(x, x) (full faithfulness), hence isomorphic to it.
Modules of Alg F₀ are the paper's right A₀-modules; they are transported to
right modules of (Alg F₀)ᵒᵖ along R ≅ Rᵒᵖᵒᵖ.
Left modules versus right modules of the opposite algebra #
noncomputable def
MultiplicativeBasisDeformations.toOpOp
{A : Type v}
[Ring A]
:
ModuleCat A ≌ RightModuleCat Aᵐᵒᵖ
Left A-modules as right Aᵒᵖ-modules.
Instances For
instance
MultiplicativeBasisDeformations.instAdditiveModuleCatRightModuleCatMulOppositeFunctorToOpOp
{A : Type v}
[Ring A]
:
toOpOp.functor.Additive
instance
MultiplicativeBasisDeformations.instAdditiveRightModuleCatMulOppositeModuleCatInverseToOpOp
{A : Type v}
[Ring A]
:
toOpOp.inverse.Additive
def
MultiplicativeBasisDeformations.toOpOpK
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
(M : ModuleCat A)
:
↑M →ₗ[k] ↑(toOpOp.functor.obj M)
The identity map is k-linear for the induced structures.
Instances For
def
MultiplicativeBasisDeformations.ofOpOpK
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
(N : RightModuleCat Aᵐᵒᵖ)
:
↑N →ₗ[k] ↑(toOpOp.inverse.obj N)
And back.
Instances For
theorem
MultiplicativeBasisDeformations.isRepresentationFinite_op_of_left
{k : Type u}
[Field k]
{A : Type v}
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
{n : ℕ}
(X : Fin n → ModuleCat A)
(hX : ∀ (i : Fin n), Module.Finite k ↑(X i) ∧ IsLocalRing (CategoryTheory.End (X i)))
(hcov : ∀ (M : ModuleCat A), Module.Finite k ↑M → CategoryTheory.Indecomposable M → ∃ (i : Fin n), Nonempty (M ≅ X i))
:
IsRepresentationFinite k Aᵐᵒᵖ
Representation-finiteness of Aᵒᵖ from a finite list of left
A-modules.
theorem
MultiplicativeBasisDeformations.CatAlg.LocalFamily.end_isLocalRing
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
(L : LocalFamily F)
(x : ι)
:
IsLocalRing (CategoryTheory.End (F x))
Endomorphism rings in a local family are local.
instance
MultiplicativeBasisDeformations.CatAlg.MeshData.instFiniteDimensionalAlgPVF0
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{L : LocalFamily F}
{D : MeshData F L}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
:
instance
MultiplicativeBasisDeformations.CatAlg.MeshData.instFiniteDimensionalRepPVF0
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{L : LocalFamily F}
{D : MeshData F L}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(x : ι)
:
def
MultiplicativeBasisDeformations.CatAlg.MeshData.evObj
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{L : LocalFamily F}
{D : MeshData F L}
(x : ι)
:
The evaluation R⁰_x of a label as a module.
Instances For
def
MultiplicativeBasisDeformations.CatAlg.MeshData.evObjK
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{L : LocalFamily F}
{D : MeshData F L}
(x : ι)
:
The identity of R⁰_x from the native k-structure.
Instances For
instance
MultiplicativeBasisDeformations.CatAlg.MeshData.evObj_finite
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{L : LocalFamily F}
{D : MeshData F L}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(x : ι)
:
Module.Finite k ↑(evObj x)
def
MultiplicativeBasisDeformations.CatAlg.MeshData.evHom
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{L : LocalFamily F}
{D : MeshData F L}
{x : ι}
(f : F x ⟶ F x)
:
The evaluation of an endomorphism.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.evHom_apply
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{L : LocalFamily F}
{D : MeshData F L}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
{x : ι}
(f : F x ⟶ F x)
(m : Rep D.F0 (F x))
:
def
MultiplicativeBasisDeformations.CatAlg.MeshData.evEndHom
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{L : LocalFamily F}
{D : MeshData F L}
(x : ι)
:
CategoryTheory.End (F x) →+* CategoryTheory.End (evObj x)
Endomorphisms of an evaluation are evaluations of endomorphisms.
Instances For
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.evEndHom_bijective
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{L : LocalFamily F}
{D : MeshData F L}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(x : ι)
:
Function.Bijective ⇑(evEndHom x)
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.evObj_isLocalRing
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{L : LocalFamily F}
{D : MeshData F L}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(x : ι)
:
IsLocalRing (CategoryTheory.End (evObj x))
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.exists_iso_evObj
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{L : LocalFamily F}
{D : MeshData F L}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(J : D.InjData)
(M : ModuleCat (Alg D.F0))
[Module.Finite k ↑M]
(hM : CategoryTheory.Indecomposable M)
:
∃ (x : ι), Nonempty (M ≅ evObj x)
Every finite-dimensional indecomposable A₀-module is the evaluation of a
label.
theorem
MultiplicativeBasisDeformations.CatAlg.MeshData.isRepresentationFinite_A0
{k : Type u}
[Field k]
{𝒞 : Type v}
[CategoryTheory.Category.{w, v} 𝒞]
[CategoryTheory.Preadditive 𝒞]
[CategoryTheory.Linear k 𝒞]
{ι : Type}
[Fintype ι]
[DecidableEq ι]
{F : ι → 𝒞}
{L : LocalFamily F}
{D : MeshData F L}
[hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)]
(J : D.InjData)
:
IsRepresentationFinite k (Alg D.F0)ᵐᵒᵖ
Proposition 2.10(2): A₀ is representation-finite.