Magnitude conjecture

MagnitudeConjecture.CategoryTheory.MeshIdealEndpoint

Endpoint normal forms for the ordinary mesh ideal #

At a fixed target, a mesh-ideal element is a left multiple of the mesh relation at that target, when it exists, plus ideal-valued coefficients followed by the incoming arrows. At a projective target the first summand is absent. The proof expands the right path-basis multiplier and peels its first reverse-quiver arrow.

source
@[reducible, inline]
noncomputable abbrev MagnitudeConjecture.MeshCategory.RightMeshData.meshIdealHom {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x z : Q) :
Submodule k (MagnitudeConjecture.MeshCategory.RightMeshData.freeObj✝ x ⟶ MagnitudeConjecture.MeshCategory.RightMeshData.freeObj✝ z)

The generated mesh-ideal submodule in one free-category Hom space.

Instances For
    source
    def MagnitudeConjecture.MeshCategory.RightMeshData.HasNonprojectiveEndingNormalForm {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : { z : Q // z ∉ T.projective }) (x : Q) (f : MagnitudeConjecture.MeshCategory.RightMeshData.freeObj✝ x ⟶ MagnitudeConjecture.MeshCategory.RightMeshData.freeObj✝ ↑z) :
    Prop

    Endpoint normal form when the target carries a mesh relation.

    Instances For
      source
      def MagnitudeConjecture.MeshCategory.RightMeshData.HasProjectiveEndingNormalForm {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z x : Q) (f : MagnitudeConjecture.MeshCategory.RightMeshData.freeObj✝ x ⟶ MagnitudeConjecture.MeshCategory.RightMeshData.freeObj✝ z) :
      Prop

      Endpoint normal form at a projective target.

      Instances For
        source
        theorem MagnitudeConjecture.MeshCategory.RightMeshData.meshIdeal_hasNonprojectiveEndingNormalForm {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : { z : Q // z ∉ T.projective }) (x : Q) {f : MagnitudeConjecture.MeshCategory.RightMeshData.freeObj✝ x ⟶ MagnitudeConjecture.MeshCategory.RightMeshData.freeObj✝ ↑z} (hf : f ∈ T.meshIdealHom x ↑z) :
        T.HasNonprojectiveEndingNormalForm z x f

        Every mesh-ideal element ending at a nonprojective vertex has the exact endpoint normal form.

        source
        theorem MagnitudeConjecture.MeshCategory.RightMeshData.meshIdeal_hasProjectiveEndingNormalForm {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (z : Q) (hz : z ∈ T.projective) (x : Q) {f : MagnitudeConjecture.MeshCategory.RightMeshData.freeObj✝ x ⟶ MagnitudeConjecture.MeshCategory.RightMeshData.freeObj✝ z} (hf : f ∈ T.meshIdealHom x z) :
        T.HasProjectiveEndingNormalForm z x f

        Every mesh-ideal element ending at a projective vertex is an incoming sum with ideal-valued coefficients; no endpoint mesh relation occurs.

        source
        theorem MagnitudeConjecture.MeshCategory.RightMeshData.quotient_map_eq_zero_iff_mem_meshIdealHom {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(x : Q) → Fintype ((y : Q) × (x ⟶ y))] (T : RightMeshData Q) (x z : Q) (f : MagnitudeConjecture.MeshCategory.RightMeshData.freeObj✝ x ⟶ MagnitudeConjecture.MeshCategory.RightMeshData.freeObj✝ z) :
        (quotientFunctor T).map f = 0 ↔ f ∈ T.meshIdealHom x z

        A free morphism maps to zero in the mesh quotient exactly when it lies in the generated mesh ideal.