The comparison from a contravariant defect to the coherent codual #
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantRepresentableToCoherentCodualLinear
{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)
:
((S.fgObj X).obj ⟶ K.X₃.obj) →ₗ[k] CategoryTheory.Abelian.Ext (S.finiteCovariantDefect K) (S.finiteCovariantRepresentableOnSkeleton.obj (Opposite.op X))
2
The reverse comparison before quotienting the contravariant representable.
Instances For
@[simp]
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantRepresentableToCoherentCodualLinear_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)
:
(S.finiteContravariantRepresentableToCoherentCodualLinear hK X) f = (S.finiteCovariantDefectPresentationLinearEquiv hK (Opposite.op X))
(Submodule.Quotient.mk (S.finiteRestrictedCovariantRepresentableMap (CategoryTheory.ObjectProperty.homMk f)))