Lemma 2.2: the Auslander--Reiten quiver is square-free

Lemma 2.2 (lem:square-free, graded-category.tex): for a basic representation-finite algebra over an algebraically closed field, Γ_A has no loops and at most one arrow between each ordered pair of vertices.

The manuscript's proof: an irreducible map is a monomorphism or an epimorphism, so its source and target have different dimensions; this excludes loops. If there are two arrows X → Y with dim X > dim Y, then Y is nonprojective, the middle term of the almost split sequence ending at Y contains X², hence dim τY ≥ 2 dim X − dim Y > dim X, and the mates give two arrows τY → X. Repeating gives indecomposables of strictly increasing dimension, contrary to finite representation type. The case dim X < dim Y is dual.

The formal proof is borrowed from the magnitude-conjecture formalization, Algebra/RightModuleRepresentationFiniteSquareFree.lean (commit 52fbbfa2b), whose argument is the same: the dimension-growth step exists_multipleArrow_pair_of_multipleArrow, and the finiteness argument choosing a pair of maximal endpoint dimension (in place of an infinite chain). Its helper declarations for parallel arrow occurrences are replaced by the vendored middle-term inclusions and components (FiniteTauIrreducible), and the exactness lemma rightKernelMap_functionExact is copied from Algebra/RightModuleHoshinoTorsion.lean. The no-loop part is added here.

noncomputable def MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.objectFinrank {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : ℕ

Coefficient-field dimension of one selected indecomposable module.

def MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.homRestrictScalars {k A : Type u} [Field k] [Ring A] [Algebra k A] {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) : ↑X →ₗ[k] ↑Y

Restrict a morphism of finitely generated right modules to a k-linear map on the same underlying function.

@[simp]

theorem MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.homRestrictScalars_apply {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {X Y : FinitelyGeneratedCategory A} (f : X ⟶ Y) (x : ↑X) : (homRestrictScalars f) x = (ModuleCat.Hom.hom f.hom) x

theorem MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.objectFinrank_lt_of_irreducible_mono {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : Fin S.n} (f : S.fgObj x ⟶ S.fgObj y) (hf : QSE.IsIrreducibleMorphism f) [CategoryTheory.Mono f] : S.objectFinrank x < S.objectFinrank y

A monic irreducible map between selected indecomposables strictly raises coefficient-field dimension.

theorem MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.objectFinrank_lt_of_irreducible_epi {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {x y : Fin S.n} (f : S.fgObj x ⟶ S.fgObj y) (hf : QSE.IsIrreducibleMorphism f) [CategoryTheory.Epi f] : S.objectFinrank y < S.objectFinrank x

An epic irreducible map between selected indecomposables strictly lowers coefficient-field dimension.

@[reducible, inline]

noncomputable abbrev MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.tauData {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : QSE.Iyama.FiniteTauCategoryData (FinitelyGeneratedCategory A) (Fin S.n)

Shorthand for the vendored right tau-category data.

@[reducible, inline]

abbrev MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.Occurrence {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (y x : Fin S.n) : Type

An occurrence of y in the chosen middle decomposition of the right mesh ending at x.

theorem MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.arrowMultiplicity_eq_card_occurrence {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (y x : Fin S.n) : FiniteTauMatrix.arrowMultiplicity S.tauData.toFiniteRightTauCategoryData y x = Fintype.card (S.Occurrence y x)

The arrow multiplicity counts occurrences.

noncomputable def MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.occurrenceMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {y x : Fin S.n} (i : S.Occurrence y x) : S.fgObj y ⟶ S.fgObj x

An occurrence gives an irreducible map from y to x.

theorem MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.occurrenceMap_isIrreducible {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {y x : Fin S.n} (i : S.Occurrence y x) : QSE.IsIrreducibleMorphism (S.occurrenceMap i)

noncomputable def MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.occurrenceInclusion {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {y x : Fin S.n} (i : S.Occurrence y x) : S.fgObj y ⟶ (S.tauData.rightMesh (S.fgObj x)).X₂

Inclusion of the occurrence i into the right-mesh middle term.

noncomputable def MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.occurrenceProjection {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {y x : Fin S.n} (i : S.Occurrence y x) : (S.tauData.rightMesh (S.fgObj x)).X₂ ⟶ S.fgObj y

Projection from the right-mesh middle term onto the occurrence i.

theorem MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.occurrenceInclusion_projection {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {y x : Fin S.n} (i : S.Occurrence y x) : CategoryTheory.CategoryStruct.comp (S.occurrenceInclusion i) (S.occurrenceProjection i) = CategoryTheory.CategoryStruct.id (S.fgObj y)

theorem MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.occurrenceInclusion_projection_ne {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {y x : Fin S.n} {i j : S.Occurrence y x} (hij : i ≠ j) : CategoryTheory.CategoryStruct.comp (S.occurrenceInclusion i) (S.occurrenceProjection j) = 0

theorem MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.two_mul_objectFinrank_le_rightMiddle {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) (hxy : 2 ≤ FiniteTauMatrix.arrowMultiplicity S.tauData.toFiniteRightTauCategoryData y x) : 2 * S.objectFinrank y ≤ Module.finrank k ↑(S.tauData.rightMesh (S.fgObj x)).X₂

Two distinct occurrences of y in the mesh ending at x bound twice the dimension of y by the dimension of the middle term.

theorem MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.rightKernelMap_functionExact {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : Function.Exact ⇑(ModuleCat.Hom.hom (S.rightKernelMap z).hom) ⇑(ModuleCat.Hom.hom (S.minimalRightAlmostSplitAt ↑z).map.hom)

The kernel map of the chosen almost split sequence is exact at the middle term. Copied from Algebra/RightModuleHoshinoTorsion.lean.

theorem MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.rightMesh_finrank_eq_translation_add_endpoint {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) : Module.finrank k ↑(S.tauData.rightMesh (S.fgObj ↑z)).X₂ = S.objectFinrank ↑(S.rightTranslationEquiv z) + S.objectFinrank ↑z

Coefficient-field dimensions are additive across the selected Auslander--Reiten sequence.

theorem MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.exists_multipleArrow_pair_of_multipleArrow {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) (hxy : 2 ≤ FiniteTauMatrix.arrowMultiplicity S.tauData.toFiniteRightTauCategoryData x y) : ∃ (x' : Fin S.n) (y' : Fin S.n), 2 ≤ FiniteTauMatrix.arrowMultiplicity S.tauData.toFiniteRightTauCategoryData x' y' ∧ max (S.objectFinrank x) (S.objectFinrank y) < max (S.objectFinrank x') (S.objectFinrank y')

A pair carrying at least two parallel irreducible maps produces another such pair with strictly larger maximal endpoint dimension: the dimension-growth step of Lemma 2.2.

theorem MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.arrowMultiplicity_le_one {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) : FiniteTauMatrix.arrowMultiplicity S.tauData.toFiniteRightTauCategoryData x y ≤ 1

At most one arrow between two selected indecomposables.

theorem MBDVendor.Magnitude.RightModule.FiniteIndecomposableSkeleton.arrowMultiplicity_self {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x : Fin S.n) : FiniteTauMatrix.arrowMultiplicity S.tauData.toFiniteRightTauCategoryData x x = 0

No loops: no occurrence of x in the mesh ending at x.

theorem MultiplicativeBasisDeformations.IndSkeleton.finrank_irr_le_one {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) : Module.finrank k (S.Irr (S.ind x) (S.ind y)) ≤ 1

Lemma 2.2 (lem:square-free). Γ_A has at most one arrow between each ordered pair of vertices.

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

Lemma 2.2 (lem:square-free). Γ_A has no loops.

theorem MultiplicativeBasisDeformations.IndSkeleton.hasAtMostOneArrow {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : IndSkeleton k A) : HasAtMostOneArrow S.ARVertex

Lemma 2.2 (lem:square-free), in the form of Definition 2.4: Γ_A has at most one arrow between each ordered pair of vertices.