feat(linear_algebra/finite_dimensional): add finrank_map_le (#8815)

Co-authored-by: Scott Morrison <scott@tqft.net>

Author: fpvandoorn

src/linear_algebra/dimension.lean

@@ -195,6 +195,11 @@ lemma dim_eq_of_injective (f : M →ₗ[R] M₁) (h : injective f) :
   module.rank R M = module.rank R f.range :=
 (linear_equiv.of_injective f (linear_map.ker_eq_bot.mpr h)).dim_eq
 
+/-- Pushforwards of submodules along a `linear_equiv` have the same dimension. -/
+lemma linear_equiv.dim_map_eq (f : M ≃ₗ[R] M₁) (p : submodule R M) :
+  module.rank R (p.map (f : M →ₗ[R] M₁)) = module.rank R p :=
+(f.of_submodule p).dim_eq.symm
+
 variables (R M)
 
 @[simp] lemma dim_top : module.rank R (⊤ : submodule R M) = module.rank R M :=

src/linear_algebra/finite_dimensional.lean

@@ -81,7 +81,7 @@ open_locale classical
 open cardinal submodule module function
 
 variables {K : Type u} {V : Type v} [field K] [add_comm_group V] [module K V]
-{V₂ : Type v'} [add_comm_group V₂] [module K V₂]
+variables {V₂ : Type v'} [add_comm_group V₂] [module K V₂]
 
 /-- `finite_dimensional` vector spaces are defined to be noetherian modules.
 Use `finite_dimensional.iff_fg` or `finite_dimensional.of_fintype_basis` to prove finite dimension
@@ -521,6 +521,26 @@ is_noetherian_span_of_finite K hA
 /-- The submodule generated by a single element is finite-dimensional. -/
 instance (x : V) : finite_dimensional K (K ∙ x) := by {apply span_of_finite, simp}
 
+/-- Pushforwards of finite-dimensional submodules are finite-dimensional. -/
+instance (f : V →ₗ[K] V₂) (p : submodule K V) [h : finite_dimensional K p] :
+  finite_dimensional K (p.map f) :=
+begin
+  unfreezingI { rw [finite_dimensional, is_noetherian.iff_dim_lt_omega ] at h ⊢ },
+  rw [← cardinal.lift_lt.{v' v}],
+  rw [← cardinal.lift_lt.{v v'}] at h,
+  rw [cardinal.lift_omega] at h ⊢,
+  exact (lift_dim_map_le f p).trans_lt h
+end
+
+/-- Pushforwards of finite-dimensional submodules have a smaller finrank. -/
+lemma finrank_map_le (f : V →ₗ[K] V₂) (p : submodule K V) [finite_dimensional K p] :
+  finrank K (p.map f) ≤ finrank K p :=
+begin
+  rw [← cardinal.nat_cast_le.{max v v'}, ← cardinal.lift_nat_cast.{v' v},
+    ← cardinal.lift_nat_cast.{v v'}, finrank_eq_dim K p, finrank_eq_dim K (p.map f)],
+  exact lift_dim_map_le f p
+end
+
 end finite_dimensional
 
 section zero_dim
@@ -709,6 +729,11 @@ begin
   simpa [← finrank_eq_dim] using f.lift_dim_eq
 end
 
+/-- Pushforwards of finite-dimensional submodules along a `linear_equiv` have the same finrank. -/
+lemma finrank_map_eq (f : V ≃ₗ[K] V₂) (p : submodule K V) [finite_dimensional K p] :
+  finrank K (p.map (f : V →ₗ[K] V₂)) = finrank K p :=
+(f.of_submodule p).finrank_eq.symm
+
 end linear_equiv
 
 instance finite_dimensional_finsupp {ι : Type*} [fintype ι] [finite_dimensional K V] :