Supports of shifted graded modules and their direct summands #
noncomputable def
MagnitudeConjecture.Graded.FiniteGradedModule.shiftedSupport
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
{R : VectorGrading k A}
(X : ShiftedModule)
:
Finset ℤ
The physical degrees of a module after applying its external shift.
Instances For
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.shiftedSupport_subset_of_injective
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
{R : VectorGrading k A}
{X Y : ShiftedModule}
(f : X ⟶ Y)
(hinj : Function.Injective fun (x : ↑X.obj.module) => (↑f).toFun x)
:
shiftedSupport X ⊆ shiftedSupport Y
Injective homogeneous maps cannot remove a nonzero source component.
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.shiftedSupport_subset_of_splitMono
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
{R : VectorGrading k A}
{X Y : ShiftedModule}
(f : X ⟶ Y)
[CategoryTheory.IsSplitMono f]
:
shiftedSupport X ⊆ shiftedSupport Y
A graded direct summand has support contained in the ambient module.
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.shiftedSupport_eq_of_iso
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
{R : VectorGrading k A}
{X Y : ShiftedModule}
(e : X ≅ Y)
:
shiftedSupport X = shiftedSupport Y
Graded isomorphisms preserve the exact shifted support.
def
MagnitudeConjecture.Graded.FiniteGradedModule.SupportedIn
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
{R : VectorGrading k A}
(m : ℕ)
(X : ShiftedModule)
:
Modules whose physical support lies in the integer interval [0,m].
Instances For
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.supportedIn_of_splitMono
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
{R : VectorGrading k A}
{m : ℕ}
{X Y : ShiftedModule}
(f : X ⟶ Y)
[CategoryTheory.IsSplitMono f]
(hY : SupportedIn m Y)
:
SupportedIn m X
theorem
MagnitudeConjecture.Graded.FiniteGradedModule.supportedIn_iff_of_iso
{k A : Type u}
[Field k]
[Ring A]
[Algebra k A]
{R : VectorGrading k A}
{m : ℕ}
{X Y : ShiftedModule}
(e : X ≅ Y)
:
SupportedIn m X ↔ SupportedIn m Y