Extending a nonnegative internal grading to integer degrees #
Mesh path lengths are natural numbers, whereas module shifts use integers. Extending the homogeneous components by zero preserves their internal sum.
def
MagnitudeConjecture.Graded.integerComponent
{k : Type u_1}
{M : Type u_2}
[Field k]
[AddCommGroup M]
[Module k M]
(A : ℕ → Submodule k M)
(d : ℤ)
:
Submodule k M
The integer-indexed family obtained by inserting zero in negative degrees.
Instances For
@[simp]
theorem
MagnitudeConjecture.Graded.integerComponent_nat
{k : Type u_1}
{M : Type u_2}
[Field k]
[AddCommGroup M]
[Module k M]
(A : ℕ → Submodule k M)
(n : ℕ)
:
integerComponent A ↑n = A n
theorem
MagnitudeConjecture.Graded.integerComponent_negative
{k : Type u_1}
{M : Type u_2}
[Field k]
[AddCommGroup M]
[Module k M]
(A : ℕ → Submodule k M)
(d : ℤ)
(hd : d < 0)
:
integerComponent A d = ⊥
theorem
MagnitudeConjecture.Graded.integerComponent_isInternal
{k : Type u_1}
{M : Type u_2}
[Field k]
[AddCommGroup M]
[Module k M]
(A : ℕ → Submodule k M)
(hA : DirectSum.IsInternal A)
:
DirectSum.IsInternal (integerComponent A)