Homogeneous ideals generated by path-category relations

If the specified relation generators in a free linear path category are homogeneous for path length, then the two-sided linear Hom ideal that they generate is homogeneous. Arbitrary multipliers are expanded in the path bases on the two sides.

def MagnitudeConjecture.LinearPathCategory.basisCompositeSet {k : Type u} [Field k] {Q : Type v} [Quiver Q] (R : (X Y : Category k Q) → Set (X ⟶ Y)) (X Y : Category k Q) : Set (X ⟶ Y)

Two-sided composites of a relation generator with path-basis morphisms on both sides.

theorem MagnitudeConjecture.LinearPathCategory.basisCompositeSet_subset_twoSidedCompositeSet {k : Type u} [Field k] {Q : Type v} [Quiver Q] (R : (X Y : Category k Q) → Set (X ⟶ Y)) (X Y : Category k Q) : basisCompositeSet R X Y ⊆ QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.twoSidedCompositeSet R X Y

theorem MagnitudeConjecture.LinearPathCategory.twoSidedComposite_mem_span_basisCompositeSet {k : Type u} [Field k] {Q : Type v} [Quiver Q] (R : (X Y : Category k Q) → Set (X ⟶ Y)) {X Y A B : Category k Q} {r : A ⟶ B} (hr : r ∈ R A B) (a : X ⟶ A) (b : B ⟶ Y) : CategoryTheory.CategoryStruct.comp a (CategoryTheory.CategoryStruct.comp r b) ∈ Submodule.span k (basisCompositeSet R X Y)

Every composite with arbitrary morphisms on the two sides is in the span of composites whose side factors are path-basis morphisms.

theorem MagnitudeConjecture.LinearPathCategory.generatedHomSubmodule_eq_span_basisCompositeSet {k : Type u} [Field k] {Q : Type v} [Quiver Q] (R : (X Y : Category k Q) → Set (X ⟶ Y)) (X Y : Category k Q) : QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k R X Y = Submodule.span k (basisCompositeSet R X Y)

The usual generated Hom submodule can be presented using path-basis multipliers only.

theorem MagnitudeConjecture.LinearPathCategory.basisCompositeSet_isHomogeneous {k : Type u} [Field k] {Q : Type v} [Quiver Q] (R : (X Y : Category k Q) → Set (X ⟶ Y)) (hR : ∀ (A B : Category k Q), ∀ r ∈ R A B, ∃ (n : ℕ), r ∈ lengthComponent A B n) {X Y : Category k Q} {f : X ⟶ Y} (hf : f ∈ basisCompositeSet R X Y) : ∃ (n : ℕ), f ∈ lengthComponent X Y n

@[instance_reducible]

noncomputable def MagnitudeConjecture.LinearPathCategory.lengthDecomposition {k : Type u} [Field k] {Q : Type v} [Quiver Q] (X Y : Category k Q) : DirectSum.Decomposition (lengthComponent X Y)

theorem MagnitudeConjecture.LinearPathCategory.linearSpan_hom_isHomogeneous {k : Type u} [Field k] {Q : Type v} [Quiver Q] (R : (X Y : Category k Q) → Set (X ⟶ Y)) (hR : ∀ (A B : Category k Q), ∀ r ∈ R A B, ∃ (n : ℕ), r ∈ lengthComponent A B n) (X Y : Category k Q) : DirectSum.SetLike.IsHomogeneous (lengthComponent X Y) ((QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.linearSpan k R).hom X Y)

A two-sided Hom ideal generated by path-length-homogeneous relations is homogeneous in every Hom space.