Corollary 2.11: the translations of Γ_{A₀} and Γ_A agree

graded-category.tex (proof of cor:same-ar-quiver): "every right mesh map is right almost split. ... Thus the meshes are the almost split sequences and give the translation."

Evaluated at the projective labels, the right mesh map at x is f_x : ⊕_a M_{mid a} → M_x (mesh0), with kernel M_{τ x} at a nonprojective x (tau0) and injective at a projective x.

Deviation: instead of proving that f_x is right minimal by degrees, we compare f_x with the chosen minimal right almost split map c of the vendored library. Every component of c is radical, so c factors through f_x (c = h' f_x), and f_x is not split epi, so f_x = h c. Minimality of c makes h' h invertible, which identifies ker c with a summand of ker f_x; as ker f_x ≅ M_{τ x} is indecomposable, the two kernels agree.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.CatAlg.MeshData.P0 {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 : ι) : Type w

The evaluated middle term ⊕_a M_{mid a}.

def MultiplicativeBasisDeformations.CatAlg.MeshData.mesh0 {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 : ι) : D.P0 x →ₗ[Alg D.F0] Rep D.F0 (F x)

The evaluated right mesh map ⊕_a M_{mid a} → M_x.

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.mesh0_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) (x : ι) (m : D.P0 x) (w : D.PV) : (D.mesh0 x) m w = ∑ a : D.Mid x, CategoryTheory.CategoryStruct.comp (m a w) (D.p x a)

def MultiplicativeBasisDeformations.CatAlg.MeshData.tau0 {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 : ι) (hx : ¬D.proj x) : Rep D.F0 (F (D.tau x hx)) →ₗ[Alg D.F0] D.P0 x

The evaluated left mesh map M_{τ x} → ⊕_a M_{mid a}.

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.tau0_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) (x : ι) (hx : ¬D.proj x) (z : Rep D.F0 (F (D.tau x hx))) (a : D.Mid x) (w : D.PV) : (D.tau0 x hx) z a w = CategoryTheory.CategoryStruct.comp (z w) (D.q x hx a)

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.mesh0_tau0 {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 : ι) (hx : ¬D.proj x) (z : Rep D.F0 (F (D.tau x hx))) : (D.mesh0 x) ((D.tau0 x hx) z) = 0

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.tau0_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) (x : ι) (hx : ¬D.proj x) : Function.Injective ⇑(D.tau0 x hx)

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.exists_tau0 {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 : ι) (hx : ¬D.proj x) (m : D.P0 x) (hm : (D.mesh0 x) m = 0) : ∃ (z : Rep D.F0 (F (D.tau x hx))), (D.tau0 x hx) z = m

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.mesh0_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) (x : ι) (hx : D.proj x) : Function.Injective ⇑(D.mesh0 x)

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.mesh0_surjective {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 : ι) (hx : ¬D.proj x) : Function.Surjective ⇑(D.mesh0 x)

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.exists_repMap_eq_mesh0 {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 y : ι) (g : F y ⟶ F x) (hg : g ∈ L.rad y x) : ∃ (h : (a : D.Mid x) → F y ⟶ F (D.mid x a)), repMap g = D.mesh0 x ∘ₗ LinearMap.pi fun (a : D.Mid x) => repMap (h a)

A radical map factors through the evaluated mesh map.

theorem MultiplicativeBasisDeformations.CatAlg.MeshData.sum_comp_p_mem_rad {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 y : ι) (g : (a : D.Mid x) → F y ⟶ F (D.mid x a)) : ∑ a : D.Mid x, CategoryTheory.CategoryStruct.comp (g a) (D.p x a) ∈ L.rad y x

A composite through the mesh arrows is radical.

theorem MultiplicativeBasisDeformations.exists_factor_of_biproduct {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {J : Type u_2} {X : J → C} {hX : CategoryTheory.Limits.HasBiproduct X} {E Z P : C} (d : E ≅ ⨁ X) (c : E ⟶ Z) (f : P ⟶ Z) (hc : ∀ (j : J), ∃ (l : X j ⟶ P), CategoryTheory.CategoryStruct.comp l f = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι X j) (CategoryTheory.CategoryStruct.comp d.inv c)) : ∃ (h : E ⟶ P), CategoryTheory.CategoryStruct.comp h f = c

A map out of a biproduct factors through f when each component does.

theorem MultiplicativeBasisDeformations.not_isSplitEpi_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X Y Z : C} (g : X ⟶ Y) (c : Y ⟶ Z) (hc : ¬CategoryTheory.IsSplitEpi c) : ¬CategoryTheory.IsSplitEpi (CategoryTheory.CategoryStruct.comp g c)

instance MultiplicativeBasisDeformations.IndSkeleton.instNoetherianA0 {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) : IsNoetherianRing (S.A0 b)ᵐᵒᵖ

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.IndSkeleton.resA0 {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) : CategoryTheory.Functor (ModuleCat (CatAlg.Alg (S.arMeshData b).F0)) (ModuleCat (S.A0 b)ᵐᵒᵖ)

Restriction along A₀ᵒᵖ ≅ Λ.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.IndSkeleton.PM {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) : RightModuleCat (S.A0 b)

The evaluated middle term, as an A₀-module.

theorem MultiplicativeBasisDeformations.IndSkeleton.finite_PM {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) : Module.Finite k ↑(S.PM b x)

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.IndSkeleton.PFG {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) : ModCat (S.A0 b)

The evaluated middle term in mod A₀.

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.fFG {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.PFG b x ⟶ (S.skelA0 b).fg x

The evaluated right mesh map f_x in mod A₀.

theorem MultiplicativeBasisDeformations.IndSkeleton.fFG_apply {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) (m : (S.arMeshData b).P0 x) : (ModuleCat.Hom.hom (S.fFG b x).hom) m = ((S.arMeshData b).mesh0 x) m

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.tFG {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 : ¬(S.arMeshData b).proj x) : (S.skelA0 b).fg ((S.arMeshData b).tau x hx) ⟶ S.PFG b x

The evaluated left mesh map in mod A₀.

theorem MultiplicativeBasisDeformations.IndSkeleton.tFG_apply {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 : ¬(S.arMeshData b).proj x) (z : CatAlg.Rep (S.arMeshData b).F0 (S.meshObj b ((S.arMeshData b).tau x hx))) : (ModuleCat.Hom.hom (S.tFG b x hx).hom) z = ((S.arMeshData b).tau0 x hx) z

theorem MultiplicativeBasisDeformations.IndSkeleton.tFG_fFG {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 : ¬(S.arMeshData b).proj x) : CategoryTheory.CategoryStruct.comp (S.tFG b x hx) (S.fFG b x) = 0

theorem MultiplicativeBasisDeformations.IndSkeleton.exists_lift_tFG {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 : ¬(S.arMeshData b).proj x) {Z : ModCat (S.A0 b)} (g : Z ⟶ S.PFG b x) (hg : CategoryTheory.CategoryStruct.comp g (S.fFG b x) = 0) : ∃ (s : Z ⟶ (S.skelA0 b).fg ((S.arMeshData b).tau x hx)), CategoryTheory.CategoryStruct.comp s (S.tFG b x hx) = g

tFG is a kernel of fFG.

theorem MultiplicativeBasisDeformations.IndSkeleton.fFG_not_isSplitEpi {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) : ¬CategoryTheory.IsSplitEpi (S.fFG b x)

f_x is not split epi: its components are radical.

theorem MultiplicativeBasisDeformations.IndSkeleton.exists_factor_fFG {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) (g : (S.skelA0 b).fg y ⟶ (S.skelA0 b).fg x) (hg : ¬CategoryTheory.IsSplitEpi g) : ∃ (l : (S.skelA0 b).fg y ⟶ S.PFG b x), CategoryTheory.CategoryStruct.comp l (S.fFG b x) = g

A map into M_x that is not split epi factors through f_x.

Comparison with the chosen minimal right almost split map

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.IndSkeleton.mras {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.skelA0 b).toVendor.almostSplitSkeleton.MinimalRightAlmostSplitDecomposition x

The chosen minimal right almost split map of A₀ ending at M_x.

theorem MultiplicativeBasisDeformations.IndSkeleton.exists_comparison {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) : ∃ (h' : (S.mras b x).middle ⟶ S.PFG b x) (h : S.PFG b x ⟶ (S.mras b x).middle), CategoryTheory.CategoryStruct.comp h' (S.fFG b x) = (S.mras b x).map ∧ CategoryTheory.CategoryStruct.comp h (S.mras b x).map = S.fFG b x ∧ CategoryTheory.IsIso (CategoryTheory.CategoryStruct.comp h' h)

c = h' f_x, f_x = h c, and h' h is invertible.

theorem MultiplicativeBasisDeformations.IndSkeleton.subsingleton_of_id_eq_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) {M : ModCat (S.A0 b)} (h : CategoryTheory.CategoryStruct.id M = 0) : Subsingleton ↑M

theorem MultiplicativeBasisDeformations.IndSkeleton.projective_fg_of_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 : S.ARVertex) (hx : (S.arMeshData b).proj x) : CategoryTheory.Projective ((S.skelA0 b).fg x)

At a projective vertex of Γ_A, M_x is projective.

theorem MultiplicativeBasisDeformations.IndSkeleton.not_projective_of_not_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 : S.ARVertex) (hx : ¬(S.arMeshData b).proj x) : ¬CategoryTheory.Projective ((S.skelA0 b).fg x)

At a nonprojective vertex of Γ_A, M_x is not projective.

theorem MultiplicativeBasisDeformations.IndSkeleton.rightTranslationLabel_eq {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 : ¬(S.arMeshData b).proj x) (hP : ¬CategoryTheory.Projective ((S.skelA0 b).toVendor.fgObj x)) : (S.skelA0 b).toVendor.rightTranslationLabel ⟨x, hP⟩ = (S.arMeshData b).tau x hx

The translations agree.

Corollary 2.11

theorem MultiplicativeBasisDeformations.IndSkeleton.nonprojective_A0_iff {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 : Fin S.n) : (S.skelA0 b).vertex x ∈ (S.skelA0 b).nonprojectiveVertices ↔ S.vertex x ∈ S.nonprojectiveVertices

theorem MultiplicativeBasisDeformations.IndSkeleton.arTau_A0 {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 : Fin S.n) (h1 : (S.skelA0 b).vertex x ∈ (S.skelA0 b).nonprojectiveVertices) (h2 : S.vertex x ∈ S.nonprojectiveVertices) : ↑((S.skelA0 b).arTau ⟨(S.skelA0 b).vertex x, h1⟩) = ↑(S.arTau ⟨S.vertex x, h2⟩)

theorem MultiplicativeBasisDeformations.IndSkeleton.noninjective_A0_iff {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 : Fin S.n) : (S.skelA0 b).vertex x ∈ (S.skelA0 b).noninjectiveVertices ↔ S.vertex x ∈ S.noninjectiveVertices

theorem MultiplicativeBasisDeformations.IndSkeleton.sameARQuiver {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 : Fin S.n), Nonempty (((S.skelA0 b).vertex x ⟶ (S.skelA0 b).vertex y) ≃ (S.vertex x ⟶ S.vertex y))) ∧ (∀ (x : Fin S.n), (S.skelA0 b).vertex x ∈ (S.skelA0 b).nonprojectiveVertices ↔ S.vertex x ∈ S.nonprojectiveVertices) ∧ (∀ (x : Fin S.n), (S.skelA0 b).vertex x ∈ (S.skelA0 b).noninjectiveVertices ↔ S.vertex x ∈ S.noninjectiveVertices) ∧ ∀ (x : Fin S.n) (h1 : (S.skelA0 b).vertex x ∈ (S.skelA0 b).nonprojectiveVertices) (h2 : S.vertex x ∈ S.nonprojectiveVertices), ↑((S.skelA0 b).arTau ⟨(S.skelA0 b).vertex x, h1⟩) = ↑(S.arTau ⟨S.vertex x, h2⟩)

Corollary 2.11 (cor:same-ar-quiver): Γ_{A₀} ≅ Γ_A as translation quivers. Both have the vertex set Fin n, and the identity matches the arrows, the nonprojective and noninjective vertices, and the translations.