Components unaffected by the relation ideal #
theorem
MagnitudeConjecture.LinearPathCategory.pathCoefficient_eq_zero
{k : Type u}
[Field k]
{Q : Type v}
[Quiver Q]
{X Y : Category k Q}
{n : ℕ}
{f : X ⟶ Y}
(hf : f ∈ lengthComponent X Y n)
(p : Quiver.Path (vertex Y) (vertex X))
(hp : p.length ≠ n)
:
((homPathLinearEquiv X Y) f) p = 0
A homogeneous morphism has no coefficient at a path of another length.
theorem
MagnitudeConjecture.LinearPathCategory.HomogeneousQuotient.component_quotient_injective
{k : Type u}
[Field k]
{Q : Type v}
[Quiver Q]
(R : (X Y : Category k Q) → Set (X ⟶ Y))
(X Y : Category k Q)
(n : ℕ)
(hR : ∀ f ∈ basisCompositeSet R X Y, ∃ (m : ℕ), m ≠ n ∧ f ∈ LinearPathCategory.lengthComponent X Y m)
:
Function.Injective ⇑((quotientHomLinearMap R X Y).submoduleMap (LinearPathCategory.lengthComponent X Y n))
If every path-basis composite of a relation avoids degree n, the quotient map is injective on that degree.
noncomputable def
MagnitudeConjecture.LinearPathCategory.HomogeneousQuotient.componentEquiv
{k : Type u}
[Field k]
{Q : Type v}
[Quiver Q]
(R : (X Y : Category k Q) → Set (X ⟶ Y))
(X Y : Category k Q)
(n : ℕ)
(hR : ∀ f ∈ basisCompositeSet R X Y, ∃ (m : ℕ), m ≠ n ∧ f ∈ LinearPathCategory.lengthComponent X Y m)
:
↥(LinearPathCategory.lengthComponent X Y n) ≃ₗ[k] ↥(lengthComponent R X Y n)
A degree avoided by all relation composites survives unchanged.