Path evaluation and powers of a Hom ideal #
Evaluating a path whose displayed arrows lie in a two-sided Hom ideal gives a morphism in the power indexed by the path length.
theorem
MagnitudeConjecture.LinearPathCategory.pathMap_mem_ideal_pow
{Q : Type v}
[Quiver Q]
{C : Type z}
[CategoryTheory.Category.{u_1, z} C]
[CategoryTheory.Preadditive C]
(F₀ : Q → C)
(F₁ : {i j : Q} → (i ⟶ j) → (F₀ j ⟶ F₀ i))
(I : QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal C)
(hF₁ : ∀ {i j : Q} (a : i ⟶ j), F₁ a ∈ I.hom (F₀ j) (F₀ i))
{x y : Q}
(p : Quiver.Path x y)
:
Evaluating a path whose arrows lie in a Hom ideal gives a morphism in the ideal power indexed by the path length.