Riedtmann conditions for the standard-form mesh category

This file descends the covering properties of the normalized universal realization to the standard-form mesh category. The first step compares its Hom spaces with the corresponding Hom spaces between the chosen indecomposable modules by reindexing the common fibres of the universal mesh projection and the normalized realization.

@[instance_reducible]

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

@[instance_reducible]

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

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.UniversalCover.SourceCategory {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) : Type

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.UniversalCover.meshProjection {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) : CategoryTheory.Functor (MeshCategory.RawCategory (MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀)) (MeshCategory.RawCategory S.standardFormRightMeshData)

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.UniversalCover.realization {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) : CategoryTheory.Functor (MeshCategory.RawCategory (MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀)) S.FGIndecCategory

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.UniversalCover.projectedIncomingArrow {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) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (d : Quiver.Star W) : MeshCategory.RightMeshData.IncomingArrow W.fst

The base incoming arrow underlying an incoming arrow at a universal-cover vertex.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.UniversalCover.meshProjection_map_incomingArrowHom {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) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (d : Quiver.Star W) : (meshProjection S x₀).map ((MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀).incomingArrowHom d) = S.standardFormRightMeshData.incomingArrowHom (projectedIncomingArrow S x₀ W d)

The universal mesh projection sends an incoming represented arrow to its underlying incoming represented arrow downstairs.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.UniversalCover.targetFiberEquiv {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) : LinearCovering.Fiber (meshProjection S x₀) (MeshCategory.obj S.standardFormRightMeshData y) ≃ LinearCovering.Fiber (realization S x₀) y

The two universal coverings have the same fibre over a base vertex: both conditions say that the underlying universal-cover vertex has that base label.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.UniversalCover.targetFiberHomReindexLinearEquiv {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) (X : SourceCategory S x₀) (y : Fin S.n) : (DirectSum (LinearCovering.Fiber (meshProjection S x₀) (MeshCategory.obj S.standardFormRightMeshData y)) fun (Z : LinearCovering.Fiber (meshProjection S x₀) (MeshCategory.obj S.standardFormRightMeshData y)) => X ⟶ ↑Z) ≃ₗ[k] DirectSum (LinearCovering.Fiber (realization S x₀) y) fun (Z : LinearCovering.Fiber (realization S x₀) y) => X ⟶ ↑Z

Reindex the fixed-source direct sum from the fibre of the universal mesh projection to the fibre of the normalized realization.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.UniversalCover.targetFiberHomReindexLinearEquiv_targetFiberLof {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) (X : SourceCategory S x₀) (y : Fin S.n) (Z : LinearCovering.Fiber (meshProjection S x₀) (MeshCategory.obj S.standardFormRightMeshData y)) (f : X ⟶ ↑Z) : (targetFiberHomReindexLinearEquiv S x₀ X y) ((LinearCovering.targetFiberLof (meshProjection S x₀) X (MeshCategory.obj S.standardFormRightMeshData y) Z) f) = (LinearCovering.targetFiberLof (realization S x₀) X y ((targetFiberEquiv S x₀ y) Z)) f

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.UniversalCover.targetFiberHomReindexLinearEquiv_targetFiberPrecomp {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) {X' X : SourceCategory S x₀} (e : X' ⟶ X) (a : DirectSum (LinearCovering.Fiber (meshProjection S x₀) (MeshCategory.obj S.standardFormRightMeshData y)) fun (Z : LinearCovering.Fiber (meshProjection S x₀) (MeshCategory.obj S.standardFormRightMeshData y)) => X ⟶ ↑Z) : (targetFiberHomReindexLinearEquiv S x₀ X' y) ((LinearCovering.targetFiberPrecomp (meshProjection S x₀) (MeshCategory.obj S.standardFormRightMeshData y) e) a) = (LinearCovering.targetFiberPrecomp (realization S x₀) y e) ((targetFiberHomReindexLinearEquiv S x₀ X y) a)

Fibre reindexing commutes with precomposition by a morphism in the common universal source category.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.UniversalCover.sourceFiberHomReindexLinearEquiv {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ x : Fin S.n) (Y : SourceCategory S x₀) : (DirectSum (LinearCovering.Fiber (meshProjection S x₀) (MeshCategory.obj S.standardFormRightMeshData x)) fun (Z : LinearCovering.Fiber (meshProjection S x₀) (MeshCategory.obj S.standardFormRightMeshData x)) => ↑Z ⟶ Y) ≃ₗ[k] DirectSum (LinearCovering.Fiber (realization S x₀) x) fun (Z : LinearCovering.Fiber (realization S x₀) x) => ↑Z ⟶ Y

Reindex the fixed-target direct sum from the fibre of the universal mesh projection to the fibre of the normalized realization.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.UniversalCover.sourceFiberHomReindexLinearEquiv_sourceFiberLof {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ x : Fin S.n) (Y : SourceCategory S x₀) (Z : LinearCovering.Fiber (meshProjection S x₀) (MeshCategory.obj S.standardFormRightMeshData x)) (f : ↑Z ⟶ Y) : (sourceFiberHomReindexLinearEquiv S x₀ x Y) ((LinearCovering.sourceFiberLof (meshProjection S x₀) (MeshCategory.obj S.standardFormRightMeshData x) Y Z) f) = (LinearCovering.sourceFiberLof (realization S x₀) x Y ((targetFiberEquiv S x₀ x) Z)) f

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.UniversalCover.sourceFiberHomReindexLinearEquiv_sourceFiberPostcomp {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ x : Fin S.n) {Y Y' : SourceCategory S x₀} (e : Y ⟶ Y') (a : DirectSum (LinearCovering.Fiber (meshProjection S x₀) (MeshCategory.obj S.standardFormRightMeshData x)) fun (Z : LinearCovering.Fiber (meshProjection S x₀) (MeshCategory.obj S.standardFormRightMeshData x)) => ↑Z ⟶ Y) : (sourceFiberHomReindexLinearEquiv S x₀ x Y') ((LinearCovering.sourceFiberPostcomp (meshProjection S x₀) (MeshCategory.obj S.standardFormRightMeshData x) e) a) = (LinearCovering.sourceFiberPostcomp (realization S x₀) x e) ((sourceFiberHomReindexLinearEquiv S x₀ x Y) a)

Fibre reindexing commutes with postcomposition by a morphism in the common universal source category.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.UniversalCover.meshHomLinearEquivFGIndec {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) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (y : Fin S.n) : (MeshCategory.obj S.standardFormRightMeshData W.fst ⟶ MeshCategory.obj S.standardFormRightMeshData y) ≃ₗ[k] (have this := W.fst; this) ⟶ have this := y; this

Hom spaces in the base mesh category and between the corresponding chosen indecomposable modules are linearly equivalent. A lift of the source vertex is enough: the two covering equivalences then have literally the same universal Hom summands after fibre reindexing.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.UniversalCover.meshHomLinearEquivFGIndec_precomp {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) (W' W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (y : Fin S.n) (e : S.standardFormUniversalMeshObj x₀ W' ⟶ S.standardFormUniversalMeshObj x₀ W) (u : MeshCategory.obj S.standardFormRightMeshData W.fst ⟶ MeshCategory.obj S.standardFormRightMeshData y) : (meshHomLinearEquivFGIndec S x₀ W' y) (CategoryTheory.CategoryStruct.comp ((meshProjection S x₀).map e) u) = CategoryTheory.CategoryStruct.comp ((realization S x₀).map e) ((meshHomLinearEquivFGIndec S x₀ W y) u)

The Hom comparison intertwines precomposition upstairs with precomposition by the images under both coverings.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.UniversalCover.meshHomLinearEquivFGIndecFixedTarget {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ x : Fin S.n) (W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) : (MeshCategory.obj S.standardFormRightMeshData x ⟶ MeshCategory.obj S.standardFormRightMeshData W.fst) ≃ₗ[k] (have this := x; this) ⟶ have this := W.fst; this

Hom spaces with a fixed lifted target are compared through the common source fibres of the universal mesh projection and normalized realization.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.UniversalCover.meshHomLinearEquivFGIndecFixedTargetFiber {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ x j : Fin S.n) (J : LinearCovering.Fiber (realization S x₀) (have this := j; this)) : (MeshCategory.obj S.standardFormRightMeshData x ⟶ MeshCategory.obj S.standardFormRightMeshData j) ≃ₗ[k] (have this := x; this) ⟶ have this := j; this

Fixed-target Hom comparison for a target supplied directly as an object of the realization fibre. The endpoint equalities in the two coverings are transported explicitly, while the common source-fibre summands are unchanged.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.UniversalCover.meshHomLinearEquivFGIndecFixedTarget_postcomp {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ x : Fin S.n) (W W' : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (e : S.standardFormUniversalMeshObj x₀ W ⟶ S.standardFormUniversalMeshObj x₀ W') (u : MeshCategory.obj S.standardFormRightMeshData x ⟶ MeshCategory.obj S.standardFormRightMeshData W.fst) : (meshHomLinearEquivFGIndecFixedTarget S x₀ x W') (CategoryTheory.CategoryStruct.comp u ((meshProjection S x₀).map e)) = CategoryTheory.CategoryStruct.comp ((meshHomLinearEquivFGIndecFixedTarget S x₀ x W) u) ((realization S x₀).map e)

The fixed-target Hom comparison intertwines postcomposition upstairs with postcomposition by the images under both coverings.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshHomFinite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.StandardFormMeshHomFinite

The normalized universal coverings imply finite-dimensionality of every Hom space in the standard-form mesh category. For each Hom space we base the universal cover at its source vertex, so no global connectedness hypothesis is needed.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRiedtmannConditionB {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.StandardFormRiedtmannConditionB

The right almost-split sinks in the normalized universal realization descend to Riedtmann's incoming-detection condition in the standard-form mesh category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveNakayamaIndecomposable {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) : CategoryTheory.Indecomposable (projectiveNakayamaFGObj (S.fgObj p))

The Nakayama image of a projective chosen indecomposable is again indecomposable.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveNakayamaVertex {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) : Fin S.n

The skeleton label representing the Nakayama image of a projective vertex.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveNakayamaIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) : projectiveNakayamaFGObj (S.fgObj p) ≅ S.fgObj (S.standardFormProjectiveNakayamaVertex p hp)

The chosen identification of the Nakayama image with its skeleton representative.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveNakayamaHomEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) (x : Fin S.n) : (S.fgObj x ⟶ S.fgObj (S.standardFormProjectiveNakayamaVertex p hp)) ≃ₗ[k] Module.Dual k (S.fgObj p ⟶ S.fgObj x)

Nakayama--Hom duality after replacing the Nakayama image by its chosen skeleton representative.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveNakayamaPairingEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) (x : Fin S.n) : (S.fgObj p ⟶ S.fgObj x) ≃ₗ[k] Module.Dual k (S.fgObj x ⟶ S.fgObj (S.standardFormProjectiveNakayamaVertex p hp))

The transposed Nakayama--Hom equivalence, in the orientation of the composition pairing in Riedtmann condition (c).

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveNakayamaEpsilon {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) : (S.fgObj p ⟶ S.fgObj (S.standardFormProjectiveNakayamaVertex p hp)) →ₗ[k] k

The socle functional on the Hom space from a projective chosen indecomposable to its Nakayama endpoint.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveNakayamaPairingEquiv_apply {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) (x : Fin S.n) (f : S.fgObj p ⟶ S.fgObj x) (g : S.fgObj x ⟶ S.fgObj (S.standardFormProjectiveNakayamaVertex p hp)) : ((S.standardFormProjectiveNakayamaPairingEquiv p hp x) f) g = (S.standardFormProjectiveNakayamaEpsilon p hp) (CategoryTheory.CategoryStruct.comp f g)

The transposed Nakayama equivalence is literally evaluation of the socle functional on composition.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveNakayamaFGIndecPairingEquiv {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) (x : Fin S.n) : ((have this := p; this) ⟶ have this := x; this) ≃ₗ[k] Module.Dual k ((have this := x; this) ⟶ have this := S.standardFormProjectiveNakayamaVertex p hp; this)

The projective Nakayama pairing, transported to the full category on the chosen indecomposable skeleton.

@[simp]

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveNakayamaFGIndecPairingEquiv_apply {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) (x : Fin S.n) (f : (have this := p; this) ⟶ have this := x; this) (g : (have this := x; this) ⟶ have this := S.standardFormProjectiveNakayamaVertex p hp; this) : ((S.standardFormProjectiveNakayamaFGIndecPairingEquiv p hp x) f) g = (S.standardFormProjectiveNakayamaEpsilon p hp) (CategoryTheory.CategoryStruct.comp f.hom g.hom)

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveNakayamaTargetFiber_nonempty {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) : Nonempty (LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor p) (have this := S.standardFormProjectiveNakayamaVertex p hp; this))

The universal realization based at a projective vertex has a lift of its Nakayama endpoint. This is derived from the perfect pairing and the covering Hom equivalence, rather than from a global connectedness hypothesis.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveNakayamaTargetFiber {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor p) (have this := S.standardFormProjectiveNakayamaVertex p hp; this)

A chosen lift of the Nakayama endpoint in the universal realization based at the projective vertex.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshNakayamaPairingEquiv {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) (x : Fin S.n) : (MeshCategory.obj S.standardFormRightMeshData p ⟶ MeshCategory.obj S.standardFormRightMeshData x) ≃ₗ[k] Module.Dual k (MeshCategory.obj S.standardFormRightMeshData x ⟶ MeshCategory.obj S.standardFormRightMeshData (S.standardFormProjectiveNakayamaVertex p hp))

The pointwise perfect pairing on the standard-form mesh category obtained by transporting the projective Nakayama pairing through the two covering Hom comparisons. Identifying this transported pairing with evaluation on composition by one functional is the remaining descent step for Riedtmann condition (c).

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshNakayamaPairingEquiv_bijective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) (x : Fin S.n) : Function.Bijective ⇑(S.standardFormMeshNakayamaPairingEquiv p hp x)

In particular, the transported mesh pairing is bijective at every intermediate vertex.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveNakayamaLinearModuleIso {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) : CoveringHom.linearCoyonedaLinearModule (have this := p; this) ≅ CoveringHom.dualLinearYonedaLinearModule (have this := S.standardFormProjectiveNakayamaVertex p hp; this)

The projective Nakayama pairings assemble naturally in the variable object. This is the module-valued form of the perfect composition pairing needed for Riedtmann condition (c).

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalTargetFiberHomFinite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (X : S.FGIndecCategory) (Y : UniversalCover.SourceCategory S p) : {J : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor p) X | Nontrivial (Y ⟶ ↑J)}.Finite

For a fixed target downstairs, only finitely many objects in its fibre receive a nonzero morphism from any fixed universal-cover object. This is a formal consequence of the covering Hom equivalence and finite-dimensionality of Hom spaces between finitely generated modules.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMeshHomFinite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (X Y : UniversalCover.SourceCategory S p) : FiniteDimensional k (X ⟶ Y)

Every Hom space in the normalized universal mesh category is finite-dimensional. A single upstairs summand embeds in the covering direct sum, which is equivalent to a Hom space between finitely generated modules.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMeshProjectionSourceFiberHomFinite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (X : S.StandardFormMeshCategory) (Y : UniversalCover.SourceCategory S p) : {I : LinearCovering.Fiber (UniversalCover.meshProjection S p) X | Nontrivial (↑I ⟶ Y)}.Finite

For a fixed target upstairs, only finitely many objects in a source fibre of the canonical universal mesh projection have a nonzero morphism to it.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMeshProjectionSourceFiberDualHomFinite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (X : S.StandardFormMeshCategory) (Y : UniversalCover.SourceCategory S p) : {I : LinearCovering.Fiber (UniversalCover.meshProjection S p) X | Nontrivial (Module.Dual k (↑I ⟶ Y))}.Finite

The same source-fibre finiteness holds after taking coefficient duals.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalDeckShiftDualHomFinite {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (J Y : UniversalCover.SourceCategory S p) : have D := MeshCategory.RightMeshData.UniversalCover.deckMeshCoherentDeckShift S.standardFormRightMeshData p; {b : Additive (MeshCategory.RightMeshData.UniversalCover.FundamentalGroup S.standardFormRightMeshData p) | Nontrivial (Module.Dual k ((CategoryTheory.shiftFunctor (UniversalCover.SourceCategory S p) b).obj Y ⟶ J))}.Finite

For one universal target, only finitely many deck shifts of any source have a nontrivial coefficient-dual Hom into that target.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalMeshEndLocal {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (X : UniversalCover.SourceCategory S p) : IsLocalRing (CategoryTheory.End X)

Every vertex of the normalized universal mesh category has a local endomorphism ring.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalBaseSourceFiber {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor p) (have this := p; this)

The distinguished base lift as an object of the projective source fibre.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNakayamaFiberSumIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) : LinearCovering.sourceFiberRepresentableLinearModule (S.standardFormUniversalIndecMeshFunctor p) (have this := p; this) ≅ LinearCovering.targetFiberDualCorepresentableLinearModule (S.standardFormUniversalIndecMeshFunctor p) (have this := S.standardFormProjectiveNakayamaVertex p hp; this)

Pulling the projective Nakayama isomorphism to the normalized universal cover and applying the two fixed-fibre covering decompositions gives the natural direct-sum isomorphism used in the Bongartz--Gabriel summand argument.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNakayamaSummandIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) : ∃ (J : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor p) (have this := S.standardFormProjectiveNakayamaVertex p hp; this)), Nonempty (CoveringHom.linearCoyonedaLinearModule ↑(S.standardFormUniversalBaseSourceFiber p) ≅ CoveringHom.dualLinearYonedaLinearModule ↑J)

The local-ring finite-support argument isolates the distinguished base representable as one dual-corepresentable summand over the Nakayama target fibre.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormUniversalNakayamaShiftOrbitSummandIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) : let D := MeshCategory.RightMeshData.UniversalCover.deckMeshCoherentDeckShift S.standardFormRightMeshData p; ∃ (J : LinearCovering.Fiber (S.standardFormUniversalIndecMeshFunctor p) (have this := S.standardFormProjectiveNakayamaVertex p hp; this)), Nonempty (CoveringHom.linearCoyonedaLinearModule (have this := ↑(S.standardFormUniversalBaseSourceFiber p); this) ≅ CoveringHom.dualLinearYonedaLinearModule (have this := ↑J; this))

The isolated universal Nakayama summand descends through the deck-shift orbit. The representable comparison is unconditional, while the dual corepresentable comparison uses the finite deck support proved above.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRiedtmannProjectiveDualityData {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : Fin S.n) (hp : CategoryTheory.Projective (S.fgObj p)) : S.StandardFormRiedtmannProjectiveDualityData p

The descended Nakayama summand supplies Riedtmann's perfect composition pairing at a projective vertex. On the component of the base lift this is the fully faithful image of the orbit pairing; outside that component both Hom spaces vanish by the empty-fibre covering decompositions.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRiedtmannConditionC {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.StandardFormRiedtmannConditionC

Riedtmann condition (c) for the standard-form mesh category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRiedtmannConditions {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.StandardFormRiedtmannConditions

All three Riedtmann inputs for the standard-form mesh category.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRestrictedYonedaFunctor_faithful {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : (S.standardFormRestrictedYonedaFunctor ⋯).Faithful

The standard-form restricted Yoneda realization is faithful. This is the first recovery consequence of the completed Riedtmann conditions.