feat(ring_theory/algebraic): alg_hom from an algebraic extension to…

… itself is bijective (#15873)

+ Generalizes `alg_hom.bijective` and [alg_equiv_equiv_alg_hom](https://leanprover-community.github.io/mathlib_docs/linear_algebra/finite_dimensional.html#alg_equiv_equiv_alg_hom) and move them so that they can be derived from the generalized versions. Upgrade `alg_equiv_equiv_alg_hom` to a `mul_equiv` by introducing the monoid instance `alg_hom.End` on self-alg_homs.

+ Show that algebraicity of an algebra is preserved under alg_equiv (`alg_equiv.is_algebraic_iff`).

[Zulip](https://leanprover.zulipchat.com/#narrow/stream/304774-FLT-regular/topic/Project.20status/near/292112817)

src/algebra/algebra/basic.lean

@@ -700,6 +700,17 @@ lemma map_list_prod (s : list A) :
   φ s.prod = (s.map φ).prod :=
 φ.to_ring_hom.map_list_prod s
 
+@[simps mul one {attrs := []}] instance End : monoid (A →ₐ[R] A) :=
+{ mul := comp,
+  mul_assoc := λ ϕ ψ χ, rfl,
+  one := alg_hom.id R A,
+  one_mul := λ ϕ, ext $ λ x, rfl,
+  mul_one := λ ϕ, ext $ λ x, rfl }
+
+@[simp] lemma one_apply (x : A) : (1 : A →ₐ[R] A) x = x := rfl
+
+@[simp] lemma mul_apply (φ ψ : A →ₐ[R] A) (x : A) : (φ * ψ) x = φ (ψ x) := rfl
+
 section prod
 
 /-- First projection as `alg_hom`. -/

src/data/polynomial/ring_division.lean

@@ -684,6 +684,15 @@ begin
   exact hp (map_injective _ (no_zero_smul_divisors.algebra_map_injective T S) h)
 end
 
+lemma root_set_maps_to {p : T[X]} {S S'} [comm_ring S] [is_domain S] [algebra T S]
+  [comm_ring S'] [is_domain S'] [algebra T S'] (hp : p.map (algebra_map T S') ≠ 0)
+  (f : S →ₐ[T] S') : (p.root_set S).maps_to f (p.root_set S') :=
+λ x hx, begin
+  rw [mem_root_set_iff' hp, ← f.comp_algebra_map, ← map_map, eval_map],
+  erw [eval₂_hom, (mem_root_set_iff' (mt (λ h, _) hp) x).1 hx, _root_.map_zero],
+  rw [← f.comp_algebra_map, ← map_map, h, polynomial.map_zero],
+end
+
 lemma ne_zero_of_mem_root_set {p : T[X]} [comm_ring S] [is_domain S] [algebra T S] {a : S}
   (h : a ∈ p.root_set S) : p ≠ 0 :=
 λ hf, by rwa [hf, root_set_zero] at h

src/field_theory/galois.lean

@@ -208,7 +208,7 @@ begin
         (set.inclusion H_le)).mpr ⟨set.inclusion_injective H_le, this⟩).2).symm },
   apply fintype.card_congr,
   refine (fixed_points.to_alg_hom_equiv H E).trans _,
-  refine (alg_equiv_equiv_alg_hom (fixed_field H) E).symm.trans _,
+  refine (alg_equiv_equiv_alg_hom (fixed_field H) E).to_equiv.symm.trans _,
   exact (fixing_subgroup_equiv (fixed_field H)).to_equiv.symm
 end
 
@@ -380,8 +380,8 @@ begin
   { rw adjoin_root at this,
     apply of_card_aut_eq_finrank,
     rw ← eq.trans this (linear_equiv.finrank_eq intermediate_field.top_equiv.to_linear_equiv),
-    exact fintype.card_congr (equiv.trans (alg_equiv_equiv_alg_hom F E)
-      (alg_equiv.arrow_congr intermediate_field.top_equiv.symm alg_equiv.refl)) },
+    exact fintype.card_congr ((alg_equiv_equiv_alg_hom F E).to_equiv.trans
+      (intermediate_field.top_equiv.symm.arrow_congr alg_equiv.refl)) },
   apply intermediate_field.induction_on_adjoin_finset s P,
   { have key := intermediate_field.card_alg_hom_adjoin_integral F
       (show is_integral F (0 : E), by exact is_integral_zero),

src/linear_algebra/finite_dimensional.lean

@@ -1191,23 +1191,6 @@ linear_equiv.of_bijective f hf $
 
 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_finrank_eq_finrank rfl).mp inj⟩
-
-end alg_hom
-
-/-- Bijection 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
 
 /-- A domain that is module-finite as an algebra over a field is a division ring. -/

src/linear_algebra/matrix/nonsingular_inverse.lean

@@ -413,7 +413,8 @@ invertible.map (diagonal_ring_hom n α) v
 
 lemma inv_of_diagonal_eq {α} [semiring α] (v : n → α) [invertible v] [invertible (diagonal v)] :
   ⅟(diagonal v) = diagonal (⅟v) :=
-by { letI := diagonal_invertible v, convert (rfl : ⅟(diagonal v) = _) }
+by { letI := diagonal_invertible v, convert (rfl : ⅟(diagonal v) = _),
+  convert subsingleton.elim _ _, apply invertible.subsingleton }
 
 /-- `v` is invertible if `diagonal v` is -/
 def invertible_of_diagonal_invertible (v : n → α) [invertible (diagonal v)] : invertible v :=

src/ring_theory/algebraic.lean

@@ -114,6 +114,20 @@ lemma is_algebraic_algebra_map_of_is_algebraic {a : S} :
   is_algebraic R a → is_algebraic R (algebra_map S A a) :=
 λ ⟨f, hf₁, hf₂⟩, ⟨f, hf₁, by rw [←algebra_map_aeval, hf₂, map_zero]⟩
 
+/-- This is slightly more general than `is_algebraic_algebra_map_of_is_algebraic` in that it
+  allows noncommutative intermediate rings `A`. -/
+lemma is_algebraic_alg_hom_of_is_algebraic {B} [ring B] [algebra R B]
+  (f : A →ₐ[R] B) {a : A} (h : is_algebraic R a) : is_algebraic R (f a) :=
+let ⟨p, hp, ha⟩ := h in ⟨p, hp, by rw [aeval_alg_hom, f.comp_apply, ha, map_zero]⟩
+
+/-- Transfer `algebra.is_algebraic` across an `alg_equiv`. -/
+lemma _root_.alg_equiv.is_algebraic {B} [ring B] [algebra R B] (e : A ≃ₐ[R] B)
+  (h : algebra.is_algebraic R A) : algebra.is_algebraic R B :=
+λ b, by convert ← is_algebraic_alg_hom_of_is_algebraic e.to_alg_hom (h _); apply e.apply_symm_apply
+
+lemma _root_.alg_equiv.is_algebraic_iff {B} [ring B] [algebra R B] (e : A ≃ₐ[R] B) :
+  algebra.is_algebraic R A ↔ algebra.is_algebraic R B := ⟨e.is_algebraic, e.symm.is_algebraic⟩
+
 lemma is_algebraic_algebra_map_iff {a : S} (h : function.injective (algebra_map S A)) :
   is_algebraic R (algebra_map S A a) ↔ is_algebraic R a :=
 ⟨λ ⟨p, hp0, hp⟩, ⟨p, hp0, h (by rwa [map_zero, algebra_map_aeval])⟩,
@@ -182,7 +196,7 @@ _root_.is_algebraic_of_larger_base_of_injective (algebra_map K L).injective A_al
 lemma is_algebraic_of_larger_base (A_alg : is_algebraic K A) : is_algebraic L A :=
 is_algebraic_of_larger_base_of_injective (algebra_map K L).injective A_alg
 
-variables {R S} (K L)
+variables (K L)
 
 /-- A field extension is integral if it is finite. -/
 lemma is_integral_of_finite [finite_dimensional K L] : algebra.is_integral K L :=
@@ -193,6 +207,40 @@ lemma is_integral_of_finite [finite_dimensional K L] : algebra.is_integral K L :
 lemma is_algebraic_of_finite [finite : finite_dimensional K L] : is_algebraic K L :=
 algebra.is_algebraic_iff_is_integral.mpr (is_integral_of_finite K L)
 
+variables {K L}
+
+theorem is_algebraic.alg_hom_bijective
+  (ha : algebra.is_algebraic K L) (f : L →ₐ[K] L) : function.bijective f :=
+begin
+  refine ⟨f.to_ring_hom.injective, λ b, _⟩,
+  obtain ⟨p, hp, he⟩ := ha b,
+  let f' : p.root_set L → p.root_set L :=
+    set.maps_to.restrict f _ _ (root_set_maps_to (map_ne_zero hp) f),
+  have : function.surjective f' := fintype.injective_iff_surjective.1
+    (λ _ _ h, subtype.eq $ f.to_ring_hom.injective $ subtype.ext_iff.1 h),
+  obtain ⟨a, ha⟩ := this ⟨b, (mem_root_set_iff hp b).2 he⟩,
+  exact ⟨a, subtype.ext_iff.1 ha⟩,
+end
+
+theorem _root_.alg_hom.bijective [finite_dimensional K L] (ϕ : L →ₐ[K] L) : function.bijective ϕ :=
+(algebra.is_algebraic_of_finite K L).alg_hom_bijective ϕ
+
+variables (K L)
+
+/-- Bijection between algebra equivalences and algebra homomorphisms -/
+@[simps] noncomputable
+def is_algebraic.alg_equiv_equiv_alg_hom
+  (ha : algebra.is_algebraic K L) : (L ≃ₐ[K] L) ≃* (L →ₐ[K] L) :=
+{ to_fun := λ ϕ, ϕ.to_alg_hom,
+  inv_fun := λ ϕ, alg_equiv.of_bijective ϕ (ha.alg_hom_bijective ϕ),
+  left_inv := λ _, by {ext, refl},
+  right_inv := λ _, by {ext, refl},
+  map_mul' := λ _ _, rfl }
+
+/-- Bijection between algebra equivalences and algebra homomorphisms -/
+@[reducible] noncomputable def _root_.alg_equiv_equiv_alg_hom [finite_dimensional K L] :
+  (L ≃ₐ[K] L) ≃* (L →ₐ[K] L) := (algebra.is_algebraic_of_finite K L).alg_equiv_equiv_alg_hom K L
+
 end algebra
 
 variables {R S : Type*} [comm_ring R] [is_domain R] [comm_ring S]