Path-length gradings supplied by a standard mesh presentation

Ringel standardness identifies the category of selected indecomposable modules with the mesh category of its Auslander--Reiten quiver. This file records the strict linear presentation obtained after choosing the skeleton objects and transports the mesh path-length grading to the ambient Hom spaces.

The quotient by the deleted-object ideal is handled separately. Keeping that step separate makes the exact content of standardness visible: a compatible family of linear Hom equivalences preserving identities and composition.

structure MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [quiver : Quiver (Fin S.n)] [arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)] (T : MeshCategory.RightMeshData (Fin S.n)) : Type u

A strict linear realization of the selected indecomposable skeleton by a mesh category. It is the choice-dependent output of Ringel standardness used by the grading argument.

• homEquiv (x y : Fin S.n) : (MeshCategory.obj T x ⟶ MeshCategory.obj T y) ≃ₗ[k] S.ambientAddPoint x ⟶ S.ambientAddPoint y
• map_id (x : Fin S.n) : (self.homEquiv x x) (CategoryTheory.CategoryStruct.id (MeshCategory.obj T x)) = CategoryTheory.CategoryStruct.id (S.ambientAddPoint x)
• map_comp {x y z : Fin S.n} (f : MeshCategory.obj T x ⟶ MeshCategory.obj T y) (g : MeshCategory.obj T y ⟶ MeshCategory.obj T z) : (self.homEquiv x z) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((self.homEquiv x y) f) ((self.homEquiv y z) g)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.ofRealizationInjective {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [quiver : Quiver (Fin S.n)] [arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)] {T : MeshCategory.RightMeshData (Fin S.n)} (R : MeshCategory.Realization T S.ambientAddPoint) [R.functor.Full] (hinjective : ∀ (x y : Fin S.n), Function.Injective fun (f : MeshCategory.obj T x ⟶ MeshCategory.obj T y) => R.functor.map f) : S.StandardMeshPresentation T

A full linear realization which is injective on every displayed Hom space is exactly a standard mesh presentation of the selected skeleton.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.ofRealization {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [quiver : Quiver (Fin S.n)] [arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)] {T : MeshCategory.RightMeshData (Fin S.n)} (R : MeshCategory.Realization T S.ambientAddPoint) [R.functor.Full] [R.functor.Faithful] : S.StandardMeshPresentation T

A full and faithful linear realization of a mesh quotient is exactly a standard mesh presentation of the selected skeleton.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.ofDirectedExact {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [quiver : Quiver (Fin S.n)] [arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)] {T : MeshCategory.RightMeshData (Fin S.n)} (R : MeshCategory.Realization T S.ambientAddPoint) [R.functor.Full] (D : R.DirectedExactData) : S.StandardMeshPresentation T

Ringel's directed target induction turns a full realization satisfying the local projective and almost-split exactness conditions into a standard mesh presentation.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.component {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [quiver : Quiver (Fin S.n)] [arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)] {T : MeshCategory.RightMeshData (Fin S.n)} (H : S.StandardMeshPresentation T) (x y : Fin S.n) (d : ℕ) : Submodule k (S.ambientAddPoint x ⟶ S.ambientAddPoint y)

The path-degree-d component transported to an ambient skeleton Hom space.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.component_isInternal {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [quiver : Quiver (Fin S.n)] [arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)] {T : MeshCategory.RightMeshData (Fin S.n)} (H : S.StandardMeshPresentation T) (x y : Fin S.n) : DirectSum.IsInternal (H.component x y)

Standardness transports the internal mesh path-length decomposition to every ambient skeleton Hom space.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.comp_mem_component {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [quiver : Quiver (Fin S.n)] [arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)] {T : MeshCategory.RightMeshData (Fin S.n)} (H : S.StandardMeshPresentation T) {x y z : Fin S.n} {i j : ℕ} {f : S.ambientAddPoint x ⟶ S.ambientAddPoint y} {g : S.ambientAddPoint y ⟶ S.ambientAddPoint z} (hf : f ∈ H.component x y i) (hg : g ∈ H.component y z j) : CategoryTheory.CategoryStruct.comp f g ∈ H.component x z (i + j)

Composition of transported homogeneous morphisms adds path degrees.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.id_mem_component_zero {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [quiver : Quiver (Fin S.n)] [arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)] {T : MeshCategory.RightMeshData (Fin S.n)} (H : S.StandardMeshPresentation T) (x : Fin S.n) : CategoryTheory.CategoryStruct.id (S.ambientAddPoint x) ∈ H.component x x 0

Ambient skeleton identities have path degree zero.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.StandardMeshPresentation.component_zero_eq_bot_of_ne {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] {S : FiniteIndecomposableSkeleton k A} [quiver : Quiver (Fin S.n)] [arrowFintype : (x y : Fin S.n) → Fintype (x ⟶ y)] {T : MeshCategory.RightMeshData (Fin S.n)} (H : S.StandardMeshPresentation T) {x y : Fin S.n} (hxy : x ≠ y) : H.component x y 0 = ⊥

Between distinct skeleton labels the transported degree-zero component vanishes.