noncomputable def MagnitudeConjecture.MeshCategory.lengthTail {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x y : Q) (n : ℕ) : Submodule k (obj T x ⟶ obj T y)

The subspace spanned by all path-length components of degree at least n.

theorem MagnitudeConjecture.MeshCategory.mem_lengthTail_of_mem_lengthComponent {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) {x y : Q} {n d : ℕ} {f : obj T x ⟶ obj T y} (hnd : n ≤ d) (hf : f ∈ lengthComponent T x y d) : f ∈ lengthTail T x y n

theorem MagnitudeConjecture.MeshCategory.lengthTail_zero_eq_top {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x y : Q) : lengthTail T x y 0 = ⊤

theorem MagnitudeConjecture.MeshCategory.lengthTail_antitone {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x y : Q) {m n : ℕ} (hmn : m ≤ n) : lengthTail T x y n ≤ lengthTail T x y m

Raising the path-length cutoff shrinks the corresponding tail.

theorem MagnitudeConjecture.MeshCategory.eq_zero_of_mem_lengthTail_all {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) {x y : Q} {f : obj T x ⟶ obj T y} (hf : ∀ (n : ℕ), f ∈ lengthTail T x y n) : f = 0

The path-length filtration of every mesh-category Hom space is separated: a morphism in every tail is zero.

theorem MagnitudeConjecture.MeshCategory.lengthTail_one_eq_top_of_ne {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) {x y : Q} (hyx : y ≠ x) : lengthTail T x y 1 = ⊤

Between distinct vertices every mesh morphism has positive path length.

theorem MagnitudeConjecture.MeshCategory.id_not_mem_lengthTail_one {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) : CategoryTheory.CategoryStruct.id (obj T x) ∉ lengthTail T x x 1

The identity of a mesh vertex does not lie in the positive-degree tail.

theorem MagnitudeConjecture.MeshCategory.lengthTail_eq_bot_of_components {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x y : Q) (n : ℕ) (hzero : ∀ (d : ℕ), n ≤ d → lengthComponent T x y d = ⊥) : lengthTail T x y n = ⊥

theorem MagnitudeConjecture.MeshCategory.comp_mem_lengthTail {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) {x y z : Q} {i j : ℕ} {f : obj T x ⟶ obj T y} {g : obj T y ⟶ obj T z} (hf : f ∈ lengthTail T x y i) (hg : g ∈ lengthTail T y z j) : CategoryTheory.CategoryStruct.comp f g ∈ lengthTail T x z (i + j)

theorem MagnitudeConjecture.MeshCategory.eq_of_obj_iso {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) {x y : Q} (e : obj T x ≅ obj T y) : x = y

Distinct quiver vertices cannot become isomorphic in the raw mesh category.

theorem MagnitudeConjecture.MeshCategory.rawCategory_skeletal {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) : CategoryTheory.Skeletal (RawCategory T)

The raw mesh category is skeletal.

theorem MagnitudeConjecture.MeshCategory.exists_lengthComponent_cutoff {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x y : Q) [FiniteDimensional k (obj T x ⟶ obj T y)] : ∃ (n : ℕ), ∀ (d : ℕ), n ≤ d → lengthComponent T x y d = ⊥

theorem MagnitudeConjecture.MeshCategory.exists_uniform_lengthComponent_cutoff {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] [Fintype Q] (T : RightMeshData Q) (hfinite : ∀ (x y : Q), FiniteDimensional k (obj T x ⟶ obj T y)) : ∃ (n : ℕ), ∀ (x y : Q) (d : ℕ), n ≤ d → lengthComponent T x y d = ⊥

On a finite vertex set, finite-dimensionality of every mesh Hom space gives one path-length cutoff valid for all pairs of vertices.

noncomputable def MagnitudeConjecture.MeshCategory.homEndLinearEquiv {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) : (obj T x ⟶ obj T x) ≃ₗ[k] CategoryTheory.End (obj T x)

The path-length pieces of a vertex endomorphism ring, with the ambient type presented as End so that ring operations are definitionally visible.

noncomputable def MagnitudeConjecture.MeshCategory.endLengthComponent {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) (n : ℕ) : Submodule k (CategoryTheory.End (obj T x))

theorem MagnitudeConjecture.MeshCategory.endLengthComponent_isInternal {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) : DirectSum.IsInternal (endLengthComponent T x)

@[instance_reducible]

noncomputable def MagnitudeConjecture.MeshCategory.endLengthComponentDecomposition {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) : DirectSum.Decomposition (endLengthComponent T x)

noncomputable def MagnitudeConjecture.MeshCategory.endLengthTail {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) (n : ℕ) : Submodule k (CategoryTheory.End (obj T x))

The positive-degree filtration on a vertex endomorphism ring.

theorem MagnitudeConjecture.MeshCategory.mem_endLengthTail_of_mem_endLengthComponent {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) {n d : ℕ} {f : CategoryTheory.End (obj T x)} (hnd : n ≤ d) (hf : f ∈ endLengthComponent T x d) : f ∈ endLengthTail T x n

theorem MagnitudeConjecture.MeshCategory.endLengthTail_zero_eq_top {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) : endLengthTail T x 0 = ⊤

theorem MagnitudeConjecture.MeshCategory.endLengthTail_eq_bot_of_components {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) (n : ℕ) (hzero : ∀ (d : ℕ), n ≤ d → endLengthComponent T x d = ⊥) : endLengthTail T x n = ⊥

theorem MagnitudeConjecture.MeshCategory.mul_mem_endLengthTail {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) {i j : ℕ} {f g : CategoryTheory.End (obj T x)} (hf : f ∈ endLengthTail T x i) (hg : g ∈ endLengthTail T x j) : f * g ∈ endLengthTail T x (i + j)

theorem MagnitudeConjecture.MeshCategory.exists_endLengthComponent_cutoff {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) [FiniteDimensional k (CategoryTheory.End (obj T x))] : ∃ (n : ℕ), ∀ (d : ℕ), n ≤ d → endLengthComponent T x d = ⊥

theorem MagnitudeConjecture.MeshCategory.one_mem_endLengthComponent_zero {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) : 1 ∈ endLengthComponent T x 0

theorem MagnitudeConjecture.MeshCategory.endLengthComponent_zero_self {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) : endLengthComponent T x 0 = k ∙ 1

theorem MagnitudeConjecture.MeshCategory.mem_endLengthTail_one_of_degreeZero_eq_zero {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) (f : CategoryTheory.End (obj T x)) (hzero : ↑(((DirectSum.decompose (endLengthComponent T x)) f) 0) = 0) : f ∈ endLengthTail T x 1

theorem MagnitudeConjecture.MeshCategory.isNilpotent_of_degreeZero_eq_zero {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) [FiniteDimensional k (CategoryTheory.End (obj T x))] (f : CategoryTheory.End (obj T x)) (hzero : ↑(((DirectSum.decompose (endLengthComponent T x)) f) 0) = 0) : IsNilpotent f

theorem MagnitudeConjecture.MeshCategory.isIso_smul_id_add_of_mem_lengthTail_one {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) [FiniteDimensional k (CategoryTheory.End (obj T x))] (c : k) (hc : c ≠ 0) (r : CategoryTheory.End (obj T x)) (hr : r.asHom ∈ lengthTail T x x 1) : CategoryTheory.IsIso (c • CategoryTheory.CategoryStruct.id (obj T x) + r.asHom)

A nonzero scalar identity plus a positive-length endomorphism is an isomorphism. Finite-dimensionality makes the positive-length summand nilpotent.

theorem MagnitudeConjecture.MeshCategory.end_isLocalRing_of_finiteDimensional {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x : Q) [FiniteDimensional k (CategoryTheory.End (obj T x))] : IsLocalRing (CategoryTheory.End (obj T x))

A finite-dimensional mesh-category vertex has a local endomorphism ring.