feat(linear_algebra/finite_dimensional): finite dimensional algebra_h…

…om of fields is bijective (#4793)

Changes to finite_dimensional.lean from #4786



Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

src/linear_algebra/finite_dimensional.lean

@@ -816,6 +816,23 @@ calc  findim K V
 
 end linear_map
 
+namespace alg_hom
+
+lemma bijective {F : Type*} [field F] {E : Type*} [field E] [algebra F E]
+  [finite_dimensional F E] (ϕ : E →ₐ[F] E) : function.bijective ϕ :=
+have inj : function.injective ϕ.to_linear_map := ϕ.to_ring_hom.injective,
+⟨inj, (linear_map.injective_iff_surjective_of_findim_eq_findim rfl).mp inj⟩
+
+end alg_hom
+
+/-- Biijection between algebra equivalences and algebra homomorphisms -/
+noncomputable def alg_equiv_equiv_alg_hom (F : Type u) [field F] (E : Type v) [field E]
+  [algebra F E] [finite_dimensional F E] : (E ≃ₐ[F] E) ≃ (E →ₐ[F] E) :=
+{ to_fun := λ ϕ, ϕ.to_alg_hom,
+  inv_fun := λ ϕ, alg_equiv.of_bijective ϕ ϕ.bijective,
+  left_inv := λ _, by {ext, refl},
+  right_inv := λ _, by {ext, refl} }
+
 section
 
 /-- An integral domain that is module-finite as an algebra over a field is a field. -/