Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardFormARShortExact

Short exact recovered standard-form meshes #

The additive standard mesh becomes a nonsplit short exact sequence under the recovered restricted-Yoneda equivalence, and its terminal map is right minimal.

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormARQuiver {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.standardFormARArrowFintype {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
      @[reducible, inline]
      noncomputable abbrev MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRecoveredRightMesh {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.ShortComplex S.StandardFormProjectiveVertexModuleCategory

      The additive standard mesh after restricted-Yoneda recovery.

      Instances For
        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRecoveredRightMesh_shortExact {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 }) :
        (S.standardFormRecoveredRightMesh z).ShortExact

        Recovered standard meshes are short exact.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRecoveredRightMesh_g_not_splitEpi {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.IsSplitEpi (S.standardFormRecoveredRightMesh z).g

        The recovered incoming mesh remains nonsplit.

        source
        theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormRecoveredRightMesh_g_rightMinimal {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 }) :
        QuotientSubmoduleEquidistribution.IsRightMinimal (S.standardFormRecoveredRightMesh z).g

        The recovered incoming mesh is right minimal.