Uniform irreducible-space bounds, including interval boundaries #
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupported_irreducible_finrank_le_hom
{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)
:
Module.finrank k
(CategoricalIrreducible.Space k (S.standardFormSupportedFamily m a) (S.standardFormSupportedFamily m b)) ≤ Module.finrank k (S.standardFormSupportedFamily m a ⟶ S.standardFormSupportedFamily m b)
Interval irreducible dimensions are bounded by their actual Hom dimensions even when restriction creates new irreducible maps.
theorem
MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupported_uniform_irreducible_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
(CategoricalIrreducible.Space k (S.standardFormSupportedFamily m a) (S.standardFormSupportedFamily m b)) ≤ D
The incoming-source and irreducible-dimension bounds use constants independent of the interval length and the target's distance from its ends.