Dimensions of images of linear maps

Main results

• LinearMap.finrank_map_add_finrank_inf_ker: rank–nullity for the restriction of a linear map to a finite-dimensional subspace V: finrank (V.map φ) + finrank (V ⊓ ker φ) = finrank V.
• LinearMap.finrank_span_range_le: extending the scalars of the span of the image of a K-linear map g : V → A to a field L cannot increase its dimension beyond finrank K V.
• LinearMap.finrank_span_range_le_of_ker_le: the same bound by the rank of any linear map whose kernel is contained in the kernel of g.

theorem LinearMap.finrank_map_add_finrank_inf_ker {K : Type u_1} {M : Type u_2} {W : Type u_3} [DivisionRing K] [AddCommGroup M] [Module K M] [AddCommGroup W] [Module K W] (φ : M →ₗ[K] W) (V : Submodule K M) [FiniteDimensional K ↥V] : Module.finrank K ↥(Submodule.map φ V) + Module.finrank K ↥(V ⊓ φ.ker) = Module.finrank K ↥V

Rank–nullity for the restriction of a linear map to a finite-dimensional subspace.

theorem LinearMap.finrank_span_range_le {K : Type u_1} {L : Type u_2} {V : Type u_3} {A : Type u_4} [Field K] [Field L] [Algebra K L] [AddCommGroup V] [Module K V] [Module.Finite K V] [AddCommGroup A] [Module K A] [Module L A] [IsScalarTower K L A] (g : V →ₗ[K] A) : Module.finrank L ↥(Submodule.span L (Set.range ⇑g)) ≤ Module.finrank K V

Extending the scalars of the span of a linear image cannot increase its dimension beyond the dimension of its source.

theorem LinearMap.finrank_span_range_le_of_ker_le {K : Type u_1} {L : Type u_2} {V : Type u_3} {W : Type u_4} {A : Type u_5} [Field K] [Field L] [Algebra K L] [AddCommGroup V] [Module K V] [Module.Finite K V] [AddCommGroup W] [Module K W] [AddCommGroup A] [Module K A] [Module L A] [IsScalarTower K L A] (f : V →ₗ[K] W) (g : V →ₗ[K] A) (h : f.ker ≤ g.ker) : Module.finrank L ↥(Submodule.span L (Set.range ⇑g)) ≤ Module.finrank K ↥f.range

A factorization through a K-linear image bounds the dimension after extending the span to L.