Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardIntervalDirected

Directedness of the actual standard-form interval modules #

source
theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalFamily_noniso_descent {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) (f : S.standardFormIntervalFamily m a ⟶ S.standardFormIntervalFamily m b) (hf : f ≠ 0) (hi : ¬CategoryTheory.IsIso f) :
↑b.snd < ↑a.snd

A nonzero nonisomorphism between actual interval modules strictly lowers the shift label.

source
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalEdge {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) :
Prop

Nonzero nonisomorphisms between the selected actual interval modules.

Instances For
    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormIntervalFamily_acyclic {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) (m : ℕ) (a : S.standardFormSupportedLabel m) :
    ¬Relation.TransGen (S.standardFormIntervalEdge m) a a

    The complete indecomposable family of the interval algebra is directed.