Fully faithful realization by standard-form graded modules #
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedFunctor
{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)
(Graded.FiniteGradedModule (S.standardFormOppositeAlgebraGrading ⋯))
The graded generator realization, retaining all underlying module maps.
Instances For
instance
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instAdditiveMat_StandardFormMeshCategoryFiniteGradedModuleMulOppositeStandardFormAlgebraStandardFormOppositeAlgebraGradingStandardFormGradedFunctor
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
:
S.standardFormGradedFunctor.Additive
instance
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instLinearMat_StandardFormMeshCategoryFiniteGradedModuleMulOppositeStandardFormAlgebraStandardFormOppositeAlgebraGradingStandardFormGradedFunctor
{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.standardFormGradedFunctor
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormGradedUnderlyingNatIso
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
:
S.standardFormGradedFunctor.comp Graded.FiniteGradedModule.underlying ≅ S.standardGradedRecovery.comp
(S.standardFormProjectiveVertexModuleAlgebraEquivalence.functor.comp
(CategoryTheory.forget₂ (FinitelyGeneratedCategory (S.standardFormAlgebra ⋯))
(Category (S.standardFormAlgebra ⋯))))
Forgetting this realization agrees naturally with the established standard-form equivalence.
Instances For
instance
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instFullMat_StandardFormMeshCategoryFiniteGradedModuleMulOppositeStandardFormAlgebraStandardFormOppositeAlgebraGradingStandardFormGradedFunctor
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
:
S.standardFormGradedFunctor.Full
instance
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.instFaithfulMat_StandardFormMeshCategoryFiniteGradedModuleMulOppositeStandardFormAlgebraStandardFormOppositeAlgebraGradingStandardFormGradedFunctor
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
:
S.standardFormGradedFunctor.Faithful