The universal mesh category as a deck orbit

The universal translation-quiver projection is invariant under its deck group. This file descends the induced raw mesh functor through the coherent shift-orbit category and identifies the resulting orbit category with the downstairs raw mesh category.

@[instance_reducible]

noncomputable instance MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.vertexStarFintype {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) [(y : Q) → Fintype (Quiver.Star y)] (W : Vertex T x₀) : Fintype (Quiver.Star W)

The canonical arrow-star finiteness on the universal cover, transported from the downstairs quiver covering.

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

The universal-cover projection on raw mesh categories, with the canonical source arrow-star finiteness retained literally.

instance MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshProjectionFunctor_additive {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] : (meshProjectionFunctor T x₀).Additive

instance MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshProjectionFunctor_linear {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] : CategoryTheory.Functor.Linear k (meshProjectionFunctor T x₀)

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshProjectionFunctor_isCovering {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] : LinearCovering.IsCovering (meshProjectionFunctor T x₀)

The raw mesh projection remains a Bongartz--Gabriel linear covering.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshProjectionFunctor_obj_deckMeshEndofunctor {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)] (X : RawCategory (rightMeshData T x₀)) : (meshProjectionFunctor T x₀).obj ((deckMeshEndofunctor T x₀ g).obj X) = (meshProjectionFunctor T x₀).obj X

Deck translation is invisible on projected raw-mesh objects.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.existsUnique_deckMeshEndofunctor_obj_eq_of_projection_eq {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] (Y Z : RawCategory (rightMeshData T x₀)) (hYZ : (meshProjectionFunctor T x₀).obj Z = (meshProjectionFunctor T x₀).obj Y) : ∃! g : FundamentalGroup T x₀, (deckMeshEndofunctor T x₀ g).obj Y = Z

Two universal raw-mesh objects in the same projection fibre differ by a unique deck transformation.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckMeshEndofunctor_obj_injective_in_group {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] (Y : RawCategory (rightMeshData T x₀)) : Function.Injective fun (g : FundamentalGroup T x₀) => (deckMeshEndofunctor T x₀ g).obj Y

At a fixed universal raw-mesh object, the deck-transformation object map is injective in the deck transformation.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckShiftTargetFiberEquiv {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] (Y : RawCategory (rightMeshData T x₀)) : Additive (FundamentalGroup T x₀) ≃ LinearCovering.Fiber (meshProjectionFunctor T x₀) ((meshProjectionFunctor T x₀).obj Y)

Additive deck-shift degrees parametrize the target fibre of the universal raw-mesh projection. The inverse appears because right shifts are defined from the inverse left deck action.

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

Projecting a deck-translated path forgets exactly the deck translation.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshProjectionFunctor_map_deckMeshEndofunctor {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)] {X Y : RawCategory (rightMeshData T x₀)} (f : X ⟶ Y) : (meshProjectionFunctor T x₀).map ((deckMeshEndofunctor T x₀ g).map f) = (meshProjectionFunctor T x₀).map f

The raw mesh projection is unchanged after any deck endofunctor.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckMeshProjectionIso {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)] : (deckMeshEndofunctor T x₀ g).comp (meshProjectionFunctor T x₀) ≅ meshProjectionFunctor T x₀

Deck translation followed by projection is naturally the projection.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshProjectionFunctor_map_deckMeshEndofunctorOneIso_hom_app {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] (X : RawCategory (rightMeshData T x₀)) : (meshProjectionFunctor T x₀).map ((deckMeshEndofunctorOneIso T x₀).hom.app X) = CategoryTheory.CategoryStruct.id ((meshProjectionFunctor T x₀).obj X)

Projection sends the identity-deck comparison to an identity morphism.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshProjectionFunctor_map_deckMeshEndofunctorMulIso_hom_app {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] (g h : FundamentalGroup T x₀) (X : RawCategory (rightMeshData T x₀)) : (meshProjectionFunctor T x₀).map ((deckMeshEndofunctorMulIso T x₀ g h).hom.app X) = CategoryTheory.CategoryStruct.id ((meshProjectionFunctor T x₀).obj X)

Projection sends the product-deck comparison to an identity morphism.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshProjectionFunctor_map_deckMeshShiftCore_zero_hom_app {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] (X : RawCategory (rightMeshData T x₀)) : (meshProjectionFunctor T x₀).map ((deckMeshShiftCore T x₀).zero.hom.app X) = CategoryTheory.CategoryStruct.id ((meshProjectionFunctor T x₀).obj X)

Projection kills the unit comparison in the deck shift core.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshProjectionFunctor_map_deckMeshShiftCore_add_hom_app {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] (a b : Additive (FundamentalGroup T x₀)) (X : RawCategory (rightMeshData T x₀)) : (meshProjectionFunctor T x₀).map (((deckMeshShiftCore T x₀).add a b).hom.app X) = CategoryTheory.CategoryStruct.id ((meshProjectionFunctor T x₀).obj X)

Projection kills every addition comparison in the deck shift core.

instance MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.deckMeshCoherentDeckShift_core_additive {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] (a : Additive (FundamentalGroup T x₀)) : ((deckMeshCoherentDeckShift T x₀).core.F a).Additive

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

@[implicit_reducible]

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshProjectionCommShift {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] : have D := deckMeshCoherentDeckShift T x₀; (meshProjectionFunctor T x₀).CommShift (Additive (FundamentalGroup T x₀))

The raw mesh projection commutes coherently with deck shifts when the downstairs category is given the trivial shift.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshProjectionCommShift_hom_app {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] (a : Additive (FundamentalGroup T x₀)) (Y : RawCategory (rightMeshData T x₀)) : have D := deckMeshCoherentDeckShift T x₀; (CategoryTheory.Functor.commShiftIso (meshProjectionFunctor T x₀) a).hom.app Y = CategoryTheory.eqToHom ⋯

The commutation isomorphism is precisely the equality transport supplied by the corresponding point of the projection fibre.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshShiftOrbitProjectionFunctor {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] : let D := deckMeshCoherentDeckShift T x₀; CategoryTheory.Functor (CoveringHom.ShiftOrbitCategory (RawCategory (rightMeshData T x₀)) (Additive (FundamentalGroup T x₀))) (RawCategory T)

The descended universal mesh projection from the concrete shift-orbit category.

instance MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshShiftOrbitProjectionFunctor_additive {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] : have D := deckMeshCoherentDeckShift T x₀; CategoryTheory.Functor.Additive (meshShiftOrbitProjectionFunctor T x₀)

instance MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshShiftOrbitProjectionFunctor_linear {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] : let D := deckMeshCoherentDeckShift T x₀; CategoryTheory.Functor.Linear k (meshShiftOrbitProjectionFunctor T x₀)

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.shiftOrbitTargetFiberLinearEquiv {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] (X Y : RawCategory (rightMeshData T x₀)) : have D := deckMeshCoherentDeckShift T x₀; CoveringHom.ShiftOrbitHom (Additive (FundamentalGroup T x₀)) X Y ≃ₗ[k] DirectSum (LinearCovering.Fiber (meshProjectionFunctor T x₀) ((meshProjectionFunctor T x₀).obj Y)) fun (Z : LinearCovering.Fiber (meshProjectionFunctor T x₀) ((meshProjectionFunctor T x₀).obj Y)) => X ⟶ ↑Z

Reindexing additive deck degrees by the corresponding projection fibre identifies an orbit Hom direct sum with the fixed-source covering direct sum.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.shiftOrbitTargetFiberLinearEquiv_shiftOrbitLof {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] (X Y : RawCategory (rightMeshData T x₀)) (a : Additive (FundamentalGroup T x₀)) (f : have D := deckMeshCoherentDeckShift T x₀; CoveringHom.ShiftHom X Y a) : let D := deckMeshCoherentDeckShift T x₀; (shiftOrbitTargetFiberLinearEquiv T x₀ X Y) ((CoveringHom.shiftOrbitLof X Y a) f) = (LinearCovering.targetFiberLof (meshProjectionFunctor T x₀) X ((meshProjectionFunctor T x₀).obj Y) ((deckShiftTargetFiberEquiv T x₀ Y) a)) f

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshShiftOrbitProjectionFunctor_map_shiftOrbitLof {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] (X Y : RawCategory (rightMeshData T x₀)) (a : Additive (FundamentalGroup T x₀)) (f : have D := deckMeshCoherentDeckShift T x₀; CoveringHom.ShiftHom X Y a) : let D := deckMeshCoherentDeckShift T x₀; (meshShiftOrbitProjectionFunctor T x₀).map ((CoveringHom.shiftOrbitLof X Y a) f) = (LinearCovering.targetFiberHomMap (meshProjectionFunctor T x₀) X ((meshProjectionFunctor T x₀).obj Y)) ((LinearCovering.targetFiberLof (meshProjectionFunctor T x₀) X ((meshProjectionFunctor T x₀).obj Y) ((deckShiftTargetFiberEquiv T x₀ Y) a)) f)

On one homogeneous deck degree, the descended orbit projection is the corresponding summand of the fixed-source covering map.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshShiftOrbitProjectionHomLinearEquiv {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] (X Y : RawCategory (rightMeshData T x₀)) : have D := deckMeshCoherentDeckShift T x₀; CoveringHom.ShiftOrbitHom (Additive (FundamentalGroup T x₀)) X Y ≃ₗ[k] (meshProjectionFunctor T x₀).obj X ⟶ (meshProjectionFunctor T x₀).obj Y

The covering Hom isomorphism, reindexed by deck degrees, is the Hom map of the descended orbit projection.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshShiftOrbitProjectionHomLinearEquiv_apply {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] (X Y : RawCategory (rightMeshData T x₀)) (f : have D := deckMeshCoherentDeckShift T x₀; CoveringHom.ShiftOrbitHom (Additive (FundamentalGroup T x₀)) X Y) : have D := deckMeshCoherentDeckShift T x₀; (meshShiftOrbitProjectionHomLinearEquiv T x₀ X Y) f = (meshShiftOrbitProjectionFunctor T x₀).map f

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshShiftOrbitProjectionFunctor_map_bijective {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] (X Y : RawCategory (rightMeshData T x₀)) : have D := deckMeshCoherentDeckShift T x₀; Function.Bijective (meshShiftOrbitProjectionFunctor T x₀).map

The descended orbit projection is bijective on every Hom space.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshShiftOrbitProjectionFunctorFullyFaithful {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] : have D := deckMeshCoherentDeckShift T x₀; CategoryTheory.Functor.FullyFaithful (meshShiftOrbitProjectionFunctor T x₀)

The descended orbit projection is fully faithful.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshShiftOrbitProjectionFunctor_obj_surjective {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] (hconnected : IsWalkConnectedAt T x₀) : have D := deckMeshCoherentDeckShift T x₀; Function.Surjective (meshShiftOrbitProjectionFunctor T x₀).obj

Based connectedness makes the descended orbit projection surjective on objects.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshShiftOrbitProjectionFunctor_isEquivalence {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] (hconnected : IsWalkConnectedAt T x₀) : have D := deckMeshCoherentDeckShift T x₀; CategoryTheory.Functor.IsEquivalence (meshShiftOrbitProjectionFunctor T x₀)

For a connected translation quiver, its raw mesh category is the deck shift-orbit category of the universal raw mesh category.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.UniversalCover.meshShiftOrbitEquivalence {Q : Type v} [Quiver Q] (T : RightMeshData Q) (x₀ : Q) {k : Type u} [Field k] [(y : Q) → Fintype (Quiver.Star y)] (hconnected : IsWalkConnectedAt T x₀) : let D := deckMeshCoherentDeckShift T x₀; CoveringHom.ShiftOrbitCategory (RawCategory (rightMeshData T x₀)) (Additive (FundamentalGroup T x₀)) ≌ RawCategory T

The explicit equivalence from the universal deck orbit to the downstairs raw mesh category.