The dimension of an internal direct sum

A vector space that is the internal direct sum of a finite family of finite-dimensional subspaces has the sum of their dimensions, Ado.finrank_eq_sum_finrank_of_isInternal. Finiteness is asked of the summands rather than of the ambient space: the two are equivalent here, and the former is the form available at a call site that only knows its summands.

Ado.finsum_finrank_eq_finrank_of_isInternal is the same count for a decomposition indexed by an arbitrary type in which all but finitely many summands vanish, written with finsum. A graded decomposition is usually indexed by ℤ even when only finitely many degrees occur, so this is the form such a decomposition meets.

Mathlib has Module.finrank_directSum for the external direct sum ⨁ i, M i and DirectSum.IsInternal for an internal decomposition, but not the dimension count that combining them gives; the bridge is the canonical isomorphism LinearEquiv.ofBijective (DirectSum.coeLinearMap V) an internal decomposition provides.

theorem Ado.finrank_eq_sum_finrank_of_isInternal {K : Type u_1} {M : Type u_2} {ι : Type u_3} [DivisionRing K] [AddCommGroup M] [Module K M] [Fintype ι] [DecidableEq ι] {V : ι → Submodule K M} [∀ (i : ι), Module.Finite K ↥(V i)] (h : DirectSum.IsInternal V) : Module.finrank K M = ∑ i : ι, Module.finrank K ↥(V i)

The dimensions of the summands of an internal direct sum add up.

theorem Ado.finrank_iSup_eq_sum_finrank_of_iSupIndep {K : Type u_1} {M : Type u_2} {ι : Type u_3} [DivisionRing K] [AddCommGroup M] [Module K M] [Fintype ι] {V : ι → Submodule K M} [∀ (i : ι), Module.Finite K ↥(V i)] (h : iSupIndep V) : Module.finrank K ↥(⨆ (i : ι), V i) = ∑ i : ι, Module.finrank K ↥(V i)

The dimension of an independent finite sum of subspaces is the sum of their dimensions. Unlike Ado.finrank_eq_sum_finrank_of_isInternal, the ambient module here is the supremum of the given family rather than an independently supplied module.

theorem Ado.finsum_finrank_eq_finrank_of_isInternal {K : Type u_1} {M : Type u_2} {ι : Type u_3} [DivisionRing K] [AddCommGroup M] [Module K M] [DecidableEq ι] {V : ι → Submodule K M} [∀ (i : ι), Module.Finite K ↥(V i)] (h : DirectSum.IsInternal V) (hV : {i : ι | V i ≠ ⊥}.Finite) : ∑ᶠ (i : ι), Module.finrank K ↥(V i) = Module.finrank K M

The dimensions of the summands of an internal direct sum add up, for a decomposition indexed by an arbitrary type in which only finitely many summands are nonzero.