Finite families of submodules under a linear map

Submodule.map preserves arbitrary suprema (Submodule.map_iSup), and along an injective map it also preserves infima (Submodule.map_inf) and hence disjointness (Submodule.disjoint_map). This file records what those facts say about a family of submodules indexed by a Finset: pushing it forward along a linear map turns a spanning family into one spanning the range of the map, and along an injective map it leaves an independent family independent.

The finite-set form is what a decomposition of a module into a Finset of submodules needs, as in TauCeti/RingTheory/KrullSchmidt/Existence.lean, when it is transported along a linear map.

Main results

• LinearMap.sup_image_map_eq_range_of_sup_eq_top: a finite family of submodules spanning the whole module is carried to one spanning the range of the map.
• LinearMap.supIndep_image_map: an injective linear map carries an independent finite family of submodules to an independent one.
• Submodule.map_eq_span_basis: the image of a based submodule is spanned by the images of its basis vectors.

theorem Submodule.map_eq_span_basis {R : Type u_1} {V : Type u_2} {W : Type u_3} {ι : Type u_4} [Semiring R] [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module R W] (p : Submodule R V) (b : Module.Basis ι R ↥p) (f : V →ₗ[R] W) : map f p = span R (Set.range fun (i : ι) => f ↑(b i))

The image of a based submodule is spanned by the images of its basis vectors.

theorem LinearMap.sup_image_map_eq_range_of_sup_eq_top {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {M' : Type v'} [AddCommMonoid M'] [Module R M'] [DecidableEq (Submodule R M')] (f : M →ₗ[R] M') {s : Finset (Submodule R M)} (hs : s.sup _root_.id = ⊤) : (Finset.image (Submodule.map f) s).sup _root_.id = f.range

A linear map carries a spanning finite family of submodules to a family spanning its range: the images of the members of a finite family with supremum ⊤ have supremum LinearMap.range f.

theorem LinearMap.supIndep_image_map {R : Type u} [Semiring R] {M : Type v} [AddCommMonoid M] [Module R M] {M' : Type v'} [AddCommMonoid M'] [Module R M'] [DecidableEq (Submodule R M')] (f : M →ₗ[R] M') (hf : Function.Injective ⇑f) {s : Finset (Submodule R M)} (hs : s.SupIndep _root_.id) : (Finset.image (Submodule.map f) s).SupIndep _root_.id

An injective linear map preserves independence of a finite family of submodules: the images of the members are again independent.