The mesh category k(Γ_A) and standardness

graded-category.tex: for Q = Γ_A, choose bases in the one-dimensional irreducible spaces. The first and second maps of the almost split sequence ending at a nonprojective Y have components u_a (σ a) and v_a a modulo J², with u_a, v_a ≠ 0; the mesh relation is r_Y = ∑_{a : X → Y} c_{Y,a} (σ a) a with c_{Y,a} = u_a v_a (eq:scalar-mesh), and k(Γ_A) = C(Γ_A, c). Definition 1.2 (def:standardness): A is standard if there is a k-linear equivalence k(Γ_A) ≃ ind(mod A) sending each vertex to its labelled module.

Formalization:

• Γ_A is the translation quiver arTranslationQuiver of ARTranslationQuiver.lean; by Lemma 2.2 (SquareFree.lean) it has at most one arrow between ordered vertices.
• An ArrowBases value chooses a basis of each Irr(x, y), indexed by the arrows x → y.
• The almost split sequence ending at a nonprojective x is the canonical one of the vendored Auslander--Reiten library, with its chosen decomposition of the middle term. For an arrow a : y → x, the summands isomorphic to y are the occurrences of y; there is exactly one, because their number is dim Irr(y, x) = 1. The coefficient is c_{x,a} = ∑_{occurrences i of y} u_i v_i, where u_i and v_i are the coordinates, in the chosen bases, of the classes of the components τx → y and y → x at i. It is nonzero because the components are irreducible, so their classes in the one-dimensional spaces Irr are nonzero.
• k(Γ_A) is the scalar mesh category C(Γ_A, c) of Definition 2.4.

The manuscript shows that a different choice of bases or almost split sequences changes k(Γ_A) only by an object-fixing isomorphism (graded-category.tex); Definition 1.2 is formalized with an existential choice of bases.

theorem MultiplicativeBasisDeformations.IndSkeleton.isRadicalMorphism_of_irreducible {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) {x y : Fin S.n} {f : S.fg x ⟶ S.fg y} (hf : MBDVendor.QSE.IsIrreducibleMorphism f) : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism f

An irreducible morphism between labelled indecomposables of mod A is a radical morphism.

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.irrClassFG {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) {x y : Fin S.n} (f : S.fg x ⟶ S.fg y) (hf : MBDVendor.QSE.CategoricalRadical.IsRadicalMorphism f) : S.Irr (S.ind x) (S.ind y)

The class in Irr(x, y) of a radical morphism of mod A between labelled indecomposables.

theorem MultiplicativeBasisDeformations.IndSkeleton.irrClassFG_ne_zero {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) {x y : Fin S.n} {f : S.fg x ⟶ S.fg y} (hf : MBDVendor.QSE.IsIrreducibleMorphism f) : S.irrClassFG f ⋯ ≠ 0

The class of an irreducible morphism in Irr is nonzero.

def MultiplicativeBasisDeformations.IndSkeleton.ArrowBases {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) : Type u

A choice of basis of every space of irreducible maps, indexed by the arrows of Γ_A.

def MultiplicativeBasisDeformations.IndSkeleton.vendorNonprojective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (x : ↑S.nonprojectiveVertices) : S.toVendor.tauData.Nonprojective

The vendored nonprojective label of a nonprojective vertex.

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.sourceComponent {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (x : ↑S.nonprojectiveVertices) {y : Fin S.n} (i : S.toVendor.Occurrence y (S.index ↑x)) : S.fg (S.index ↑(S.arTau x)) ⟶ S.fg y

The component τx → y of the first map of the almost split sequence ending at x, at an occurrence i of y in its middle term.

theorem MultiplicativeBasisDeformations.IndSkeleton.sourceComponent_isIrreducible {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (x : ↑S.nonprojectiveVertices) {y : Fin S.n} (i : S.toVendor.Occurrence y (S.index ↑x)) : MBDVendor.QSE.IsIrreducibleMorphism (S.sourceComponent x i)

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.occurrenceCoefficient {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (x : ↑S.nonprojectiveVertices) (y : S.ARVertex) (a : y ⟶ ↑x) (i : S.toVendor.Occurrence (S.index y) (S.index ↑x)) : k

The scalar u_i v_i contributed by one occurrence.

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.arCoefficient {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (x : ↑S.nonprojectiveVertices) (y : S.ARVertex) (a : y ⟶ ↑x) : k

The mesh coefficient c_{x,a} = ∑_i u_i v_i (eq:scalar-mesh).

theorem MultiplicativeBasisDeformations.IndSkeleton.basis_repr_ne_zero {k : Type u} [Field k] {ι : Type u_1} {V : Type u_2} [AddCommGroup V] [Module k V] [Subsingleton ι] (b : Module.Basis ι k V) {v : V} (hv : v ≠ 0) (j : ι) : (b.repr v) j ≠ 0

A vector of a space with a basis indexed by a subsingleton type has a nonzero coordinate if it is nonzero.

theorem MultiplicativeBasisDeformations.IndSkeleton.arCoefficient_ne_zero {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) (x : ↑S.nonprojectiveVertices) (y : S.ARVertex) (a : y ⟶ ↑x) : S.arCoefficient b x y a ≠ 0

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.arCoefficients {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) : MeshCoefficients k S.arTranslationQuiver

The coefficient system of Γ_A defined by the arrow bases and the almost split sequences (eq:scalar-mesh).

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.IndSkeleton.ARMeshCategory {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (b : S.ArrowBases) : Type

The mesh category k(Γ_A) = C(Γ_A, c) for the coefficients defined by the arrow bases and the almost split sequences.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.IndSkeleton.meshObj {k A : Type u} [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.ARMeshCategory b

A vertex of Γ_A, as an object of k(Γ_A).

def MultiplicativeBasisDeformations.IsLinearFunctor {k : Type u} [Field k] {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.Preadditive C] [CategoryTheory.Preadditive D] [CategoryTheory.Linear k C] [CategoryTheory.Linear k D] (F : CategoryTheory.Functor C D) : Prop

A functor between k-linear categories is k-linear on morphisms.

def MultiplicativeBasisDeformations.IndSkeleton.IsStandard {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) : Prop

Definition 1.2 for a chosen skeleton: for some choice of arrow bases there is a k-linear equivalence k(Γ_A) ≃ ind(mod A) sending each vertex to its labelled module.

def MultiplicativeBasisDeformations.IsStandard (k A : Type u') [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] : Prop

Definition 1.2 (def:standardness): A is standard, for every choice of representatives of the indecomposable modules.

def MultiplicativeBasisDeformations.IndSkeleton.homToLinearMap {k A : Type w} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) (X Y : S.Ind) : (X ⟶ Y) →ₗ[k] ↑(S.obj X) →ₗ[k] ↑(S.obj Y)

Morphisms of ind(mod A), as k-linear maps of the underlying spaces.

theorem MultiplicativeBasisDeformations.IndSkeleton.homToLinearMap_injective {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (X Y : S.Ind) : Function.Injective ⇑(S.homToLinearMap X Y)

instance MultiplicativeBasisDeformations.IndSkeleton.finiteDimensional_hom {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (X Y : S.Ind) : FiniteDimensional k (X ⟶ Y)

instance MultiplicativeBasisDeformations.IndSkeleton.finiteDimensional_layer {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) (d : ℕ) (X Y : S.Ind) : FiniteDimensional k (S.layer d X Y)

theorem MultiplicativeBasisDeformations.IndSkeleton.nonempty_arrowBases {k A : Type w} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) : Nonempty S.ArrowBases

Arrow bases exist, so the definition of standardness is not vacuous.