Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardFormARIncomingPreimage

Positive-length form of a nonsplit recovered morphism #

A nonsplit morphism between recovered standard-form vertices has no nonzero degree-zero scalar term, so its mesh-category preimage is an incoming sum.

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormARIncomingPreimageQuiver {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.standardFormARIncomingPreimageArrowFintype {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.exists_standardFormIncomingCoefficient_preimage_eq_incomingSum {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (x z : Fin S.n) (q : S.standardFormProjectiveVertexModuleIndecomposableSkeleton.obj x ⟶ S.standardFormProjectiveVertexModuleIndecomposableSkeleton.obj z) (hq : ¬CategoryTheory.IsSplitEpi q) :
      ∃ (coeff : S.standardFormRightMeshData.IncomingCoefficient x z), (S.standardFormRestrictedYonedaFunctor ⋯).preimage q = S.standardFormRightMeshData.incomingSum coeff

      A nonsplit recovered morphism has an incoming-sum preimage in the mesh category.