Direct sums whose summands vanish outside a finite set

A direct sum ⨁ i, M i over an infinite index type still behaves like a finite one as soon as all but finitely many summands are trivial: a family graded by ℤ with finitely many nonzero degrees is the standard example. TauCeti.DirectSum.restrictLinearEquiv identifies such a direct sum with the direct sum over a finite set of indices carrying the nonzero summands. The two consequences a graded dimension count needs follow: such a direct sum is a finite module, and its dimension is the finite sum of the dimensions of its summands. Mathlib's Module.finrank_directSum asks the index type itself to be finite, which a family graded by ℤ does not satisfy. The parallel count for an internal decomposition of a fixed module is in TauCeti.LinearAlgebra.Dimension.DirectSum.

Main definitions

• TauCeti.DirectSum.restrictLinearEquiv: the equivalence (⨁ i, M i) ≃ₗ[R] ⨁ i : s, M i for a finite set s outside which the summands are trivial.
• TauCeti.DirectSum.componentLinearEquiv: the extreme case of a single surviving index, where the direct sum is the equivalence (⨁ i, M i) ≃ₗ[R] M d.

Main results

• TauCeti.DirectSum.finite_of_subsingleton_notMem: such a direct sum is a finite module.
• TauCeti.finrank_directSum_eq_sum: its dimension is the sum of the dimensions of the summands indexed by the finite set.

def TauCeti.DirectSum.restrictLinearEquiv {ι : Type v} [DecidableEq ι] {R : Type u} [Semiring R] (M : ι → Type w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (s : Finset ι) (hs : ∀ i ∉ s, Subsingleton (M i)) : (DirectSum ι fun (i : ι) => M i) ≃ₗ[R] DirectSum ↥s fun (i : ↥s) => M ↑i

Restricting a direct sum to a finite set of indices. If every summand outside a finite set s is trivial, then ⨁ i, M i is the direct sum of the summands indexed by s.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.DirectSum.restrictLinearEquiv_lof {ι : Type v} [DecidableEq ι] {R : Type u} [Semiring R] (M : ι → Type w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (s : Finset ι) (hs : ∀ i ∉ s, Subsingleton (M i)) {i : ι} (hi : i ∈ s) (x : M i) : (restrictLinearEquiv M s hs) ((DirectSum.lof R ι M i) x) = (DirectSum.lof R (↥s) (fun (j : ↥s) => M ↑j) ⟨i, hi⟩) x

The restriction equivalence sends the summand at an index of s to the same summand.

@[simp]

theorem TauCeti.DirectSum.restrictLinearEquiv_lof_of_notMem {ι : Type v} [DecidableEq ι] {R : Type u} [Semiring R] (M : ι → Type w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (s : Finset ι) (hs : ∀ i ∉ s, Subsingleton (M i)) {i : ι} (hi : i ∉ s) (x : M i) : (restrictLinearEquiv M s hs) ((DirectSum.lof R ι M i) x) = 0

The restriction equivalence sends a summand outside s to zero.

@[simp]

theorem TauCeti.DirectSum.restrictLinearEquiv_symm_lof {ι : Type v} [DecidableEq ι] {R : Type u} [Semiring R] (M : ι → Type w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (s : Finset ι) (hs : ∀ i ∉ s, Subsingleton (M i)) (i : ↥s) (x : M ↑i) : (restrictLinearEquiv M s hs).symm ((DirectSum.lof R (↥s) (fun (j : ↥s) => M ↑j) i) x) = (DirectSum.lof R ι M ↑i) x

The restriction equivalence is inverse to the evident inclusion of the summands indexed by s.

def TauCeti.DirectSum.componentLinearEquiv {ι : Type v} [DecidableEq ι] {R : Type u} [Semiring R] (M : ι → Type w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (d : ι) (hd : ∀ (i : ι), i ≠ d → Subsingleton (M i)) : (DirectSum ι fun (i : ι) => M i) ≃ₗ[R] M d

A direct sum concentrated in a single index is that summand. This is the extreme case of TauCeti.DirectSum.restrictLinearEquiv, in the form in which a grading concentrated in one degree meets it.

Equations

• TauCeti.DirectSum.componentLinearEquiv M d hd = LinearEquiv.ofLinearMap (DirectSum.component R ι M d) (DirectSum.lof R ι M d) ⋯ ⋯

@[simp]

theorem TauCeti.DirectSum.componentLinearEquiv_apply {ι : Type v} [DecidableEq ι] {R : Type u} [Semiring R] (M : ι → Type w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (d : ι) (hd : ∀ (i : ι), i ≠ d → Subsingleton (M i)) (x : DirectSum ι fun (i : ι) => M i) : (componentLinearEquiv M d hd) x = (DirectSum.component R ι M d) x

The equivalence with a single surviving summand is the projection to that summand.

@[simp]

theorem TauCeti.DirectSum.componentLinearEquiv_symm_apply {ι : Type v} [DecidableEq ι] {R : Type u} [Semiring R] (M : ι → Type w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (d : ι) (hd : ∀ (i : ι), i ≠ d → Subsingleton (M i)) (x : M d) : (componentLinearEquiv M d hd).symm x = (DirectSum.lof R ι M d) x

Its inverse is the inclusion of that summand.

theorem TauCeti.DirectSum.finite_of_subsingleton_notMem {ι : Type v} {R : Type u} [Semiring R] (M : ι → Type w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (s : Finset ι) [∀ (i : ↥s), Module.Finite R (M ↑i)] (hs : ∀ i ∉ s, Subsingleton (M i)) : Module.Finite R (DirectSum ι fun (i : ι) => M i)

A direct sum whose potentially nontrivial summands lie in a finite set and are finite modules is a finite module, even though the index type may be infinite.

theorem TauCeti.finrank_directSum_eq_sum {ι : Type v} {K : Type u} [DivisionRing K] (M : ι → Type w) [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module K (M i)] (s : Finset ι) [∀ (i : ↥s), Module.Finite K (M ↑i)] (hs : ∀ i ∉ s, Subsingleton (M i)) : Module.finrank K (DirectSum ι fun (i : ι) => M i) = ∑ i ∈ s, Module.finrank K (M i)

The dimension of a direct sum with finitely many nonzero summands. Unlike Module.finrank_directSum, the index type here may be infinite; what is asked instead is a finite set of finite-dimensional summands outside which the summands are trivial.