The reverse coherent dual of an exact covariant defect

The descended reverse comparison is pointwise bijective. Thus the reverse coherent dual of an exact covariant defect is naturally isomorphic to the corresponding contravariant defect.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantCokernelToCoherentCodual_π_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 S.FiniteCovariantFunctor] {K : CategoryTheory.ShortComplex FG} (hK : K.ShortExact) (X : S.IndecCategory) (f : (S.fgObj X).obj ⟶ K.X₃.obj) : (CategoryTheory.ConcreteCategory.hom ((S.finiteContravariantCokernelToCoherentCodual hK).app (Opposite.op X))) ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Limits.cokernel.π (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.reverseComparisonSourceMap✝ S K)).app (Opposite.op X))) f) = (S.finiteContravariantRepresentableToCoherentCodualLinear hK X) f

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

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantCokernelToCoherentCodual_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 S.FiniteCovariantFunctor] {K : CategoryTheory.ShortComplex FG} (hK : K.ShortExact) (X : S.IndecCategoryᵒᵖ) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((S.finiteContravariantCokernelToCoherentCodual hK).app X))

Every component of the descended reverse comparison is surjective.

theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantCokernelToCoherentCodual_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 S.FiniteCovariantFunctor] {K : CategoryTheory.ShortComplex FG} (hK : K.ShortExact) (X : S.IndecCategoryᵒᵖ) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((S.finiteContravariantCokernelToCoherentCodual hK).app X))

Every component of the descended reverse comparison is injective.

instance MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantCokernelToCoherentCodual_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 S.FiniteCovariantFunctor] {K : CategoryTheory.ShortComplex FG} (hK : K.ShortExact) (X : S.IndecCategoryᵒᵖ) : CategoryTheory.IsIso ((S.finiteContravariantCokernelToCoherentCodual hK).app X)

Each component of the descended reverse comparison is an isomorphism.

noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantCokernelCoherentCodualIso {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) [CategoryTheory.HasExt S.FiniteCovariantFunctor] {K : CategoryTheory.ShortComplex FG} (hK : K.ShortExact) : CategoryTheory.Limits.cokernel (MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.reverseComparisonSourceMap✝ S K) ≅ S.coherentCodualObj (S.finiteCovariantDefect K)

The ambient cokernel of the contravariant presentation is the reverse coherent dual.

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

The reverse coherent dual of an exact covariant defect is naturally isomorphic to the corresponding contravariant defect.