Magnitude conjecture

MagnitudeConjecture.Algebra.RightModuleStandardInteriorIrreducibleSpace

Exact irreducible-space comparison at interior interval targets #

source
noncomputable def MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupported_interior_irreducibleEquiv {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) (ht0 : 0 ≤ ↑b.snd) (htm : ↑b.snd ≤ ↑m - 2 * ↑S.standardFormIntervalControlHeight) :
CategoricalIrreducible.Space k (S.standardFormSupportedFamily m a).obj (S.standardFormSupportedFamily m b).obj ≃ₗ[k] CategoricalIrreducible.Space k (S.standardFormSupportedFamily m a) (S.standardFormSupportedFamily m b)

At an interior target, the full supported inclusion preserves the linear irreducible quotient exactly.

Instances For
    source
    theorem MagnitudeConjecture.RightModule.FiniteIndecomposableSkeleton.standardFormSupported_interior_irreducible_finrank {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) (ht0 : 0 ≤ ↑b.snd) (htm : ↑b.snd ≤ ↑m - 2 * ↑S.standardFormIntervalControlHeight) :
    Module.finrank k (CategoricalIrreducible.Space k (S.standardFormSupportedFamily m a) (S.standardFormSupportedFamily m b)) = Module.finrank k (CategoricalIrreducible.Space k (S.standardFormSupportedFamily m a).obj (S.standardFormSupportedFamily m b).obj)

    The interior comparison retains irreducible multiplicities.