Evaluation at the projective labels: essential surjectivity

Lemma 2.9 (second part, graded-category.tex): "Given 0 → X → I⁰ → I¹ over Λ_e, lift its injectives to projectives Q⁰, Q¹ and their map to f : Q⁰ → Q¹. Its kernel is a second syzygy and hence projective, since gl.dim Λ ≤ 2. Exactness of M ↦ Me gives X ≅ (ker f)e." Proposition 2.10 (graded-category.tex): the injective A₀-modules D(A₀ e_x) are the evaluations of the injective labels I_x, by the socle and a dimension count.

Here: the extension ext : A₀ → Λ by zero; the e-part of kernels; the dual representables J_p and injective copresentations; J_p ≅ ev(I_p) from the Hom-dimensions; essential surjectivity.

def MultiplicativeBasisDeformations.CatAlg.MeshData.extA {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) (a : Alg D.F0) : Alg F

Extension by zero A₀ → Λ.

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.extA_mul {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) (a b : Alg D.F0) : D.extA (a * b) = D.extA a * D.extA b

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.extA_add {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) (a b : Alg D.F0) : D.extA (a + b) = D.extA a + D.extA b

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.extA_rows {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) (a : Alg D.F0) (y z : ι) : ¬D.proj y → D.extA a y z = 0

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.resAlg_extA {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) (a : Alg D.F0) : D.resAlg (D.extA a) = a

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.extA_smul_extZ {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 : 𝒞} (a : Alg D.F0) (m : Rep D.F0 X) : D.extA a • (D.extZ X) m = (D.extZ X) (a • m)

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.restr_extA_smul {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 : 𝒞} (a : Alg D.F0) (m : Rep F X) : (D.restr X) (D.extA a • m) = a • (D.restr X) m

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.extA_one_smul {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 : 𝒞} (m : Rep F X) : D.extA 1 • m = (D.extZ X) ((D.restr X) m)

def MultiplicativeBasisDeformations.CatAlg.MeshData.restrs {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} (Z : κ → ι) : RZ F Z →ₗ[k] D.EZ Z

Restriction to the projective labels, componentwise.

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.restrs_extZs {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} [Fintype κ] [DecidableEq κ] (Z : κ → ι) (m : D.EZ Z) : (D.restrs Z) ((D.extZs Z) m) = m

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.extA_one_smul_RZ {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} [Fintype κ] [DecidableEq κ] (Z : κ → ι) (m : RZ F Z) : D.extA 1 • m = (D.extZs Z) ((D.restrs Z) m)

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.restrs_smul {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} [Fintype κ] [DecidableEq κ] (Z : κ → ι) (a : Alg D.F0) (m : RZ F Z) : (D.restrs Z) (D.extA a • m) = a • (D.restrs Z) m

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.extZs_smul {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} [Fintype κ] [DecidableEq κ] (Z : κ → ι) (a : Alg D.F0) (m : D.EZ Z) : (D.extZs Z) (a • m) = D.extA a • (D.extZs Z) m

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.ker_evMap_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) {κ κ' : Type} [Fintype κ] [DecidableEq κ] [Fintype κ'] [DecidableEq κ'] [hfd : ∀ (x y : ι), FiniteDimensional k (F x ⟶ F y)] {Z : κ → ι} {Z' : κ' → ι} (f : Mat F Z Z') : ∃ (μ : Type) (x : Fintype μ) (x : DecidableEq μ) (W : μ → ι), Nonempty (↥(D.evMap f).ker ≃ₗ[Alg D.F0] D.EZ W)

The kernel of an evaluated matrix is the evaluation of a family.