Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleCoherentCoduality

The reverse coherent dual on the finite right-module skeleton #

For a finite covariant functor G, the reverse coherent dual is

X ↦ Ext²(G, Hom(X, -)).

Its exact-presentation calculation will recover the corresponding contravariant defect and provide the inverse half of Auslander's duality.

source
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantRepresentableOnSkeleton {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
CategoryTheory.Functor S.IndecCategoryᵒᵖ S.FiniteCovariantFunctor

Restricted covariant representables, contravariantly functorial in the chosen representing indecomposable.

Instances For
    source
    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.coherentCodualObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt S.FiniteCovariantFunctor] (G : S.FiniteCovariantFunctor) :
    CategoryTheory.Functor S.IndecCategoryᵒᵖ (ModuleCat k)

    The reverse coherent-dual expression on one finite covariant functor.

    Instances For
      source
      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.coherentCodualRaw {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt S.FiniteCovariantFunctor] :
      CategoryTheory.Functor S.FiniteCovariantFunctorᵒᵖ (CategoryTheory.Functor S.IndecCategoryᵒᵖ (ModuleCat k))

      The reverse coherent dual is contravariantly functorial in the finite covariant functor.

      Instances For