Directed boundary Hom bounds by finite kernels #
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finrank_rightTranslation_hom_injective_le_one
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[IsAlgClosed k]
(S : FiniteIndecomposableSkeleton k A)
(H : S.HasAcyclicNonzeroNonisomorphisms)
(z : { z : Fin S.n // ¬CategoryTheory.Projective (S.fgObj z) })
(i : Fin S.n)
[CategoryTheory.Injective (S.fgObj i)]
(hHom : ∀ (f : S.fgObj ↑z ⟶ S.fgObj i), f = 0)
:
Module.finrank k (S.fgObj (S.rightTranslationLabel z) ⟶ S.fgObj i) ≤ 1
The finite-kernel argument bounds maps from an AR translate to an indecomposable injective whenever the untranslated endpoint has no such maps.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.finrank_injective_hom_injective_le_one
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
[FiniteDimensional k A]
[IsNoetherianRing Aᵐᵒᵖ]
[IsAlgClosed k]
(S : FiniteIndecomposableSkeleton k A)
(H : S.HasAcyclicNonzeroNonisomorphisms)
(z i : Fin S.n)
[CategoryTheory.Injective (S.fgObj z)]
[CategoryTheory.Injective (S.fgObj i)]
:
The injective-source case of the same boundary bound.