The comparison from a covariant defect to the coherent dual #
For a short exact presentation K, a map K.X₁ → X determines a map
from the first representable in the four-term resolution to Hom(-, X).
Its presentation class and the degree-two Ext calculation define the
canonical natural map from the covariant defect to Auslander's coherent
dual.
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantRepresentableToCoherentDualLinear
{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.FiniteContravariantFunctor]
{K : CategoryTheory.ShortComplex FG}
(hK : K.ShortExact)
(X : S.IndecCategory)
:
(K.X₁.obj ⟶ (S.fgObj X).obj) →ₗ[k] CategoryTheory.Abelian.Ext (S.finiteContravariantDefect K) (S.finiteContravariantRepresentableOnSkeleton.obj X) 2
The comparison before quotienting the covariant representable.
Instances For
@[simp]
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantRepresentableToCoherentDualLinear_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)
:
(S.finiteCovariantRepresentableToCoherentDualLinear hK X) f = (S.finiteContravariantDefectPresentationLinearEquiv hK X)
(Submodule.Quotient.mk (S.finiteRestrictedContravariantRepresentableMap (CategoryTheory.ObjectProperty.homMk f)))