feat(group_theory/subgroup): add {monoid,add_monoid,ring}_hom.lift_of_right_inverse (#6814)

This provides a computable alternative to `lift_of_surjective`.

Author: eric-wieser

src/data/zmod/basic.lean

@@ -835,8 +835,10 @@ lemma ring_hom_surjective [ring R] (f : R →+* (zmod n)) : function.surjective
 
 lemma ring_hom_eq_of_ker_eq [comm_ring R] (f g : R →+* (zmod n))
   (h : f.ker = g.ker) : f = g :=
-by rw [← f.lift_of_surjective_comp (zmod.ring_hom_surjective f) g (le_of_eq h),
-      ring_hom.ext_zmod (f.lift_of_surjective _ _ _) (ring_hom.id _),
-      ring_hom.id_comp]
+begin
+  have := f.lift_of_right_inverse_comp _ (zmod.ring_hom_right_inverse f) ⟨g, le_of_eq h⟩,
+  rw subtype.coe_mk at this,
+  rw [←this, ring_hom.ext_zmod (f.lift_of_right_inverse _ _ _) (ring_hom.id _), ring_hom.id_comp],
+end
 
 end zmod

src/group_theory/subgroup.lean

@@ -1252,15 +1252,43 @@ end subgroup
 namespace monoid_hom
 
 variables {G₁ G₂ G₃ : Type*} [group G₁] [group G₂] [group G₃]
-variables (f : G₁ →* G₂)
+variables (f : G₁ →* G₂) (f_inv : G₂ → G₁)
 
-/-- `lift_of_surjective f hf g hg` is the unique group homomorphism `φ`
+/-- Auxiliary definition used to define `lift_of_right_inverse` -/
+@[to_additive "Auxiliary definition used to define `lift_of_right_inverse`"]
+def lift_of_right_inverse_aux
+  (hf : function.right_inverse f_inv f) (g : G₁ →* G₃) (hg : f.ker ≤ g.ker) :
+  G₂ →* G₃ :=
+{ to_fun := λ b, g (f_inv b),
+  map_one' := hg (hf 1),
+  map_mul' :=
+  begin
+    intros x y,
+    rw [← g.map_mul, ← mul_inv_eq_one, ← g.map_inv, ← g.map_mul, ← g.mem_ker],
+    apply hg,
+    rw [f.mem_ker, f.map_mul, f.map_inv, mul_inv_eq_one, f.map_mul],
+    simp only [hf _],
+  end }
+
+@[simp, to_additive]
+lemma lift_of_right_inverse_aux_comp_apply
+  (hf : function.right_inverse f_inv f) (g : G₁ →* G₃) (hg : f.ker ≤ g.ker) (x : G₁) :
+  (f.lift_of_right_inverse_aux f_inv hf g hg) (f x) = g x :=
+begin
+  dsimp [lift_of_right_inverse_aux],
+  rw [← mul_inv_eq_one, ← g.map_inv, ← g.map_mul, ← g.mem_ker],
+  apply hg,
+  rw [f.mem_ker, f.map_mul, f.map_inv, mul_inv_eq_one],
+  simp only [hf _],
+end
 
-* such that `φ.comp f = g` (`lift_of_surjective_comp`),
-* where `f : G₁ →+* G₂` is surjective (`hf`),
+/-- `lift_of_right_inverse f hf g hg` is the unique group homomorphism `φ`
+
+* such that `φ.comp f = g` (`monoid_hom.lift_of_right_inverse_comp`),
+* where `f : G₁ →+* G₂` has a right_inverse `f_inv` (`hf`),
 * and `g : G₂ →+* G₃` satisfies `hg : f.ker ≤ g.ker`.
 
-See `lift_of_surjective_eq` for the uniqueness lemma.
+See `monoid_hom.eq_lift_of_right_inverse` for the uniqueness lemma.
 
 ```
    G₁.
@@ -1272,13 +1300,13 @@ See `lift_of_surjective_eq` for the uniqueness lemma.
       ∃!φ
 ```
  -/
-@[to_additive "`lift_of_surjective f hf g hg` is the unique additive group homomorphism `φ`
+@[to_additive "`lift_of_right_inverse f f_inv hf g hg` is the unique additive group homomorphism `φ`
 
-* such that `φ.comp f = g` (`lift_of_surjective_comp`),
-* where `f : G₁ →+* G₂` is surjective (`hf`),
-* and `g : G₂ →+* G₃` satisfies `hg : f.ker ≤ g.ker`.
+* such that `φ.comp f = g` (`add_monoid_hom.lift_of_right_inverse_comp`),
+* where `f : G₁ →+ G₂` has a right_inverse `f_inv` (`hf`),
+* and `g : G₂ →+ G₃` satisfies `hg : f.ker ≤ g.ker`.
 
-See `lift_of_surjective_eq` for the uniqueness lemma.
+See `add_monoid_hom.eq_lift_of_right_inverse` for the uniqueness lemma.
 
 ```
    G₁.
@@ -1289,44 +1317,45 @@ See `lift_of_surjective_eq` for the uniqueness lemma.
    G₂----> G₃
       ∃!φ
 ```"]
-noncomputable def lift_of_surjective
-  (hf : function.surjective f) (g : G₁ →* G₃) (hg : f.ker ≤ g.ker) :
-  G₂ →* G₃ :=
-{ to_fun := λ b, g (classical.some (hf b)),
-  map_one' := hg (classical.some_spec (hf 1)),
-  map_mul' :=
-  begin
-    intros x y,
-    rw [← g.map_mul, ← mul_inv_eq_one, ← g.map_inv, ← g.map_mul, ← g.mem_ker],
-    apply hg,
-    rw [f.mem_ker, f.map_mul, f.map_inv, mul_inv_eq_one, f.map_mul],
-    simp only [classical.some_spec (hf _)],
-  end }
+def lift_of_right_inverse
+  (hf : function.right_inverse f_inv f) : {g : G₁ →* G₃ // f.ker ≤ g.ker} ≃ (G₂ →* G₃) :=
+{ to_fun := λ g, f.lift_of_right_inverse_aux f_inv hf g.1 g.2,
+  inv_fun := λ φ, ⟨φ.comp f, λ x hx, (mem_ker _).mpr $ by simp [(mem_ker _).mp hx]⟩,
+  left_inv := λ g, by {
+    ext,
+    simp only [comp_apply, lift_of_right_inverse_aux_comp_apply, subtype.coe_mk,
+      subtype.val_eq_coe], },
+  right_inv := λ φ, by {
+    ext b,
+    simp [lift_of_right_inverse_aux, hf b], } }
+
+/-- A non-computable version of `monoid_hom.lift_of_right_inverse` for when no computable right
+inverse is available, that uses `function.surj_inv`. -/
+@[simp, to_additive "A non-computable version of `add_monoid_hom.lift_of_right_inverse` for when no
+computable right inverse is available."]
+noncomputable abbreviation lift_of_surjective
+  (hf : function.surjective f) : {g : G₁ →* G₃ // f.ker ≤ g.ker} ≃ (G₂ →* G₃) :=
+f.lift_of_right_inverse (function.surj_inv hf) (function.right_inverse_surj_inv hf)
 
 @[simp, to_additive]
-lemma lift_of_surjective_comp_apply
-  (hf : function.surjective f) (g : G₁ →* G₃) (hg : f.ker ≤ g.ker) (x : G₁) :
-  (f.lift_of_surjective hf g hg) (f x) = g x :=
-begin
-  dsimp [lift_of_surjective],
-  rw [← mul_inv_eq_one, ← g.map_inv, ← g.map_mul, ← g.mem_ker],
-  apply hg,
-  rw [f.mem_ker, f.map_mul, f.map_inv, mul_inv_eq_one],
-  simp only [classical.some_spec (hf _)],
-end
+lemma lift_of_right_inverse_comp_apply
+  (hf : function.right_inverse f_inv f) (g : {g : G₁ →* G₃ // f.ker ≤ g.ker}) (x : G₁) :
+  (f.lift_of_right_inverse f_inv hf g) (f x) = g x :=
+f.lift_of_right_inverse_aux_comp_apply f_inv hf g.1 g.2 x
 
 @[simp, to_additive]
-lemma lift_of_surjective_comp (hf : function.surjective f) (g : G₁ →* G₃) (hg : f.ker ≤ g.ker) :
-  (f.lift_of_surjective hf g hg).comp f = g :=
-by { ext, simp only [comp_apply, lift_of_surjective_comp_apply] }
+lemma lift_of_right_inverse_comp (hf : function.right_inverse f_inv f)
+  (g : {g : G₁ →* G₃ // f.ker ≤ g.ker}) :
+  (f.lift_of_right_inverse f_inv hf g).comp f = g :=
+monoid_hom.ext $ f.lift_of_right_inverse_comp_apply f_inv hf g
 
 @[to_additive]
-lemma eq_lift_of_surjective (hf : function.surjective f) (g : G₁ →* G₃) (hg : f.ker ≤ g.ker)
-  (h : G₂ →* G₃) (hh : h.comp f = g) :
-  h = (f.lift_of_surjective hf g hg) :=
+lemma eq_lift_of_right_inverse (hf : function.right_inverse f_inv f) (g : G₁ →* G₃)
+  (hg : f.ker ≤ g.ker) (h : G₂ →* G₃) (hh : h.comp f = g) :
+  h = (f.lift_of_right_inverse f_inv hf ⟨g, hg⟩) :=
 begin
-  ext b, rcases hf b with ⟨a, rfl⟩,
-  simp only [← comp_apply, hh, f.lift_of_surjective_comp],
+  simp_rw ←hh,
+  exact ((f.lift_of_right_inverse f_inv hf).apply_symm_apply _).symm,
 end
 
 end monoid_hom

src/ring_theory/ideal/operations.lean

@@ -1443,62 +1443,88 @@ end submodule
 
 namespace ring_hom
 variables {A B C : Type*} [comm_ring A] [comm_ring B] [comm_ring C]
-variables (f : A →+* B)
+variables (f : A →+* B) (f_inv : B → A)
 
-/-- `lift_of_surjective f hf g hg` is the unique ring homomorphism `φ`
-
-* such that `φ.comp f = g` (`lift_of_surjective_comp`),
-* where `f : A →+* B` is surjective (`hf`),
-* and `g : B →+* C` satisfies `hg : f.ker ≤ g.ker`.
-
-See `lift_of_surjective_eq` for the uniqueness lemma.
-
-```
-   A .
-   |  \
- f |   \ g
-   |    \
-   v     \⌟
-   B ----> C
-      ∃!φ
-```
- -/
-noncomputable def lift_of_surjective
-  (hf : function.surjective f) (g : A →+* C) (hg : f.ker ≤ g.ker) :
+/-- Auxiliary definition used to define `lift_of_right_inverse` -/
+def lift_of_right_inverse_aux
+  (hf : function.right_inverse f_inv f) (g : A →+* C) (hg : f.ker ≤ g.ker) :
   B →+* C :=
-{ to_fun := λ b, g (classical.some (hf b)),
+{ to_fun := λ b, g (f_inv b),
   map_one' :=
   begin
     rw [← g.map_one, ← sub_eq_zero, ← g.map_sub, ← g.mem_ker],
     apply hg,
     rw [f.mem_ker, f.map_sub, sub_eq_zero, f.map_one],
-    exact classical.some_spec (hf 1)
+    exact hf 1
   end,
   map_mul' :=
   begin
     intros x y,
     rw [← g.map_mul, ← sub_eq_zero, ← g.map_sub, ← g.mem_ker],
     apply hg,
     rw [f.mem_ker, f.map_sub, sub_eq_zero, f.map_mul],
-    simp only [classical.some_spec (hf _)],
+    simp only [hf _],
   end,
-  .. add_monoid_hom.lift_of_surjective f.to_add_monoid_hom hf g.to_add_monoid_hom hg }
+  .. add_monoid_hom.lift_of_right_inverse f.to_add_monoid_hom f_inv hf ⟨g.to_add_monoid_hom, hg⟩ }
 
-@[simp] lemma lift_of_surjective_comp_apply
-  (hf : function.surjective f) (g : A →+* C) (hg : f.ker ≤ g.ker) (a : A) :
-  (f.lift_of_surjective hf g hg) (f a) = g a :=
-f.to_add_monoid_hom.lift_of_surjective_comp_apply hf g.to_add_monoid_hom hg a
+@[simp] lemma lift_of_right_inverse_aux_comp_apply
+  (hf : function.right_inverse f_inv f) (g : A →+* C) (hg : f.ker ≤ g.ker) (a : A) :
+  (f.lift_of_right_inverse_aux f_inv hf g hg) (f a) = g a :=
+f.to_add_monoid_hom.lift_of_right_inverse_comp_apply f_inv hf ⟨g.to_add_monoid_hom, hg⟩ a
 
-@[simp] lemma lift_of_surjective_comp (hf : function.surjective f) (g : A →+* C)
-  (hg : f.ker ≤ g.ker) : (f.lift_of_surjective hf g hg).comp f = g :=
-by { ext, simp only [comp_apply, lift_of_surjective_comp_apply] }
+/-- `lift_of_right_inverse f hf g hg` is the unique ring homomorphism `φ`
 
-lemma eq_lift_of_surjective (hf : function.surjective f) (g : A →+* C) (hg : f.ker ≤ g.ker)
-  (h : B →+* C) (hh : h.comp f = g) :
-  h = (f.lift_of_surjective hf g hg) :=
+* such that `φ.comp f = g` (`ring_hom.lift_of_right_inverse_comp`),
+* where `f : A →+* B` is has a right_inverse `f_inv` (`hf`),
+* and `g : B →+* C` satisfies `hg : f.ker ≤ g.ker`.
+
+See `ring_hom.eq_lift_of_right_inverse` for the uniqueness lemma.
+
+```
+   A .
+   |  \
+ f |   \ g
+   |    \
+   v     \⌟
+   B ----> C
+      ∃!φ
+```
+-/
+def lift_of_right_inverse
+  (hf : function.right_inverse f_inv f) : {g : A →+* C // f.ker ≤ g.ker} ≃ (B →+* C) :=
+{ to_fun := λ g, f.lift_of_right_inverse_aux f_inv hf g.1 g.2,
+  inv_fun := λ φ, ⟨φ.comp f, λ x hx, (mem_ker _).mpr $ by simp [(mem_ker _).mp hx]⟩,
+  left_inv := λ g, by {
+    ext,
+    simp only [comp_apply, lift_of_right_inverse_aux_comp_apply, subtype.coe_mk,
+      subtype.val_eq_coe], },
+  right_inv := λ φ, by {
+    ext b,
+    simp [lift_of_right_inverse_aux, hf b], } }
+
+/-- A non-computable version of `ring_hom.lift_of_right_inverse` for when no computable right
+inverse is available, that uses `function.surj_inv`. -/
+@[simp]
+noncomputable abbreviation lift_of_surjective
+  (hf : function.surjective f) : {g : A →+* C // f.ker ≤ g.ker} ≃ (B →+* C) :=
+f.lift_of_right_inverse (function.surj_inv hf) (function.right_inverse_surj_inv hf)
+
+lemma lift_of_right_inverse_comp_apply
+  (hf : function.right_inverse f_inv f) (g : {g : A →+* C // f.ker ≤ g.ker}) (x : A) :
+  (f.lift_of_right_inverse f_inv hf g) (f x) = g x :=
+f.lift_of_right_inverse_aux_comp_apply f_inv hf g.1 g.2 x
+
+lemma lift_of_right_inverse_comp (hf : function.right_inverse f_inv f)
+  (g : {g : A →+* C // f.ker ≤ g.ker}) :
+  (f.lift_of_right_inverse f_inv hf g).comp f = g :=
+ring_hom.ext $ f.lift_of_right_inverse_comp_apply f_inv hf g
+
+lemma eq_lift_of_right_inverse (hf : function.right_inverse f_inv f) (g : A →+* C)
+  (hg : f.ker ≤ g.ker) (h : B →+* C) (hh : h.comp f = g) :
+  h = (f.lift_of_right_inverse f_inv hf ⟨g, hg⟩) :=
 begin
-  ext b, rcases hf b with ⟨a, rfl⟩,
-  simp only [← comp_apply, hh, f.lift_of_surjective_comp],
+  simp_rw ←hh,
+  exact ((f.lift_of_right_inverse f_inv hf).apply_symm_apply _).symm,
 end
 
 end ring_hom

src/ring_theory/roots_of_unity.lean

@@ -488,44 +488,35 @@ h.pow_eq_one
 and the powers of a primitive root of unity `ζ`. -/
 def zmod_equiv_gpowers (h : is_primitive_root ζ k) : zmod k ≃+ additive (subgroup.gpowers ζ) :=
 add_equiv.of_bijective
-(add_monoid_hom.lift_of_surjective (int.cast_add_hom _)
-  zmod.int_cast_surjective
-  { to_fun := λ i, additive.of_mul (⟨_, i, rfl⟩ : subgroup.gpowers ζ),
-    map_zero' := by { simp only [gpow_zero], refl },
-    map_add' := by { intros i j, simp only [gpow_add], refl } }
-  (λ i hi,
+  (add_monoid_hom.lift_of_right_inverse (int.cast_add_hom $ zmod k) _ zmod.int_cast_right_inverse
+    ⟨{ to_fun := λ i, additive.of_mul (⟨_, i, rfl⟩ : subgroup.gpowers ζ),
+      map_zero' := by { simp only [gpow_zero], refl },
+      map_add' := by { intros i j, simp only [gpow_add], refl } },
+    (λ i hi,
+    begin
+      simp only [add_monoid_hom.mem_ker, char_p.int_cast_eq_zero_iff (zmod k) k,
+        add_monoid_hom.coe_mk, int.coe_cast_add_hom] at hi ⊢,
+      obtain ⟨i, rfl⟩ := hi,
+      simp only [gpow_mul, h.pow_eq_one, one_gpow, gpow_coe_nat],
+      refl
+    end)⟩)
   begin
-    simp only [add_monoid_hom.mem_ker, char_p.int_cast_eq_zero_iff (zmod k) k,
-      add_monoid_hom.coe_mk, int.coe_cast_add_hom] at hi ⊢,
-    obtain ⟨i, rfl⟩ := hi,
-    simp only [gpow_mul, h.pow_eq_one, one_gpow, gpow_coe_nat],
-    refl
-  end)) $
-begin
-  split,
-  { rw add_monoid_hom.injective_iff,
-    intros i hi,
-    rw subtype.ext_iff at hi,
-    have := (h.gpow_eq_one_iff_dvd _).mp hi,
-    rw [← (char_p.int_cast_eq_zero_iff (zmod k) k _).mpr this, eq_comm],
-    exact classical.some_spec (zmod.int_cast_surjective i) },
-  { rintro ⟨ξ, i, rfl⟩,
-    refine ⟨int.cast_add_hom _ i, _⟩,
-    rw [add_monoid_hom.lift_of_surjective_comp_apply],
-    refl }
-end
+    split,
+    { rw add_monoid_hom.injective_iff,
+      intros i hi,
+      rw subtype.ext_iff at hi,
+      have := (h.gpow_eq_one_iff_dvd _).mp hi,
+      rw [← (char_p.int_cast_eq_zero_iff (zmod k) k _).mpr this, eq_comm],
+      exact zmod.int_cast_right_inverse i },
+    { rintro ⟨ξ, i, rfl⟩,
+      refine ⟨int.cast_add_hom _ i, _⟩,
+      rw [add_monoid_hom.lift_of_right_inverse_comp_apply],
+      refl }
+  end
 
 @[simp] lemma zmod_equiv_gpowers_apply_coe_int (i : ℤ) :
   h.zmod_equiv_gpowers i = additive.of_mul (⟨ζ ^ i, i, rfl⟩ : subgroup.gpowers ζ) :=
-begin
-  apply add_monoid_hom.lift_of_surjective_comp_apply,
-  intros j hj,
-  simp only [add_monoid_hom.mem_ker, char_p.int_cast_eq_zero_iff (zmod k) k,
-    add_monoid_hom.coe_mk, int.coe_cast_add_hom] at hj ⊢,
-  obtain ⟨j, rfl⟩ := hj,
-  simp only [gpow_mul, h.pow_eq_one, one_gpow, gpow_coe_nat],
-  refl
-end
+add_monoid_hom.lift_of_right_inverse_comp_apply _ _ zmod.int_cast_right_inverse _ _
 
 @[simp] lemma zmod_equiv_gpowers_apply_coe_nat (i : ℕ) :
   h.zmod_equiv_gpowers i = additive.of_mul (⟨ζ ^ i, i, rfl⟩ : subgroup.gpowers ζ) :=

src/ring_theory/witt_vector/truncated.lean

@@ -198,7 +198,7 @@ variable [comm_ring R]
 
 lemma truncate_fun_surjective :
   surjective (@truncate_fun p n R) :=
-λ x, ⟨x.out, truncated_witt_vector.truncate_fun_out x⟩
+function.right_inverse.surjective truncated_witt_vector.truncate_fun_out
 
 include hp
 
@@ -300,24 +300,22 @@ A ring homomorphism that truncates a truncated Witt vector of length `m` to
 a truncated Witt vector of length `n`, for `n ≤ m`.
 -/
 def truncate {m : ℕ} (hm : n ≤ m) : truncated_witt_vector p m R →+* truncated_witt_vector p n R :=
-ring_hom.lift_of_surjective
-  (witt_vector.truncate m)
-  (witt_vector.truncate_surjective p m R)
-  (witt_vector.truncate n)
+ring_hom.lift_of_right_inverse (witt_vector.truncate m) out truncate_fun_out
+  ⟨witt_vector.truncate n,
   begin
     intro x,
     simp only [witt_vector.mem_ker_truncate],
     intros h i hi,
     exact h i (lt_of_lt_of_le hi hm)
-  end
+  end⟩
 
 @[simp] lemma truncate_comp_witt_vector_truncate {m : ℕ} (hm : n ≤ m) :
   (@truncate p _ n R _ m hm).comp (witt_vector.truncate m) = witt_vector.truncate n :=
-ring_hom.lift_of_surjective_comp _ _ _ _
+ring_hom.lift_of_right_inverse_comp _ _ _ _
 
 @[simp] lemma truncate_witt_vector_truncate {m : ℕ} (hm : n ≤ m) (x : 𝕎 R) :
   truncate hm (witt_vector.truncate m x) = witt_vector.truncate n x :=
-ring_hom.lift_of_surjective_comp_apply _ _ _ _ _
+ring_hom.lift_of_right_inverse_comp_apply _ _ _ _ _
 
 @[simp] lemma truncate_truncate {n₁ n₂ n₃ : ℕ} (h1 : n₁ ≤ n₂) (h2 : n₂ ≤ n₃)
   (x : truncated_witt_vector p n₃ R) :