Hom exactness for the standard-form mesh-simple resolution #
@[instance_reducible]
def
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshHomExactQuiver
{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.standardFormMeshHomExactArrowFintype
{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_hom_exact
{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)
:
∃ (b :
S.standardFormRightMeshData.contravariantRepresentableFiniteModule hP ↑z ⟶ S.standardFormRightMeshData.contravariantRepresentableFiniteModule hP x),
CategoryTheory.CategoryStruct.comp (S.standardFormRightMeshData.incomingMapFinite hP ↑z) b = h
Applying Hom(-, k(Γ)(-,x)) to the first two maps of the standard
nonprojective simple resolution is exact at the incoming coefficient term.