The mesh sequences of k(Γ_A) on homogeneous paths

Proposition 2.6(1)(2) transported to k(Γ_A) = C(Γ_A, c) through the realization of Proposition 2.6(3) (graded-category.tex). For a homogeneous family of morphisms of kQ the statements read, modulo the mesh ideal:

• (cov_homog) if ∑_a G_a a lies in the mesh ideal, then at a projective vertex every G_a does, and at a nonprojective vertex y there is H with G_a ≡ c_{y,a} H (σa) for every arrow a ending at y (the manuscript's "comes from h ∈ C_{n-2}(W, τY)", as in the injectivity step of (3));
• (cov_mono_homog) if every H (σa) lies in the mesh ideal, so does H;
• (contra_homog) if ∑_a c_{y,a} (σa) V_a lies in the mesh ideal, then V_a ≡ a U for one U;
• (contra_mono_homog) if every a U lies in the mesh ideal, so does U.

The first two use the first sequence of (1), the last two the second sequence (LayerExactnessDual.lean).

theorem MultiplicativeBasisDeformations.IndSkeleton.exists_occ {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) {Y : S.ARVertex} (a : (X : S.ARVertex) × (X ⟶ Y)) : ∃ (i : Fin (S.arity (S.index Y))), a = ⟨S.vertex (S.midLabel (S.index Y) i), S.occArrow Y i⟩

Every arrow ending at Y is the arrow of a summand of the middle term.

theorem MultiplicativeBasisDeformations.IndSkeleton.realize_mem_of_mem_ideal {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) {d : ℕ} {x y : S.ARVertex} {g : LinearPaths.obj x ⟶ LinearPaths.obj y} (hd : g ∈ LinearPaths.degreePart d x y) (hg : g ∈ (S.meshIdeal b).hom (LinearPaths.obj x) (LinearPaths.obj y)) : (S.realize b x y) g ∈ S.radPow (d + 1) (S.label x) (S.label y)

A homogeneous element of the mesh ideal is realized one radical degree higher.

theorem MultiplicativeBasisDeformations.IndSkeleton.cov_homog {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) (d : ℕ) {W Y : S.ARVertex} (G : (a : (X : S.ARVertex) × (X ⟶ Y)) → LinearPaths.obj W ⟶ LinearPaths.obj a.fst) (hG : ∀ (a : (X : S.ARVertex) × (X ⟶ Y)), G a ∈ LinearPaths.degreePart d W a.fst) (hsum : ∑ a : (X : S.ARVertex) × (X ⟶ Y), CategoryTheory.CategoryStruct.comp (G a) (LinearPaths.arrow a.snd) ∈ (S.meshIdeal b).hom (LinearPaths.obj W) (LinearPaths.obj Y)) : (Y ∉ S.nonprojectiveVertices → ∀ (a : (X : S.ARVertex) × (X ⟶ Y)), G a ∈ (S.meshIdeal b).hom (LinearPaths.obj W) (LinearPaths.obj a.fst)) ∧ ∀ (hY : Y ∈ S.nonprojectiveVertices), ∃ (H : LinearPaths.obj W ⟶ LinearPaths.obj ↑(S.arTranslationQuiver.tau ⟨Y, hY⟩)), ∀ (a : (X : S.ARVertex) × (X ⟶ Y)), G a - ↑(S.arCoefficients b ⟨Y, hY⟩ a.fst a.snd) • CategoryTheory.CategoryStruct.comp H (LinearPaths.arrow ((S.arTranslationQuiver.mate ⟨Y, hY⟩ a.fst) a.snd)) ∈ (S.meshIdeal b).hom (LinearPaths.obj W) (LinearPaths.obj a.fst)

Proposition 2.6(1)(2) for k(Γ_A), covariant form on homogeneous families.

theorem MultiplicativeBasisDeformations.IndSkeleton.cov_mono_homog {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) (m : ℕ) {W : S.ARVertex} (y : ↑S.nonprojectiveVertices) (H : LinearPaths.obj W ⟶ LinearPaths.obj ↑(S.arTranslationQuiver.tau y)) (hH : H ∈ LinearPaths.degreePart m W ↑(S.arTranslationQuiver.tau y)) (h : ∀ (a : (X : S.ARVertex) × (X ⟶ ↑y)), CategoryTheory.CategoryStruct.comp H (LinearPaths.arrow ((S.arTranslationQuiver.mate y a.fst) a.snd)) ∈ (S.meshIdeal b).hom (LinearPaths.obj W) (LinearPaths.obj a.fst)) : H ∈ (S.meshIdeal b).hom (LinearPaths.obj W) (LinearPaths.obj ↑(S.arTranslationQuiver.tau y))

Proposition 2.6(1) for k(Γ_A): the first map of a mesh is injective on homogeneous families.

theorem MultiplicativeBasisDeformations.IndSkeleton.contra_mono_homog {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) (m : ℕ) {W : S.ARVertex} (y : ↑S.nonprojectiveVertices) (U : LinearPaths.obj ↑y ⟶ LinearPaths.obj W) (hU : U ∈ LinearPaths.degreePart m (↑y) W) (h : ∀ (a : (X : S.ARVertex) × (X ⟶ ↑y)), CategoryTheory.CategoryStruct.comp (LinearPaths.arrow a.snd) U ∈ (S.meshIdeal b).hom (LinearPaths.obj a.fst) (LinearPaths.obj W)) : U ∈ (S.meshIdeal b).hom (LinearPaths.obj ↑y) (LinearPaths.obj W)

Proposition 2.6(1) for k(Γ_A), second sequence: precomposition with the arrows into a nonprojective vertex is injective on homogeneous morphisms.

theorem MultiplicativeBasisDeformations.IndSkeleton.mem_of_smul_mem {k A : Type w} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) {n : ℕ} {X Y : S.Ind} {f : X ⟶ Y} {v : k} (hv : v ≠ 0) (h : v • f ∈ S.radPow n X Y) : f ∈ S.radPow n X Y

theorem MultiplicativeBasisDeformations.IndSkeleton.contra_homog {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) (d : ℕ) {W : S.ARVertex} (y : ↑S.nonprojectiveVertices) (V : (a : (X : S.ARVertex) × (X ⟶ ↑y)) → LinearPaths.obj a.fst ⟶ LinearPaths.obj W) (hV : ∀ (a : (X : S.ARVertex) × (X ⟶ ↑y)), V a ∈ LinearPaths.degreePart d a.fst W) (hsum : ∑ 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) ∈ (S.meshIdeal b).hom (LinearPaths.obj ↑(S.arTranslationQuiver.tau y)) (LinearPaths.obj W)) : ∃ (U : LinearPaths.obj ↑y ⟶ LinearPaths.obj W), ∀ (a : (X : S.ARVertex) × (X ⟶ ↑y)), V a - CategoryTheory.CategoryStruct.comp (LinearPaths.arrow a.snd) U ∈ (S.meshIdeal b).hom (LinearPaths.obj a.fst) (LinearPaths.obj W)

Proposition 2.6(1) for k(Γ_A), second sequence, exactness on homogeneous families: if ∑_a c_{y,a} (σa) V_a lies in the mesh ideal, then V_a ≡ a U for one U.