Almost-split maps and nonprojectivity inside finite graded intervals #
def
MagnitudeConjecture.Graded.FiniteGradedModule.supportedUnderlying
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
{R : VectorGrading k A}
(m : ℕ)
:
CategoryTheory.Functor (SupportedCategory m) (ModuleCat A)
The actual module underlying an interval-supported graded module.
Instances For
instance
MagnitudeConjecture.Graded.FiniteGradedModule.instFaithfulSupportedCategoryModuleCatSupportedUnderlying
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
{R : VectorGrading k A}
(m : ℕ)
:
(supportedUnderlying m).Faithful
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.supported_rightAlmostSplit_of_underlying
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
{R : VectorGrading k A}
{m : ℕ}
{X Y : SupportedCategory m}
(f : X ⟶ Y)
(hf : QuotientSubmoduleEquidistribution.IsRightAlmostSplit (ModuleCat.ofHom ↑f.hom))
:
A homogeneous almost-split map stays almost split when both terms lie in the interval; all degree-zero factorizations remain in this full subcategory.
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.supported_rightMinimal_of_underlying
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
{R : VectorGrading k A}
{m : ℕ}
{X Y : SupportedCategory m}
(f : X ⟶ Y)
(hf : QuotientSubmoduleEquidistribution.IsRightMinimal (ModuleCat.ofHom ↑f.hom))
:
An ungraded right-minimal homogeneous map is right minimal in the interval.
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.supported_not_projective_of_underlying_nonsplit_epi
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
{R : VectorGrading k A}
{m : ℕ}
{X Y : SupportedCategory m}
(f : X ⟶ Y)
(hepi : CategoryTheory.Epi (ModuleCat.ofHom ↑f.hom))
(hn : ¬CategoryTheory.IsSplitEpi (ModuleCat.ofHom ↑f.hom))
:
¬CategoryTheory.Projective Y
A nonsplit epimorphism of underlying modules inside the interval witnesses nonprojectivity of its target in the interval category.