The reflected Yoneda mesh relation #
The generic linear-Yoneda relation lemma reflects the translation relation without repeating the finite-sum calculation for standard-form objects.
@[instance_reducible]
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshYonedaReflectedRelationQuiver
{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.standardFormMeshYonedaReflectedRelationArrowFintype
{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.standardFormSimpleResolution_yoneda_reflected_relation
{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)
(hh : CategoryTheory.CategoryStruct.comp (S.standardFormRightMeshData.translationMapFinite hP z) h = 0)
:
∑ a : MeshCategory.RightMeshData.IncomingArrow ↑z,
CategoryTheory.CategoryStruct.comp (S.standardFormSimpleResolutionPairedIncoming z a)
(S.standardFormSimpleResolutionYonedaCoefficient hP z x h a) = 0
The relation killed by the translation map reflects through the linear Yoneda embedding.