Grading a path-category quotient by homogeneous relations

A family of homogeneous relations generates a homogeneous two-sided ideal. The categorical quotient therefore inherits the path-length grading by taking the images of the source components. Composition adds degrees in the quotient, and degree zero is unchanged.

noncomputable def MagnitudeConjecture.LinearPathCategory.HomogeneousQuotient.relationIdeal {k : Type u} [Field k] {Q : Type v} [Quiver Q] (R : (X Y : Category k Q) → Set (X ⟶ Y)) : QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal (Category k Q)

The two-sided linear ideal generated by a family of path-category relations.

@[reducible, inline]

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

The raw categorical quotient by the generated relation ideal.

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.LinearPathCategory.HomogeneousQuotient.quotientFunctor {k : Type u} [Field k] {Q : Type v} [Quiver Q] (R : (X Y : Category k Q) → Set (X ⟶ Y)) : CategoryTheory.Functor (Category k Q) (CategoryTheory.Quotient (relationIdeal R).rel)

The quotient functor from the free linear path category.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.LinearPathCategory.HomogeneousQuotient.rawPreadditive {k : Type u} [Field k] {Q : Type v} [Quiver Q] (R : (X Y : Category k Q) → Set (X ⟶ Y)) : CategoryTheory.Preadditive (RawCategory R)

instance MagnitudeConjecture.LinearPathCategory.HomogeneousQuotient.quotientFunctorAdditive {k : Type u} [Field k] {Q : Type v} [Quiver Q] (R : (X Y : Category k Q) → Set (X ⟶ Y)) : (quotientFunctor R).Additive

@[instance_reducible]

noncomputable instance MagnitudeConjecture.LinearPathCategory.HomogeneousQuotient.rawLinear {k : Type u} [Field k] {Q : Type v} [Quiver Q] (R : (X Y : Category k Q) → Set (X ⟶ Y)) : CategoryTheory.Linear k (RawCategory R)

instance MagnitudeConjecture.LinearPathCategory.HomogeneousQuotient.quotientFunctorLinear {k : Type u} [Field k] {Q : Type v} [Quiver Q] (R : (X Y : Category k Q) → Set (X ⟶ Y)) : CategoryTheory.Functor.Linear k (quotientFunctor R)

@[reducible, inline]

noncomputable abbrev MagnitudeConjecture.LinearPathCategory.HomogeneousQuotient.obj {k : Type u} [Field k] {Q : Type v} [Quiver Q] (R : (X Y : Category k Q) → Set (X ⟶ Y)) (X : Category k Q) : RawCategory R

An original vertex as an object of the quotient category.

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

The quotient map on a Hom space as a linear map.

theorem MagnitudeConjecture.LinearPathCategory.HomogeneousQuotient.quotientHom_surjective {k : Type u} [Field k] {Q : Type v} [Quiver Q] (R : (X Y : Category k Q) → Set (X ⟶ Y)) (X Y : Category k Q) : Function.Surjective ⇑(quotientHomLinearMap R X Y)

The quotient map is surjective on every Hom space.

theorem MagnitudeConjecture.LinearPathCategory.HomogeneousQuotient.ker_quotientHomLinearMap {k : Type u} [Field k] {Q : Type v} [Quiver Q] (R : (X Y : Category k Q) → Set (X ⟶ Y)) (X Y : Category k Q) : (quotientHomLinearMap R X Y).ker = QuotientSubmoduleEquidistribution.CategoricalIdeal.HomIdeal.generatedHomSubmodule k R X Y

The kernel of the quotient map is exactly the generated relation submodule.

noncomputable def MagnitudeConjecture.LinearPathCategory.HomogeneousQuotient.lengthComponent {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 : ℕ) : Submodule k (obj R X ⟶ obj R Y)

The degree-n part of a quotient Hom space is the image of the path-length-n part upstairs.

theorem MagnitudeConjecture.LinearPathCategory.HomogeneousQuotient.lengthComponent_isInternal {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 ∈ LinearPathCategory.lengthComponent A B n) (X Y : Category k Q) : DirectSum.IsInternal (lengthComponent R X Y)

Homogeneous relations give an internal path-length decomposition of each quotient Hom space.

theorem MagnitudeConjecture.LinearPathCategory.HomogeneousQuotient.comp_mem_lengthComponent {k : Type u} [Field k] {Q : Type v} [Quiver Q] (R : (X Y : Category k Q) → Set (X ⟶ Y)) {X Y Z : Category k Q} {i j : ℕ} {f : obj R X ⟶ obj R Y} {g : obj R Y ⟶ obj R Z} (hf : f ∈ lengthComponent R X Y i) (hg : g ∈ lengthComponent R Y Z j) : CategoryTheory.CategoryStruct.comp f g ∈ lengthComponent R X Z (i + j)

Composition in a homogeneous relation quotient adds path length.

@[simp]

theorem MagnitudeConjecture.LinearPathCategory.HomogeneousQuotient.id_mem_lengthComponent_zero {k : Type u} [Field k] {Q : Type v} [Quiver Q] (R : (X Y : Category k Q) → Set (X ⟶ Y)) (X : Category k Q) : CategoryTheory.CategoryStruct.id (obj R X) ∈ lengthComponent R X X 0

theorem MagnitudeConjecture.LinearPathCategory.HomogeneousQuotient.lengthComponent_zero_eq_bot_of_vertex_ne {k : Type u} [Field k] {Q : Type v} [Quiver Q] (R : (X Y : Category k Q) → Set (X ⟶ Y)) {X Y : Category k Q} (hXY : vertex Y ≠ vertex X) : lengthComponent R X Y 0 = ⊥

Distinct vertices still have zero degree-zero quotient morphisms.

theorem MagnitudeConjecture.LinearPathCategory.HomogeneousQuotient.lengthComponent_zero_self {k : Type u} [Field k] {Q : Type v} [Quiver Q] (R : (X Y : Category k Q) → Set (X ⟶ Y)) (X : Category k Q) : lengthComponent R X X 0 = k ∙ CategoryTheory.CategoryStruct.id (obj R X)

At a vertex, the quotient degree-zero part consists exactly of scalar multiples of the identity.

theorem MagnitudeConjecture.LinearPathCategory.HomogeneousQuotient.id_ne_zero_of_basisCompositeSet_positive {k : Type u} [Field k] {Q : Type v} [Quiver Q] (R : (X Y : Category k Q) → Set (X ⟶ Y)) (X : Category k Q) (hpositive : ∀ f ∈ basisCompositeSet R X X, ∃ (n : ℕ), n ≠ 0 ∧ f ∈ LinearPathCategory.lengthComponent X X n) : CategoryTheory.CategoryStruct.id (obj R X) ≠ 0

If every path-basis two-sided composite of a relation has positive length, then the homogeneous quotient does not kill any vertex identity.