The quotient equivalence underlying the reverse comparison #
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantPresentationToCoherentCodualLinearEquiv
{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) ⧸ S.finiteContravariantPresentationRange K X) ≃ₗ[k] CategoryTheory.Abelian.Ext (S.finiteCovariantDefect K) (S.finiteCovariantRepresentableOnSkeleton.obj (Opposite.op X))
2
The contravariant module-presentation quotient is canonically the degree-two Ext group defining the reverse coherent dual.
Instances For
@[simp]
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteContravariantPresentationToCoherentCodualLinearEquiv_mk
{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.finiteContravariantPresentationToCoherentCodualLinearEquiv hK X) (Submodule.Quotient.mk f) = (S.finiteContravariantRepresentableToCoherentCodualLinear hK X) f