Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardFormSimpleResolution

Projective simple resolutions in the standard-form mesh category #

The generic mesh-simple presentation is exact at its middle term, but its translation map need not be monic for an arbitrary translation quiver. For the standard form the normalized universal realization identifies the arrows leaving a translated mesh source with a genuine left almost-split monomorphism. The two covering Hom equivalences therefore make the translation map monic downstairs.

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSimpleResolutionQuiver {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.standardFormSimpleResolutionArrowFintype {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
      noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.UniversalCover.projectedOutgoingArrow {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (d : Quiver.Costar W) :
      MeshCategory.RightMeshData.OutgoingArrow W.fst

      The base outgoing categorical arrow underlying an outgoing arrow at a universal-cover vertex.

      Instances For
        source
        @[simp]
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.UniversalCover.meshProjection_map_outgoingArrowHom {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 : MeshCategory.RightMeshData.UniversalCover.Vertex S.standardFormRightMeshData x₀) (d : Quiver.Costar W) :
        (meshProjection S x₀).map ((MeshCategory.RightMeshData.UniversalCover.rightMeshData S.standardFormRightMeshData x₀).outgoingArrowHom d) = S.standardFormRightMeshData.outgoingArrowHom (projectedOutgoingArrow S x₀ W d)

        The universal mesh projection sends an outgoing represented arrow to its underlying outgoing represented arrow downstairs.

        source
        @[simp]
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.UniversalCover.projectedOutgoingArrow_meshStarCostarEquiv {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) :
        projectedOutgoingArrow S x₀ (MeshCategory.RightMeshData.UniversalCover.tau S.standardFormRightMeshData x₀ W) ((S.standardFormUniversalMeshStarCostarEquiv x₀ W) d) = ⟨d.fst.fst, (S.standardFormRightMeshData.arrowEquiv (MeshCategory.RightMeshData.UniversalCover.baseNonprojective S.standardFormRightMeshData x₀ W) d.fst.fst) ((MeshCategory.RightMeshData.UniversalCover.projection S.standardFormRightMeshData x₀).map d.snd)⟩
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormPairedCoefficientLinearMap_injective {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) :
        Function.Injective ⇑(S.standardFormRightMeshData.pairedCoefficientLinearMap z x)

        Every evaluated translation map in the standard-form mesh-simple presentation is injective.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormAdditiveTranslationMap_mono {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 }) :
        CategoryTheory.Mono (S.standardFormRightMeshData.additiveTranslationMap z)

        The first map of the standard-form right mesh is already monic in the finite additive hull of the raw mesh category.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormTranslationMap_mono {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 }) :
        CategoryTheory.Mono (S.standardFormRightMeshData.translationMap z)

        The first differential in the standard-form mesh-simple presentation is a monomorphism in the ambient module category.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormTranslationMapFinite_mono {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hP : S.standardFormRightMeshData.FiniteContravariantRepresentables) (z : { z : Fin S.n // z ∉ S.standardFormProjectiveSet }) :
        CategoryTheory.Mono (S.standardFormRightMeshData.translationMapFinite hP z)

        The finite-dimensional lift of the standard-form translation map is monic.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIncomingMap_mono_of_projective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (z : Fin S.n) (hz : z ∈ S.standardFormProjectiveSet) :
        CategoryTheory.Mono (S.standardFormRightMeshData.incomingMap z)

        At a projective boundary vertex, the incoming map is monic in the ambient module category.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIncomingMapFinite_mono_of_projective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hP : S.standardFormRightMeshData.FiniteContravariantRepresentables) (z : Fin S.n) (hz : z ∈ S.standardFormProjectiveSet) :
        CategoryTheory.Mono (S.standardFormRightMeshData.incomingMapFinite hP z)

        The finite-dimensional incoming map at a projective boundary vertex is monic.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormProjectiveSimpleFiniteModule_hasProjectiveDimensionLE_one {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hP : S.standardFormRightMeshData.FiniteContravariantRepresentables) (z : Fin S.n) (hz : z ∈ S.standardFormProjectiveSet) :
        CategoryTheory.HasProjectiveDimensionLE (S.standardFormRightMeshData.simpleFiniteModule z) 1

        At a projective boundary vertex, the finite mesh simple has projective dimension at most one.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSimpleFiniteModule_hasProjectiveDimensionLE_two_of_nonprojective {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hP : S.standardFormRightMeshData.FiniteContravariantRepresentables) (z : { z : Fin S.n // z ∉ S.standardFormProjectiveSet }) :
        CategoryTheory.HasProjectiveDimensionLE (S.standardFormRightMeshData.simpleFiniteModule ↑z) 2

        At a nonprojective vertex, the standard-form mesh complex is a length-two projective resolution of the corresponding finite mesh simple.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSimpleFiniteModule_hasProjectiveDimensionLE_two {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (hP : S.standardFormRightMeshData.FiniteContravariantRepresentables) (z : Fin S.n) :
        CategoryTheory.HasProjectiveDimensionLE (S.standardFormRightMeshData.simpleFiniteModule z) 2

        Every standard-form finite mesh simple has projective dimension at most two, with the projective boundary case bounded by one.