The coherent dual of an exact contravariant defect

The descended comparison is pointwise bijective, hence a natural isomorphism. Composing with preservation of the cokernel by the finite functor-category inclusion identifies the coherent dual of an exact contravariant defect with its covariant defect.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantCokernelToCoherentDual_π_app_apply {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] {K : CategoryTheory.ShortComplex FG} (hK : K.ShortExact) (X : S.IndecCategory) (f : K.X₁.obj ⟶ (S.fgObj X).obj) : (CategoryTheory.ConcreteCategory.hom ((S.finiteCovariantCokernelToCoherentDual hK).app X)) ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Limits.cokernel.π (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.comparisonSourceMap✝ S K)).app X)) f) = (S.finiteCovariantRepresentableToCoherentDualLinear hK X) f

The descended comparison agrees with the quotient equivalence after the cokernel projection.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantCokernelToCoherentDual_app_surjective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] {K : CategoryTheory.ShortComplex FG} (hK : K.ShortExact) (X : S.IndecCategory) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((S.finiteCovariantCokernelToCoherentDual hK).app X))

Every component of the descended comparison is surjective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantCokernelToCoherentDual_app_injective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] {K : CategoryTheory.ShortComplex FG} (hK : K.ShortExact) (X : S.IndecCategory) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((S.finiteCovariantCokernelToCoherentDual hK).app X))

Every component of the descended comparison is injective.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantCokernelToCoherentDual_app_isIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] {K : CategoryTheory.ShortComplex FG} (hK : K.ShortExact) (X : S.IndecCategory) : CategoryTheory.IsIso ((S.finiteCovariantCokernelToCoherentDual hK).app X)

Each component of the descended comparison is an isomorphism.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantCokernelCoherentDualIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] {K : CategoryTheory.ShortComplex FG} (hK : K.ShortExact) : CategoryTheory.Limits.cokernel (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.comparisonSourceMap✝ S K) ≅ S.coherentDualObj (S.finiteContravariantDefect K)

The ambient cokernel of the covariant presentation is the coherent dual.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefectCoherentDualIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt FG] [CategoryTheory.HasExt S.FiniteContravariantFunctor] {K : CategoryTheory.ShortComplex FG} (hK : K.ShortExact) : S.finiteCovariantFunctorInclusion.obj (S.finiteCovariantDefect K) ≅ S.coherentDualObj (S.finiteContravariantDefect K)

Auslander's pointwise coherent dual of an exact contravariant defect is naturally isomorphic to the corresponding covariant defect.