Integer grading on the universal translation-quiver cover

Bongartz--Gabriel's universal-cover construction carries a canonical integer grading. Positive ordinary arrows have degree one, positive formal mesh edges have degree two, and formal reverses have the opposite degrees. The defining walk homotopy preserves this degree, so it descends to universal-cover vertices. Consequently every lifted ordinary arrow raises vertex degree by one and translation raises it by two.

def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.arrowDegree {Q : Type v} [Quiver Q] (T : RightMeshData Q) {x y : Q} : (x ⟶ y) → ℤ

Degree of a symmetric augmented arrow: ordinary arrows have absolute degree one and formal mesh edges have absolute degree two.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.arrowDegree_oldArrow {Q : Type v} [Quiver Q] (T : RightMeshData Q) {x y : Q} (a : x ⟶ y) : arrowDegree T (oldArrow T a) = 1

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.arrowDegree_meshArrow {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x : { x : Q // x ∉ T.projective }) : arrowDegree T (meshArrow T x) = 2

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.arrowDegree_reverse {Q : Type v} [Quiver Q] (T : RightMeshData Q) {x y : Q} (e : x ⟶ y) : arrowDegree T (Quiver.reverse e) = -arrowDegree T e

def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.walkDegree {Q : Type v} [Quiver Q] (T : RightMeshData Q) {x y : Q} : Walk T x y → ℤ

Signed degree of a walk in the symmetrified augmented quiver.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.walkDegree_nil {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x : Q) : walkDegree T Quiver.Path.nil = 0

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.walkDegree_cons {Q : Type v} [Quiver Q] (T : RightMeshData Q) {x y z : Q} (p : Walk T x y) (e : y ⟶ z) : walkDegree T (Quiver.Path.cons p e) = walkDegree T p + arrowDegree T e

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.walkDegree_toPath {Q : Type v} [Quiver Q] (T : RightMeshData Q) {x y : Q} (e : x ⟶ y) : walkDegree T e.toPath = arrowDegree T e

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.walkDegree_comp {Q : Type v} [Quiver Q] (T : RightMeshData Q) {x y z : Q} (p : Walk T x y) (q : Walk T y z) : walkDegree T (Quiver.Path.comp p q) = walkDegree T p + walkDegree T q

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.walkDegree_cast {Q : Type v} [Quiver Q] (T : RightMeshData Q) {x y x' y' : Quiver.Symmetrify (AugmentedVertex T)} (p : Quiver.Path x y) (hx : x = x') (hy : y = y') : walkDegree T (Quiver.Path.cast hx hy p) = walkDegree T p

Transporting the endpoints of an augmented walk does not change its signed degree.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.Homotopic.walkDegree_eq {Q : Type v} [Quiver Q] (T : RightMeshData Q) {x₀ y : Q} {p q : Walk T x₀ y} (h : Homotopic T x₀ p q) : walkDegree T p = walkDegree T q

Bongartz--Gabriel walk homotopy preserves signed degree.

def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.classDegree {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {y : Q} : Quotient (homotopySetoid T x₀ y) → ℤ

Degree of one homotopy class of walks with a fixed endpoint.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.classDegree_mk {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {y : Q} (p : Walk T x₀ y) : classDegree T x₀ ⟦p⟧ = walkDegree T p

def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.vertexDegree {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W : Vertex T x₀) : ℤ

Canonical integer degree of a universal-cover vertex.

def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.baseVertex {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) : Vertex T x₀

The universal-cover vertex represented by the empty walk at the base.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.baseVertex_vertex {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) : (baseVertex T x₀).fst = x₀

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.vertexDegree_baseVertex {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) : vertexDegree T x₀ (baseVertex T x₀) = 0

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.vertexDegree_extend {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W : Vertex T x₀) {z : Q} (e : W.fst ⟶ z) : vertexDegree T x₀ (extend T x₀ W e) = vertexDegree T x₀ W + arrowDegree T e

Appending one symmetric augmented arrow adds its signed degree.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.vertexDegree_extendOld {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W : Vertex T x₀) {z : Q} (a : W.fst ⟶ z) : vertexDegree T x₀ (extendOld T x₀ W a) = vertexDegree T x₀ W + 1

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.vertexDegree_arrow {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {W Z : Vertex T x₀} (a : W ⟶ Z) : vertexDegree T x₀ Z = vertexDegree T x₀ W + 1

Every arrow of the universal cover raises vertex degree by one.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.vertexDegree_tau {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W : { W : Vertex T x₀ // W ∉ projectiveSet T x₀ }) : vertexDegree T x₀ (tau T x₀ W) = vertexDegree T x₀ ↑W + 2

Translation in the universal cover raises vertex degree by two.

def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.vertexHeight {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W : Vertex T x₀) : ℤ

Bongartz--Gabriel height convention, opposite to the positive degree of the reversed quiver used by this package.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.vertexHeight_baseVertex {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) : vertexHeight T x₀ (baseVertex T x₀) = 0

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.vertexHeight_arrow {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {W Z : Vertex T x₀} (a : W ⟶ Z) : vertexHeight T x₀ Z = vertexHeight T x₀ W - 1

In the package's reversed-quiver orientation, every quiver arrow lowers Bongartz--Gabriel height by one. The represented module morphism points in the opposite direction and therefore raises height by one.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.vertexHeight_tau {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W : { W : Vertex T x₀ // W ∉ projectiveSet T x₀ }) : vertexHeight T x₀ (tau T x₀ W) = vertexHeight T x₀ ↑W - 2

Translation lowers Bongartz--Gabriel height by two in the reversed quiver orientation.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.vertexHeight_arrow_positive_target_or_nonpositive_source {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {W Z : Vertex T x₀} (a : W ⟶ Z) : 0 < vertexHeight T x₀ W ∨ vertexHeight T x₀ Z ≤ 0

The two Bongartz--Gabriel inductions cover every represented arrow: either its module-theoretic target has positive height, or its module-theoretic source has nonpositive height.