Recovery from the projective vertices of the standard mesh

Restriction from finite contravariant modules on the whole standard mesh to the full subcategory on its projective vertices is an equivalence on projective objects. The proof compares the Auslander--Bongartz--Gabriel equivalence with kernel realization and uses two injective presentations to show that every target module is such a kernel.

Consequently the restricted Yoneda functor is full, and every indecomposable finite module on the projective vertices is represented by a standard-mesh vertex.

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRecoveryQuiver {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.standardFormRecoveryArrowFintype {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.StandardFormProjectiveVertexModuleCategory {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : Type (u + 1)

Finite contravariant modules on the projective vertices of the standard mesh.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveInjectiveRestrictionUnderlyingFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor (CategoryTheory.ProjectiveInjectiveObject S.StandardFormFiniteContravariantModuleCategory) S.StandardFormProjectiveVertexModuleCategory

Restriction of projective-injective whole-mesh modules, with the target injectivity witness forgotten.

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

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instFullProjectiveInjectiveObjectStandardFormFiniteContravariantModuleCategoryStandardFormProjectiveVertexModuleCategoryStandardFormProjectiveInjectiveRestrictionUnderlyingFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormProjectiveInjectiveRestrictionUnderlyingFunctor.Full

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instFaithfulProjectiveInjectiveObjectStandardFormFiniteContravariantModuleCategoryStandardFormProjectiveVertexModuleCategoryStandardFormProjectiveInjectiveRestrictionUnderlyingFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormProjectiveInjectiveRestrictionUnderlyingFunctor.Faithful

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRestrictedInjectiveKernelFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor (CategoryTheory.Preadditive.LeftFreyd (CategoryTheory.ProjectiveInjectiveObject S.StandardFormFiniteContravariantModuleCategory)) S.StandardFormProjectiveVertexModuleCategory

Kernel realization after restricting projective-injective whole-mesh modules to the projective vertices.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instFullLeftFreydProjectiveInjectiveObjectStandardFormFiniteContravariantModuleCategoryStandardFormProjectiveVertexModuleCategoryStandardFormRestrictedInjectiveKernelFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormRestrictedInjectiveKernelFunctor.Full

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instFaithfulLeftFreydProjectiveInjectiveObjectStandardFormFiniteContravariantModuleCategoryStandardFormProjectiveVertexModuleCategoryStandardFormRestrictedInjectiveKernelFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormRestrictedInjectiveKernelFunctor.Faithful

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRestrictedInjectiveKernelPresentation_nonempty {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (M : S.StandardFormProjectiveVertexModuleCategory) : Nonempty (CategoryTheory.Preadditive.LeftFreyd.KernelPresentationAlong S.standardFormProjectiveInjectiveRestrictionUnderlyingFunctor M)

Every finite module on the projective vertices has a two-term kernel presentation by restricted projective-injective whole-mesh modules.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instEssSurjLeftFreydProjectiveInjectiveObjectStandardFormFiniteContravariantModuleCategoryStandardFormProjectiveVertexModuleCategoryStandardFormRestrictedInjectiveKernelFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormRestrictedInjectiveKernelFunctor.EssSurj

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instIsEquivalenceLeftFreydProjectiveInjectiveObjectStandardFormFiniteContravariantModuleCategoryStandardFormProjectiveVertexModuleCategoryStandardFormRestrictedInjectiveKernelFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormRestrictedInjectiveKernelFunctor.IsEquivalence

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRestrictedInjectiveKernelEquivalence {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Preadditive.LeftFreyd (CategoryTheory.ProjectiveInjectiveObject S.StandardFormFiniteContravariantModuleCategory) ≌ S.StandardFormProjectiveVertexModuleCategory

The equivalence obtained by realizing formal arrows as kernels after restriction to the projective vertices.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveModuleRestrictionFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor (CategoryTheory.ProjectiveObject S.StandardFormFiniteContravariantModuleCategory) S.StandardFormProjectiveVertexModuleCategory

Restriction from projective whole-mesh modules to finite modules on the projective vertices.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormAuslanderUnderlyingNatIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormAuslanderBongartzGabrielEquivalence.functor.comp (CategoryTheory.ProjectiveObject.ι S.StandardFormFiniteContravariantModuleCategory) ≅ CategoryTheory.Preadditive.LeftFreyd.projectiveInjectiveKernelFunctor S.StandardFormFiniteContravariantModuleCategory

Forgetting the projectivity witness after the standard-form Auslander--Bongartz--Gabriel equivalence recovers its kernel realization functor.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormAuslanderRestrictionKernelNatIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormAuslanderBongartzGabrielEquivalence.functor.comp S.standardFormProjectiveModuleRestrictionFunctor ≅ S.standardFormRestrictedInjectiveKernelFunctor

The composite of the Auslander--Bongartz--Gabriel equivalence with projective restriction agrees with restricted kernel realization.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instIsEquivalenceProjectiveObjectStandardFormFiniteContravariantModuleCategoryStandardFormProjectiveVertexModuleCategoryStandardFormProjectiveModuleRestrictionFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormProjectiveModuleRestrictionFunctor.IsEquivalence

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveModuleRestrictionEquivalence {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.ProjectiveObject S.StandardFormFiniteContravariantModuleCategory ≌ S.StandardFormProjectiveVertexModuleCategory

Projective restriction as an explicit equivalence.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshVertexFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor S.StandardFormMeshCategory S.standardFormRightMeshData.VertexCategory

The strict standard-mesh category and its induced vertex category have the same objects and morphisms.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instFullStandardFormMeshCategoryVertexCategoryFinNStandardFormRightMeshDataStandardFormMeshVertexFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormMeshVertexFunctor.Full

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instFaithfulStandardFormMeshCategoryVertexCategoryFinNStandardFormRightMeshDataStandardFormMeshVertexFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormMeshVertexFunctor.Faithful

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instEssSurjStandardFormMeshCategoryVertexCategoryFinNStandardFormRightMeshDataStandardFormMeshVertexFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormMeshVertexFunctor.EssSurj

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instIsEquivalenceStandardFormMeshCategoryVertexCategoryFinNStandardFormRightMeshDataStandardFormMeshVertexFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormMeshVertexFunctor.IsEquivalence

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshRawFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor S.standardFormRightMeshData.VertexCategory S.StandardFormMeshCategory

The concrete inverse from the induced vertex category back to the strict raw standard-mesh category.

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

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instFullVertexCategoryFinNStandardFormRightMeshDataStandardFormMeshCategoryStandardFormMeshRawFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormMeshRawFunctor.Full

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instFaithfulVertexCategoryFinNStandardFormRightMeshDataStandardFormMeshCategoryStandardFormMeshRawFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormMeshRawFunctor.Faithful

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instEssSurjVertexCategoryFinNStandardFormRightMeshDataStandardFormMeshCategoryStandardFormMeshRawFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormMeshRawFunctor.EssSurj

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instIsEquivalenceVertexCategoryFinNStandardFormRightMeshDataStandardFormMeshCategoryStandardFormMeshRawFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormMeshRawFunctor.IsEquivalence

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormVertexRestrictedYonedaFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor S.standardFormRightMeshData.VertexCategory S.StandardFormProjectiveVertexModuleCategory

Restricted Yoneda written on the literal vertex model of the standard mesh.

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

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

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instFaithfulVertexCategoryFinNStandardFormRightMeshDataStandardFormProjectiveVertexModuleCategoryStandardFormVertexRestrictedYonedaFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormVertexRestrictedYonedaFunctor.Faithful

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRepresentableProjectiveFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor S.StandardFormMeshCategory (CategoryTheory.ProjectiveObject S.StandardFormFiniteContravariantModuleCategory)

A standard-mesh vertex, sent to its finite contravariant representable and bundled as a projective whole-mesh module.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instFullStandardFormMeshCategoryProjectiveObjectStandardFormFiniteContravariantModuleCategoryStandardFormRepresentableProjectiveFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormRepresentableProjectiveFunctor.Full

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instFaithfulStandardFormMeshCategoryProjectiveObjectStandardFormFiniteContravariantModuleCategoryStandardFormRepresentableProjectiveFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormRepresentableProjectiveFunctor.Faithful

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRepresentableRestrictionNatIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormRepresentableProjectiveFunctor.comp S.standardFormProjectiveModuleRestrictionFunctor ≅ S.standardFormRestrictedYonedaFunctor ⋯

Restricting the projective representable attached to a mesh vertex is the restricted Yoneda module of that vertex.

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

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instFullVertexCategoryFinNStandardFormRightMeshDataStandardFormProjectiveVertexModuleCategoryStandardFormVertexRestrictedYonedaFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormVertexRestrictedYonedaFunctor.Full

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveRestriction_indecomposable_underlying {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (P : CategoryTheory.ProjectiveObject S.StandardFormFiniteContravariantModuleCategory) (hP : CategoryTheory.Indecomposable (S.standardFormProjectiveModuleRestrictionFunctor.obj P)) : CategoryTheory.Indecomposable P.obj

If the restriction of a projective whole-mesh module is indecomposable, then its underlying whole-mesh module is indecomposable.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRestrictedYonedaFunctor_indec_dense {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (M : S.StandardFormProjectiveVertexModuleCategory) (hM : CategoryTheory.Indecomposable M) : ∃ (X : S.StandardFormMeshCategory), Nonempty ((S.standardFormRestrictedYonedaFunctor ⋯).obj X ≅ M)

Every indecomposable finite module on the projective vertices is the restricted Yoneda module of a standard-mesh vertex.

@[reducible, inline]

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

The finite additive hull of the strict standard-mesh category.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormAdditiveRestrictedYonedaFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor S.StandardFormAdditiveMeshCategory S.StandardFormProjectiveVertexModuleCategory

The additive extension of restricted Yoneda from mesh vertices to finite formal sums of mesh vertices.

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

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instFullStandardFormAdditiveMeshCategoryStandardFormProjectiveVertexModuleCategoryStandardFormAdditiveRestrictedYonedaFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormAdditiveRestrictedYonedaFunctor.Full

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instFaithfulStandardFormAdditiveMeshCategoryStandardFormProjectiveVertexModuleCategoryStandardFormAdditiveRestrictedYonedaFunctor {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormAdditiveRestrictedYonedaFunctor.Faithful

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormAdditiveRestrictedYonedaSingletonIso {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) : S.standardFormAdditiveRestrictedYonedaFunctor.obj (S.standardFormRightMeshData.additiveVertexObj x) ≅ (S.standardFormRestrictedYonedaFunctor ⋯).obj (MeshCategory.obj S.standardFormRightMeshData x)

On a singleton matrix object, additive restricted Yoneda is the original restricted Yoneda module.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormAdditiveRestrictedYonedaFunctor_essSurj {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormAdditiveRestrictedYonedaFunctor.EssSurj

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormAdditiveRestrictedYonedaFunctor_isEquivalence {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormAdditiveRestrictedYonedaFunctor.IsEquivalence

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

The finite additive hull of the standard mesh is equivalent to finite modules on its projective vertices.

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

Algebra-facing form of standard-mesh recovery: its finite additive hull is equivalent to finitely generated right modules over the standard-form category algebra.