Injective labels and essential surjectivity (Proposition 2.10)

graded-category.tex: "Write S_x = P_x/rad P_x … Since dim C(P_y, S_x) = dim Hom_A(P_y, S_x) = δ_{xy}, its evaluation is the simple A₀-module S_x⁰. For the original injective I_x = D_k(Ae_x), put N_x = ev(R_{I_x}). … full faithfulness gives dim Hom_{A₀}(S_y⁰, N_x) = dim C(S_y, I_x) = δ_{xy}. Thus soc N_x = S_x⁰. Also dim N_x e_y = dim C(P_y, I_x) = … = dim e_y A₀ e_x. Extend the inclusion of soc N_x in D_k(A₀ e_x) to a map N_x → D_k(A₀ e_x). Its kernel is zero, since every nonzero submodule meets the socle. Equality of dimensions then makes it an isomorphism."

The labels S_x, I_x and the three dimension identities are the inputs (InjData); they come from mod A through the graded Hom dimensions.

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.extA_injective {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) : Function.Injective D.extA

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.extA_list_prod {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) (l : List (Alg D.F0)) (hl : l ≠ []) : D.extA l.prod = (List.map D.extA l).prod

def MultiplicativeBasisDeformations.CatAlg.MeshData.L0 {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) : LocalFamily D.F0

The local structure restricted to the projective labels.

structure MultiplicativeBasisDeformations.CatAlg.MeshData.InjData {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) : Type

The simple and injective labels at the projective labels, with the Hom dimensions of graded-category.tex.

• S : D.PV → ι
• I : D.PV → ι
• dimS (p q : D.PV) : Module.finrank k (F ↑q ⟶ F (self.S p)) = if q = p then 1 else 0
• dimSI (p q : D.PV) : Module.finrank k (F (self.S q) ⟶ F (self.I p)) = if q = p then 1 else 0
• dimI (p q : D.PV) : Module.finrank k (F ↑q ⟶ F (self.I p)) = Module.finrank k (F ↑p ⟶ F ↑q)

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.CatAlg.MeshData.InjData.S0 {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} (J : D.InjData) (p : D.PV) : Type w

S_p⁰ = ev(S_p).

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.CatAlg.MeshData.InjData.N0 {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} (J : D.InjData) (p : D.PV) : Type w

N_p = ev(I_p).

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.InjData.S0_conc {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) (p : D.PV) (m : J.S0 p) (q : D.PV) (hq : q ≠ p) : m q = 0

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.InjData.idem_smul_S0 {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) (p : D.PV) (m : J.S0 p) : idem p • m = m

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.InjData.finrank_S0 {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) (p : D.PV) : Module.finrank k (J.S0 p) = 1

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.InjData.eq_smul_of_S0 {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) (p : D.PV) {s₀ : J.S0 p} (hs₀ : s₀ ≠ 0) (m : J.S0 p) : ∃ (c : k), m = c • s₀

instance MultiplicativeBasisDeformations.CatAlg.MeshData.InjData.instIsSimpleModuleAlgPVF0S0 {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) (p : D.PV) : IsSimpleModule (Alg D.F0) (J.S0 p)

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.CatAlg.MeshData.uZ {ι : Type} (x : ι) : Unit → ι

One-object families.

def MultiplicativeBasisDeformations.CatAlg.MeshData.eU {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 : 𝒞) : Rep D.F0 X ≃ₗ[Alg D.F0] Unit → Rep D.F0 X

R⁰_X ≅ ⊕_{Unit} R⁰_X.

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.hom_eq_repMap {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 y : ι) (g : Rep D.F0 (F x) →ₗ[Alg D.F0] Rep D.F0 (F y)) : ∃ (h : F x ⟶ F y), ∀ (m : Rep D.F0 (F x)), g m = (repMap h) m

Maps between evaluations of labels are evaluations of morphisms.

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.repMap_eq_zero {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 y : ι) (h : F x ⟶ F y) (hz : ∀ (m : Rep D.F0 (F x)), (repMap h) m = 0) : h = 0

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.InjData.N0_equiv {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) (p : D.PV) : Nonempty (J.N0 p ≃ₗ[Alg D.F0] DRep D.F0 p)

ev(I_p) ≅ D(A₀ e_p) (graded-category.tex).

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.InjData.essSurj {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) {X : Type u_1} [AddCommGroup X] [Module k X] [Module (Alg D.F0) X] [IsScalarTower k (Alg D.F0) X] [FiniteDimensional k X] : ∃ (μ : Type) (x : Fintype μ) (x : DecidableEq μ) (W : μ → ι), Nonempty (X ≃ₗ[Alg D.F0] D.EZ W)

Evaluation is essentially surjective (Lemma 2.9 with Proposition 2.10): every finite-dimensional A₀-module is the evaluation of a family of labels.