Restriction from the standard mesh to its projective vertices

The manuscript's restricted Yoneda functor factors through restriction of finite contravariant modules on the whole standard mesh. On projective-injective modules this restriction is fully faithful: both sides have finite coordinates indexed by the projective mesh vertices, and restriction identifies the corresponding dual corepresentables.

@[instance_reducible]

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRestrictionQuiver {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.standardFormRestrictionArrowFintype {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.standardFormProjectiveVertexInclusion {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.StandardFormProjectiveMeshCategory S.standardFormRightMeshData.VertexCategory

The full inclusion of projective standard-mesh vertices into the strict vertex model of the whole standard mesh.

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

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instLinearStandardFormProjectiveMeshCategoryVertexCategoryFinNStandardFormRightMeshDataStandardFormProjectiveVertexInclusion {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor.Linear k S.standardFormProjectiveVertexInclusion

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

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

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instLinearOppositeStandardFormProjectiveMeshCategoryVertexCategoryFinNStandardFormRightMeshDataOpStandardFormProjectiveVertexInclusion {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : CategoryTheory.Functor.Linear k S.standardFormProjectiveVertexInclusion.op

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormModuleRestrictionFunctor {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.StandardFormFiniteContravariantModuleCategory (CoveringHom.FiniteDimensionalModuleCategory k)

Restriction of finite contravariant modules on the whole standard mesh to the full subcategory on its projective vertices.

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

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormModuleRestriction_preservesKernel {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {X Y : S.StandardFormFiniteContravariantModuleCategory} (f : X ⟶ Y) : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) S.standardFormModuleRestrictionFunctor

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRestrictedRepresentableIso {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.standardFormModuleRestrictionFunctor.obj (S.standardFormRightMeshData.contravariantRepresentableFiniteModule ⋯ x) ≅ (S.standardFormRestrictedYonedaFunctor ⋯).obj (MeshCategory.obj S.standardFormRightMeshData x)

Restricting the whole-mesh representable at x gives the manuscript's restricted representable module at x.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveMeshFiniteDualCorepresentables {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : S.StandardFormProjectiveMeshCategoryᵒᵖ) : CoveringHom.IsFiniteDimensionalModule k (CoveringHom.dualLinearYonedaLinearModule X)

Dual corepresentables on the projective standard-mesh subcategory are finite-dimensional modules.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveDualSourceFunctor {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.StandardFormProjectiveMeshCategory S.StandardFormFiniteContravariantModuleCategory

The projective vertices parameterize the projective-injective coordinate modules on the whole standard mesh.

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

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

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveDualTargetFunctor {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.StandardFormProjectiveMeshCategory (CoveringHom.FiniteDimensionalModuleCategory k)

The projective vertices also parameterize the injective coordinate modules over the projective full subcategory.

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

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

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRestrictedProjectiveDualIso {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) : S.standardFormModuleRestrictionFunctor.obj (CoveringHom.finiteDimensionalDualLinearYoneda (S.standardFormOppositeVertex ↑p) ⋯) ≅ CoveringHom.finiteDimensionalDualLinearYoneda (Opposite.op p) ⋯

Restriction identifies a whole-mesh projective-injective coordinate D Hom(p,-) with the corresponding dual corepresentable on the projective full subcategory.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveDualRestrictionNatIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormProjectiveDualSourceFunctor.comp S.standardFormModuleRestrictionFunctor ≅ S.standardFormProjectiveDualTargetFunctor

The coordinatewise restriction isomorphisms are natural in the projective vertex.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormModuleRestriction_injective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (I : S.StandardFormFiniteContravariantModuleCategory) [CategoryTheory.Projective I] [CategoryTheory.Injective I] : CategoryTheory.Injective (S.standardFormModuleRestrictionFunctor.obj I)

Restriction carries every projective-injective whole-mesh module to an injective module on the projective full subcategory.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveInjectiveRestrictionFunctor {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) (CategoryTheory.InjectiveObject (CoveringHom.FiniteDimensionalModuleCategory k))

Restriction, with its injectivity property recorded in the codomain.

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

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveInjectiveCoordinateFunctor {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.StandardFormProjectiveMeshCategory (CategoryTheory.ProjectiveInjectiveObject S.StandardFormFiniteContravariantModuleCategory)

Projective vertices as projective-injective coordinate objects on the whole standard mesh.

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

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

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormInjectiveCoordinateFunctor {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.StandardFormProjectiveMeshCategory (CategoryTheory.InjectiveObject (CoveringHom.FiniteDimensionalModuleCategory k))

Projective vertices as injective coordinate objects over the projective full subcategory.

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

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

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveInjectiveCoordinateRestrictionNatIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) : S.standardFormProjectiveInjectiveCoordinateFunctor.comp S.standardFormProjectiveInjectiveRestrictionFunctor ≅ S.standardFormInjectiveCoordinateFunctor

Restriction identifies the projective-injective and injective coordinate functors.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveInjectiveCoordinateFunctor_nonempty {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (I : CategoryTheory.ProjectiveInjectiveObject S.StandardFormFiniteContravariantModuleCategory) : ∃ (n : ℕ) (p : Fin n → S.StandardFormProjectiveMeshCategory), Nonempty ((⨁ fun (i : Fin n) => S.standardFormProjectiveInjectiveCoordinateFunctor.obj (p i)) ≅ I)

Every projective-injective whole-mesh module has finite coordinates in the lifted projective-injective coordinate functor.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveInjectiveCoordinate_map_surjective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p q : S.StandardFormProjectiveMeshCategory) : Function.Surjective fun (f : S.standardFormProjectiveInjectiveCoordinateFunctor.obj p ⟶ S.standardFormProjectiveInjectiveCoordinateFunctor.obj q) => S.standardFormProjectiveInjectiveRestrictionFunctor.map f

Restriction is surjective on morphisms between projective-injective coordinate objects.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveInjectiveCoordinate_map_injective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p q : S.StandardFormProjectiveMeshCategory) : Function.Injective fun (f : S.standardFormProjectiveInjectiveCoordinateFunctor.obj p ⟶ S.standardFormProjectiveInjectiveCoordinateFunctor.obj q) => S.standardFormProjectiveInjectiveRestrictionFunctor.map f

Restriction is injective on morphisms between projective-injective coordinate objects.

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

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

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

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