The raw standard-form mesh relation #
@[instance_reducible]
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshYonedaRawRelationQuiver
{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.standardFormMeshYonedaRawRelationArrowFintype
{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_raw_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.standardFormRightMeshData.incomingArrowHom
⟨S.standardFormRightMeshData.tau z, (S.standardFormRightMeshData.arrowEquiv z a.fst) a.snd⟩)
(S.standardFormSimpleResolutionYonedaCoefficient hP z x h a).hom = 0
The reflected relation after passing from the induced category to raw mesh-category morphisms.