Hom-space quotient squares for mesh coverings

This file compares the free path-category covering equivalences with the two direct-sum Hom maps of the induced mesh-category functor. The comparison is set up using the literal fibres of the mesh functor, so that the eventual covering theorem has exactly the Bongartz--Gabriel type.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.meshFunctorFiberVertexEquiv {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₂) : LinearCovering.Fiber C.functor (obj T₂ y) ≃ { z : Q₁ // C.toPrefunctor.obj z = y }

A fibre object of the mesh functor is the same thing as a source vertex lying over the chosen target vertex.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.targetMeshFunctorPathEquiv {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₁) (y : Q₂) : (Z : LinearCovering.Fiber C.functor (obj T₂ y)) × Quiver.Path (LinearPathCategory.vertex (↑Z).as) x ≃ Quiver.Path y (C.toPrefunctor.obj x)

Fixed-terminal path indices written using fibres of the mesh functor.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.sourceMeshFunctorPathEquiv {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₂) (y : Q₁) : (Z : LinearCovering.Fiber C.functor (obj T₂ x)) × Quiver.Path y (LinearPathCategory.vertex (↑Z).as) ≃ Quiver.Path (C.toPrefunctor.obj y) x

Fixed-initial path indices written using fibres of the mesh functor.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.targetFreeFiberHomBasis {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₁) (y : Q₂) : Module.Basis ((Z : LinearCovering.Fiber C.functor (obj T₂ y)) × Quiver.Path (LinearPathCategory.vertex (↑Z).as) x) k (DirectSum (LinearCovering.Fiber C.functor (obj T₂ y)) fun (Z : LinearCovering.Fiber C.functor (obj T₂ y)) => LinearPathCategory.obj k Q₁ x ⟶ (↑Z).as)

The free path basis on the fixed-source direct sum indexed by fibres of the mesh functor.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.sourceFreeFiberHomBasis {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₂) (y : Q₁) : Module.Basis ((Z : LinearCovering.Fiber C.functor (obj T₂ x)) × Quiver.Path y (LinearPathCategory.vertex (↑Z).as)) k (DirectSum (LinearCovering.Fiber C.functor (obj T₂ x)) fun (Z : LinearCovering.Fiber C.functor (obj T₂ x)) => (↑Z).as ⟶ LinearPathCategory.obj k Q₁ y)

The free path basis on the fixed-target direct sum indexed by fibres of the mesh functor.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.targetFreeFiberLof {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₁) (y : Q₂) (Z : LinearCovering.Fiber C.functor (obj T₂ y)) : (LinearPathCategory.obj k Q₁ x ⟶ (↑Z).as) →ₗ[k] DirectSum (LinearCovering.Fiber C.functor (obj T₂ y)) fun (W : LinearCovering.Fiber C.functor (obj T₂ y)) => LinearPathCategory.obj k Q₁ x ⟶ (↑W).as

Include one free fixed-source Hom space in the direct sum indexed by the mesh-functor fibre.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.sourceFreeFiberLof {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₂) (y : Q₁) (Z : LinearCovering.Fiber C.functor (obj T₂ x)) : ((↑Z).as ⟶ LinearPathCategory.obj k Q₁ y) →ₗ[k] DirectSum (LinearCovering.Fiber C.functor (obj T₂ x)) fun (W : LinearCovering.Fiber C.functor (obj T₂ x)) => (↑W).as ⟶ LinearPathCategory.obj k Q₁ y

Include one free fixed-target Hom space in the direct sum indexed by the mesh-functor fibre.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.targetFreeFiberHomBasis_apply {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₁) (y : Q₂) (Z : LinearCovering.Fiber C.functor (obj T₂ y)) (p : Quiver.Path (LinearPathCategory.vertex (↑Z).as) x) : (C.targetFreeFiberHomBasis x y) ⟨Z, p⟩ = (C.targetFreeFiberLof x y Z) (LinearPathCategory.pathHom p)

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.sourceFreeFiberHomBasis_apply {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₂) (y : Q₁) (Z : LinearCovering.Fiber C.functor (obj T₂ x)) (p : Quiver.Path y (LinearPathCategory.vertex (↑Z).as)) : (C.sourceFreeFiberHomBasis x y) ⟨Z, p⟩ = (C.sourceFreeFiberLof x y Z) (LinearPathCategory.pathHom p)

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.targetFreeFiberHomMap {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₁) (y : Q₂) : (DirectSum (LinearCovering.Fiber C.functor (obj T₂ y)) fun (Z : LinearCovering.Fiber C.functor (obj T₂ y)) => LinearPathCategory.obj k Q₁ x ⟶ (↑Z).as) →ₗ[k] LinearPathCategory.obj k Q₂ (C.toPrefunctor.obj x) ⟶ LinearPathCategory.obj k Q₂ y

The free fixed-source direct-sum map, indexed by fibres of the mesh functor but evaluated before imposing mesh relations.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.sourceFreeFiberHomMap {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₂) (y : Q₁) : (DirectSum (LinearCovering.Fiber C.functor (obj T₂ x)) fun (Z : LinearCovering.Fiber C.functor (obj T₂ x)) => (↑Z).as ⟶ LinearPathCategory.obj k Q₁ y) →ₗ[k] LinearPathCategory.obj k Q₂ x ⟶ LinearPathCategory.obj k Q₂ (C.toPrefunctor.obj y)

The free fixed-target direct-sum map, indexed by fibres of the mesh functor but evaluated before imposing mesh relations.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.targetFreeFiberHomMap_lof {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₁) (y : Q₂) (Z : LinearCovering.Fiber C.functor (obj T₂ y)) (f : LinearPathCategory.obj k Q₁ x ⟶ (↑Z).as) : (C.targetFreeFiberHomMap x y) ((C.targetFreeFiberLof x y Z) f) = CategoryTheory.CategoryStruct.comp ((LinearPathCategory.prefunctorFunctor C.toPrefunctor).map f) (CategoryTheory.eqToHom ⋯)

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.sourceFreeFiberHomMap_lof {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₂) (y : Q₁) (Z : LinearCovering.Fiber C.functor (obj T₂ x)) (f : (↑Z).as ⟶ LinearPathCategory.obj k Q₁ y) : (C.sourceFreeFiberHomMap x y) ((C.sourceFreeFiberLof x y Z) f) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((LinearPathCategory.prefunctorFunctor C.toPrefunctor).map f)

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.targetFreeFiberHomEquiv {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₁) (y : Q₂) : (DirectSum (LinearCovering.Fiber C.functor (obj T₂ y)) fun (Z : LinearCovering.Fiber C.functor (obj T₂ y)) => LinearPathCategory.obj k Q₁ x ⟶ (↑Z).as) ≃ₗ[k] LinearPathCategory.obj k Q₂ (C.toPrefunctor.obj x) ⟶ LinearPathCategory.obj k Q₂ y

The free fixed-source Hom equivalence, indexed by the literal mesh-functor fibre.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.sourceFreeFiberHomEquiv {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₂) (y : Q₁) : (DirectSum (LinearCovering.Fiber C.functor (obj T₂ x)) fun (Z : LinearCovering.Fiber C.functor (obj T₂ x)) => (↑Z).as ⟶ LinearPathCategory.obj k Q₁ y) ≃ₗ[k] LinearPathCategory.obj k Q₂ x ⟶ LinearPathCategory.obj k Q₂ (C.toPrefunctor.obj y)

The free fixed-target Hom equivalence, indexed by the literal mesh-functor fibre.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.targetFreeFiberHomEquiv_eq_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 : Q₁) (y : Q₂) : ↑(C.targetFreeFiberHomEquiv x y) = C.targetFreeFiberHomMap x y

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.sourceFreeFiberHomEquiv_eq_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 : Q₂) (y : Q₁) : ↑(C.sourceFreeFiberHomEquiv x y) = C.sourceFreeFiberHomMap x y

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.quotientObjectEq {k : Type u} [Field k] {Q : Type v₁} [Quiver Q] (T : RightMeshData Q) [(z : Q) → Fintype (Quiver.Star z)] (Z : RawCategory T) : (quotientFunctor T).obj Z.as = Z

Every quotient-category object is canonically the quotient functor applied to its stored source object.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.targetComponentQuotientMap {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₁) (y : Q₂) (Z : LinearCovering.Fiber C.functor (obj T₂ y)) : (LinearPathCategory.obj k Q₁ x ⟶ (↑Z).as) →ₗ[k] obj T₁ x ⟶ ↑Z

Quotient one free fixed-source Hom component, with the canonical object transport to the literal fibre object.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.sourceComponentQuotientMap {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₂) (y : Q₁) (Z : LinearCovering.Fiber C.functor (obj T₂ x)) : ((↑Z).as ⟶ LinearPathCategory.obj k Q₁ y) →ₗ[k] ↑Z ⟶ obj T₁ y

Quotient one free fixed-target Hom component, with the canonical object transport from the literal fibre object.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.targetComponentQuotientMap_apply {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₁) (y : Q₂) (Z : LinearCovering.Fiber C.functor (obj T₂ y)) (f : LinearPathCategory.obj k Q₁ x ⟶ (↑Z).as) : (C.targetComponentQuotientMap x y Z) f = CategoryTheory.CategoryStruct.comp ((quotientFunctor T₁).map f) (CategoryTheory.eqToHom ⋯)

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.sourceComponentQuotientMap_apply {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₂) (y : Q₁) (Z : LinearCovering.Fiber C.functor (obj T₂ x)) (f : (↑Z).as ⟶ LinearPathCategory.obj k Q₁ y) : (C.sourceComponentQuotientMap x y Z) f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((quotientFunctor T₁).map f)

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.targetComponentQuotientMap_surjective {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₁) (y : Q₂) (Z : LinearCovering.Fiber C.functor (obj T₂ y)) : Function.Surjective ⇑(C.targetComponentQuotientMap x y Z)

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.sourceComponentQuotientMap_surjective {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₂) (y : Q₁) (Z : LinearCovering.Fiber C.functor (obj T₂ x)) : Function.Surjective ⇑(C.sourceComponentQuotientMap x y Z)

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.sourceComponentQuotientMap_eq_zero_of_mem_meshIdealHom {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₂) (y : Q₁) (Z : LinearCovering.Fiber C.functor (obj T₂ x)) (f : (↑Z).as ⟶ LinearPathCategory.obj k Q₁ y) : f ∈ T₁.meshIdealHom (LinearPathCategory.vertex (↑Z).as) y → (C.sourceComponentQuotientMap x y Z) f = 0

A source mesh-ideal element is killed by the fixed-target component quotient map.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.targetComponentQuotientMap_eq_zero_of_mem_meshIdealHom {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₁) (y : Q₂) (Z : LinearCovering.Fiber C.functor (obj T₂ y)) (f : LinearPathCategory.obj k Q₁ x ⟶ (↑Z).as) : f ∈ T₁.meshIdealHom x (LinearPathCategory.vertex (↑Z).as) → (C.targetComponentQuotientMap x y Z) f = 0

A source mesh-ideal element is killed by the fixed-source component quotient map.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.targetFiberQuotientMap {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₁) (y : Q₂) : (DirectSum (LinearCovering.Fiber C.functor (obj T₂ y)) fun (Z : LinearCovering.Fiber C.functor (obj T₂ y)) => LinearPathCategory.obj k Q₁ x ⟶ (↑Z).as) →ₗ[k] DirectSum (LinearCovering.Fiber C.functor (obj T₂ y)) fun (Z : LinearCovering.Fiber C.functor (obj T₂ y)) => obj T₁ x ⟶ ↑Z

Quotient every component in the fixed-source free direct sum by the source mesh ideal.

noncomputable def MagnitudeConjecture.MeshCategory.RightMeshData.Cover.sourceFiberQuotientMap {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₂) (y : Q₁) : (DirectSum (LinearCovering.Fiber C.functor (obj T₂ x)) fun (Z : LinearCovering.Fiber C.functor (obj T₂ x)) => (↑Z).as ⟶ LinearPathCategory.obj k Q₁ y) →ₗ[k] DirectSum (LinearCovering.Fiber C.functor (obj T₂ x)) fun (Z : LinearCovering.Fiber C.functor (obj T₂ x)) => ↑Z ⟶ obj T₁ y

Quotient every component in the fixed-target free direct sum by the source mesh ideal.

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.targetFiberQuotientMap_lof {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₁) (y : Q₂) (Z : LinearCovering.Fiber C.functor (obj T₂ y)) (f : LinearPathCategory.obj k Q₁ x ⟶ (↑Z).as) : (C.targetFiberQuotientMap x y) ((C.targetFreeFiberLof x y Z) f) = (LinearCovering.targetFiberLof C.functor (obj T₁ x) (obj T₂ y) Z) ((C.targetComponentQuotientMap x y Z) f)

@[simp]

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.sourceFiberQuotientMap_lof {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₂) (y : Q₁) (Z : LinearCovering.Fiber C.functor (obj T₂ x)) (f : (↑Z).as ⟶ LinearPathCategory.obj k Q₁ y) : (C.sourceFiberQuotientMap x y) ((C.sourceFreeFiberLof x y Z) f) = (LinearCovering.sourceFiberLof C.functor (obj T₂ x) (obj T₁ y) Z) ((C.sourceComponentQuotientMap x y Z) f)

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.targetFiberQuotientMap_surjective {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₁) (y : Q₂) : Function.Surjective ⇑(C.targetFiberQuotientMap x y)

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.sourceFiberQuotientMap_surjective {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₂) (y : Q₁) : Function.Surjective ⇑(C.sourceFiberQuotientMap x y)

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.targetFiber_quotient_square {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₁) (y : Q₂) (a : DirectSum (LinearCovering.Fiber C.functor (obj T₂ y)) fun (Z : LinearCovering.Fiber C.functor (obj T₂ y)) => LinearPathCategory.obj k Q₁ x ⟶ (↑Z).as) : (LinearCovering.targetFiberHomMap C.functor (obj T₁ x) (obj T₂ y)) ((C.targetFiberQuotientMap x y) a) = (quotientFunctor T₂).map ((C.targetFreeFiberHomMap x y) a)

The fixed-source free covering equivalence and the mesh-functor Hom map form a commutative square with the componentwise quotient maps.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.sourceFiber_quotient_square {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₂) (y : Q₁) (a : DirectSum (LinearCovering.Fiber C.functor (obj T₂ x)) fun (Z : LinearCovering.Fiber C.functor (obj T₂ x)) => (↑Z).as ⟶ LinearPathCategory.obj k Q₁ y) : (LinearCovering.sourceFiberHomMap C.functor (obj T₂ x) (obj T₁ y)) ((C.sourceFiberQuotientMap x y) a) = (quotientFunctor T₂).map ((C.sourceFreeFiberHomMap x y) a)

The fixed-target free covering equivalence and the mesh-functor Hom map form a commutative square with the componentwise quotient maps.

structure MagnitudeConjecture.MeshCategory.RightMeshData.Cover.HasMeshIdealLifting {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)] : Prop

The exact remaining relation-lifting condition for a polarized mesh covering. It says that a free direct-sum element which lands in the target mesh ideal is already componentwise zero after quotienting by the source mesh ideal, in both Hom variables.

• target (x : Q₁) (y : Q₂) (a : DirectSum (LinearCovering.Fiber C.functor (obj T₂ y)) fun (Z : LinearCovering.Fiber C.functor (obj T₂ y)) => LinearPathCategory.obj k Q₁ x ⟶ (↑Z).as) : (quotientFunctor T₂).map ((C.targetFreeFiberHomMap x y) a) = 0 → (C.targetFiberQuotientMap x y) a = 0
• source (x : Q₂) (y : Q₁) (a : DirectSum (LinearCovering.Fiber C.functor (obj T₂ x)) fun (Z : LinearCovering.Fiber C.functor (obj T₂ x)) => (↑Z).as ⟶ LinearPathCategory.obj k Q₁ y) : (quotientFunctor T₂).map ((C.sourceFreeFiberHomMap x y) a) = 0 → (C.sourceFiberQuotientMap x y) a = 0

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.targetFiberHomMap_bijective_of_hasMeshIdealLifting {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)] (hC : C.HasMeshIdealLifting) (x : Q₁) (y : Q₂) : Function.Bijective ⇑(LinearCovering.targetFiberHomMap C.functor (obj T₁ x) (obj T₂ y))

Mesh-ideal lifting gives the fixed-source covering bijection at literal vertex objects.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.sourceFiberHomMap_bijective_of_hasMeshIdealLifting {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)] (hC : C.HasMeshIdealLifting) (x : Q₂) (y : Q₁) : Function.Bijective ⇑(LinearCovering.sourceFiberHomMap C.functor (obj T₂ x) (obj T₁ y))

Mesh-ideal lifting gives the fixed-target covering bijection at literal vertex objects.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.functor_isCovering_of_hasMeshIdealLifting {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)] (hC : C.HasMeshIdealLifting) : LinearCovering.IsCovering C.functor

Once mesh-ideal lifting is known, the induced mesh-category functor is a linear covering functor.