Universal covers of polarized right translation quivers

Following Bongartz--Gabriel, the universal-cover vertices are homotopy classes of walks from a fixed base vertex. The walk quiver augments the ordinary arrows by one formal mesh edge from each nonprojective vertex to its translate. Homotopy cancels an arrow with its formal inverse and identifies a formal mesh edge with every polarized length-two route through that mesh.

def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.AugmentedVertex {Q : Type v} [Quiver Q] (_T : RightMeshData Q) : Type v

A type synonym on which the augmented walk quiver is installed without replacing the original quiver structure on Q.

inductive MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.AugmentedArrow {Q : Type v} [Quiver Q] (T : RightMeshData Q) : AugmentedVertex T → AugmentedVertex T → Type (max v w)

The augmented arrows: ordinary arrows and one formal degree-two edge from each nonprojective vertex to its translate.

• old {Q : Type v} [Quiver Q] {T : RightMeshData Q} {x y : Q} (a : x ⟶ y) : AugmentedArrow T x y
• mesh {Q : Type v} [Quiver Q] {T : RightMeshData Q} (x : { x : Q // x ∉ T.projective }) : AugmentedArrow T (↑x) (T.tau x)

@[instance_reducible]

instance MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.augmentedQuiver {Q : Type v} [Quiver Q] (T : RightMeshData Q) : Quiver (AugmentedVertex T)

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

An ordinary arrow regarded as a positive arrow of the symmetrified augmented quiver.

def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshArrow {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x : { x : Q // x ∉ T.projective }) : ↑x ⟶ T.tau x

The formal mesh edge regarded as a positive arrow of the symmetrified augmented quiver.

def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.oldArrowPath {Q : Type v} [Quiver Q] (T : RightMeshData Q) {x y : Q} (a : x ⟶ y) : Quiver.Path x y

The one-edge walk associated with an ordinary arrow.

def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshArrowPath {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x : { x : Q // x ∉ T.projective }) : Quiver.Path (↑x) (T.tau x)

The one-edge walk associated with a formal mesh edge.

@[reducible, inline]

abbrev MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.Walk {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ y : Q) : Type (max v w)

Walks in the symmetrified augmented quiver from a fixed base vertex.

inductive MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.Homotopic {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {y : Q} : Walk T x₀ y → Walk T x₀ y → Prop

Bongartz--Gabriel homotopy of augmented walks with fixed endpoints.

• refl {Q : Type v} [Quiver Q] {T : RightMeshData Q} {x₀ y : Q} (p : Walk T x₀ y) : Homotopic T x₀ p p
• symm {Q : Type v} [Quiver Q] {T : RightMeshData Q} {x₀ y : Q} {p q : Walk T x₀ y} : Homotopic T x₀ p q → Homotopic T x₀ q p
• trans {Q : Type v} [Quiver Q] {T : RightMeshData Q} {x₀ y : Q} {p q r : Walk T x₀ y} : Homotopic T x₀ p q → Homotopic T x₀ q r → Homotopic T x₀ p r
• comp {Q : Type v} [Quiver Q] {T : RightMeshData Q} {x₀ y z : Q} {p q : Walk T x₀ y} (h : Homotopic T x₀ p q) (r : Quiver.Path y z) : Homotopic T x₀ (Quiver.Path.comp p r) (Quiver.Path.comp q r)
• cancel {Q : Type v} [Quiver Q] {T : RightMeshData Q} {x₀ y z : Q} (p : Walk T x₀ y) (e : y ⟶ z) : Homotopic T x₀ ((Quiver.Path.comp p e.toPath).comp (Quiver.reverse e).toPath) p
• mesh {Q : Type v} [Quiver Q] {T : RightMeshData Q} {x₀ : Q} (s : { s : Q // s ∉ T.projective }) (p : Walk T x₀ ↑s) (a : T.MeshArrow s) : Homotopic T x₀ (Quiver.Path.comp p (meshArrowPath T s)) ((Quiver.Path.comp p (oldArrowPath T a.snd)).comp (oldArrowPath T ((T.arrowEquiv s a.fst) a.snd)))

def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.homotopySetoid {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ y : Q) : Setoid (Walk T x₀ y)

Augmented-walk homotopy as a setoid at one endpoint.

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

Vertices of the universal cover based at x₀: an endpoint together with a homotopy class of walks from x₀ to that endpoint.

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

Projection of a universal-cover vertex to its endpoint downstairs.

def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.extend {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W : Vertex T x₀) {z : Q} (e : W.fst ⟶ z) : Vertex T x₀

Append one symmetric augmented arrow to a universal-cover vertex.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.extend_cast_target {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W : Vertex T x₀) {z z' : Q} (e : W.fst ⟶ z) (h : z = z') : extend T x₀ W (Quiver.Hom.cast ⋯ h e) = extend T x₀ W e

Transporting the target witness of an appended arrow does not change the resulting universal-cover vertex.

@[simp]

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

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

Appending an arrow and then its formal inverse does not change a cover vertex.

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

Appending a formal inverse and then the original arrow does not change a cover vertex.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.extend_mesh {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W : Vertex T x₀) (s : { s : Q // s ∉ T.projective }) (hs : W.fst = ↑s) (a : T.MeshArrow s) : extend T x₀ W (Quiver.Hom.cast ⋯ ⋯ (meshArrow T s)) = extend T x₀ (extend T x₀ W (Quiver.Hom.cast ⋯ ⋯ (oldArrow T a.snd))) (oldArrow T ((T.arrowEquiv s a.fst) a.snd))

A formal mesh edge and every polarized length-two mesh route have the same endpoint in the universal cover.

def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.extendOld {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W : Vertex T x₀) {z : Q} (a : W.fst ⟶ z) : Vertex T x₀

Lift an ordinary arrow by appending it to a walk class.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.source_eq_reverse_extend {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (Z W : Vertex T x₀) (a : Z.fst ⟶ W.fst) (ha : extendOld T x₀ Z a = W) : Z = extend T x₀ W (Quiver.reverse (oldArrow T a))

The source of a lifted ordinary arrow is recovered by appending the formal inverse to its target.

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

Arrows of the universal cover are the unique ordinary-arrow lifts with a specified endpoint.

@[instance_reducible]

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

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

Projection from the universal-cover quiver to the original quiver.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.projection_star_bijective {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W : Vertex T x₀) : Function.Bijective ((projection T x₀).star W)

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.projection_costar_bijective {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W : Vertex T x₀) : Function.Bijective ((projection T x₀).costar W)

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.projection_isCovering {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) : (projection T x₀).IsCovering

The endpoint projection is a quiver covering.

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

Projective vertices in the universal cover are exactly those lying over projective vertices downstairs.

def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.baseNonprojective {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W : { W : Vertex T x₀ // W ∉ projectiveSet T x₀ }) : { x : Q // x ∉ T.projective }

The downstairs nonprojective vertex underlying a nonprojective universal-cover vertex.

def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.tau {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W : { W : Vertex T x₀ // W ∉ projectiveSet T x₀ }) : Vertex T x₀

Translation in the universal cover is obtained by appending the formal mesh edge.

def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.pairedArrow {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W : { W : Vertex T x₀ // W ∉ projectiveSet T x₀ }) (Y : Vertex T x₀) (a : ↑W ⟶ Y) : Y ⟶ tau T x₀ W

Lift the polarized partner of one arrow in a universal-cover mesh.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.pairedArrow_val {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W : { W : Vertex T x₀ // W ∉ projectiveSet T x₀ }) (Y : Vertex T x₀) (a : ↑W ⟶ Y) : ↑(pairedArrow T x₀ W Y a) = (T.arrowEquiv (baseNonprojective T x₀ W) Y.fst) ↑a

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.pairedArrow_injective {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W : { W : Vertex T x₀ // W ∉ projectiveSet T x₀ }) (Y : Vertex T x₀) : Function.Injective (pairedArrow T x₀ W Y)

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.pairedArrow_surjective {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W : { W : Vertex T x₀ // W ∉ projectiveSet T x₀ }) (Y : Vertex T x₀) : Function.Surjective (pairedArrow T x₀ W Y)

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.arrowEquiv {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W : { W : Vertex T x₀ // W ∉ projectiveSet T x₀ }) (Y : Vertex T x₀) : (↑W ⟶ Y) ≃ (Y ⟶ tau T x₀ W)

Polarization of the lifted mesh, obtained from mesh homotopy and the local star/costar uniqueness of the quiver cover.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.arrowEquiv_apply {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W : { W : Vertex T x₀ // W ∉ projectiveSet T x₀ }) (Y : Vertex T x₀) (a : ↑W ⟶ Y) : (arrowEquiv T x₀ W Y) a = pairedArrow T x₀ W Y a

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

The polarized right-mesh data lifted to the universal-cover quiver.

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

The endpoint projection, together with the lifted translation and polarization, is a covering of polarized right translation quivers.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshFunctor_isCovering {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] : have C := cover T x₀; LinearCovering.IsCovering C.functor

The universal-cover projection induces a Bongartz--Gabriel covering functor between the associated raw mesh categories.