Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardSupportedUniformIncoming

Uniform incoming bounds independent of the interval length #

source
@[instance_reducible]
def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.uniformIncomingQuiver {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.uniformIncomingArrowFintype {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_uniform_incoming_bounds {k A : Type u} [Field k] [IsAlgClosed k] [Ring A] [Algebra k A] [FiniteDimensional k A] [IsNoetherianRing Aᵐᵒᵖ] (S : FiniteIndecomposableSkeleton k A) :
      ∃ (h : ℕ) (D : ℕ), 1 ≤ h ∧ ∀ (m : ℕ), (∀ (b : S.standardFormSupportedLabel m), Nat.card (S.standardFormSupportedIncomingLabel b) ≤ S.n * (h + 1)) ∧ ∀ (a b : S.standardFormSupportedLabel m), Module.finrank k (S.standardFormSupportedFamily m a ⟶ S.standardFormSupportedFamily m b) ≤ D

      One pair of constants bounds the number of incoming indecomposable sources and every Hom dimension for every finite interval.