Deck transformations of the universal translation-quiver cover

The fundamental group consists of homotopy classes of closed augmented walks at the chosen base vertex. Prepending such a loop gives the deck action on the based-walk universal cover.

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

Formal reversal with the symmetrified augmented-quiver instance fixed explicitly.

@[simp]

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

@[simp]

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

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.reverseWalk_cons {Q : Type v} [Quiver Q] (T : RightMeshData Q) {x y z : Q} (p : Walk T x y) (e : y ⟶ z) : reverseWalk T (Quiver.Path.cons p e) = (Quiver.reverse e).toPath.comp (reverseWalk T p)

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

def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.compWalk {Q : Type v} [Quiver Q] (T : RightMeshData Q) {x y z : Q} (p : Walk T x y) (q : Walk T y z) : Walk T x z

Composition with the symmetrified augmented-quiver instance fixed explicitly.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.reverseWalk_reverseWalk {Q : Type v} [Quiver Q] (T : RightMeshData Q) {x y : Q} (p : Walk T x y) : reverseWalk T (reverseWalk T p) = p

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.Homotopic.left_comp {Q : Type v} [Quiver Q] (T : RightMeshData Q) {x₀ y z : Q} {p q : Walk T x₀ y} (s : Walk T z x₀) (h : Homotopic T x₀ p q) : Homotopic T z (Quiver.Path.comp s p) (Quiver.Path.comp s q)

Augmented-walk homotopy is also compatible with composition on the left, with the base point changed to the source of the prefix.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.Homotopic.comp_reverse {Q : Type v} [Quiver Q] (T : RightMeshData Q) {x₀ y z : Q} (s : Walk T x₀ y) (p : Walk T y z) : Homotopic T x₀ ((Quiver.Path.comp s p).comp (reverseWalk T p)) s

A path followed by its formal reverse cancels inside any prefixed walk.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.Homotopic.reverse_comp {Q : Type v} [Quiver Q] (T : RightMeshData Q) {x₀ y z : Q} (s : Walk T x₀ z) (p : Walk T y z) : Homotopic T x₀ ((Quiver.Path.comp s (reverseWalk T p)).comp p) s

The formal reverse of a path followed by that path also cancels inside any prefixed walk.

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

Reversing augmented walks preserves their homotopy class, while changing the base point from their common source to their common endpoint.

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

The fundamental group at x₀: homotopy classes of closed augmented walks based at x₀.

def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.loopClass {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (p : Walk T x₀ x₀) : FundamentalGroup T x₀

The fundamental-group class of one based loop.

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

Composition of based loops descends to homotopy classes.

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

Reversal of based loops descends to homotopy classes.

@[instance_reducible]

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

@[instance_reducible]

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

@[instance_reducible]

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

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.loopClass_mul {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (p q : Walk T x₀ x₀) : loopClass T x₀ p * loopClass T x₀ q = loopClass T x₀ (Quiver.Path.comp p q)

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.loopClass_inv {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (p : Walk T x₀ x₀) : (loopClass T x₀ p)⁻¹ = loopClass T x₀ (reverseWalk T p)

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.loopClass_one {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) : loopClass T x₀ Quiver.Path.nil = 1

@[instance_reducible]

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

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

The universal-cover vertex represented by one augmented walk.

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

Prepending a fundamental-group loop to a based walk.

@[instance_reducible]

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

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.loopClass_smul_walkVertex {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (g : Walk T x₀ x₀) {y : Q} (p : Walk T x₀ y) : loopClass T x₀ g • walkVertex T x₀ p = walkVertex T x₀ (Quiver.Path.comp g p)

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckActVertex_vertex {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (g : FundamentalGroup T x₀) (W : Vertex T x₀) : (g • W).fst = W.fst

@[instance_reducible]

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

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.exists_smul_eq_of_vertex_eq {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W Z : Vertex T x₀) (hvertex : W.fst = Z.fst) : ∃ (g : FundamentalGroup T x₀), g • W = Z

Two universal-cover vertices over the same downstairs vertex differ by a deck transformation.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.vertex_eq_of_smul_eq {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (g : FundamentalGroup T x₀) (W Z : Vertex T x₀) (h : g • W = Z) : W.fst = Z.fst

Deck transformations preserve the downstairs endpoint.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.vertex_eq_iff_exists_smul_eq {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W Z : Vertex T x₀) : W.fst = Z.fst ↔ ∃ (g : FundamentalGroup T x₀), g • W = Z

Projection fibres are exactly fundamental-group orbits.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deck_smul_injective {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (W : Vertex T x₀) : Function.Injective fun (g : FundamentalGroup T x₀) => g • W

The deck action is free at every universal-cover vertex.

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

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

Deck translation commutes with appending one symmetric augmented arrow.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.smul_extendOld {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (g : FundamentalGroup T x₀) (W : Vertex T x₀) {z : Q} (a : W.fst ⟶ z) : g • extendOld T x₀ W a = extendOld T x₀ (g • W) a

Deck translation commutes with lifting one ordinary arrow.

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

One deck transformation as an automorphism of the universal-cover quiver. It fixes the underlying downstairs arrow.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckPrefunctor_obj {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (g : FundamentalGroup T x₀) (W : Vertex T x₀) : (deckPrefunctor T x₀ g).obj W = g • W

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckPrefunctor_map_val {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (g : FundamentalGroup T x₀) {W Z : Vertex T x₀} (a : W ⟶ Z) : ↑((deckPrefunctor T x₀ g).map a) = ↑a

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckPrefunctor_comp_projection {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (g : FundamentalGroup T x₀) : deckPrefunctor T x₀ g ⋙q projection T x₀ = projection T x₀

The endpoint projection is invariant under every deck transformation.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckPrefunctor_isCovering {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (g : FundamentalGroup T x₀) : (deckPrefunctor T x₀ g).IsCovering

Every deck transformation is itself a quiver covering.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckPrefunctor_map_tau {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (g : FundamentalGroup T x₀) (W : { W : Vertex T x₀ // W ∉ projectiveSet T x₀ }) : (deckPrefunctor T x₀ g).obj ((rightMeshData T x₀).tau W) = (rightMeshData T x₀).tau ((rightMeshData T x₀).mappedNonprojective (rightMeshData T x₀) (deckPrefunctor T x₀ g) ⋯ W)

A deck transformation commutes with the lifted translation.

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

A deck transformation preserves the lifted projective boundary, translation, and polarization.

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

Every vertex is reachable from the chosen base by an augmented walk. For a connected translation quiver this is the based form of connectedness used by the universal-cover construction.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.vertex_surjective {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (hconnected : IsWalkConnectedAt T x₀) : Function.Surjective (vertex T x₀)

Under based connectedness, the endpoint projection is surjective on vertices.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.vertexOrbitEquiv {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (hconnected : IsWalkConnectedAt T x₀) : MulAction.orbitRel.Quotient (FundamentalGroup T x₀) (Vertex T x₀) ≃ Q

For a connected base, the orbit set of universal-cover vertices under the fundamental group is exactly the downstairs vertex set.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.vertexOrbitEquiv_mk {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (hconnected : IsWalkConnectedAt T x₀) (W : Vertex T x₀) : (vertexOrbitEquiv T x₀ hconnected) (Quotient.mk'' W) = W.fst

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckMeshEndofunctor {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (g : FundamentalGroup T x₀) {k : Type u} [Field k] [(W : Vertex T x₀) → Fintype (Quiver.Star W)] : CategoryTheory.Functor (RawCategory (rightMeshData T x₀)) (RawCategory (rightMeshData T x₀))

A deck transformation, viewed as a literal endofunctor of the universal raw mesh category by retaining its ambient source-star finiteness data.

instance MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckMeshEndofunctor_additive {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (g : FundamentalGroup T x₀) {k : Type u} [Field k] [(W : Vertex T x₀) → Fintype (Quiver.Star W)] : (deckMeshEndofunctor T x₀ g).Additive

instance MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckMeshEndofunctor_linear {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (g : FundamentalGroup T x₀) {k : Type u} [Field k] [(W : Vertex T x₀) → Fintype (Quiver.Star W)] : CategoryTheory.Functor.Linear k (deckMeshEndofunctor T x₀ g)

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckMeshEndofunctor_obj_obj {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (g : FundamentalGroup T x₀) {k : Type u} [Field k] [(W : Vertex T x₀) → Fintype (Quiver.Star W)] (W : Vertex T x₀) : (deckMeshEndofunctor T x₀ g).obj (obj (rightMeshData T x₀) W) = obj (rightMeshData T x₀) (g • W)

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckMeshEndofunctor_obj_bijective {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (g : FundamentalGroup T x₀) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] : have C := cover T x₀; Function.Bijective (deckMeshEndofunctor T x₀ g).obj

A deck transformation is bijective on the objects of the universal raw mesh category.

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

Every literal deck endofunctor is a Bongartz--Gabriel linear covering.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckMeshEndofunctor_isEquivalence {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (g : FundamentalGroup T x₀) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] : have C := cover T x₀; (deckMeshEndofunctor T x₀ g).IsEquivalence

Every deck transformation acts by an equivalence of universal raw mesh categories.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckMeshEquivalence {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (g : FundamentalGroup T x₀) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] : have C := cover T x₀; RawCategory (rightMeshData T x₀) ≌ RawCategory (rightMeshData T x₀)

The categorical autoequivalence induced by one deck transformation.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckMeshEndofunctor_one_obj {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(W : Vertex T x₀) → Fintype (Quiver.Star W)] (X : RawCategory (rightMeshData T x₀)) : (deckMeshEndofunctor T x₀ 1).obj X = X

The identity deck transformation acts identically on raw mesh-category objects.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckMeshEndofunctor_mul_obj {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(W : Vertex T x₀) → Fintype (Quiver.Star W)] (g h : FundamentalGroup T x₀) (X : RawCategory (rightMeshData T x₀)) : (deckMeshEndofunctor T x₀ (h * g)).obj X = (deckMeshEndofunctor T x₀ h).obj ((deckMeshEndofunctor T x₀ g).obj X)

Composition of two deck transformations has the expected left-action law on raw mesh-category objects.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckPrefunctor_one_map_heq {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {W Z : Vertex T x₀} (e : W ⟶ Z) : (deckPrefunctor T x₀ 1).map e ≍ e

The identity deck transformation fixes every universal-cover arrow up to the dependent endpoint witnesses.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckPrefunctor_one_mapPath_cast {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {W Z : Vertex T x₀} (p : Quiver.Path W Z) : Quiver.Path.cast ⋯ ⋯ ((deckPrefunctor T x₀ 1).mapPath p) = p

Mapping a path by the identity deck transformation and then restoring its endpoints gives the original path.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckPrefunctor_one_mapPath_heq {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {W Z : Vertex T x₀} (p : Quiver.Path W Z) : (deckPrefunctor T x₀ 1).mapPath p ≍ p

Mapping a path by the identity deck transformation changes only its dependent endpoint witnesses.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckPrefunctor_mul_map_heq {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (g h : FundamentalGroup T x₀) {W Z : Vertex T x₀} (e : W ⟶ Z) : (deckPrefunctor T x₀ (h * g)).map e ≍ (deckPrefunctor T x₀ h).map ((deckPrefunctor T x₀ g).map e)

The product deck transformation and the corresponding composite deck maps agree on arrows up to their dependent endpoint witnesses.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckPrefunctor_mul_mapPath_cast {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (g h : FundamentalGroup T x₀) {W Z : Vertex T x₀} (p : Quiver.Path W Z) : Quiver.Path.cast ⋯ ⋯ ((deckPrefunctor T x₀ (h * g)).mapPath p) = (deckPrefunctor T x₀ h).mapPath ((deckPrefunctor T x₀ g).mapPath p)

The product deck map on a path equals successive deck mapping after restoring the action-law endpoints.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckPrefunctor_mul_mapPath_heq {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) (g h : FundamentalGroup T x₀) {W Z : Vertex T x₀} (p : Quiver.Path W Z) : (deckPrefunctor T x₀ (h * g)).mapPath p ≍ (deckPrefunctor T x₀ h).mapPath ((deckPrefunctor T x₀ g).mapPath p)

Product mapping of a path differs from successive deck mapping only by dependent endpoint witnesses.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckMeshEndofunctorOneIso {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(W : Vertex T x₀) → Fintype (Quiver.Star W)] : deckMeshEndofunctor T x₀ 1 ≅ CategoryTheory.Functor.id (RawCategory (rightMeshData T x₀))

The objectwise identity comparison for the identity deck transformation.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckMeshEndofunctorMulIso {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(W : Vertex T x₀) → Fintype (Quiver.Star W)] (g h : FundamentalGroup T x₀) : deckMeshEndofunctor T x₀ (h * g) ≅ (deckMeshEndofunctor T x₀ g).comp (deckMeshEndofunctor T x₀ h)

The natural product comparison for categorical deck transformations. The order is the left-action order: first g, then h, equals h * g.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.rawMeshDeckSMul {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(W : Vertex T x₀) → Fintype (Quiver.Star W)] (g : FundamentalGroup T x₀) (X : RawCategory (rightMeshData T x₀)) : RawCategory (rightMeshData T x₀)

The fundamental group acts on the objects of the universal raw mesh category through the already constructed vertex action.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.rawMeshDeckMulAction {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(W : Vertex T x₀) → Fintype (Quiver.Star W)] : MulAction (FundamentalGroup T x₀) (RawCategory (rightMeshData T x₀))

instance MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.rawMeshDeckIsCancelSMul {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(W : Vertex T x₀) → Fintype (Quiver.Star W)] : IsCancelSMul (FundamentalGroup T x₀) (RawCategory (rightMeshData T x₀))

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckMeshEndofunctor_obj_eq_smul {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(W : Vertex T x₀) → Fintype (Quiver.Star W)] (g : FundamentalGroup T x₀) (X : RawCategory (rightMeshData T x₀)) : (deckMeshEndofunctor T x₀ g).obj X = g • X

The categorical deck endofunctor has exactly the induced deck action as its object map.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.additiveToMul_add {G : Type u_1} [Mul G] (a b : Additive G) : Additive.toMul (a + b) = Additive.toMul a * Additive.toMul b

Multiplication written through the additive type synonym, with an explicit equality proof suitable for dependent coherence calculations.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckMeshShiftCore {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(W : Vertex T x₀) → Fintype (Quiver.Star W)] : CategoryTheory.ShiftMkCore (RawCategory (rightMeshData T x₀)) (Additive (FundamentalGroup T x₀))

The coherent right-shift core obtained from the left fundamental-group action. Additive degree g is the inverse deck transformation g⁻¹.

instance MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckMeshShiftCore_additive {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(W : Vertex T x₀) → Fintype (Quiver.Star W)] (a : Additive (FundamentalGroup T x₀)) : ((deckMeshShiftCore T x₀).F a).Additive

instance MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckMeshShiftCore_linear {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(W : Vertex T x₀) → Fintype (Quiver.Star W)] (a : Additive (FundamentalGroup T x₀)) : CategoryTheory.Functor.Linear k ((deckMeshShiftCore T x₀).F a)

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckMeshCoherentDeckShift {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(W : Vertex T x₀) → Fintype (Quiver.Star W)] : CoveringHom.CoherentDeckShift (RawCategory (rightMeshData T x₀)) (FundamentalGroup T x₀)

The universal raw mesh category equipped with its coherent fundamental-group deck shifts.