feat(linear_algebra/finite_dimensional): finrank_range_of_inj (#12067)

The dimensions of the domain and range of an injective linear map are
equal.





Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: hparshall

src/linear_algebra/finite_dimensional.lean

@@ -793,15 +793,21 @@ protected theorem finite_dimensional (f : V ≃ₗ[K] V₂) [finite_dimensional
 module.finite.equiv f
 
 /-- The dimension of a finite dimensional space is preserved under linear equivalence. -/
-theorem finrank_eq (f : V ≃ₗ[K] V₂) [finite_dimensional K V] :
+theorem finrank_eq (f : V ≃ₗ[K] V₂) :
   finrank K V = finrank K V₂ :=
 begin
-  haveI : finite_dimensional K V₂ := f.finite_dimensional,
-  simpa [← finrank_eq_dim] using f.lift_dim_eq
+  by_cases h : finite_dimensional K V,
+  { resetI,
+    haveI : finite_dimensional K V₂ := f.finite_dimensional,
+    simpa [← finrank_eq_dim] using f.lift_dim_eq },
+  { rw [finrank_of_infinite_dimensional h, finrank_of_infinite_dimensional],
+    contrapose! h,
+    resetI,
+    exact f.symm.finite_dimensional }
 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] :
+lemma finrank_map_eq (f : V ≃ₗ[K] V₂) (p : submodule K V) :
   finrank K (p.map (f : V →ₗ[K] V₂)) = finrank K p :=
 (f.submodule_map p).finrank_eq.symm
 
@@ -858,6 +864,11 @@ lemma eq_of_le_of_finrank_eq {S₁ S₂ : submodule K V} [finite_dimensional K S
   (hd : finrank K S₁ = finrank K S₂) : S₁ = S₂ :=
 eq_of_le_of_finrank_le hle hd.ge
 
+@[simp]
+lemma finrank_map_subtype_eq (p : subspace K V) (q : subspace K p) :
+  finite_dimensional.finrank K (q.map p.subtype) = finite_dimensional.finrank K q :=
+(submodule.equiv_subtype_map p q).symm.finrank_eq
+
 variables [finite_dimensional K V] [finite_dimensional K V₂]
 
 /-- Given isomorphic subspaces `p q` of vector spaces `V` and `V₁` respectively,
@@ -881,11 +892,6 @@ begin
       ← linear_equiv.finrank_eq f, add_comm, submodule.finrank_quotient_add_finrank]
 end
 
-@[simp]
-lemma finrank_map_subtype_eq (p : subspace K V) (q : subspace K p) :
-  finite_dimensional.finrank K (q.map p.subtype) = finite_dimensional.finrank K q :=
-(submodule.equiv_subtype_map p q).symm.finrank_eq
-
 end finite_dimensional
 
 namespace linear_map
@@ -950,6 +956,11 @@ theorem finrank_range_add_finrank_ker [finite_dimensional K V] (f : V →ₗ[K]
   finrank K f.range + finrank K f.ker = finrank K V :=
 by { rw [← f.quot_ker_equiv_range.finrank_eq], exact submodule.finrank_quotient_add_finrank _ }
 
+/-- The dimensions of the domain and range of an injective linear map are equal. -/
+lemma finrank_range_of_inj {f : V →ₗ[K] V₂} (hf : function.injective f) :
+  finrank K f.range = finrank K V :=
+by rw (linear_equiv.of_injective f hf).finrank_eq
+
 end linear_map
 
 namespace linear_equiv