Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardSupportedIncomingBounds

Incoming shift and dimension bounds inside every supported interval #

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.supportedIncomingQuiver {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.supportedIncomingArrowFintype {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
      theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupported_incoming_shift_bounds {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (h : ℕ) (hb : ∀ (X Y : S.StandardFormMeshCategory) (d : ℤ), d < 0 ∨ ↑h < d → S.standardFormIntegerHomGrading.component X Y d = ⊥) {m : ℕ} (a b : S.standardFormSupportedLabel m) (f : S.standardFormSupportedFamily m a ⟶ S.standardFormSupportedFamily m b) (hf : f ≠ 0) :
      ↑b.snd ≤ ↑a.snd ∧ ↑a.snd ≤ ↑b.snd + ↑h

      Passing to supported modules preserves the common incoming shift window.

      source
      def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupportedHomEquiv {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {m : ℕ} (a b : S.standardFormSupportedLabel m) :
      (S.standardFormSupportedFamily m a ⟶ S.standardFormSupportedFamily m b) ≃ₗ[k] (S.standardFormSupportedFamily m a).obj ⟶ (S.standardFormSupportedFamily m b).obj

      The full supported subcategory retains exactly the ambient graded Hom space.

      Instances For
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupported_hom_finrank_le {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) {m : ℕ} (a b : S.standardFormSupportedLabel m) :
        Module.finrank k (S.standardFormSupportedFamily m a ⟶ S.standardFormSupportedFamily m b) ≤ Module.finrank k (MeshCategory.obj S.standardFormRightMeshData a.fst ⟶ MeshCategory.obj S.standardFormRightMeshData b.fst)

        Restricting to an interval leaves the fixed mesh Hom dimension as a bound, even for pairs whose irreducibility changes at the boundary.