Coverings of polarized right translation quivers

This file connects Mathlib's star-and-costar notion of a quiver covering to the polarized right-mesh data used by the magnitude formalization. A mesh cover preserves projective vertices, translation, and the polarization. Its star bijections transport local finiteness and identify every lifted mesh with the corresponding mesh downstairs.

def MagnitudeConjecture.MeshCategory.RightMeshData.mappedNonprojective {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (T₁ : RightMeshData Q₁) (T₂ : RightMeshData Q₂) (π : Q₁ ⥤q Q₂) (hprojective : ∀ (x : Q₁), x ∈ T₁.projective ↔ π.obj x ∈ T₂.projective) (x : { x : Q₁ // x ∉ T₁.projective }) : { x : Q₂ // x ∉ T₂.projective }

A nonprojective vertex remains nonprojective under a map preserving and reflecting projective vertices.

structure MagnitudeConjecture.MeshCategory.RightMeshData.Cover {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (T₁ : RightMeshData Q₁) (T₂ : RightMeshData Q₂) : Type (max (max (max v₁ v₂) w₁) w₂)

A covering of polarized right translation quivers. Besides Mathlib's local star-and-costar bijections, it preserves the projective boundary, translation, and the chosen pairing of the two sides of every mesh.

• toPrefunctor : Q₁ ⥤q Q₂
• isCovering : self.toPrefunctor.IsCovering
• map_projective_iff (x : Q₁) : x ∈ T₁.projective ↔ self.toPrefunctor.obj x ∈ T₂.projective
• map_tau (x : { x : Q₁ // x ∉ T₁.projective }) : self.toPrefunctor.obj (T₁.tau x) = T₂.tau (T₁.mappedNonprojective T₂ self.toPrefunctor ⋯ x)
• map_arrowEquiv (x : { x : Q₁ // x ∉ T₁.projective }) (y : Q₁) (a : ↑x ⟶ y) : Quiver.Hom.cast ⋯ ⋯ (self.toPrefunctor.map ((T₁.arrowEquiv x y) a)) = (T₂.arrowEquiv (T₁.mappedNonprojective T₂ self.toPrefunctor ⋯ x) (self.toPrefunctor.obj y)) (self.toPrefunctor.map a)

@[reducible, inline]

abbrev MagnitudeConjecture.MeshCategory.RightMeshData.Cover.mapNonprojective {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} (C : T₁.Cover T₂) (x : { x : Q₁ // x ∉ T₁.projective }) : { x : Q₂ // x ∉ T₂.projective }

The image of a nonprojective source vertex as a nonprojective target vertex.

def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.meshArrowMap {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} (C : T₁.Cover T₂) (x : { x : Q₁ // x ∉ T₁.projective }) : T₁.MeshArrow x → T₂.MeshArrow (C.mapNonprojective x)

The map of incoming mesh-arrow stars induced by the underlying quiver prefunctor.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.meshArrowEquiv {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} (C : T₁.Cover T₂) (x : { x : Q₁ // x ∉ T₁.projective }) : T₁.MeshArrow x ≃ T₂.MeshArrow (C.mapNonprojective x)

A quiver covering identifies each lifted incoming mesh-arrow star with the corresponding star downstairs.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.meshArrowEquiv_apply {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} (C : T₁.Cover T₂) (x : { x : Q₁ // x ∉ T₁.projective }) (a : T₁.MeshArrow x) : (C.meshArrowEquiv x) a = C.meshArrowMap x a

@[reducible]

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.sourceStarFintype {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} (C : T₁.Cover T₂) [(y : Q₂) → Fintype (Quiver.Star y)] (x : Q₁) : Fintype (Quiver.Star x)

Local finiteness of arrow stars pulls back along a quiver covering.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.mapPath_meshPath {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} (C : T₁.Cover T₂) (x : { x : Q₁ // x ∉ T₁.projective }) (a : T₁.MeshArrow x) : Quiver.Path.cast ⋯ ⋯ (C.toPrefunctor.mapPath (T₁.meshPath x a)) = T₂.meshPath (C.mapNonprojective x) (C.meshArrowMap x a)

Mapping a lifted mesh path gives the corresponding mesh path downstairs, after transporting its translated endpoint along translation compatibility.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.prefunctorFunctor_map_meshRelation {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} {k : Type u} [Field k] (C : T₁.Cover T₂) [(y : Q₂) → Fintype (Quiver.Star y)] (x : { x : Q₁ // x ∉ T₁.projective }) : (LinearPathCategory.prefunctorFunctor C.toPrefunctor).map (T₁.meshRelation x) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (T₂.meshRelation (C.mapNonprojective x))

The free path-category functor sends a lifted mesh relation exactly to the corresponding target mesh relation, with the required transport along translation compatibility.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.mappedArrowHom {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} {k : Type u} [Field k] (C : T₁.Cover T₂) [(y : Q₂) → Fintype (Quiver.Star y)] {i j : Q₁} (a : i ⟶ j) : obj T₂ (C.toPrefunctor.obj j) ⟶ obj T₂ (C.toPrefunctor.obj i)

The represented target-mesh morphism attached to one source-quiver arrow.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.pathMap_mappedArrowHom {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} {k : Type u} [Field k] (C : T₁.Cover T₂) [(y : Q₂) → Fintype (Quiver.Star y)] {i j : Q₁} (p : Quiver.Path i j) : LinearPathCategory.pathMap (fun (x : Q₁) => obj T₂ (C.toPrefunctor.obj x)) (fun {x x_1 : Q₁} (a : x ⟶ x_1) => C.mappedArrowHom a) p = (quotientFunctor T₂).map (LinearPathCategory.pathHom (C.toPrefunctor.mapPath p))

Reversed path evaluation for the mapped-arrow realization is the target mesh quotient applied to the mapped quiver path.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.map_pathHom_eq_eqToHom_comp_cast {Q₂ : Type v₂} [Quiver Q₂] {T₂ : RightMeshData Q₂} {k : Type u} [Field k] [(y : Q₂) → Fintype (Quiver.Star y)] {i j j' : Q₂} (p : Quiver.Path i j) (h : j = j') : (quotientFunctor T₂).map (LinearPathCategory.pathHom p) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((quotientFunctor T₂).map (LinearPathCategory.pathHom (Quiver.Path.cast ⋯ h p)))

Changing the target vertex of a quiver path becomes precomposition by the corresponding equality morphism in the raw mesh category.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.map_pathHom_meshPath {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} {k : Type u} [Field k] (C : T₁.Cover T₂) [(y : Q₂) → Fintype (Quiver.Star y)] (x : { x : Q₁ // x ∉ T₁.projective }) (a : T₁.MeshArrow x) : (quotientFunctor T₂).map (LinearPathCategory.pathHom (C.toPrefunctor.mapPath (T₁.meshPath x a))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((quotientFunctor T₂).map (LinearPathCategory.pathHom (T₂.meshPath (C.mapNonprojective x) (C.meshArrowMap x a))))

One mapped lifted mesh path is the corresponding target mesh path, including the categorical transport along translation compatibility.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.lift_map_meshRelation {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} {k : Type u} [Field k] (C : T₁.Cover T₂) [(y : Q₂) → Fintype (Quiver.Star y)] (x : { x : Q₁ // x ∉ T₁.projective }) : (LinearPathCategory.lift (fun (y : Q₁) => obj T₂ (C.toPrefunctor.obj y)) fun {x x_1 : Q₁} (a : x ⟶ x_1) => C.mappedArrowHom a).map (T₁.meshRelation x) = 0

The mapped-arrow free realization sends every lifted mesh relation to zero in the target mesh category.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.lift_map_meshRelationUsingSourceFintype {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} {k : Type u} [Field k] (C : T₁.Cover T₂) [(y : Q₁) → Fintype (Quiver.Star y)] [(y : Q₂) → Fintype (Quiver.Star y)] (x : { x : Q₁ // x ∉ T₁.projective }) : (LinearPathCategory.lift (fun (y : Q₁) => obj T₂ (C.toPrefunctor.obj y)) fun {x x_1 : Q₁} (a : x ⟶ x_1) => C.mappedArrowHom a).map (T₁.meshRelation x) = 0

The mapped-arrow free realization kills every source mesh relation when the source arrow-star finiteness structure has already been fixed by the ambient construction.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.realizationUsingSourceFintype {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} {k : Type u} [Field k] (C : T₁.Cover T₂) [(y : Q₁) → Fintype (Quiver.Star y)] [(y : Q₂) → Fintype (Quiver.Star y)] : Realization T₁ fun (y : Q₁) => obj T₂ (C.toPrefunctor.obj y)

The mesh realization induced by a polarized quiver covering, using an ambiently chosen source arrow-star finiteness structure. This is essential for endocovers, where reconstructing the source instance would otherwise change the Lean type of the source mesh category.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.functorUsingSourceFintype {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} {k : Type u} [Field k] (C : T₁.Cover T₂) [(y : Q₁) → Fintype (Quiver.Star y)] [(y : Q₂) → Fintype (Quiver.Star y)] : CategoryTheory.Functor (RawCategory T₁) (RawCategory T₂)

The linear mesh functor induced by a polarized quiver covering, with the source finiteness structure supplied by the ambient category.

instance MagnitudeConjecture.MeshCategory.RightMeshData.Cover.functorUsingSourceFintype_additive {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} {k : Type u} [Field k] (C : T₁.Cover T₂) [(y : Q₁) → Fintype (Quiver.Star y)] [(y : Q₂) → Fintype (Quiver.Star y)] : C.functorUsingSourceFintype.Additive

instance MagnitudeConjecture.MeshCategory.RightMeshData.Cover.functorUsingSourceFintype_linear {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} {k : Type u} [Field k] (C : T₁.Cover T₂) [(y : Q₁) → Fintype (Quiver.Star y)] [(y : Q₂) → Fintype (Quiver.Star y)] : CategoryTheory.Functor.Linear k C.functorUsingSourceFintype

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.functorUsingSourceFintype_obj_obj {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} {k : Type u} [Field k] (C : T₁.Cover T₂) [(y : Q₁) → Fintype (Quiver.Star y)] [(y : Q₂) → Fintype (Quiver.Star y)] (x : Q₁) : C.functorUsingSourceFintype.obj (obj T₁ x) = obj T₂ (C.toPrefunctor.obj x)

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.functorUsingSourceFintype_map_quotient_pathHom {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} {k : Type u} [Field k] (C : T₁.Cover T₂) [(y : Q₁) → Fintype (Quiver.Star y)] [(y : Q₂) → Fintype (Quiver.Star y)] {i j : Q₁} (p : Quiver.Path i j) : C.functorUsingSourceFintype.map ((quotientFunctor T₁).map (LinearPathCategory.pathHom p)) = (quotientFunctor T₂).map (LinearPathCategory.pathHom (C.toPrefunctor.mapPath p))

The ambient-source mesh functor sends a represented path to its represented image path.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.realization {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} {k : Type u} [Field k] (C : T₁.Cover T₂) [(y : Q₂) → Fintype (Quiver.Star y)] : Realization T₁ fun (y : Q₁) => obj T₂ (C.toPrefunctor.obj y)

The mesh realization of a lifted translation quiver in the target mesh category induced by a polarized quiver covering.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.functor {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} {k : Type u} [Field k] (C : T₁.Cover T₂) [(y : Q₂) → Fintype (Quiver.Star y)] : CategoryTheory.Functor (RawCategory T₁) (RawCategory T₂)

The linear functor between raw mesh categories induced by a polarized translation-quiver covering.

instance MagnitudeConjecture.MeshCategory.RightMeshData.Cover.functor_additive {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} {k : Type u} [Field k] (C : T₁.Cover T₂) [(y : Q₂) → Fintype (Quiver.Star y)] : C.functor.Additive

instance MagnitudeConjecture.MeshCategory.RightMeshData.Cover.functor_linear {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} {k : Type u} [Field k] (C : T₁.Cover T₂) [(y : Q₂) → Fintype (Quiver.Star y)] : CategoryTheory.Functor.Linear k C.functor

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.functor_obj_obj {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} {k : Type u} [Field k] (C : T₁.Cover T₂) [(y : Q₂) → Fintype (Quiver.Star y)] (x : Q₁) : C.functor.obj (obj T₁ x) = obj T₂ (C.toPrefunctor.obj x)

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.functor_map_quotient_pathHom {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} {k : Type u} [Field k] (C : T₁.Cover T₂) [(y : Q₂) → Fintype (Quiver.Star y)] {i j : Q₁} (p : Quiver.Path i j) : C.functor.map ((quotientFunctor T₁).map (LinearPathCategory.pathHom p)) = (quotientFunctor T₂).map (LinearPathCategory.pathHom (C.toPrefunctor.mapPath p))

The induced mesh functor sends every represented lifted path to its represented image path downstairs.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.functor_map_quotient_map {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} {k : Type u} [Field k] (C : T₁.Cover T₂) [(y : Q₂) → Fintype (Quiver.Star y)] {X Y : LinearPathCategory.Category k Q₁} (f : X ⟶ Y) : C.functor.map ((quotientFunctor T₁).map f) = (quotientFunctor T₂).map ((LinearPathCategory.prefunctorFunctor C.toPrefunctor).map f)

The induced mesh functor is the quotient of the free path-category functor induced by the underlying quiver prefunctor.