chore(algebra/algebra): trivial lemmas for alg_equiv (#8139)

src/algebra/algebra/basic.lean

@@ -584,8 +584,8 @@ def to_linear_map : A →ₗ B :=
 
 @[simp] lemma to_linear_map_apply (p : A) : φ.to_linear_map p = φ p := rfl
 
-theorem to_linear_map_inj {φ₁ φ₂ : A →ₐ[R] B} (H : φ₁.to_linear_map = φ₂.to_linear_map) : φ₁ = φ₂ :=
-ext $ λ x, show φ₁.to_linear_map x = φ₂.to_linear_map x, by rw H
+theorem to_linear_map_injective : function.injective (to_linear_map : _ → (A →ₗ[R] B)) :=
+λ φ₁ φ₂ h, ext $ linear_map.congr_fun h
 
 @[simp] lemma comp_to_linear_map (f : A →ₐ[R] B) (g : B →ₐ[R] C) :
   (g.comp f).to_linear_map = g.to_linear_map.comp f.to_linear_map := rfl
@@ -732,14 +732,8 @@ rfl
 @[simp, norm_cast] lemma coe_ring_equiv : ((e : A₁ ≃+* A₂) : A₁ → A₂) = e := rfl
 @[simp] lemma coe_ring_equiv' : (e.to_ring_equiv : A₁ → A₂) = e := rfl
 
-lemma coe_ring_equiv_injective : function.injective (λ e : A₁ ≃ₐ[R] A₂, (e : A₁ ≃+* A₂)) :=
-begin
-  intros f g w,
-  ext,
-  replace w : ((f : A₁ ≃+* A₂) : A₁ → A₂) = ((g : A₁ ≃+* A₂) : A₁ → A₂) :=
-    congr_arg (λ e : A₁ ≃+* A₂, (e : A₁ → A₂)) w,
-  exact congr_fun w a,
-end
+lemma coe_ring_equiv_injective : function.injective (coe : (A₁ ≃ₐ[R] A₂) → (A₁ ≃+* A₂)) :=
+λ e₁ e₂ h, ext $ ring_equiv.congr_fun h
 
 @[simp] lemma map_add : ∀ x y, e (x + y) = e x + e y := e.to_add_equiv.map_add
 
@@ -775,6 +769,9 @@ instance has_coe_to_alg_hom : has_coe (A₁ ≃ₐ[R] A₂) (A₁ →ₐ[R] A₂
 @[simp, norm_cast] lemma coe_alg_hom : ((e : A₁ →ₐ[R] A₂) : A₁ → A₂) = e :=
 rfl
 
+lemma coe_alg_hom_injective : function.injective (coe : (A₁ ≃ₐ[R] A₂) → (A₁ →ₐ[R] A₂)) :=
+λ e₁ e₂ h, ext $ alg_hom.congr_fun h
+
 /-- The two paths coercion can take to a `ring_hom` are equivalent -/
 lemma coe_ring_hom_commutes : ((e : A₁ →ₐ[R] A₂) : A₁ →+* A₂) = ((e : A₁ ≃+* A₂) : A₁ →+* A₂) :=
 rfl
@@ -894,11 +891,22 @@ by { ext, refl }
 /-- If an algebra morphism has an inverse, it is a algebra isomorphism. -/
 def of_alg_hom (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ : f.comp g = alg_hom.id R A₂)
   (h₂ : g.comp f = alg_hom.id R A₁) : A₁ ≃ₐ[R] A₂ :=
-{ inv_fun   := g,
+{ to_fun    := f,
+  inv_fun   := g,
   left_inv  := alg_hom.ext_iff.1 h₂,
   right_inv := alg_hom.ext_iff.1 h₁,
   ..f }
 
+lemma coe_alg_hom_of_alg_hom (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ h₂) :
+  ↑(of_alg_hom f g h₁ h₂) = f := alg_hom.ext $ λ _, rfl
+
+@[simp]
+lemma of_alg_hom_coe_alg_hom (f : A₁ ≃ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ h₂) :
+  of_alg_hom ↑f g h₁ h₂ = f := ext $ λ _, rfl
+
+lemma of_alg_hom_symm (f : A₁ →ₐ[R] A₂) (g : A₂ →ₐ[R] A₁) (h₁ h₂) :
+  (of_alg_hom f g h₁ h₂).symm = of_alg_hom g f h₂ h₁ := rfl
+
 /-- Promotes a bijective algebra homomorphism to an algebra equivalence. -/
 noncomputable def of_bijective (f : A₁ →ₐ[R] A₂) (hf : function.bijective f) : A₁ ≃ₐ[R] A₂ :=
 { .. ring_equiv.of_bijective (f : A₁ →+* A₂) hf, .. f }
@@ -919,9 +927,8 @@ noncomputable def of_bijective (f : A₁ →ₐ[R] A₂) (hf : function.bijectiv
 @[simp] lemma to_linear_equiv_trans (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) :
   (e₁.trans e₂).to_linear_equiv = e₁.to_linear_equiv.trans e₂.to_linear_equiv := rfl
 
-theorem to_linear_equiv_inj {e₁ e₂ : A₁ ≃ₐ[R] A₂} (H : e₁.to_linear_equiv = e₂.to_linear_equiv) :
-  e₁ = e₂ :=
-ext $ λ x, show e₁.to_linear_equiv x = e₂.to_linear_equiv x, by rw H
+theorem to_linear_equiv_injective : function.injective (to_linear_equiv : _ → (A₁ ≃ₗ[R] A₂)) :=
+λ e₁ e₂ h, ext $ linear_equiv.congr_fun h
 
 /-- Interpret an algebra equivalence as a linear map. -/
 def to_linear_map : A₁ →ₗ[R] A₂ :=
@@ -935,9 +942,8 @@ e.to_alg_hom.to_linear_map
 
 @[simp] lemma to_linear_map_apply (x : A₁) : e.to_linear_map x = e x := rfl
 
-theorem to_linear_map_inj {e₁ e₂ : A₁ ≃ₐ[R] A₂} (H : e₁.to_linear_map = e₂.to_linear_map) :
-  e₁ = e₂ :=
-ext $ λ x, show e₁.to_linear_map x = e₂.to_linear_map x, by rw H
+theorem to_linear_map_injective : function.injective (to_linear_map : _ → (A₁ →ₗ[R] A₂)) :=
+λ e₁ e₂ h, ext $ linear_map.congr_fun h
 
 @[simp] lemma trans_to_linear_map (f : A₁ ≃ₐ[R] A₂) (g : A₂ ≃ₐ[R] A₃) :
   (f.trans g).to_linear_map = g.to_linear_map.comp f.to_linear_map := rfl
@@ -952,13 +958,21 @@ variables (l : A₁ ≃ₗ[R] A₂)
 Upgrade a linear equivalence to an algebra equivalence,
 given that it distributes over multiplication and action of scalars.
 -/
+@[simps apply]
 def of_linear_equiv : A₁ ≃ₐ[R] A₂ :=
 { to_fun := l,
   inv_fun := l.symm,
   map_mul' := map_mul,
   commutes' := commutes,
   ..l }
 
+@[simp]
+lemma of_linear_equiv_symm :
+  (of_linear_equiv l map_mul commutes).symm = of_linear_equiv l.symm
+    ((of_linear_equiv l map_mul commutes).symm.map_mul)
+    ((of_linear_equiv l map_mul commutes).symm.commutes) :=
+rfl
+
 @[simp] lemma of_linear_equiv_to_linear_equiv (map_mul) (commutes) :
   of_linear_equiv e.to_linear_equiv map_mul commutes = e :=
 by { ext, refl }
@@ -967,8 +981,6 @@ by { ext, refl }
   to_linear_equiv (of_linear_equiv l map_mul commutes) = l :=
 by { ext, refl }
 
-@[simp] lemma of_linear_equiv_apply (x : A₁) : of_linear_equiv l map_mul commutes x = l x := rfl
-
 end of_linear_equiv
 
 instance aut : group (A₁ ≃ₐ[R] A₁) :=

src/algebra/monoid_algebra.lean

@@ -557,7 +557,7 @@ def lift_nc_alg_hom (f : A →ₐ[k] B) (g : G →* B) (h_comm : ∀ x y, commut
 values on the functions `single a 1`. -/
 lemma alg_hom_ext ⦃φ₁ φ₂ : monoid_algebra k G →ₐ[k] A⦄
   (h : ∀ x, φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂ :=
-alg_hom.to_linear_map_inj $ finsupp.lhom_ext' $ λ a, linear_map.ext_ring (h a)
+alg_hom.to_linear_map_injective $ finsupp.lhom_ext' $ λ a, linear_map.ext_ring (h a)
 
 /-- See note [partially-applied ext lemmas]. -/
 @[ext] lemma alg_hom_ext' ⦃φ₁ φ₂ : monoid_algebra k G →ₐ[k] A⦄

src/ring_theory/tensor_product.lean

@@ -397,7 +397,7 @@ variables {C : Type v₃} [semiring C] [algebra R C]
 theorem ext {g h : (A ⊗[R] B) →ₐ[R] C}
   (H : ∀ a b, g (a ⊗ₜ b) = h (a ⊗ₜ b)) : g = h :=
 begin
-  apply @alg_hom.to_linear_map_inj R (A ⊗[R] B) C _ _ _ _ _ _ _ _,
+  apply @alg_hom.to_linear_map_injective R (A ⊗[R] B) C _ _ _ _ _ _ _ _,
   ext,
   simp [H],
 end