Evaluation of the named Yoneda coefficient #
@[instance_reducible]
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshHomCoordinateNamedEvaluationQuiver
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
:
Quiver (Fin S.n)
Instances For
@[instance_reducible]
noncomputable def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshHomCoordinateNamedEvaluationArrowFintype
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(x y : Fin S.n)
:
Fintype (x ⟶ y)
Instances For
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSimpleResolutionYonedaCoefficientMap_eq_finiteCoordinate
{k A : Type u}
[Field k]
[IsAlgClosed k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
(S : FiniteIndecomposableSkeleton k A)
(hP : S.standardFormRightMeshData.FiniteContravariantRepresentables)
(z : { z : Fin S.n // z ∉ S.standardFormProjectiveSet })
(x : Fin S.n)
(h :
S.standardFormRightMeshData.incomingCoefficientFiniteModule hP ↑z ⟶ S.standardFormRightMeshData.contravariantRepresentableFiniteModule hP x)
(a : MeshCategory.RightMeshData.IncomingArrow ↑z)
:
S.standardFormSimpleResolutionYonedaCoefficientMap hP z x h a = S.standardFormSimpleResolutionFiniteCoordinateComposite hP z x h a
The named coefficient map is the underlying finite-module coordinate.