Descent of the reverse coherent-defect comparison #
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantRepresentableToCoherentCodualLinear_comp_g_zero
{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)
(b : (S.fgObj X).obj ⟶ K.X₂.obj)
:
(S.finiteContravariantRepresentableToCoherentCodualLinear hK X) (CategoryTheory.CategoryStruct.comp b K.g.hom) = 0
Maps factoring through K.X₂ have zero reverse coherent-dual class.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantRepresentableToCoherentCodual_comp_eq_zero
{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.CategoryStruct.comp
(S.finiteContravariantFunctorInclusion.map (S.finiteRestrictedContravariantRepresentableMap K.g))
(S.finiteContravariantRepresentableToCoherentCodual hK) = 0
The reverse comparison annihilates the image of the first contravariant representable.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantCokernelToCoherentCodual
{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
(S.finiteContravariantFunctorInclusion.map (S.finiteRestrictedContravariantRepresentableMap K.g)) ⟶ S.coherentCodualObj (S.finiteCovariantDefect K)
The reverse comparison descended to the ambient cokernel.