Magnitude conjecture

MagnitudeConjecture.CategoryTheory.PositiveWeightStrictness

Positive right-additive weights imply strictness #

This is the finite tau-category form of Iyama's strictness argument. A positive label weight whose Euler defect is nonnegative at the projective boundary and zero elsewhere forces every first right-mesh map to be monic.

The proof uses the source-faithful generic Nakayama-ladder extraction vendored from the clean equidistribution formalization. It contains no module classification or OP-conjecture theorem layer.

source
noncomputable def MagnitudeConjecture.FiniteTauMatrix.rightMeshLabelWeightDefect {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (weight : Ind → ℤ) (x : Ind) :
ℤ

The Euler defect of the chosen right mesh at one label, evaluated by the canonical additive extension of a label weight.

Instances For
    source
    def MagnitudeConjecture.FiniteTauMatrix.IsPositiveRightAdditiveLabelWeight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (weight : Ind → ℤ) :
    Prop

    Iyama's positive right-additivity condition, expressed on the chosen indecomposable labels.

    Instances For
      source
      theorem MagnitudeConjecture.FiniteTauMatrix.rightMesh_mono_of_positiveRightAdditiveLabelWeight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] {Ind : Type w} [Fintype Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (weight : Ind → ℤ) (hweight : IsPositiveRightAdditiveLabelWeight T weight) (x : Ind) :
      CategoryTheory.Mono (T.rightMesh (T.obj x)).f

      A positive right-additive label weight makes every first map of the chosen right tau-sequences monic.

      source
      theorem MagnitudeConjecture.FiniteTauMatrix.HomMeshInverseData.ofPositiveRightAdditiveLabelWeight {k : Type s} [Field k] [IsAlgClosed k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.IsIdempotentComplete C] [CategoryTheory.Linear k C] [∀ (X Y : C), FiniteDimensional k (X ⟶ Y)] {Ind : Type w} [Fintype Ind] [DecidableEq Ind] (T : QuotientSubmoduleEquidistribution.Iyama.FiniteTauCategoryData C Ind) (weight : Ind → ℤ) (hweight : IsPositiveRightAdditiveLabelWeight T weight) :
      HomMeshInverseData T

      Over an algebraically closed field, a positive right-additive label weight supplies every hypothesis of the Hom--mesh inverse recurrence.