From de20a3943257d203dff1fad335ce52b3a8f1d525 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Fri, 21 Aug 2020 10:07:47 +0000
Subject: [PATCH] feat(group_theory/subroup,ring_theory/ideal/operations):
 lift_of_surjective (#3888)

Surjective homomorphisms behave like quotient maps
---
 src/group_theory/abelianization.lean  |  2 +-
 src/group_theory/presented_group.lean |  4 +-
 src/group_theory/quotient_group.lean  |  4 +-
 src/group_theory/subgroup.lean        | 84 ++++++++++++++++++++++++++-
 src/ring_theory/ideal/operations.lean | 62 ++++++++++++++++++++
 5 files changed, 150 insertions(+), 6 deletions(-)

diff --git a/src/group_theory/abelianization.lean b/src/group_theory/abelianization.lean
index ff55180624085..df7dc9e81030b 100644
--- a/src/group_theory/abelianization.lean
+++ b/src/group_theory/abelianization.lean
@@ -66,7 +66,7 @@ begin
 end
 
 def lift : abelianization G →* A :=
-quotient_group.lift _ f (λ x h, monoid_hom.mem_ker.2 $ commutator_subset_ker _ h)
+quotient_group.lift _ f (λ x h, f.mem_ker.2 $ commutator_subset_ker _ h)
 
 @[simp] lemma lift.of (x : G) : lift f (of x) = f x :=
 rfl
diff --git a/src/group_theory/presented_group.lean b/src/group_theory/presented_group.lean
index 7717689ceb5ee..b16ae36e6db93 100644
--- a/src/group_theory/presented_group.lean
+++ b/src/group_theory/presented_group.lean
@@ -41,10 +41,10 @@ variable (h : ∀ r ∈ rels, F r = 1)
 
 -- FIXME why is apply_instance needed here? surely this should be a [] argument in `subgroup.normal_closure_le_normal`
 lemma closure_rels_subset_ker : subgroup.normal_closure rels ≤ monoid_hom.ker F :=
-subgroup.normal_closure_le_normal (by apply_instance) (λ x w, monoid_hom.mem_ker.2 (h x w))
+subgroup.normal_closure_le_normal (by apply_instance) (λ x w, (monoid_hom.mem_ker _).2 (h x w))
 
 lemma to_group_eq_one_of_mem_closure : ∀ x ∈ subgroup.normal_closure rels, F x = 1 :=
-λ x w, monoid_hom.mem_ker.1 $ closure_rels_subset_ker h w
+λ x w, (monoid_hom.mem_ker _).1 $ closure_rels_subset_ker h w
 
 /-- The extension of a map f : α → β that satisfies the given relations to a group homomorphism
 from presented_group rels → β. -/
diff --git a/src/group_theory/quotient_group.lean b/src/group_theory/quotient_group.lean
index 53bf02c7d3c04..6a7a0ef712ead 100644
--- a/src/group_theory/quotient_group.lean
+++ b/src/group_theory/quotient_group.lean
@@ -123,7 +123,7 @@ open function monoid_hom
 @[to_additive quotient_add_group.ker_lift "The induced map from the quotient by the kernel to the
 codomain."]
 def ker_lift : quotient (ker φ) →* H :=
-lift _ φ $ λ g, mem_ker.mp
+lift _ φ $ λ g, φ.mem_ker.mp
 
 @[simp, to_additive quotient_add_group.ker_lift_mk]
 lemma ker_lift_mk (g : G) : (ker_lift φ) g = φ g :=
@@ -147,7 +147,7 @@ show a⁻¹ * b ∈ ker φ, by rw [mem_ker,
 @[to_additive quotient_add_group.range_ker_lift "The induced map from the quotient by the kernel to
 the range."]
 def range_ker_lift : quotient (ker φ) →* φ.range :=
-lift _ (to_range φ) $ λ g hg, mem_ker.mp $ by rwa to_range_ker
+lift _ (to_range φ) $ λ g hg, (mem_ker _).mp $ by rwa to_range_ker
 
 @[to_additive quotient_add_group.range_ker_lift_injective]
 lemma range_ker_lift_injective : injective (range_ker_lift φ) :=
diff --git a/src/group_theory/subgroup.lean b/src/group_theory/subgroup.lean
index d840ff584b553..8682ab96c16a5 100644
--- a/src/group_theory/subgroup.lean
+++ b/src/group_theory/subgroup.lean
@@ -942,7 +942,7 @@ such that `f x = 0`"]
 def ker (f : G →* N) := (⊥ : subgroup N).comap f
 
 @[to_additive]
-lemma mem_ker {f : G →* N} {x : G} : x ∈ f.ker ↔ f x = 1 := iff.rfl
+lemma mem_ker (f : G →* N) {x : G} : x ∈ f.ker ↔ f x = 1 := iff.rfl
 
 @[to_additive]
 lemma comap_ker (g : N →* P) (f : G →* N) : g.ker.comap f = (g.comp f).ker := rfl
@@ -995,6 +995,88 @@ le_antisymm
 
 end monoid_hom
 
+namespace monoid_hom
+
+variables {G₁ G₂ G₃ : Type*} [group G₁] [group G₂] [group G₃]
+variables (f : G₁ →* G₂)
+
+/-- `lift_of_surjective f hf g hg` is the unique 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`.
+
+See `lift_of_surjective_eq` for the uniqueness lemma.
+
+```
+   G₁.
+   |  \
+ f |   \ g
+   |    \
+   v     \⌟
+   G₂----> G₃
+      ∃!φ
+```
+ -/
+@[to_additive "`lift_of_surjective f 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`.
+
+See `lift_of_surjective_eq` for the uniqueness lemma.
+
+```
+   G₁.
+   |  \\
+ f |   \\ g
+   |    \\
+   v     \\⌟
+   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 }
+
+@[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
+
+@[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] }
+
+@[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) :=
+begin
+  ext b, rcases hf b with ⟨a, rfl⟩,
+  simp only [← comp_apply, hh, f.lift_of_surjective_comp],
+end
+
+end monoid_hom
+
 variables {N : Type*} [group N]
 
 @[to_additive]
diff --git a/src/ring_theory/ideal/operations.lean b/src/ring_theory/ideal/operations.lean
index 5b89bafc7bada..bde457f121397 100644
--- a/src/ring_theory/ideal/operations.lean
+++ b/src/ring_theory/ideal/operations.lean
@@ -875,3 +875,65 @@ instance semimodule_submodule : semimodule (ideal R) (submodule R M) :=
   smul_zero := smul_bot }
 
 end submodule
+
+namespace ring_hom
+variables {A B C : Type*} [comm_ring A] [comm_ring B] [comm_ring C]
+variables (f : A →+* B)
+
+/-- `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) :
+  B →+* C :=
+{ to_fun := λ b, g (classical.some (hf 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)
+  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 _)],
+  end,
+  .. add_monoid_hom.lift_of_surjective f.to_add_monoid_hom 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_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] }
+
+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) :=
+begin
+  ext b, rcases hf b with ⟨a, rfl⟩,
+  simp only [← comp_apply, hh, f.lift_of_surjective_comp],
+end
+
+end ring_hom