The mesh data of k(Γ_A)

Lemma 2.7 and Proposition 2.6(1)(2) for C = k(Γ_A) in the form used by the proof of Proposition 2.10 (graded-category.tex): the categorical radical of C is its positive-degree part (ScalarMeshCategory.localFamily), the right mesh maps at x are the arrows ending at x, and at a nonprojective x the sequences

0 → C(W, τx) → ⊕_a C(W, E_a) → C(W, x) and 0 → C(x, W) → ⊕_a C(E_a, W) → C(τx, W)

are exact, with first map given by c_{x,a} (σa); at a projective x the right mesh map is a monomorphism. Exactness is reduced to homogeneous families of paths (ARMeshExactness.lean) by the path-length grading.

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.arLocal {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) : CatAlg.LocalFamily fun (x : S.ARVertex) => S.meshObj b x

The local structure of k(Γ_A).

theorem MultiplicativeBasisDeformations.IndSkeleton.proj_sum_comp_arrow {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (e : ℕ) {W Y : S.ARVertex} (G : (a : (X : S.ARVertex) × (X ⟶ Y)) → LinearPaths.obj W ⟶ LinearPaths.obj a.fst) : (LinearPaths.proj (e + 1) W Y) (∑ a : (X : S.ARVertex) × (X ⟶ Y), CategoryTheory.CategoryStruct.comp (G a) (LinearPaths.arrow a.snd)) = ∑ a : (X : S.ARVertex) × (X ⟶ Y), CategoryTheory.CategoryStruct.comp ((LinearPaths.proj e W a.fst) (G a)) (LinearPaths.arrow a.snd)

The degree-(e+1) component of a sum over the arrows ending at Y.

theorem MultiplicativeBasisDeformations.IndSkeleton.proj_mem_meshIdeal {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (e : ℕ) {X Y : S.ARVertex} {F : LinearPaths.obj X ⟶ LinearPaths.obj Y} (hF : F ∈ (S.meshIdeal b).hom (LinearPaths.obj X) (LinearPaths.obj Y)) : (LinearPaths.proj e X Y) F ∈ (S.meshIdeal b).hom (LinearPaths.obj X) (LinearPaths.obj Y)

theorem MultiplicativeBasisDeformations.IndSkeleton.map_eq_of_sub_mem {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) {X Y : S.ARVertex} {F G : LinearPaths.obj X ⟶ LinearPaths.obj Y} (h : F - G ∈ (S.meshIdeal b).hom (LinearPaths.obj X) (LinearPaths.obj Y)) : (S.meshQuot b).map F = (S.meshQuot b).map G

theorem MultiplicativeBasisDeformations.IndSkeleton.map_eq_sum_proj {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) {X Y : S.ARVertex} {F : LinearPaths.obj X ⟶ LinearPaths.obj Y} {N : ℕ} (hN : F = ∑ e ∈ Finset.range N, (LinearPaths.proj e X Y) F) : (S.meshQuot b).map F = ∑ e ∈ Finset.range N, (S.meshQuot b).map ((LinearPaths.proj e X Y) F)

theorem MultiplicativeBasisDeformations.IndSkeleton.proj_sum_arrow_comp {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (e : ℕ) {W : S.ARVertex} (y : ↑S.nonprojectiveVertices) (V : (a : (X : S.ARVertex) × (X ⟶ ↑y)) → LinearPaths.obj a.fst ⟶ LinearPaths.obj W) : (LinearPaths.proj (e + 1) (↑(S.arTranslationQuiver.tau y)) W) (∑ a : (X : S.ARVertex) × (X ⟶ ↑y), ↑(S.arCoefficients b y a.fst a.snd) • CategoryTheory.CategoryStruct.comp (LinearPaths.arrow ((S.arTranslationQuiver.mate y a.fst) a.snd)) (V a)) = ∑ a : (X : S.ARVertex) × (X ⟶ ↑y), ↑(S.arCoefficients b y a.fst a.snd) • CategoryTheory.CategoryStruct.comp (LinearPaths.arrow ((S.arTranslationQuiver.mate y a.fst) a.snd)) ((LinearPaths.proj e a.fst W) (V a))

theorem MultiplicativeBasisDeformations.IndSkeleton.map_arrow {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) {X Y : S.ARVertex} (a : X ⟶ Y) : (S.meshQuot b).map (LinearPaths.arrow a) = ScalarMeshCategory.arrowMor (S.arCoefficients b) a

map of an arrow is the arrow morphism.

theorem MultiplicativeBasisDeformations.IndSkeleton.mem_of_proj_mem {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) {X Y : S.ARVertex} {F : LinearPaths.obj X ⟶ LinearPaths.obj Y} (h : ∀ (e : ℕ), (LinearPaths.proj e X Y) F ∈ (S.meshIdeal b).hom (LinearPaths.obj X) (LinearPaths.obj Y)) : F ∈ (S.meshIdeal b).hom (LinearPaths.obj X) (LinearPaths.obj Y)

theorem MultiplicativeBasisDeformations.IndSkeleton.ar_cov_exact {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (x : S.ARVertex) (hx : x ∈ S.nonprojectiveVertices) (w : S.ARVertex) (g : (a : (y : S.ARVertex) × (y ⟶ x)) → S.meshObj b w ⟶ S.meshObj b a.fst) (hg : ∑ a : (y : S.ARVertex) × (y ⟶ x), CategoryTheory.CategoryStruct.comp (g a) (ScalarMeshCategory.arrowMor (S.arCoefficients b) a.snd) = 0) : ∃ (z : S.meshObj b w ⟶ S.meshObj b ↑(S.arTranslationQuiver.tau ⟨x, hx⟩)), ∀ (a : (y : S.ARVertex) × (y ⟶ x)), g a = CategoryTheory.CategoryStruct.comp z (↑(S.arCoefficients b ⟨x, hx⟩ a.fst a.snd) • ScalarMeshCategory.arrowMor (S.arCoefficients b) ((S.arTranslationQuiver.mate ⟨x, hx⟩ a.fst) a.snd))

Covariant exactness at a nonprojective vertex.

theorem MultiplicativeBasisDeformations.IndSkeleton.ar_cov_mono {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (x : S.ARVertex) (hx : x ∈ S.nonprojectiveVertices) (w : S.ARVertex) (z : S.meshObj b w ⟶ S.meshObj b ↑(S.arTranslationQuiver.tau ⟨x, hx⟩)) (hz : ∀ (a : (y : S.ARVertex) × (y ⟶ x)), CategoryTheory.CategoryStruct.comp z (↑(S.arCoefficients b ⟨x, hx⟩ a.fst a.snd) • ScalarMeshCategory.arrowMor (S.arCoefficients b) ((S.arTranslationQuiver.mate ⟨x, hx⟩ a.fst) a.snd)) = 0) : z = 0

Covariant injectivity at a nonprojective vertex.

theorem MultiplicativeBasisDeformations.IndSkeleton.ar_proj_mono {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (x : S.ARVertex) (hx : x ∉ S.nonprojectiveVertices) (w : S.ARVertex) (g : (a : (y : S.ARVertex) × (y ⟶ x)) → S.meshObj b w ⟶ S.meshObj b a.fst) (hg : ∑ a : (y : S.ARVertex) × (y ⟶ x), CategoryTheory.CategoryStruct.comp (g a) (ScalarMeshCategory.arrowMor (S.arCoefficients b) a.snd) = 0) (a : (y : S.ARVertex) × (y ⟶ x)) : g a = 0

At a projective vertex the right mesh map is a monomorphism.

theorem MultiplicativeBasisDeformations.IndSkeleton.ar_contra_exact {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (x : S.ARVertex) (hx : x ∈ S.nonprojectiveVertices) (w : S.ARVertex) (v : (a : (y : S.ARVertex) × (y ⟶ x)) → S.meshObj b a.fst ⟶ S.meshObj b w) (hv : ∑ a : (y : S.ARVertex) × (y ⟶ x), CategoryTheory.CategoryStruct.comp (↑(S.arCoefficients b ⟨x, hx⟩ a.fst a.snd) • ScalarMeshCategory.arrowMor (S.arCoefficients b) ((S.arTranslationQuiver.mate ⟨x, hx⟩ a.fst) a.snd)) (v a) = 0) : ∃ (u : S.meshObj b x ⟶ S.meshObj b w), ∀ (a : (y : S.ARVertex) × (y ⟶ x)), v a = CategoryTheory.CategoryStruct.comp (ScalarMeshCategory.arrowMor (S.arCoefficients b) a.snd) u

Contravariant exactness at a nonprojective vertex.

theorem MultiplicativeBasisDeformations.IndSkeleton.ar_contra_mono {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (x : S.ARVertex) (hx : x ∈ S.nonprojectiveVertices) (w : S.ARVertex) (u : S.meshObj b x ⟶ S.meshObj b w) (hu : ∀ (a : (y : S.ARVertex) × (y ⟶ x)), CategoryTheory.CategoryStruct.comp (ScalarMeshCategory.arrowMor (S.arCoefficients b) a.snd) u = 0) : u = 0

Contravariant injectivity at a nonprojective vertex.

theorem MultiplicativeBasisDeformations.IndSkeleton.ar_comp_zero {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (x : S.ARVertex) (hx : x ∈ S.nonprojectiveVertices) : ∑ a : (y : S.ARVertex) × (y ⟶ x), CategoryTheory.CategoryStruct.comp (↑(S.arCoefficients b ⟨x, hx⟩ a.fst a.snd) • ScalarMeshCategory.arrowMor (S.arCoefficients b) ((S.arTranslationQuiver.mate ⟨x, hx⟩ a.fst) a.snd)) (ScalarMeshCategory.arrowMor (S.arCoefficients b) a.snd) = 0

The mesh relation at a nonprojective vertex holds in k(Γ_A).

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.arMeshData {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) : CatAlg.MeshData (fun (x : S.ARVertex) => S.meshObj b x) (S.arLocal b)

The mesh data of k(Γ_A): the right mesh maps are the arrows ending at each vertex, with the exact mesh sequences of Proposition 2.6(1)(2).

theorem MultiplicativeBasisDeformations.IndSkeleton.meshSimpleTops {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (x : S.ARVertex) : ((S.arMeshData b).meshMap x).range = (S.arLocal b).radRep x ∧ IsSimpleModule (CatAlg.Alg fun (x : S.ARVertex) => S.meshObj b x) (CatAlg.Rep (fun (x : S.ARVertex) => S.meshObj b x) (S.meshObj b x) ⧸ ((S.arMeshData b).meshMap x).range)

Lemma 2.7 (lem:mesh-simple-tops): at every label X of C = k(Γ_A), projective or not, the right mesh map ⊕_a C(-, mid a) → C(-, X) (at a projective label, the initial forms of the components of rad P → P, the arrows into P) has image the radical of the representable C(-, X), and its cokernel is the simple top of C(-, X).