Descent of the coherent-defect comparison #
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantRepresentableToCoherentDualLinear_comp_f_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 FG]
[CategoryTheory.HasExt S.FiniteContravariantFunctor]
{K : CategoryTheory.ShortComplex FG}
(hK : K.ShortExact)
(X : S.IndecCategory)
(b : K.X₂.obj ⟶ (S.fgObj X).obj)
:
(S.finiteCovariantRepresentableToCoherentDualLinear hK X) (CategoryTheory.CategoryStruct.comp K.f.hom b) = 0
Maps extending across K.X₂ have zero coherent-dual class.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantRepresentableToCoherentDual_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 FG]
[CategoryTheory.HasExt S.FiniteContravariantFunctor]
{K : CategoryTheory.ShortComplex FG}
(hK : K.ShortExact)
:
CategoryTheory.CategoryStruct.comp
(S.finiteCovariantFunctorInclusion.map (S.finiteRestrictedCovariantRepresentableMap K.f))
(S.finiteCovariantRepresentableToCoherentDual hK) = 0
The comparison annihilates the image of the second covariant representable.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantCokernelToCoherentDual
{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
(S.finiteCovariantFunctorInclusion.map (S.finiteRestrictedCovariantRepresentableMap K.f)) ⟶ S.coherentDualObj (S.finiteContravariantDefect K)
The canonical comparison descended to the ambient cokernel.