Auslander's coherent dual on the finite right-module skeleton

For a finite contravariant functor F, Auslander's coherent dual is the covariant functor

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

This file first constructs that expression functorially, including its contravariance in F. The subsequent exact-presentation comparison will identify its value on finiteContravariantDefect K with finiteCovariantDefect K when K is short exact.

@[reducible, inline]

abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.FiniteContravariantFunctor {k A : Type u} [Field k] [Ring A] [Algebra k A] (S : FiniteIndecomposableSkeleton k A) : Type (max u (u_1 + 1))

def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantRepresentableOnSkeleton {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.FiniteContravariantFunctor

Restricted contravariant representables, with the represented object confined to the chosen indecomposable skeleton. Naming this functor keeps the substantially larger Ext² expressions below from repeatedly unfolding the full-subcategory maps.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.coherentDualObj {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt S.FiniteContravariantFunctor] (F : S.FiniteContravariantFunctor) : CategoryTheory.Functor S.IndecCategory (ModuleCat k)

The Ext² expression defining Auslander's coherent dual of one finite contravariant functor. At this stage the codomain is the ambient functor category; finiteness will follow from an exact presentation.

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

Auslander's coherent-dual construction is contravariantly functorial in the finite contravariant functor.