The Auslander--Reiten quiver as a translation quiver

graded-category.tex: the vertices of Γ_A are the indecomposable modules, and the arrows X → Y form a basis of Irr(X, Y) = J(X, Y)/J²(X, Y). The translation τ sends a nonprojective indecomposable Y to the starting term of the almost split sequence ending at Y; it is a bijection from the nonprojective onto the noninjective vertices. The mates of the arrows ending at a nonprojective Y are the arrows starting at τY, indexed by the same summands of the middle term.

Formally the arrows X → Y are Fin (dim Irr(X, Y)); the mate bijection (y ⟶ x) ≃ (τx ⟶ y) is the identification of these index sets, which have the same size because both dimensions equal the multiplicity of y in the middle term of the almost split sequence ending at x. The projective and injective vertices are those whose module is projective, respectively injective, in mod A. The translation and the dimension identities come from the vendored Auslander--Reiten theory through ARBridge.lean.

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

The vertices of the Auslander--Reiten quiver Γ_A.

@[instance_reducible]

instance MultiplicativeBasisDeformations.IndSkeleton.arQuiver {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) : Quiver S.ARVertex

The Auslander--Reiten quiver: the arrows x → y are indexed by Fin (dim Irr(x, y)).

@[instance_reducible]

noncomputable instance MultiplicativeBasisDeformations.IndSkeleton.instFintypeHomARVertex {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) (x y : S.ARVertex) : Fintype (x ⟶ y)

@[instance_reducible]

noncomputable instance MultiplicativeBasisDeformations.IndSkeleton.instDecidableEqHomARVertex {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) (x y : S.ARVertex) : DecidableEq (x ⟶ y)

@[instance_reducible]

instance MultiplicativeBasisDeformations.IndSkeleton.instFintypeARVertex {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) : Fintype S.ARVertex

@[instance_reducible]

instance MultiplicativeBasisDeformations.IndSkeleton.instDecidableEqARVertex {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) : DecidableEq S.ARVertex

def MultiplicativeBasisDeformations.IndSkeleton.vertex {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) (x : Fin S.n) : S.ARVertex

A vertex of Γ_A from an index.

def MultiplicativeBasisDeformations.IndSkeleton.label {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) (x : S.ARVertex) : S.Ind

The labelled module of a vertex, as an object of ind(mod A).

def MultiplicativeBasisDeformations.IndSkeleton.index {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) (x : S.ARVertex) : Fin S.n

The index of a vertex.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.IndSkeleton.arrowMultiplicity {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (x y : Fin S.n) : ℕ

The arrow multiplicity of the vendored library: the multiplicity of x in the middle term of the chosen minimal right almost split map ending at y.

theorem MultiplicativeBasisDeformations.IndSkeleton.finrank_irr_eq_arrowMultiplicity {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsAlgClosed k] (x y : Fin S.n) : Module.finrank k (S.Irr (S.ind x) (S.ind y)) = S.arrowMultiplicity x y

Over an algebraically closed field, dim Irr(x, y) is the multiplicity of x in the middle term of the minimal right almost split map ending at y.

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

The nonprojective vertices of Γ_A.

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

The noninjective vertices of Γ_A.

noncomputable def MultiplicativeBasisDeformations.IndSkeleton.arTau {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] : ↑S.nonprojectiveVertices ≃ ↑S.noninjectiveVertices

The Auslander--Reiten translation, a bijection from the nonprojective onto the noninjective vertices.

theorem MultiplicativeBasisDeformations.IndSkeleton.finrank_irr_mate {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsAlgClosed k] (x : ↑S.nonprojectiveVertices) (y : S.ARVertex) : Module.finrank k (S.Irr (S.ind (S.index y)) (S.ind (S.index ↑x))) = Module.finrank k (S.Irr (S.ind (S.index ↑(S.arTau x))) (S.ind (S.index y)))

The two sides of a mesh have the same arrow count: dim Irr(y, x) = dim Irr(τ x, y) for a nonprojective x.

@[reducible, inline]

noncomputable abbrev MultiplicativeBasisDeformations.IndSkeleton.arTranslationQuiver {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : IndSkeleton k A) [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] [IsAlgClosed k] : TranslationQuiver S.ARVertex

Γ_A as a translation quiver (Definition 2.3).