Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardFormMeshExact

Downstairs mesh exactness in standard form #

Universal-cover mesh exactness descends to the standard-form mesh category. This is the first chain-level stage in the proof of mesh Ext vanishing.

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshExtVanishingQuiver {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
Quiver (Fin S.n)
Instances For
    source
    @[instance_reducible]
    noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMeshExtVanishingArrowFintype {k A : Type u} [Field k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x y : Fin S.n) :
    Fintype (x ⟶ y)
    Instances For
      source
      @[simp]
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.UniversalCover.meshProjection_map_standardFormUniversalPairedIncomingHom {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x₀ : Fin S.n) (W : { W : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀ // W ∉ MeshCategory.RightMeshData.UniversalCover.projectiveSet S.standardFormRightMeshData x₀ }) (d : Quiver.Star ↑W) :
      (meshProjection S x₀).map (S.standardFormUniversalPairedIncomingHom x₀ W d) = S.standardFormRightMeshData.incomingArrowHom ⟨S.standardFormTau (MeshCategory.RightMeshData.UniversalCover.baseNonprojective S.standardFormRightMeshData x₀ W), (S.standardFormRightMeshData.arrowEquiv (MeshCategory.RightMeshData.UniversalCover.baseNonprojective S.standardFormRightMeshData x₀ W) (projectedIncomingArrow S x₀ (↑W) d).fst) (projectedIncomingArrow S x₀ (↑W) d).snd⟩

      Projection sends a polarized partner upstairs to the polarized partner of the projected incoming arrow downstairs.

      source
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormMesh_nonprojective_outgoing_exact {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : { z : Fin S.n // z ∉ S.standardFormProjectiveSet }) (x : Fin S.n) (c : (a : MeshCategory.RightMeshData.IncomingArrow ↑z) → MeshCategory.obj S.standardFormRightMeshData a.fst ⟶ MeshCategory.obj S.standardFormRightMeshData x) (hc : ∑ a : MeshCategory.RightMeshData.IncomingArrow ↑z, CategoryTheory.CategoryStruct.comp (S.standardFormRightMeshData.incomingArrowHom ⟨S.standardFormTau z, (S.standardFormRightMeshData.arrowEquiv z a.fst) a.snd⟩) (c a) = 0) :
      ∃ (t : MeshCategory.obj S.standardFormRightMeshData ↑z ⟶ MeshCategory.obj S.standardFormRightMeshData x), ∀ (a : MeshCategory.RightMeshData.IncomingArrow ↑z), c a = CategoryTheory.CategoryStruct.comp (S.standardFormRightMeshData.incomingArrowHom a) t

      Downstairs Hom exactness at the middle term of the nonprojective mesh-simple resolution. A relation among the polarized partners is obtained by postcomposing all incoming arrows with one morphism.