Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleCoherentCodefectCoyonedaQuotient

Restricted covariant Yoneda and the reverse presentation quotient #

Restricted covariant Yoneda carries the ordinary module coboundaries in a covariant-defect presentation onto the corresponding natural-transformation coboundaries. It therefore descends to the quotient computing reverse coherent duality.

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefectPresentationRange_map_coyoneda {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) (X : S.IndecCategory) :
Submodule.map (↑(S.ambientFiniteRestrictedCovariantRepresentableHomLinearEquiv K.X₃ X)) (S.finiteContravariantPresentationRange K X) = ProjectivePresentationExt.presentationRange (S.finiteCovariantDefectLeftShortComplex K) (S.finiteCovariantRepresentableOnSkeleton.obj (Opposite.op X))

Restricted covariant Yoneda identifies the two presentation ranges.

source
noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefectPresentationCoyonedaLinearEquiv {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) (X : S.IndecCategory) :
(((S.fgObj X).obj ⟶ K.X₃.obj) ⧸ S.finiteContravariantPresentationRange K X) ≃ₗ[k] ((S.finiteCovariantDefectLeftShortComplex K).X₁ ⟶ S.finiteCovariantRepresentableOnSkeleton.obj (Opposite.op X)) ⧸ ProjectivePresentationExt.presentationRange (S.finiteCovariantDefectLeftShortComplex K) (S.finiteCovariantRepresentableOnSkeleton.obj (Opposite.op X))

The module presentation quotient and the corresponding quotient of natural-transformation spaces are canonically linearly equivalent.

Instances For
    source
    @[simp]
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finiteCovariantDefectPresentationCoyonedaLinearEquiv_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) (X : S.IndecCategory) (f : (S.fgObj X).obj ⟶ K.X₃.obj) :
    (S.finiteCovariantDefectPresentationCoyonedaLinearEquiv K X) (Submodule.Quotient.mk f) = Submodule.Quotient.mk (S.finiteRestrictedCovariantRepresentableMap (CategoryTheory.ObjectProperty.homMk f))