refactor(linear_algebra/*): linear_equiv.of_bijective over semirings (#…

…9061)

`linear_equiv.of_injective` and `linear_equiv.of_bijective`
took as assumption `f.ker = \bot`,
which is equivalent to injectivity of `f` over rings,
but not over semirings.

This PR changes the assumption to `injective f`.
For reasons of symmetry,
the surjectivity assumption is also switched to `surjective f`.

As a consequence, this PR also renames:

* `linear_equiv_of_ker_eq_bot` to `linear_equiv_of_injective`
* `linear_equiv_of_ker_eq_bot_apply` to `linear_equiv_of_injective_apply`

src/algebra/category/Module/subobject.lean

@@ -33,8 +33,10 @@ noncomputable def subobject_Module : subobject M ≃o submodule R M := order_iso
     fapply eq_mk_of_comm,
     { apply linear_equiv.to_Module_iso'_left,
       apply linear_equiv.of_bijective (linear_map.cod_restrict S.arrow.range S.arrow _),
-      { simpa only [linear_map.ker_cod_restrict] using ker_eq_bot_of_mono _ },
-      { rw [linear_map.range_cod_restrict, submodule.comap_subtype_self] },
+      { simpa only [← linear_map.ker_eq_bot, linear_map.ker_cod_restrict]
+          using ker_eq_bot_of_mono _ },
+      { rw [← linear_map.range_eq_top, linear_map.range_cod_restrict,
+          submodule.comap_subtype_self] },
       { exact linear_map.mem_range_self _ } },
     { apply linear_map.ext,
       intros x,

src/algebra/lie/subalgebra.lean

@@ -495,9 +495,8 @@ variables [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [li
 /-- An injective Lie algebra morphism is an equivalence onto its range. -/
 noncomputable def of_injective (f : L₁ →ₗ⁅R⁆ L₂) (h : function.injective f) :
   L₁ ≃ₗ⁅R⁆ f.range :=
-have h' : (f : L₁ →ₗ[R] L₂).ker = ⊥ := linear_map.ker_eq_bot_of_injective h,
 { map_lie' := λ x y, by { apply set_coe.ext, simpa, },
-..(linear_equiv.of_injective ↑f h')}
+..(linear_equiv.of_injective ↑f $ by rwa [lie_hom.coe_to_linear_map])}
 
 @[simp] lemma of_injective_apply (f : L₁ →ₗ⁅R⁆ L₂) (h : function.injective f) (x : L₁) :
   ↑(of_injective f h x) = f x := rfl

src/analysis/normed_space/banach.lean

@@ -309,7 +309,8 @@ namespace continuous_linear_equiv
 to a continuous linear equivalence. -/
 noncomputable def of_bijective (f : E →L[𝕜] F) (hinj : f.ker = ⊥) (hsurj : f.range = ⊤) :
   E ≃L[𝕜] F :=
-(linear_equiv.of_bijective ↑f hinj hsurj).to_continuous_linear_equiv_of_continuous f.continuous
+(linear_equiv.of_bijective ↑f (linear_map.ker_eq_bot.mp hinj) (linear_map.range_eq_top.mp hsurj))
+.to_continuous_linear_equiv_of_continuous f.continuous
 
 @[simp] lemma coe_fn_of_bijective (f : E →L[𝕜] F) (hinj : f.ker = ⊥) (hsurj : f.range = ⊤) :
   ⇑(of_bijective f hinj hsurj) = f := rfl

src/analysis/normed_space/bounded_linear_maps.lean

@@ -458,5 +458,5 @@ a linear map that is also an isometry with full range. -/
 def continuous_linear_equiv.of_isometry (f : E →ₗ[𝕜] F) (hf : isometry f) (hfr : f.range = ⊤) :
   E ≃L[𝕜] F :=
 continuous_linear_equiv.of_homothety
-(linear_equiv.of_bijective f (linear_map.ker_eq_bot.mpr (isometry.injective hf)) hfr)
-1 zero_lt_one (λ _, by simp [one_mul, f.norm_apply_of_isometry hf])
+  (linear_equiv.of_bijective f (isometry.injective hf) (linear_map.range_eq_top.mp hfr))
+  1 zero_lt_one (λ _, by simp [one_mul, f.norm_apply_of_isometry hf])

src/analysis/normed_space/finite_dimension.lean

@@ -204,7 +204,8 @@ lemma linear_map.exists_antilipschitz_with [finite_dimensional 𝕜 E] (f : E 
 begin
   cases subsingleton_or_nontrivial E; resetI,
   { exact ⟨1, zero_lt_one, antilipschitz_with.of_subsingleton⟩ },
-  { let e : E ≃L[𝕜] f.range := (linear_equiv.of_injective f hf).to_continuous_linear_equiv,
+  { rw linear_map.ker_eq_bot at hf,
+    let e : E ≃L[𝕜] f.range := (linear_equiv.of_injective f hf).to_continuous_linear_equiv,
     exact ⟨_, e.nnnorm_symm_pos, e.antilipschitz⟩ }
 end
 

src/analysis/normed_space/linear_isometry.lean

@@ -368,8 +368,8 @@ variables {R₁ : Type*} [field R₁] [module R₁ E₁] [module R₁ F]
     to a linear isometry equivalence. -/
 noncomputable def to_linear_isometry_equiv
   (li : E₁ →ₗᵢ[R₁] F) (h : finrank R₁ E₁ = finrank R₁ F) : E₁ ≃ₗᵢ[R₁] F :=
-{ to_linear_equiv := li.to_linear_map.linear_equiv_of_ker_eq_bot
-    (ker_eq_bot_of_injective li.injective) h,
+{ to_linear_equiv :=
+    li.to_linear_map.linear_equiv_of_injective li.injective h,
   norm_map' := li.norm_map' }
 
 @[simp] lemma coe_to_linear_isometry_equiv

src/linear_algebra/basic.lean

@@ -359,7 +359,7 @@ end
 lemma surjective_of_iterate_surjective {n : ℕ} (hn : n ≠ 0) (h : surjective ⇑(f' ^ n)) :
   surjective f' :=
 begin
-  rw [← nat.succ_pred_eq_of_pos (pos_iff_ne_zero.mpr hn), 
+  rw [← nat.succ_pred_eq_of_pos (pos_iff_ne_zero.mpr hn),
     nat.succ_eq_add_one, add_comm, pow_add] at h,
   exact surjective.of_comp h,
 end
@@ -2382,6 +2382,23 @@ def of_left_inverse {g : M₂ → M} (h : function.left_inverse g f) : M ≃ₗ[
   (h : function.left_inverse g f) (x : f.range) :
   (of_left_inverse h).symm x = g x := rfl
 
+variables (f)
+
+/-- An `injective` linear map `f : M →ₗ[R] M₂` defines a linear equivalence
+between `M` and `f.range`. See also `linear_map.of_left_inverse`. -/
+noncomputable def of_injective (h : injective f) : M ≃ₗ[R] f.range :=
+of_left_inverse $ classical.some_spec h.has_left_inverse
+
+@[simp] theorem of_injective_apply {h : injective f} (x : M) :
+  ↑(of_injective f h x) = f x := rfl
+
+/-- A bijective linear map is a linear equivalence. -/
+noncomputable def of_bijective (hf₁ : injective f) (hf₂ : surjective f) : M ≃ₗ[R] M₂ :=
+(of_injective f hf₁).trans (of_top _ $ linear_map.range_eq_top.2 hf₂)
+
+@[simp] theorem of_bijective_apply {hf₁ hf₂} (x : M) :
+  of_bijective f hf₁ hf₂ x = f x := rfl
+
 end
 
 end add_comm_monoid
@@ -2417,32 +2434,8 @@ lemma neg_apply (x : M) : neg R x = -x := by simp
 
 end neg
 
-section ring
-
-variables [ring R] [add_comm_group M] [add_comm_group M₂]
-variables {module_M : module R M} {module_M₂ : module R M₂}
-variables (f : M →ₗ[R] M₂) (e : M ≃ₗ[R] M₂)
-
-/-- An `injective` linear map `f : M →ₗ[R] M₂` defines a linear equivalence
-between `M` and `f.range`. See also `linear_map.of_left_inverse`. -/
-noncomputable def of_injective (h : f.ker = ⊥) : M ≃ₗ[R] f.range :=
-of_left_inverse $ classical.some_spec (linear_map.ker_eq_bot.1 h).has_left_inverse
-
-@[simp] theorem of_injective_apply {h : f.ker = ⊥} (x : M) :
-  ↑(of_injective f h x) = f x := rfl
-
-/-- A bijective linear map is a linear equivalence. Here, bijectivity is described by saying that
-the kernel of `f` is `{0}` and the range is the universal set. -/
-noncomputable def of_bijective (hf₁ : f.ker = ⊥) (hf₂ : f.range = ⊤) : M ≃ₗ[R] M₂ :=
-(of_injective f hf₁).trans (of_top _ hf₂)
-
-@[simp] theorem of_bijective_apply {hf₁ hf₂} (x : M) :
-  of_bijective f hf₁ hf₂ x = f x := rfl
-
-end ring
-
-section comm_ring
-variables [comm_ring R] [add_comm_group M] [add_comm_group M₂] [add_comm_group M₃]
+section comm_semiring
+variables [comm_semiring R] [add_comm_monoid M] [add_comm_monoid M₂] [add_comm_monoid M₃]
 variables [module R M] [module R M₂] [module R M₃]
 open linear_map
 
@@ -2454,8 +2447,8 @@ of_linear ((a:R) • 1 : M →ₗ[R] M) (((a⁻¹ : units R) : R) • 1 : M →
 
 /-- A linear isomorphism between the domains and codomains of two spaces of linear maps gives a
 linear isomorphism between the two function spaces. -/
-def arrow_congr {R M₁ M₂ M₂₁ M₂₂ : Sort*} [comm_ring R]
-  [add_comm_group M₁] [add_comm_group M₂] [add_comm_group M₂₁] [add_comm_group M₂₂]
+def arrow_congr {R M₁ M₂ M₂₁ M₂₂ : Sort*} [comm_semiring R]
+  [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₂₁] [add_comm_monoid M₂₂]
   [module R M₁] [module R M₂] [module R M₂₁] [module R M₂₂]
   (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) :
   (M₁ →ₗ[R] M₂₁) ≃ₗ[R] (M₂ →ₗ[R] M₂₂) :=
@@ -2466,31 +2459,31 @@ def arrow_congr {R M₁ M₂ M₂₁ M₂₂ : Sort*} [comm_ring R]
   map_add' := λ f g, by { ext x, simp only [map_add, add_apply, coe_comp, comp_app, coe_coe] },
   map_smul' := λ c f, by { ext x, simp only [map_smul, smul_apply, coe_comp, comp_app, coe_coe] } }
 
-@[simp] lemma arrow_congr_apply {R M₁ M₂ M₂₁ M₂₂ : Sort*} [comm_ring R]
-  [add_comm_group M₁] [add_comm_group M₂] [add_comm_group M₂₁] [add_comm_group M₂₂]
+@[simp] lemma arrow_congr_apply {R M₁ M₂ M₂₁ M₂₂ : Sort*} [comm_semiring R]
+  [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₂₁] [add_comm_monoid M₂₂]
   [module R M₁] [module R M₂] [module R M₂₁] [module R M₂₂]
   (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) (f : M₁ →ₗ[R] M₂₁) (x : M₂) :
   arrow_congr e₁ e₂ f x = e₂ (f (e₁.symm x)) :=
 rfl
 
-@[simp] lemma arrow_congr_symm_apply {R M₁ M₂ M₂₁ M₂₂ : Sort*} [comm_ring R]
-  [add_comm_group M₁] [add_comm_group M₂] [add_comm_group M₂₁] [add_comm_group M₂₂]
+@[simp] lemma arrow_congr_symm_apply {R M₁ M₂ M₂₁ M₂₂ : Sort*} [comm_semiring R]
+  [add_comm_monoid M₁] [add_comm_monoid M₂] [add_comm_monoid M₂₁] [add_comm_monoid M₂₂]
   [module R M₁] [module R M₂] [module R M₂₁] [module R M₂₂]
   (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : M₂₁ ≃ₗ[R] M₂₂) (f : M₂ →ₗ[R] M₂₂) (x : M₁) :
   (arrow_congr e₁ e₂).symm f x = e₂.symm (f (e₁ x)) :=
 rfl
 
 lemma arrow_congr_comp {N N₂ N₃ : Sort*}
-  [add_comm_group N] [add_comm_group N₂] [add_comm_group N₃]
+  [add_comm_monoid N] [add_comm_monoid N₂] [add_comm_monoid N₃]
   [module R N] [module R N₂] [module R N₃]
   (e₁ : M ≃ₗ[R] N) (e₂ : M₂ ≃ₗ[R] N₂) (e₃ : M₃ ≃ₗ[R] N₃) (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) :
   arrow_congr e₁ e₃ (g.comp f) = (arrow_congr e₂ e₃ g).comp (arrow_congr e₁ e₂ f) :=
 by { ext, simp only [symm_apply_apply, arrow_congr_apply, linear_map.comp_apply], }
 
 lemma arrow_congr_trans {M₁ M₂ M₃ N₁ N₂ N₃ : Sort*}
-  [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂]
-  [add_comm_group M₃] [module R M₃] [add_comm_group N₁] [module R N₁]
-  [add_comm_group N₂] [module R N₂] [add_comm_group N₃] [module R N₃]
+  [add_comm_monoid M₁] [module R M₁] [add_comm_monoid M₂] [module R M₂]
+  [add_comm_monoid M₃] [module R M₃] [add_comm_monoid N₁] [module R N₁]
+  [add_comm_monoid N₂] [module R N₂] [add_comm_monoid N₃] [module R N₃]
   (e₁ : M₁ ≃ₗ[R] M₂) (e₂ : N₁ ≃ₗ[R] N₂) (e₃ : M₂ ≃ₗ[R] M₃) (e₄ : N₂ ≃ₗ[R] N₃) :
   (arrow_congr e₁ e₂).trans (arrow_congr e₃ e₄) = arrow_congr (e₁.trans e₃) (e₂.trans e₄) :=
 rfl
@@ -2521,7 +2514,7 @@ by { ext f x, refl, }
 @[simp] lemma conj_id (e : M ≃ₗ[R] M₂) : e.conj linear_map.id = linear_map.id :=
 by { ext, simp [conj_apply], }
 
-end comm_ring
+end comm_semiring
 
 section field
 variables [field K] [add_comm_group M] [add_comm_group M₂] [add_comm_group M₃]
@@ -2555,7 +2548,7 @@ end
     isomorphism.-/
 def to_span_nonzero_singleton (x : M) (h : x ≠ 0) : K ≃ₗ[K] (K ∙ x) :=
 linear_equiv.trans
-  (linear_equiv.of_injective (to_span_singleton K M x) (ker_to_span_singleton K M h))
+  (linear_equiv.of_injective (to_span_singleton K M x) (ker_eq_bot.1 $ ker_to_span_singleton K M h))
   (of_eq (to_span_singleton K M x).range (K ∙ x)
     (span_singleton_eq_range K M x).symm)
 
@@ -2763,7 +2756,7 @@ variables (f : M →ₗ[R] M₂)
 equivalent to the range of `f`. -/
 noncomputable def quot_ker_equiv_range : f.ker.quotient ≃ₗ[R] f.range :=
 (linear_equiv.of_injective (f.ker.liftq f $ le_refl _) $
-  submodule.ker_liftq_eq_bot _ _ _ (le_refl f.ker)).trans
+  ker_eq_bot.mp $ submodule.ker_liftq_eq_bot _ _ _ (le_refl f.ker)).trans
   (linear_equiv.of_eq _ _ $ submodule.range_liftq _ _ _)
 
 /-- The first isomorphism theorem for surjective linear maps. -/
@@ -2798,12 +2791,12 @@ noncomputable def quotient_inf_equiv_sup_quotient (p p' : submodule R M) :
   (comap p.subtype (p ⊓ p')).quotient ≃ₗ[R] (comap (p ⊔ p').subtype p').quotient :=
 linear_equiv.of_bijective (quotient_inf_to_sup_quotient p p')
   begin
-    rw [quotient_inf_to_sup_quotient, ker_liftq_eq_bot],
+    rw [← ker_eq_bot, quotient_inf_to_sup_quotient, ker_liftq_eq_bot],
     rw [ker_comp, ker_mkq],
     exact λ ⟨x, hx1⟩ hx2, ⟨hx1, hx2⟩
   end
   begin
-    rw [quotient_inf_to_sup_quotient, range_liftq, eq_top_iff'],
+    rw [← range_eq_top, quotient_inf_to_sup_quotient, range_liftq, eq_top_iff'],
     rintros ⟨x, hx⟩, rcases mem_sup.1 hx with ⟨y, hy, z, hz, rfl⟩,
     use [⟨y, hy⟩], apply (submodule.quotient.eq _).2,
     change y - (y + z) ∈ p',

src/linear_algebra/bilinear_form.lean

@@ -1350,9 +1350,12 @@ begin
   { refine λ m hm, h _ (λ x, _),
     rw [← to_lin_apply, hm], refl },
   { intros m hm, apply h,
-    ext, exact hm x }
+    ext x, exact hm x }
 end
 
+lemma nondegenerate.ker_eq_bot {B : bilin_form R₂ M₂} (h : B.nondegenerate) :
+  B.to_lin.ker = ⊥ := nondegenerate_iff_ker_eq_bot.mp h
+
 /-- The restriction of a nondegenerate bilinear form `B` onto a submodule `W` is
 nondegenerate if `disjoint W (B.orthogonal W)`. -/
 lemma nondegenerate_restrict_of_disjoint_orthogonal
@@ -1458,8 +1461,8 @@ the linear equivalence between a vector space and its dual with the underlying l
 `B.to_lin`. -/
 noncomputable def to_dual (B : bilin_form K V) (b : B.nondegenerate) :
   V ≃ₗ[K] module.dual K V :=
-B.to_lin.linear_equiv_of_ker_eq_bot
-  (nondegenerate_iff_ker_eq_bot.mp b) subspace.dual_finrank_eq.symm
+B.to_lin.linear_equiv_of_injective
+  (linear_map.ker_eq_bot.mp $ b.ker_eq_bot) subspace.dual_finrank_eq.symm
 
 lemma to_dual_def {B : bilin_form K V} (b : B.nondegenerate) {m n : V} :
   B.to_dual b m n = B m n := rfl

src/linear_algebra/dimension.lean

@@ -193,7 +193,7 @@ cardinal.lift_inj.1 f.lift_dim_eq
 
 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
+(linear_equiv.of_injective f 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) :
@@ -976,8 +976,9 @@ begin
       simp only [add_eq_zero_iff_eq_neg, linear_map.prod_apply, mem_ker,
         coprod_apply, neg_neg, map_neg, neg_apply],
       exact linear_map.ext_iff.1 eq c } },
-  { rw [ker_cod_restrict, ker_prod, hgd, bot_inf_eq] },
-  { rw [eq_top_iff, range_cod_restrict, ← map_le_iff_le_comap, map_top, range_subtype],
+  { rw [← ker_eq_bot, ker_cod_restrict, ker_prod, hgd, bot_inf_eq] },
+  { rw [← range_eq_top, eq_top_iff, range_cod_restrict, ← map_le_iff_le_comap,
+      map_top, range_subtype],
     rintros ⟨d, e⟩,
     have h := eq₂ d (-e),
     simp only [add_eq_zero_iff_eq_neg, linear_map.prod_apply, mem_ker, set_like.mem_coe,

src/linear_algebra/dual.lean

@@ -183,7 +183,8 @@ variables (b : basis ι R M)
 /-- A vector space is linearly equivalent to its dual space. -/
 @[simps]
 def to_dual_equiv [fintype ι] : M ≃ₗ[R] (dual R M) :=
-linear_equiv.of_bijective b.to_dual b.to_dual_ker b.to_dual_range
+linear_equiv.of_bijective b.to_dual
+  (ker_eq_bot.mp b.to_dual_ker) (range_eq_top.mp b.to_dual_range)
 
 /-- Maps a basis for `V` to a basis for the dual space. -/
 def dual_basis [fintype ι] : basis ι R (dual R M) :=
@@ -245,7 +246,8 @@ end
 
 /-- A module with a basis is linearly equivalent to the dual of its dual space. -/
 def eval_equiv  {ι : Type*} [fintype ι] (b : basis ι R M) : M ≃ₗ[R] dual R (dual R M) :=
-linear_equiv.of_bijective (eval R M) b.eval_ker b.eval_range
+linear_equiv.of_bijective (eval R M)
+  (ker_eq_bot.mp b.eval_ker) (range_eq_top.mp b.eval_range)
 
 @[simp] lemma eval_equiv_to_linear_map {ι : Type*} [fintype ι] (b : basis ι R M) :
   (b.eval_equiv).to_linear_map = dual.eval R M := rfl
@@ -292,7 +294,8 @@ variables (K V)
 
 /-- A vector space is linearly equivalent to the dual of its dual space. -/
 def eval_equiv [finite_dimensional K V] : V ≃ₗ[K] dual K (dual K V) :=
-linear_equiv.of_bijective (eval K V) eval_ker (erange_coe)
+linear_equiv.of_bijective (eval K V)
+  (ker_eq_bot.mp eval_ker) (range_eq_top.mp erange_coe)
 
 variables {K V}
 
@@ -517,7 +520,7 @@ noncomputable def quot_annihilator_equiv (W : subspace K V) :
 /-- The natural isomorphism forom the dual of a subspace `W` to `W.dual_lift.range`. -/
 noncomputable def dual_equiv_dual (W : subspace K V) :
   module.dual K W ≃ₗ[K] W.dual_lift.range :=
-linear_equiv.of_injective _ $ ker_eq_bot.2 dual_lift_injective
+linear_equiv.of_injective _ dual_lift_injective
 
 lemma dual_equiv_dual_def (W : subspace K V) :
   W.dual_equiv_dual.to_linear_map = W.dual_lift.range_restrict := rfl

src/linear_algebra/finite_dimensional.lean

@@ -899,18 +899,17 @@ open finite_dimensional
 variables [finite_dimensional K V]
 
 /-- The linear equivalence corresponging to an injective endomorphism. -/
-noncomputable def of_injective_endo (f : V →ₗ[K] V) (h_inj : f.ker = ⊥) : V ≃ₗ[K] V :=
-(linear_equiv.of_injective f h_inj).trans
-  (linear_equiv.of_top _ (linear_map.ker_eq_bot_iff_range_eq_top.1 h_inj))
+noncomputable def of_injective_endo (f : V →ₗ[K] V) (h_inj : injective f) : V ≃ₗ[K] V :=
+linear_equiv.of_bijective f h_inj $ linear_map.injective_iff_surjective.mp h_inj
 
-@[simp] lemma coe_of_injective_endo (f : V →ₗ[K] V) (h_inj : f.ker = ⊥) :
+@[simp] lemma coe_of_injective_endo (f : V →ₗ[K] V) (h_inj : injective f) :
   ⇑(of_injective_endo f h_inj) = f := rfl
 
-@[simp] lemma of_injective_endo_right_inv (f : V →ₗ[K] V) (h_inj : f.ker = ⊥) :
+@[simp] lemma of_injective_endo_right_inv (f : V →ₗ[K] V) (h_inj : injective f) :
   f * (of_injective_endo f h_inj).symm = 1 :=
 linear_map.ext $ (of_injective_endo f h_inj).apply_symm_apply
 
-@[simp] lemma of_injective_endo_left_inv (f : V →ₗ[K] V) (h_inj : f.ker = ⊥) :
+@[simp] lemma of_injective_endo_left_inv (f : V →ₗ[K] V) (h_inj : injective f) :
   ((of_injective_endo f h_inj).symm : V →ₗ[K] V) * f = 1 :=
 linear_map.ext $ (of_injective_endo f h_inj).symm_apply_apply
 
@@ -923,7 +922,7 @@ begin
   split,
   { rintro ⟨u, rfl⟩,
     exact linear_map.ker_eq_bot_of_inverse u.inv_mul },
-  { intro h_inj,
+  { intro h_inj, rw ker_eq_bot at h_inj,
     exact ⟨⟨f, (linear_equiv.of_injective_endo f h_inj).symm.to_linear_map,
       linear_equiv.of_injective_endo_right_inv f h_inj,
       linear_equiv.of_injective_endo_left_inv f h_inj⟩, rfl⟩ }
@@ -979,18 +978,18 @@ calc  finrank K V
 ... ≤ finrank K V₂ : submodule.finrank_le _
 
 /-- Given a linear map `f` between two vector spaces with the same dimension, if
-`ker f = ⊥` then `linear_equiv_of_ker_eq_bot` is the induced isomorphism
+`ker f = ⊥` then `linear_equiv_of_injective` is the induced isomorphism
 between the two vector spaces. -/
-noncomputable def linear_equiv_of_ker_eq_bot
+noncomputable def linear_equiv_of_injective
   [finite_dimensional K V] [finite_dimensional K V₂]
-  (f : V →ₗ[K] V₂) (hf : f.ker = ⊥) (hdim : finrank K V = finrank K V₂) : V ≃ₗ[K] V₂ :=
-linear_equiv.of_bijective f hf (linear_map.range_eq_top.2 $
-  (linear_map.injective_iff_surjective_of_finrank_eq_finrank hdim).1 (linear_map.ker_eq_bot.1 hf))
+  (f : V →ₗ[K] V₂) (hf : injective f) (hdim : finrank K V = finrank K V₂) : V ≃ₗ[K] V₂ :=
+linear_equiv.of_bijective f hf $
+  (linear_map.injective_iff_surjective_of_finrank_eq_finrank hdim).mp hf
 
-@[simp] lemma linear_equiv_of_ker_eq_bot_apply
+@[simp] lemma linear_equiv_of_injective_apply
   [finite_dimensional K V] [finite_dimensional K V₂]
-  {f : V →ₗ[K] V₂} (hf : f.ker = ⊥) (hdim : finrank K V = finrank K V₂) (x : V) :
-  f.linear_equiv_of_ker_eq_bot hf hdim x = f x := rfl
+  {f : V →ₗ[K] V₂} (hf : injective f) (hdim : finrank K V = finrank K V₂) (x : V) :
+  f.linear_equiv_of_injective hf hdim x = f x := rfl
 
 end linear_map
 

src/linear_algebra/free_module_pid.lean

@@ -636,7 +636,7 @@ begin
   let φ : M →ₗ[R] M := linear_map.lsmul R M A,
   have : φ.ker = ⊥,
     from linear_map.ker_lsmul hA,
-  let ψ : M ≃ₗ[R] φ.range := linear_equiv.of_injective φ this,
+  let ψ : M ≃ₗ[R] φ.range := linear_equiv.of_injective φ (linear_map.ker_eq_bot.mp this),
   have : φ.range ≤ N, -- as announced, `A • M ⊆ N`
   { suffices : ∀ i, φ (s i) ∈ N,
     { rw [linear_map.range_eq_map, ← hs, φ.map_span_le],