feat(algebra/algebra,linear_algebra): add *_equiv.of_left_inverse (#6167)

The main purpose of this change is to add equivalences onto the range of a function with a left-inverse:
* `algebra_equiv.of_left_inverse`
* `linear_equiv.of_left_inverse`
* `ring_equiv.of_left_inverse`
* `ring_equiv.sof_left_inverse` (the sub***S***emiring version)

This also:
* Renames `alg_hom.alg_equiv.of_injective` to `alg_equiv.of_injective`
* Adds `subalgebra.mem_range_self` and `subsemiring.mem_srange_self` for consistency with `subring.mem_range_self`
* Replaces `subring.surjective_onto_range` with `subring.range_restrict_surjective`, which have defeq statements

These are computable versions of `*_equiv.of_injective`, with the benefit of having a known inverse, and in the case of `linear_equiv` working for `semiring` and not just `ring`.

Author: eric-wieser

src/algebra/algebra/subalgebra.lean

@@ -290,6 +290,8 @@ protected def range (φ : A →ₐ[R] B) : subalgebra R B :=
 @[simp] lemma mem_range (φ : A →ₐ[R] B) {y : B} :
   y ∈ φ.range ↔ ∃ x, φ x = y := ring_hom.mem_srange
 
+theorem mem_range_self (φ : A →ₐ[R] B) (x : A) : φ x ∈ φ.range := φ.mem_range.2 ⟨x, rfl⟩
+
 @[simp] lemma coe_range (φ : A →ₐ[R] B) : (φ.range : set B) = set.range φ :=
 by { ext, rw [subalgebra.mem_coe, mem_range], refl }
 
@@ -298,24 +300,22 @@ def cod_restrict (f : A →ₐ[R] B) (S : subalgebra R B) (hf : ∀ x, f x ∈ S
 { commutes' := λ r, subtype.eq $ f.commutes r,
   .. ring_hom.cod_srestrict (f : A →+* B) S hf }
 
+@[simp] lemma val_comp_cod_restrict (f : A →ₐ[R] B) (S : subalgebra R B) (hf : ∀ x, f x ∈ S) :
+  S.val.comp (f.cod_restrict S hf) = f :=
+alg_hom.ext $ λ _, rfl
+
+@[simp] lemma coe_cod_restrict (f : A →ₐ[R] B) (S : subalgebra R B) (hf : ∀ x, f x ∈ S) (x : A) :
+  ↑(f.cod_restrict S hf x) = f x := rfl
+
 theorem injective_cod_restrict (f : A →ₐ[R] B) (S : subalgebra R B) (hf : ∀ x, f x ∈ S) :
   function.injective (f.cod_restrict S hf) ↔ function.injective f :=
 ⟨λ H x y hxy, H $ subtype.eq hxy, λ H x y hxy, H (congr_arg subtype.val hxy : _)⟩
 
-/-- Restrict an injective algebra homomorphism to an algebra isomorphism -/
-noncomputable def alg_equiv.of_injective (f : A →ₐ[R] B) (hf : function.injective f) :
-  A ≃ₐ[R] f.range :=
-alg_equiv.of_bijective (f.cod_restrict f.range (λ x, f.mem_range.mpr ⟨x, rfl⟩))
-⟨(f.injective_cod_restrict f.range (λ x, f.mem_range.mpr ⟨x, rfl⟩)).mpr hf,
-  λ x, Exists.cases_on (f.mem_range.mp (subtype.mem x)) (λ y hy, ⟨y, subtype.ext hy⟩)⟩
-
-@[simp] lemma alg_equiv.of_injective_apply (f : A →ₐ[R] B) (hf : function.injective f) (x : A) :
-  ↑(alg_equiv.of_injective f hf x) = f x := rfl
+/-- Restrict the codomain of a alg_hom `f` to `f.range`.
 
-/-- Restrict an algebra homomorphism between fields to an algebra isomorphism -/
-noncomputable def alg_equiv.of_injective_field {E F : Type*} [division_ring E] [semiring F]
-  [nontrivial F] [algebra R E] [algebra R F] (f : E →ₐ[R] F) : E ≃ₐ[R] f.range :=
-alg_equiv.of_injective f f.to_ring_hom.injective
+This is the bundled version of `set.range_factorization`. -/
+@[reducible] def range_restrict (f : A →ₐ[R] B) : A →ₐ[R] f.range :=
+f.cod_restrict f.range f.mem_range_self
 
 /-- The equalizer of two R-algebra homomorphisms -/
 def equalizer (ϕ ψ : A →ₐ[R] B) : subalgebra R A :=
@@ -341,6 +341,48 @@ def equalizer (ϕ ψ : A →ₐ[R] B) : subalgebra R A :=
 
 end alg_hom
 
+namespace alg_equiv
+
+variables {R : Type u} {A : Type v} {B : Type w}
+variables [comm_semiring R] [semiring A] [semiring B] [algebra R A] [algebra R B]
+
+/-- Restrict an algebra homomorphism with a left inverse to an algebra isomorphism to its range.
+
+This is a computable alternative to `alg_equiv.of_injective`. -/
+def of_left_inverse
+  {g : B → A} {f : A →ₐ[R] B} (h : function.left_inverse g f) :
+  A ≃ₐ[R] f.range :=
+{ to_fun := f.range_restrict,
+  inv_fun := g ∘ f.range.val,
+  left_inv := h,
+  right_inv := λ x, subtype.ext $
+    let ⟨x', hx'⟩ := f.mem_range.mp x.prop in
+    show f (g x) = x, by rw [←hx', h x'],
+  ..f.range_restrict }
+
+@[simp] lemma of_left_inverse_apply
+  {g : B → A} {f : A →ₐ[R] B} (h : function.left_inverse g f) (x : A) :
+  ↑(of_left_inverse h x) = f x := rfl
+
+@[simp] lemma of_left_inverse_symm_apply
+  {g : B → A} {f : A →ₐ[R] B} (h : function.left_inverse g f) (x : f.range) :
+  (of_left_inverse h).symm x = g x := rfl
+
+/-- Restrict an injective algebra homomorphism to an algebra isomorphism -/
+noncomputable def of_injective (f : A →ₐ[R] B) (hf : function.injective f) :
+  A ≃ₐ[R] f.range :=
+of_left_inverse (classical.some_spec hf.has_left_inverse)
+
+@[simp] lemma of_injective_apply (f : A →ₐ[R] B) (hf : function.injective f) (x : A) :
+  ↑(of_injective f hf x) = f x := rfl
+
+/-- Restrict an algebra homomorphism between fields to an algebra isomorphism -/
+noncomputable def of_injective_field {E F : Type*} [division_ring E] [semiring F]
+  [nontrivial F] [algebra R E] [algebra R F] (f : E →ₐ[R] F) : E ≃ₐ[R] f.range :=
+of_injective f f.to_ring_hom.injective
+
+end alg_equiv
+
 namespace algebra
 
 variables (R : Type u) {A : Type v} {B : Type w}

src/field_theory/normal.lean

@@ -216,13 +216,13 @@ def alg_hom.restrict_normal_aux [h : normal F E] :
 
 /-- Restrict algebra homomorphism to normal subfield -/
 def alg_hom.restrict_normal [normal F E] : E →ₐ[F] E :=
-((alg_hom.alg_equiv.of_injective_field (is_scalar_tower.to_alg_hom F E K)).symm.to_alg_hom.comp
+((alg_equiv.of_injective_field (is_scalar_tower.to_alg_hom F E K)).symm.to_alg_hom.comp
   (ϕ.restrict_normal_aux E)).comp
-    (alg_hom.alg_equiv.of_injective_field (is_scalar_tower.to_alg_hom F E K)).to_alg_hom
+    (alg_equiv.of_injective_field (is_scalar_tower.to_alg_hom F E K)).to_alg_hom
 
 @[simp] lemma alg_hom.restrict_normal_commutes [normal F E] (x : E) :
   algebra_map E K (ϕ.restrict_normal E x) = ϕ (algebra_map E K x) :=
-subtype.ext_iff.mp (alg_equiv.apply_symm_apply (alg_hom.alg_equiv.of_injective_field
+subtype.ext_iff.mp (alg_equiv.apply_symm_apply (alg_equiv.of_injective_field
   (is_scalar_tower.to_alg_hom F E K)) (ϕ.restrict_normal_aux E
     ⟨is_scalar_tower.to_alg_hom F E K x, ⟨x, ⟨subsemiring.mem_top x, rfl⟩⟩⟩))
 

src/field_theory/polynomial_galois_group.lean

@@ -123,7 +123,7 @@ variables {p E}
 @[simp] lemma restrict_smul [h : fact (p.splits (algebra_map F E))]
   (ϕ : E ≃ₐ[F] E) (x : root_set p E) : ↑((restrict p E ϕ) • x) = ϕ x :=
 begin
-  let ψ := alg_hom.alg_equiv.of_injective_field (is_scalar_tower.to_alg_hom F p.splitting_field E),
+  let ψ := alg_equiv.of_injective_field (is_scalar_tower.to_alg_hom F p.splitting_field E),
   change ↑(ψ (ψ.symm _)) = ϕ x,
   rw alg_equiv.apply_symm_apply ψ,
   change ϕ (roots_equiv_roots p E ((roots_equiv_roots p E).symm x)) = ϕ x,

src/linear_algebra/basic.lean

@@ -1286,7 +1286,9 @@ by rw [range, map_le_iff_le_comap, eq_top_iff]
 lemma map_le_range {f : M →ₗ[R] M₂} {p : submodule R M} : map f p ≤ range f :=
 map_mono le_top
 
-/-- Restrict the codomain of a linear map `f` to `f.range`. -/
+/-- Restrict the codomain of a linear map `f` to `f.range`.
+
+This is the bundled version of `set.range_factorization`. -/
 @[reducible] def range_restrict (f : M →ₗ[R] M₂) : M →ₗ[R] f.range :=
 f.cod_restrict f.range f.mem_range_self
 
@@ -1848,6 +1850,30 @@ end
 @[simp] protected theorem ker : (e : M →ₗ[R] M₂).ker = ⊥ :=
 linear_map.ker_eq_bot_of_injective e.to_equiv.injective
 
+variables {f g}
+
+/-- An linear map `f : M →ₗ[R] M₂` with a left-inverse `g : M₂ →ₗ[R] M` defines a linear equivalence
+between `M` and `f.range`.
+
+This is a computable alternative to `linear_equiv.of_injective`, and a bidirectional version of
+`linear_map.range_restrict`. -/
+def of_left_inverse {g : M₂ → M} (h : function.left_inverse g f) : M ≃ₗ[R] f.range :=
+{ to_fun := f.range_restrict,
+  inv_fun := g ∘ f.range.subtype,
+  left_inv := h,
+  right_inv := λ x, subtype.ext $
+    let ⟨x', hx'⟩ := linear_map.mem_range.mp x.prop in
+    show f (g x) = x, by rw [←hx', h x'],
+  .. f.range_restrict }
+
+@[simp] lemma of_left_inverse_apply
+  (h : function.left_inverse g f) (x : M) :
+  ↑(of_left_inverse h x) = f x := rfl
+
+@[simp] lemma of_left_inverse_symm_apply
+  (h : function.left_inverse g f) (x : f.range) :
+  (of_left_inverse h).symm x = g x := rfl
+
 end
 
 end add_comm_monoid
@@ -1890,10 +1916,9 @@ variables {semimodule_M : semimodule R M} {semimodule_M₂ : semimodule 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`. -/
+between `M` and `f.range`. See also `linear_map.of_left_inverse`. -/
 noncomputable def of_injective (h : f.ker = ⊥) : M ≃ₗ[R] f.range :=
-{ .. (equiv.set.range f $ linear_map.ker_eq_bot.1 h).trans (equiv.set.of_eq f.range_coe.symm),
-  .. f.cod_restrict f.range (λ x, f.mem_range_self x) }
+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

src/ring_theory/jacobson.lean

@@ -372,7 +372,7 @@ begin
   introI hI,
   let R' : subring I.quotient := ((quotient.mk I).comp C).range,
   let i : R →+* R' := ((quotient.mk I).comp C).range_restrict,
-  have hi : function.surjective (i : R → R') := ((quotient.mk I).comp C).surjective_onto_range,
+  have hi : function.surjective (i : R → R') := ((quotient.mk I).comp C).range_restrict_surjective,
   have hi' : (polynomial.map_ring_hom i : polynomial R →+* polynomial R').ker ≤ I,
   { refine λ f hf, polynomial_mem_ideal_of_coeff_mem_ideal I f (λ n, _),
     replace hf := congr_arg (λ (g : polynomial (((quotient.mk I).comp C).range)), g.coeff n) hf,

src/ring_theory/noetherian.lean

@@ -516,8 +516,8 @@ end
 
 instance is_noetherian_ring_range {R} [comm_ring R] {S} [comm_ring S] (f : R →+* S)
   [is_noetherian_ring R] : is_noetherian_ring f.range :=
-is_noetherian_ring_of_surjective R f.range (f.cod_restrict' f.range f.mem_range_self)
-  f.surjective_onto_range
+is_noetherian_ring_of_surjective R f.range f.range_restrict
+  f.range_restrict_surjective
 
 theorem is_noetherian_ring_of_ring_equiv (R) [comm_ring R] {S} [comm_ring S]
   (f : R ≃+* S) [is_noetherian_ring R] : is_noetherian_ring S :=

src/ring_theory/polynomial/basic.lean

@@ -347,7 +347,7 @@ begin
   simp only [ring_hom.comp_apply, quotient.eq_zero_iff_mem, subring.coe_zero, subtype.val_eq_coe],
   suffices : C (i y) ∈ (I.map (polynomial.map_ring_hom i)),
   { obtain ⟨f, hf⟩ := mem_image_of_mem_map_of_surjective (polynomial.map_ring_hom i)
-      (polynomial.map_surjective _ (((quotient.mk I).comp C).surjective_onto_range)) this,
+      (polynomial.map_surjective _ (((quotient.mk I).comp C).range_restrict_surjective)) this,
     refine sub_add_cancel (C y) f ▸ I.add_mem (hi' _ : (C y - f) ∈ I) hf.1,
     rw [ring_hom.mem_ker, ring_hom.map_sub, hf.2, sub_eq_zero_iff_eq, coe_map_ring_hom, map_C] },
   exact hx,

src/ring_theory/subring.lean

@@ -359,9 +359,6 @@ def cod_restrict' {R : Type u} {S : Type v} [ring R] [ring S] (f : R →+* S)
   map_mul' := λ x y, subtype.eq $ f.map_mul x y,
   map_one' := subtype.eq f.map_one }
 
-lemma surjective_onto_range : function.surjective (f.cod_restrict' f.range f.mem_range_self) :=
-λ ⟨y, hy⟩, let ⟨x, hx⟩ := mem_range.mp hy in ⟨x, subtype.ext hx⟩
-
 end ring_hom
 
 namespace subring
@@ -639,12 +636,17 @@ def restrict (f : R →+* S) (s : subring R) : s →+* S := f.comp s.subtype
 
 @[simp] lemma restrict_apply (f : R →+* S) (x : s) : f.restrict s x = f x := rfl
 
-/-- Restriction of a ring homomorphism to its range interpreted as a subsemiring. -/
+/-- Restriction of a ring homomorphism to its range interpreted as a subsemiring.
+
+This is the bundled version of `set.range_factorization`. -/
 def range_restrict (f : R →+* S) : R →+* f.range :=
 f.cod_restrict' f.range $ λ x, ⟨x, subring.mem_top x, rfl⟩
 
 @[simp] lemma coe_range_restrict (f : R →+* S) (x : R) : (f.range_restrict x : S) = f x := rfl
 
+lemma range_restrict_surjective (f : R →+* S) : function.surjective f.range_restrict :=
+λ ⟨y, hy⟩, let ⟨x, hx⟩ := mem_range.mp hy in ⟨x, subtype.ext hx⟩
+
 lemma range_top_iff_surjective {f : R →+* S} :
   f.range = (⊤ : subring S) ↔ function.surjective f :=
 subring.ext'_iff.trans $ iff.trans (by rw [coe_range, coe_top]) set.range_iff_surjective
@@ -725,6 +727,26 @@ variables {s t : subring R}
 def subring_congr (h : s = t) : s ≃+* t :=
 { map_mul' :=  λ _ _, rfl, map_add' := λ _ _, rfl, ..equiv.set_congr $ subring.ext'_iff.1 h }
 
+/-- Restrict a ring homomorphism with a left inverse to a ring isomorphism to its
+`ring_hom.range`. -/
+def of_left_inverse {g : S → R} {f : R →+* S} (h : function.left_inverse g f) :
+  R ≃+* f.range :=
+{ to_fun := λ x, f.range_restrict x,
+  inv_fun := λ x, (g ∘ f.range.subtype) x,
+  left_inv := h,
+  right_inv := λ x, subtype.ext $
+    let ⟨x', hx'⟩ := ring_hom.mem_range.mp x.prop in
+    show f (g x) = x, by rw [←hx', h x'],
+  ..f.range_restrict }
+
+@[simp] lemma of_left_inverse_apply
+  {g : S → R} {f : R →+* S} (h : function.left_inverse g f) (x : R) :
+  ↑(of_left_inverse h x) = f x := rfl
+
+@[simp] lemma of_left_inverse_symm_apply
+  {g : S → R} {f : R →+* S} (h : function.left_inverse g f) (x : f.range) :
+  (of_left_inverse h).symm x = g x := rfl
+
 end ring_equiv
 
 namespace subring

src/ring_theory/subsemiring.lean

@@ -259,6 +259,9 @@ def srange : subsemiring S := (⊤ : subsemiring R).map f
 @[simp] lemma mem_srange {f : R →+* S} {y : S} : y ∈ f.srange ↔ ∃ x, f x = y :=
 by simp [srange]
 
+lemma mem_srange_self (f : R →+* S) (x : R) : f x ∈ f.srange :=
+mem_srange.mpr ⟨x, rfl⟩
+
 lemma map_srange : f.srange.map g = (g.comp f).srange :=
 (⊤ : subsemiring R).map_map g f
 
@@ -517,14 +520,19 @@ def cod_srestrict (f : R →+* S) (s : subsemiring S) (h : ∀ x, f x ∈ s) : R
   .. (f : R →* S).cod_mrestrict s.to_submonoid h,
   .. (f : R →+ S).cod_mrestrict s.to_add_submonoid h }
 
-/-- Restriction of a ring homomorphism to its range iterpreted as a subsemiring. -/
+/-- Restriction of a ring homomorphism to its range interpreted as a subsemiring.
+
+This is the bundled version of `set.range_factorization`. -/
 def srange_restrict (f : R →+* S) : R →+* f.srange :=
-f.cod_srestrict f.srange $ λ x, ⟨x, subsemiring.mem_top x, rfl⟩
+f.cod_srestrict f.srange f.mem_srange_self
 
 @[simp] lemma coe_srange_restrict (f : R →+* S) (x : R) :
   (f.srange_restrict x : S) = f x :=
 rfl
 
+lemma srange_restrict_surjective (f : R →+* S) : function.surjective f.srange_restrict :=
+λ ⟨y, hy⟩, let ⟨x, hx⟩ := mem_srange.mp hy in ⟨x, subtype.ext hx⟩
+
 lemma srange_top_iff_surjective {f : R →+* S} :
   f.srange = (⊤ : subsemiring S) ↔ function.surjective f :=
 subsemiring.ext'_iff.trans $ iff.trans (by rw [coe_srange, coe_top]) set.range_iff_surjective
@@ -604,4 +612,24 @@ variables {s t : subsemiring R}
 def subsemiring_congr (h : s = t) : s ≃+* t :=
 { map_mul' :=  λ _ _, rfl, map_add' := λ _ _, rfl, ..equiv.set_congr $ subsemiring.ext'_iff.1 h }
 
+/-- Restrict a ring homomorphism with a left inverse to a ring isomorphism to its
+`ring_hom.srange`. -/
+def sof_left_inverse {g : S → R} {f : R →+* S} (h : function.left_inverse g f) :
+  R ≃+* f.srange :=
+{ to_fun := λ x, f.srange_restrict x,
+  inv_fun := λ x, (g ∘ f.srange.subtype) x,
+  left_inv := h,
+  right_inv := λ x, subtype.ext $
+    let ⟨x', hx'⟩ := ring_hom.mem_srange.mp x.prop in
+    show f (g x) = x, by rw [←hx', h x'],
+  ..f.srange_restrict }
+
+@[simp] lemma sof_left_inverse_apply
+  {g : S → R} {f : R →+* S} (h : function.left_inverse g f) (x : R) :
+  ↑(sof_left_inverse h x) = f x := rfl
+
+@[simp] lemma sof_left_inverse_symm_apply
+  {g : S → R} {f : R →+* S} (h : function.left_inverse g f) (x : f.srange) :
+  (sof_left_inverse h).symm x = g x := rfl
+
 end ring_equiv