The indecomposable skeleton of the standard-form algebra

The restricted-Yoneda recovery equivalence identifies the original standard mesh vertices with a duplicate-free complete family of modules on the projective vertices. The finite-category algebra equivalence then transports that literal Fin S.n family to the standard-form algebra.

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormAlgebraSkeletonQuiver {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.standardFormAlgebraSkeletonArrowFintype {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)

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveVertexModuleIndecomposableSkeleton {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CoveringHom.FiniteDimensionalModuleIndecomposableSkeleton

The restricted-Yoneda images of the standard-mesh vertices form a duplicate-free complete skeleton of modules on the projective vertices.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveRestrictedYonedaIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.StandardFormProjectiveVertex) : CoveringHom.finiteDimensionalLinearCoyoneda (Opposite.op (have this := p; this)) ⋯ ≅ S.standardFormProjectiveVertexModuleIndecomposableSkeleton.obj ↑p

At a projective mesh vertex, restricted Yoneda is the corresponding representable module on the projective full subcategory.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveVertexModule_projective_of_original {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) (hi : CategoryTheory.Projective (S.fgObj i)) : CategoryTheory.Projective (S.standardFormProjectiveVertexModuleIndecomposableSkeleton.obj i)

Every original projective vertex remains projective in the recovered module category on the standard-form projective vertices.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveVertexModule_projective_iff_original {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) : CategoryTheory.Projective (S.standardFormProjectiveVertexModuleIndecomposableSkeleton.obj i) ↔ CategoryTheory.Projective (S.fgObj i)

Restricted Yoneda preserves and reflects the original projective vertex set. Reflection uses the nonsplit epic incoming mesh at every nonprojective vertex.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveVertexModuleAlgebraEquivalence {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.StandardFormProjectiveVertexModuleCategory ≌ FinitelyGeneratedCategory (S.standardFormAlgebra ⋯)

The finite-category projective-generator equivalence for the projective vertex category of the standard mesh.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instAdditiveStandardFormProjectiveVertexModuleCategoryFinitelyGeneratedCategoryStandardFormAlgebraFunctorStandardFormProjectiveVertexModuleAlgebraEquivalence {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormProjectiveVertexModuleAlgebraEquivalence.functor.Additive

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormAlgebraIndecomposableSkeleton {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : FiniteIndecomposableSkeleton k (S.standardFormAlgebra ⋯)

The standard-form algebra has a duplicate-free complete indecomposable skeleton indexed by the original Auslander--Reiten vertices.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormAlgebraSkeleton_projective_iff_original {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (i : Fin S.n) : CategoryTheory.Projective (S.standardFormAlgebraIndecomposableSkeleton.fgObj i) ↔ CategoryTheory.Projective (S.fgObj i)

The standard-form algebra skeleton has exactly the original projective labels.