The Auslander--Reiten mesh of a directed right-module skeleton

This file constructs the concrete translation quiver used by Ringel standardness. An arrow z ⟶ y is an occurrence of the summand y in a fixed minimal right almost-split middle term ending at z; this is the reversed orientation used by the free path category. At a projective endpoint the middle term is the module radical and the map is its canonical inclusion.

For a nonprojective endpoint, the same displayed middle decomposition is also the middle decomposition of the left almost-split kernel map. The right- and left-occurrence bases of rad/rad² therefore give the cardinal equality needed to pair the two sides of each mesh. No multiplicity-one or classification result is used.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshProjectiveBoundaryMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) : S.projectiveBoundaryRadical z ⟶ S.almostSplitSkeleton.obj z

The projective radical inclusion written in the selected skeleton's object vocabulary.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshRightAlmostSplitAt {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) : S.almostSplitSkeleton.MinimalRightAlmostSplitDecomposition z

A minimal right almost-split decomposition at every vertex, using the radical inclusion at a projective vertex and the chosen AR decomposition at a nonprojective vertex.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshRightAlmostSplitAt_eq_of_not_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) (hz : ¬CategoryTheory.Projective (S.fgObj z)) : S.meshRightAlmostSplitAt z = S.minimalRightAlmostSplitAt z

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshRightAlmostSplitAt_eq_of_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) (hz : CategoryTheory.Projective (S.fgObj z)) : S.meshRightAlmostSplitAt z = QuotientSubmoduleEquidistribution.IndecomposableSkeleton.MinimalRightAlmostSplitDecomposition.ofMap S.almostSplitSkeleton (S.meshProjectiveBoundaryMap z) ⋯ ⋯ ⋯

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshRightAlmostSplitAt_middle_eq_of_projective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) (hz : CategoryTheory.Projective (S.fgObj z)) : (S.meshRightAlmostSplitAt z).middle = S.projectiveBoundaryRadical z

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.labelRightMesh_X₂ {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) : (S.labelRightMesh z).X₂ = (S.meshRightAlmostSplitAt z).middle

The middle term of the unified label mesh is the displayed middle term of the corresponding minimal right almost-split decomposition.

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshProjectiveSet {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : Set (Fin S.n)

Projective vertices of the translation quiver.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.mem_meshProjectiveSet_iff {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) : z ∈ S.meshProjectiveSet ↔ CategoryTheory.Projective (S.fgObj z)

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.MeshArrow {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z y : Fin S.n) : Type

Reversed AR-quiver arrows. Thus an element of z ⟶ y represents an irreducible module morphism S(y) ⟶ S(z).

@[reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshQuiver {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Quiver (Fin S.n)

The reversed Auslander--Reiten quiver on the selected labels.

@[reducible]

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshArrowFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z y : Fin S.n) : Fintype (S.MeshArrow z y)

Every displayed arrow type is finite.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshArrowMap {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {z y : Fin S.n} (a : S.MeshArrow z y) : S.almostSplitSkeleton.obj y ⟶ S.almostSplitSkeleton.obj z

The module morphism represented by a reversed AR-quiver arrow.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshMiddleIndexEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) : (S.meshRightAlmostSplitAt z).index.obj ≃ (y : Fin S.n) × S.MeshArrow z y

The displayed middle summands at z are canonically the disjoint union of all arrows into z, with parallel occurrences kept distinct.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshMiddleLift {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X : FGModuleCat Aᵐᵒᵖ} (z : Fin S.n) (c : (a : (y : Fin S.n) × S.MeshArrow z y) → X ⟶ S.almostSplitSkeleton.obj a.fst) : X ⟶ (S.meshRightAlmostSplitAt z).middle

Assemble a map to the displayed right almost-split middle term from one component for every incoming mesh arrow.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshMiddleLift_decomposition_π {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X : FGModuleCat Aᵐᵒᵖ} (z : Fin S.n) (c : (a : (y : Fin S.n) × S.MeshArrow z y) → X ⟶ S.almostSplitSkeleton.obj a.fst) (t : (S.meshRightAlmostSplitAt z).index.obj) : CategoryTheory.CategoryStruct.comp (S.meshMiddleLift z c) (CategoryTheory.CategoryStruct.comp (S.meshRightAlmostSplitAt z).decomposition.hom (CategoryTheory.Limits.biproduct.π (fun (j : (S.meshRightAlmostSplitAt z).index.obj) => S.almostSplitSkeleton.obj ((S.meshRightAlmostSplitAt z).label j)) t)) = c ((S.meshMiddleIndexEquiv z) t)

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshMiddleLift_decomposition_π_assoc {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X : FGModuleCat Aᵐᵒᵖ} (z : Fin S.n) (c : (a : (y : Fin S.n) × S.MeshArrow z y) → X ⟶ S.almostSplitSkeleton.obj a.fst) (t : (S.meshRightAlmostSplitAt z).index.obj) {Z : FGModuleCat Aᵐᵒᵖ} (h : S.almostSplitSkeleton.obj ((S.meshRightAlmostSplitAt z).label t) ⟶ Z) : CategoryTheory.CategoryStruct.comp (S.meshMiddleLift z c) (CategoryTheory.CategoryStruct.comp (S.meshRightAlmostSplitAt z).decomposition.hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.π (fun (j : (S.meshRightAlmostSplitAt z).index.obj) => S.almostSplitSkeleton.obj ((S.meshRightAlmostSplitAt z).label j)) t) h)) = CategoryTheory.CategoryStruct.comp (c ((S.meshMiddleIndexEquiv z) t)) h

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshArrowMap_isIrreducible {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {z y : Fin S.n} (a : S.MeshArrow z y) : QuotientSubmoduleEquidistribution.IsIrreducibleMorphism (S.meshArrowMap a)

Every displayed quiver arrow represents an irreducible module morphism.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshArrow_lt {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) {z y : Fin S.n} (a : S.MeshArrow z y) : y < z

Reversed mesh arrows strictly lower the directed order.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.meshArrowEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) (z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) }) (y : Fin S.n) : S.MeshArrow (↑z) y ≃ S.MeshArrow y (S.rightTranslationLabel z)

A choice of pairing between the incoming arrows at a nonprojective vertex and the outgoing arrows from its AR translate. Its existence is the right/left occurrence-basis theorem for rad/rad².

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.rightMeshData {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [IsAlgClosed k] (H : S.HasAcyclicNonzeroNonisomorphisms) : MeshCategory.RightMeshData (Fin S.n)

The concrete right-translation-quiver data of the selected module skeleton.