Ranges of composite linear maps

Range identities for factoring a composite through a linear map's image.

theorem LinearMap.range_comp_rangeRestrict {R : Type u_1} {V : Type u_2} {W : Type u_3} {N : Type u_4} [Semiring R] [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module R W] [AddCommMonoid N] [Module R N] (f : V →ₗ[R] W) (g : W →ₗ[R] N) : Set.range ⇑(g ∘ₗ f) = Set.range ⇑(g ∘ₗ f.range.subtype)

Composing through the range restriction does not change a composite linear map's range.

theorem LinearMap.range_comp_map_subtype {R : Type u_1} {V : Type u_2} {W : Type u_3} {N : Type u_4} [Semiring R] [AddCommMonoid V] [Module R V] [AddCommMonoid W] [Module R W] [AddCommMonoid N] [Module R N] (f : V →ₗ[R] W) (I : Submodule R V) (g : W →ₗ[R] N) : Set.range ⇑(g ∘ₗ f ∘ₗ I.subtype) = Set.range ⇑((g ∘ₗ f.range.subtype) ∘ₗ (Submodule.map f.rangeRestrict I).subtype)

Mapping a submodule into a linear map's range does not change the composite range.