Refining an internal direct sum by decompositions of its summands #
If a module M is identified with an external direct sum ⨁ i, N i, and each summand N i is
in turn the internal direct sum of a family of submodules B i j, then M is the internal direct
sum of the images of all the B i j, indexed by the pairs ⟨i, j⟩ of the sigma type. This is the
step that iterates a decomposition, as in building a basis adapted to a chain of subgroups one
link at a time.
Main results #
LinearEquiv.isInternal_sigma_map: the images of theB i jform an internal direct sum.
theorem
LinearEquiv.isInternal_sigma_map
{R : Type u_1}
{ι : Type u_2}
{M : Type u_3}
[Semiring R]
[DecidableEq ι]
[AddCommMonoid M]
[Module R M]
{N : ι → Type u_4}
[(i : ι) → AddCommMonoid (N i)]
[(i : ι) → Module R (N i)]
{κ : ι → Type u_5}
[(i : ι) → DecidableEq (κ i)]
(E : (DirectSum ι fun (i : ι) => N i) ≃ₗ[R] M)
{B : (i : ι) → κ i → Submodule R (N i)}
(hB : ∀ (i : ι), DirectSum.IsInternal (B i))
:
DirectSum.IsInternal fun (x : (i : ι) × κ i) => Submodule.map (↑E ∘ₗ DirectSum.lof R ι N x.fst) (B x.fst x.snd)
Refining a decomposition by decompositions of its summands. If E identifies the
external direct sum ⨁ i, N i with M, and each N i is the internal direct sum of a family
B i, then M is the internal direct sum of the images of all the B i j in M, indexed by the
pairs ⟨i, j⟩.