Coverings of free linear path categories

A quiver prefunctor induces a linear functor between the corresponding free linear path categories. This file identifies the path bases occurring in the two direct-sum Hom maps of a categorical covering. The fixed-starting-point half uses Mathlib's path-star lifting; the fixed-terminal-point half uses the dual path-costar lifting established in QuiverPathCostar.

noncomputable def MagnitudeConjecture.LinearPathCategory.prefunctorArrowHom {k : Type u} [Field k] {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) {i j : Q₁} (a : i ⟶ j) : obj k Q₂ (π.obj j) ⟶ obj k Q₂ (π.obj i)

The image of a reversed quiver arrow as a path-basis morphism in the target free linear path category.

theorem MagnitudeConjecture.LinearPathCategory.pathMap_prefunctorArrowHom {k : Type u} [Field k] {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) {i j : Q₁} (p : Quiver.Path i j) : pathMap (fun (x : Q₁) => obj k Q₂ (π.obj x)) (fun {x x_1 : Q₁} (a : x ⟶ x_1) => prefunctorArrowHom π a) p = pathHom (π.mapPath p)

Mapping a source path under the reversed free realization gives the path-basis morphism of its mapped path.

noncomputable def MagnitudeConjecture.LinearPathCategory.prefunctorFunctor {k : Type u} [Field k] {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) : CategoryTheory.Functor (Category k Q₁) (Category k Q₂)

The linear functor on free path categories induced by a quiver prefunctor.

instance MagnitudeConjecture.LinearPathCategory.prefunctorFunctor_additive {k : Type u} [Field k] {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) : (prefunctorFunctor π).Additive

instance MagnitudeConjecture.LinearPathCategory.prefunctorFunctor_linear {k : Type u} [Field k] {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) : CategoryTheory.Functor.Linear k (prefunctorFunctor π)

@[simp]

theorem MagnitudeConjecture.LinearPathCategory.prefunctorFunctor_obj {k : Type u} [Field k] {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) (x : Q₁) : (prefunctorFunctor π).obj (obj k Q₁ x) = obj k Q₂ (π.obj x)

@[simp]

theorem MagnitudeConjecture.LinearPathCategory.vertex_prefunctorFunctor_obj {k : Type u} [Field k] {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) (x : Q₁) : vertex ((prefunctorFunctor π).obj (obj k Q₁ x)) = π.obj x

@[simp]

theorem MagnitudeConjecture.LinearPathCategory.prefunctorFunctor_map_pathHom {k : Type u} [Field k] {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) {i j : Q₁} (p : Quiver.Path i j) : (prefunctorFunctor π).map (pathHom p) = pathHom (π.mapPath p)

def MagnitudeConjecture.LinearPathCategory.targetPathMap {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) (x : Q₁) (y : Q₂) : (Z : { z : Q₁ // π.obj z = y }) × Quiver.Path (↑Z) x → Quiver.Path y (π.obj x)

Path-basis indices with fixed lifted terminal vertex and varying initial vertex over y map to paths downstairs.

def MagnitudeConjecture.LinearPathCategory.sourcePathMap {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) (x : Q₂) (y : Q₁) : (Z : { z : Q₁ // π.obj z = x }) × Quiver.Path y ↑Z → Quiver.Path (π.obj y) x

Path-basis indices with fixed lifted initial vertex and varying terminal vertex over x map to paths downstairs.

theorem MagnitudeConjecture.LinearPathCategory.targetPathMap_bijective {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) (hπ : π.IsCovering) (x : Q₁) (y : Q₂) : Function.Bijective (targetPathMap π x y)

theorem MagnitudeConjecture.LinearPathCategory.sourcePathMap_bijective {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) (hπ : π.IsCovering) (x : Q₂) (y : Q₁) : Function.Bijective (sourcePathMap π x y)

noncomputable def MagnitudeConjecture.LinearPathCategory.targetPathEquiv {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) (hπ : π.IsCovering) (x : Q₁) (y : Q₂) : (Z : { z : Q₁ // π.obj z = y }) × Quiver.Path (↑Z) x ≃ Quiver.Path y (π.obj x)

The fixed-terminal path index equivalence of a quiver covering.

noncomputable def MagnitudeConjecture.LinearPathCategory.sourcePathEquiv {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) (hπ : π.IsCovering) (x : Q₂) (y : Q₁) : (Z : { z : Q₁ // π.obj z = x }) × Quiver.Path y ↑Z ≃ Quiver.Path (π.obj y) x

The fixed-initial path index equivalence of a quiver covering.

@[simp]

theorem MagnitudeConjecture.LinearPathCategory.targetPathEquiv_apply {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) (hπ : π.IsCovering) (x : Q₁) (y : Q₂) (p : (Z : { z : Q₁ // π.obj z = y }) × Quiver.Path (↑Z) x) : (targetPathEquiv π hπ x y) p = targetPathMap π x y p

@[simp]

theorem MagnitudeConjecture.LinearPathCategory.sourcePathEquiv_apply {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) (hπ : π.IsCovering) (x : Q₂) (y : Q₁) (p : (Z : { z : Q₁ // π.obj z = x }) × Quiver.Path y ↑Z) : (sourcePathEquiv π hπ x y) p = sourcePathMap π x y p

theorem MagnitudeConjecture.LinearPathCategory.dfinsuppBasis_apply {k : Type u} [Field k] {ι : Type u_1} {M : ι → Type u_2} [DecidableEq ι] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module k (M i)] {η : ι → Type u_3} (b : (i : ι) → Module.Basis (η i) k (M i)) (i : ι) (j : η i) : (DFinsupp.basis b) ⟨i, j⟩ = (DirectSum.lof k ι M i) ((b i) j)

A basis assembled on a dependent direct sum evaluates by including the corresponding component basis vector.

theorem MagnitudeConjecture.LinearPathCategory.pathHom_comp_eqToHom_eq_cast_start {k : Type u} [Field k] {Q₂ : Type v₂} [Quiver Q₂] {i i' j : Q₂} (p : Quiver.Path i j) (h : i = i') : CategoryTheory.CategoryStruct.comp (pathHom p) (CategoryTheory.eqToHom ⋯) = pathHom (Quiver.Path.cast h ⋯ p)

Postcomposing a represented reversed path by an object equality casts the initial vertex of the path.

theorem MagnitudeConjecture.LinearPathCategory.eqToHom_comp_pathHom_eq_cast_end {k : Type u} [Field k] {Q₂ : Type v₂} [Quiver Q₂] {i j j' : Q₂} (p : Quiver.Path i j) (h : j = j') : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (pathHom p) = pathHom (Quiver.Path.cast ⋯ h p)

Precomposing a represented reversed path by an object equality casts the terminal vertex of the path.

theorem MagnitudeConjecture.LinearPathCategory.pathHom_eq_eqToHom_comp_cast_end {k : Type u} [Field k] {Q₂ : Type v₂} [Quiver Q₂] {i j j' : Q₂} (p : Quiver.Path i j) (h : j = j') : pathHom p = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (pathHom (Quiver.Path.cast ⋯ h p))

A represented path equals its endpoint cast preceded by the corresponding object equality.

def MagnitudeConjecture.LinearPathCategory.functorFiberVertexEquiv {k : Type u} [Field k] {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) (y : Q₂) : LinearCovering.Fiber (prefunctorFunctor π) (obj k Q₂ y) ≃ { z : Q₁ // π.obj z = y }

The fibre of the free path functor is the corresponding fibre of the underlying quiver map.

noncomputable def MagnitudeConjecture.LinearPathCategory.targetFunctorPathEquiv {k : Type u} [Field k] {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) (hπ : π.IsCovering) (x : Q₁) (y : Q₂) : (Z : LinearCovering.Fiber (prefunctorFunctor π) (obj k Q₂ y)) × Quiver.Path (vertex ↑Z) x ≃ Quiver.Path y (π.obj x)

Path indices expressed through categorical fibres are equivalent to the fixed-terminal paths downstairs.

noncomputable def MagnitudeConjecture.LinearPathCategory.sourceFunctorPathEquiv {k : Type u} [Field k] {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) (hπ : π.IsCovering) (x : Q₂) (y : Q₁) : (Z : LinearCovering.Fiber (prefunctorFunctor π) (obj k Q₂ x)) × Quiver.Path y (vertex ↑Z) ≃ Quiver.Path (π.obj y) x

Path indices expressed through categorical fibres are equivalent to the fixed-initial paths downstairs.

noncomputable def MagnitudeConjecture.LinearPathCategory.targetFiberHomBasis {k : Type u} [Field k] {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) (x : Q₁) (y : Q₂) : Module.Basis ((Z : LinearCovering.Fiber (prefunctorFunctor π) (obj k Q₂ y)) × Quiver.Path (vertex ↑Z) x) k (DirectSum (LinearCovering.Fiber (prefunctorFunctor π) (obj k Q₂ y)) fun (Z : LinearCovering.Fiber (prefunctorFunctor π) (obj k Q₂ y)) => obj k Q₁ x ⟶ ↑Z)

The path basis on the fixed-source, varying-target direct sum.

noncomputable def MagnitudeConjecture.LinearPathCategory.sourceFiberHomBasis {k : Type u} [Field k] {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) (x : Q₂) (y : Q₁) : Module.Basis ((Z : LinearCovering.Fiber (prefunctorFunctor π) (obj k Q₂ x)) × Quiver.Path y (vertex ↑Z)) k (DirectSum (LinearCovering.Fiber (prefunctorFunctor π) (obj k Q₂ x)) fun (Z : LinearCovering.Fiber (prefunctorFunctor π) (obj k Q₂ x)) => ↑Z ⟶ obj k Q₁ y)

The path basis on the fixed-target, varying-source direct sum.

theorem MagnitudeConjecture.LinearPathCategory.targetFiberHomBasis_apply {k : Type u} [Field k] {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) (x : Q₁) (y : Q₂) (Z : LinearCovering.Fiber (prefunctorFunctor π) (obj k Q₂ y)) (p : Quiver.Path (vertex ↑Z) x) : (targetFiberHomBasis π x y) ⟨Z, p⟩ = (LinearCovering.targetFiberLof (prefunctorFunctor π) (obj k Q₁ x) (obj k Q₂ y) Z) (pathHom p)

theorem MagnitudeConjecture.LinearPathCategory.sourceFiberHomBasis_apply {k : Type u} [Field k] {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) (x : Q₂) (y : Q₁) (Z : LinearCovering.Fiber (prefunctorFunctor π) (obj k Q₂ x)) (p : Quiver.Path y (vertex ↑Z)) : (sourceFiberHomBasis π x y) ⟨Z, p⟩ = (LinearCovering.sourceFiberLof (prefunctorFunctor π) (obj k Q₂ x) (obj k Q₁ y) Z) (pathHom p)

noncomputable def MagnitudeConjecture.LinearPathCategory.targetFiberHomBasisEquiv {k : Type u} [Field k] {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) (hπ : π.IsCovering) (x : Q₁) (y : Q₂) : (DirectSum (LinearCovering.Fiber (prefunctorFunctor π) (obj k Q₂ y)) fun (Z : LinearCovering.Fiber (prefunctorFunctor π) (obj k Q₂ y)) => obj k Q₁ x ⟶ ↑Z) ≃ₗ[k] (prefunctorFunctor π).obj (obj k Q₁ x) ⟶ obj k Q₂ y

The basis equivalence underlying the fixed-source covering map for a quiver covering.

noncomputable def MagnitudeConjecture.LinearPathCategory.sourceFiberHomBasisEquiv {k : Type u} [Field k] {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) (hπ : π.IsCovering) (x : Q₂) (y : Q₁) : (DirectSum (LinearCovering.Fiber (prefunctorFunctor π) (obj k Q₂ x)) fun (Z : LinearCovering.Fiber (prefunctorFunctor π) (obj k Q₂ x)) => ↑Z ⟶ obj k Q₁ y) ≃ₗ[k] obj k Q₂ x ⟶ (prefunctorFunctor π).obj (obj k Q₁ y)

The basis equivalence underlying the fixed-target covering map for a quiver covering.

theorem MagnitudeConjecture.LinearPathCategory.targetFiberHomBasisEquiv_eq_map {k : Type u} [Field k] {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) (hπ : π.IsCovering) (x : Q₁) (y : Q₂) : ↑(targetFiberHomBasisEquiv π hπ x y) = LinearCovering.targetFiberHomMap (prefunctorFunctor π) (obj k Q₁ x) (obj k Q₂ y)

theorem MagnitudeConjecture.LinearPathCategory.sourceFiberHomBasisEquiv_eq_map {k : Type u} [Field k] {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) (hπ : π.IsCovering) (x : Q₂) (y : Q₁) : ↑(sourceFiberHomBasisEquiv π hπ x y) = LinearCovering.sourceFiberHomMap (prefunctorFunctor π) (obj k Q₂ x) (obj k Q₁ y)

theorem MagnitudeConjecture.LinearPathCategory.prefunctorFunctor_isCovering {k : Type u} [Field k] {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] (π : Q₁ ⥤q Q₂) (hπ : π.IsCovering) : LinearCovering.IsCovering (prefunctorFunctor π)

A quiver covering induces a covering functor between its free linear path categories.