Lifting mesh ideals along polarized quiver coverings

This file proves the relation-lifting statement left open by the quotient squares for mesh coverings. The first half treats the fixed-target Hom map: a path-basis composite through a target mesh lifts to one source mesh composite in a uniquely determined fibre component.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.exists_lifted_nonprojective_of_tau_fiber {Q₁ : Type v₁} [Quiver Q₁] {Q₂ : Type v₂} [Quiver Q₂] {T₁ : RightMeshData Q₁} {T₂ : RightMeshData Q₂} (C : T₁.Cover T₂) (s : { z : Q₂ // z ∉ T₂.projective }) (t : Q₁) (ht : C.toPrefunctor.obj t = T₂.tau s) (a : T₂.MeshArrow s) : ∃ (s₁ : { z : Q₁ // z ∉ T₁.projective }), C.mapNonprojective s₁ = s ∧ T₁.tau s₁ = t

A vertex over the translated end of a nonempty target mesh is itself the translate of a uniquely determined lift of the mesh vertex.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.source_basisComposite_has_ideal_preimage {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₂) [(z : Q₂) → Fintype (Quiver.Star z)] (x : Q₂) (y : Q₁) {f : LinearPathCategory.obj k Q₂ x ⟶ LinearPathCategory.obj k Q₂ (C.toPrefunctor.obj y)} (hf : f ∈ LinearPathCategory.basisCompositeSet T₂.meshGeneratorSet (LinearPathCategory.obj k Q₂ x) (LinearPathCategory.obj k Q₂ (C.toPrefunctor.obj y))) : ∃ (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), (C.sourceFreeFiberHomMap x y) a = f ∧ (C.sourceFiberQuotientMap x y) a = 0

A path-basis composite through one target mesh has a free fixed-target preimage supported in one fibre component, and that preimage belongs to the source mesh ideal.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.target_basisComposite_has_ideal_preimage {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₂) [(z : Q₂) → Fintype (Quiver.Star z)] (x : Q₁) (y : Q₂) {f : LinearPathCategory.obj k Q₂ (C.toPrefunctor.obj x) ⟶ LinearPathCategory.obj k Q₂ y} (hf : f ∈ LinearPathCategory.basisCompositeSet T₂.meshGeneratorSet (LinearPathCategory.obj k Q₂ (C.toPrefunctor.obj x)) (LinearPathCategory.obj k Q₂ y)) : ∃ (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), (C.targetFreeFiberHomMap x y) a = f ∧ (C.targetFiberQuotientMap x y) a = 0

A path-basis composite through one target mesh has a free fixed-source preimage supported in one fibre component, and that preimage belongs to the source mesh ideal.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.target_meshIdeal_has_ideal_preimage {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₂) [(z : Q₂) → Fintype (Quiver.Star z)] (x : Q₁) (y : Q₂) {f : LinearPathCategory.obj k Q₂ (C.toPrefunctor.obj x) ⟶ LinearPathCategory.obj k Q₂ y} (hf : f ∈ T₂.meshIdealHom (C.toPrefunctor.obj x) y) : ∃ (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), (C.targetFreeFiberHomMap x y) a = f ∧ (C.targetFiberQuotientMap x y) a = 0

Every target mesh-ideal element has a free fixed-source preimage which is already zero after componentwise quotienting by the source mesh ideal.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.target_meshIdealLifting {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₂) [(z : Q₂) → Fintype (Quiver.Star z)] (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

The fixed-source half of mesh-ideal lifting holds for every polarized quiver covering.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.source_meshIdeal_has_ideal_preimage {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₂) [(z : Q₂) → Fintype (Quiver.Star z)] (x : Q₂) (y : Q₁) {f : LinearPathCategory.obj k Q₂ x ⟶ LinearPathCategory.obj k Q₂ (C.toPrefunctor.obj y)} (hf : f ∈ T₂.meshIdealHom x (C.toPrefunctor.obj y)) : ∃ (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), (C.sourceFreeFiberHomMap x y) a = f ∧ (C.sourceFiberQuotientMap x y) a = 0

Every target mesh-ideal element has a free fixed-target preimage which is already zero after componentwise quotienting by the source mesh ideal.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.source_meshIdealLifting {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₂) [(z : Q₂) → Fintype (Quiver.Star z)] (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

The fixed-target half of mesh-ideal lifting holds for every polarized quiver covering.

theorem 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₂) [(z : Q₂) → Fintype (Quiver.Star z)] : C.HasMeshIdealLifting

Every polarized quiver covering lifts the generated mesh ideal in both Hom variables.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.functor_isCovering {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₂) [(z : Q₂) → Fintype (Quiver.Star z)] : LinearCovering.IsCovering C.functor

A covering of polarized right translation quivers induces a Bongartz-- Gabriel covering functor between their mesh categories.

theorem MagnitudeConjecture.MeshCategory.RightMeshData.Cover.functorUsingSourceFintype_isCovering {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₂) [sourceStarFintype : (z : Q₁) → Fintype (Quiver.Star z)] [(z : Q₂) → Fintype (Quiver.Star z)] : LinearCovering.IsCovering C.functorUsingSourceFintype

The ambient-source version of the mesh functor is also a Bongartz-- Gabriel covering. The only comparison needed is uniqueness of the Fintype structure on each arrow star.