Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardGradedRecovery

Realization of the graded mesh generator by restricted Yoneda #

source
instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRestrictedYonedaLinear {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.standardFormRestrictedYonedaFunctor ⋯)
source
noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardGradedRecovery {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.Mat_ S.StandardFormMeshCategory) S.StandardFormProjectiveVertexModuleCategory

Restricted Yoneda on the raw mesh additive envelope used by the grading.

Instances For
    source
    instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instAdditiveMat_StandardFormMeshCategoryStandardFormProjectiveVertexModuleCategoryStandardGradedRecovery {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
    S.standardGradedRecovery.Additive
    source
    instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instLinearMat_StandardFormMeshCategoryStandardFormProjectiveVertexModuleCategoryStandardGradedRecovery {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.standardGradedRecovery
    source
    instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instFullMat_StandardFormMeshCategoryStandardFormProjectiveVertexModuleCategoryStandardGradedRecovery {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
    S.standardGradedRecovery.Full
    source
    instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instFaithfulMat_StandardFormMeshCategoryStandardFormProjectiveVertexModuleCategoryStandardGradedRecovery {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
    S.standardGradedRecovery.Faithful
    source
    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardGradedRecoverySingletonIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : S.StandardFormMeshCategory) :
    S.standardGradedRecovery.obj ((CategoryTheory.Mat_.embedding S.StandardFormMeshCategory).obj X) ≅ (S.standardFormRestrictedYonedaFunctor ⋯).obj X

    The realization of a singleton is its original restricted Yoneda module.

    Instances For
      source
      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardGradedRecoveryProjectiveIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (p : S.StandardFormProjectiveMeshCategory) :
      S.standardGradedRecovery.obj (S.standardGradedProjectiveFamily p) ≅ CoveringHom.finiteDimensionalLinearCoyoneda (Opposite.op p) ⋯

      Each projective singleton realizes the corresponding representable.

      Instances For
        source
        noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardGradedRecoveryGeneratorIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
        S.standardGradedRecovery.obj (⨁ S.standardGradedProjectiveFamily) ≅ CoveringHom.finiteCategoryProjectiveGenerator ⋯

        The mesh projective sum realizes the category-algebra projective generator.

        Instances For
          source
          noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardGradedRecoveryEndEquiv {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
          CategoryTheory.End (⨁ S.standardGradedProjectiveFamily) ≃ₐ[k] S.standardFormAlgebra ⋯

          Algebra comparison induced directly by restricted Yoneda realization.

          Instances For
            source
            noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardGradedRecoveryModuleEquiv {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (X : CategoryTheory.Mat_ S.StandardFormMeshCategory) :
            (⨁ S.standardGradedProjectiveFamily ⟶ X) ≃ₗ[S.StandardGradedGeneratorAlgebra] CoveringHom.finiteCategoryProjectiveGenerator ⋯ ⟶ S.standardGradedRecovery.obj X

            The graded construction and restricted Yoneda have the same represented right modules, with scalars transported by the realized algebra comparison.

            Instances For