[Merged by Bors] - refactor(group_theory/free_*): remove API duplicated by lift, promote lift functions to equivs

src/algebra/category/Group/adjunctions.lean

@@ -61,7 +61,7 @@ The free-forgetful adjunction for abelian groups.
 -/
 def adj : free ⊣ forget AddCommGroup.{u} :=
 adjunction.mk_of_hom_equiv
-{ hom_equiv := λ X G, free_abelian_group.hom_equiv X G,
+{ hom_equiv := λ X G, free_abelian_group.lift.symm,
   hom_equiv_naturality_left_symm' :=
   by { intros, ext, refl} }
 
@@ -90,7 +90,7 @@ def free : Type u ⥤ Group :=
 -/
 def adj : free ⊣ forget Group.{u} :=
 adjunction.mk_of_hom_equiv
-{ hom_equiv := λ X G, (free_group.lift X G).symm,
+{ hom_equiv := λ X G, free_group.lift.symm,
   hom_equiv_naturality_left_symm' := λ X Y G f g, begin ext1, refl end  }
 
 end Group
@@ -110,7 +110,7 @@ def abelianize : Group.{u} ⥤ CommGroup.{u} :=
 /-- The abelianization-forgetful adjuction from `Group` to `CommGroup`.-/
 def abelianize_adj : abelianize ⊣ forget₂ CommGroup.{u} Group.{u} :=
 adjunction.mk_of_hom_equiv
-{ hom_equiv := λ G A, abelianization.hom_equiv,
+{ hom_equiv := λ G A, abelianization.lift.symm,
   hom_equiv_naturality_left_symm' := λ G H A f g, by { ext1, refl } }
 
 end abelianization

src/algebra/free_monoid.lean

@@ -52,6 +52,7 @@ def of (x : α) : free_monoid α := [x]
 @[to_additive]
 lemma of_def (x : α) : of x = [x] := rfl
 
+@[to_additive]
 lemma of_injective : function.injective (@of α) :=
 λ a b, list.head_eq_of_cons_eq
 
@@ -98,9 +99,11 @@ congr_fun (lift_comp_of f) x
 lemma lift_restrict (f : free_monoid α →* M) : lift (f ∘ of) = f :=
 lift.apply_symm_apply f
 
+@[to_additive]
 lemma comp_lift (g : M →* N) (f : α → M) : g.comp (lift f) = lift (g ∘ f) :=
 by { ext, simp }
 
+@[to_additive]
 lemma hom_map_lift (g : M →* N) (f : α → M) (x : free_monoid α) : g (lift f x) = lift (g ∘ f) x :=
 monoid_hom.ext_iff.1 (comp_lift g f) x
 

src/group_theory/abelianization.lean

@@ -75,8 +75,11 @@ end
 
 /-- If `f : G → A` is a group homomorphism to an abelian group, then `lift f` is the unique map from
   the abelianization of a `G` to `A` that factors through `f`. -/
-def lift : abelianization G →* A :=
-quotient_group.lift _ f (λ x h, f.mem_ker.2 $ commutator_subset_ker _ h)
+def lift : (G →* A) ≃ (abelianization G →* A) :=
+{ to_fun := λ f, quotient_group.lift _ f (λ x h, f.mem_ker.2 $ commutator_subset_ker _ h),
+  inv_fun := λ F, F.comp of,
+  left_inv := λ f, monoid_hom.ext $ λ x, rfl,
+  right_inv := λ F, monoid_hom.ext $ λ x, quotient_group.induction_on x $ λ z, rfl }
 
 @[simp] lemma lift.of (x : G) : lift f (of x) = f x :=
 rfl
@@ -97,30 +100,6 @@ variables {A : Type v} [monoid A]
 @[ext]
 theorem hom_ext (φ ψ : abelianization G →* A)
   (h : φ.comp of = ψ.comp of) : φ = ψ :=
-begin
-  ext x,
-  apply quotient_group.induction_on x,
-  intro z,
-  show φ.comp of z = _,
-  rw h,
-  refl,
-end
-
-section lift
-
-variables {B : Type v} [comm_group B]
-
-/-- The bijection underlying the abelianization-forgetful adjuction from groups to abelian groups.
--/
-@[simps]
-def hom_equiv : (abelianization G →* B) ≃ (G →* B) :=
-{ to_fun := λ f, { to_fun := f.1 ∘ abelianization.of ,
-  map_one' := by simp,
-  map_mul' := by simp } ,
-  inv_fun := λ g, abelianization.lift g,
-  left_inv := by { intro x, ext, simp },
-  right_inv := by { intro x, ext, simp } }
-
-end lift
+monoid_hom.ext $ λ x, quotient_group.induction_on x $ monoid_hom.congr_fun h
 
 end abelianization

src/group_theory/free_abelian_group.lean

@@ -32,10 +32,8 @@ Here we use the following variables: `(α β : Type*) (A : Type*) [add_comm_grou
 group it is `α →₀ ℤ`, the functions from `α` to `ℤ` such that all but finitely
 many elements get mapped to zero, however this is not how it is implemented.
 
-* `lift (f : α → A) : free_abelian_group α →+ A` : the group homomorphism induced
-by the map `f`.
-
-* `hom_equiv : (free_abelian_group α →+ A) ≃ (α → A)` : the bijection witnessing adjointness.
+* `lift f : free_abelian_group α →+ A` : the group homomorphism induced
+  by the map `f : α → A`.
 
 * `map (f : α → β) : free_abelian_group α →+ free_abelian_group β` : functoriality
     of `free_abelian_group`
@@ -91,9 +89,9 @@ def of (x : α) : free_abelian_group α :=
 abelianization.of $ free_group.of x
 
 /-- The map `free_abelian_group α →+ A` induced by a map of types `α → A`. -/
-def lift {β : Type v} [add_comm_group β] (f : α → β) : free_abelian_group α →+ β :=
-(@abelianization.lift _ _ (multiplicative β) _
-  (monoid_hom.of (@free_group.to_group _ (multiplicative β) _ f))).to_additive
+def lift {β : Type v} [add_comm_group β] : (α → β) ≃ (free_abelian_group α →+ β) :=
+(@free_group.lift _ (multiplicative β) _).trans $
+  (@abelianization.lift _ _ (multiplicative β) _).trans monoid_hom.to_additive
 
 namespace lift
 variables {β : Type v} [add_comm_group β] (f : α → β)
@@ -102,25 +100,20 @@ open free_abelian_group
 @[simp] protected lemma of (x : α) : lift f (of x) = f x :=
 begin
   convert @abelianization.lift.of (free_group α) _ (multiplicative β) _ _ _,
-  convert free_group.to_group.of.symm
+  convert free_group.lift.of.symm
 end
 
 protected theorem unique (g : free_abelian_group α →+ β)
   (hg : ∀ x, g (of x) = f x) {x} :
   g x = lift f x :=
-@abelianization.lift.unique (free_group α) _ (multiplicative β) _
-  (@free_group.to_group _ (multiplicative β) _ f) g.to_multiplicative
-  (λ x, @free_group.to_group.unique α (multiplicative β) _ _
-    ((add_monoid_hom.to_multiplicative' g).comp abelianization.of)
-    hg x) _
+add_monoid_hom.congr_fun ((lift.symm_apply_eq).mp (funext hg : g ∘ of = f)) _
 
 /-- See note [partially-applied ext lemmas]. -/
 @[ext]
 protected theorem ext (g h : free_abelian_group α →+ β)
   (H : ∀ x, g (of x) = h (of x)) :
   g = h :=
-add_monoid_hom.ext $ λ x, (lift.unique (g ∘ of) g (λ _, rfl)).trans $
-eq.symm $ lift.unique _ _ $ λ x, eq.symm $ H x
+lift.symm.injective $ funext H
 
 lemma map_hom {α β γ} [add_comm_group β] [add_comm_group γ]
   (a : free_abelian_group α) (f : α → β) (g : β →+ γ) :
@@ -141,31 +134,14 @@ open_locale classical
 
 lemma of_injective : function.injective (of : α → free_abelian_group α) :=
 λ x y hoxy, classical.by_contradiction $ assume hxy : x ≠ y,
-  let f : free_abelian_group α →+ ℤ := lift (λ z, if x = z then 1 else 0) in
+  let f : free_abelian_group α →+ ℤ := lift (λ z, if x = z then (1 : ℤ) else 0) in
   have hfx1 : f (of x) = 1, from (lift.of _ _).trans $ if_pos rfl,
   have hfy1 : f (of y) = 1, from hoxy ▸ hfx1,
   have hfy0 : f (of y) = 0, from (lift.of _ _).trans $ if_neg hxy,
   one_ne_zero $ hfy1.symm.trans hfy0
 
 end
 
-section
-variables (X : Type*) (G : Type*) [add_comm_group G]
-
-/-- The bijection underlying the free-forgetful adjunction for abelian groups.-/
-def hom_equiv : (free_abelian_group X →+ G) ≃ (X → G) :=
-{ to_fun := λ f, f.1 ∘ of,
-  inv_fun := λ f, lift f,
-  left_inv := λ f, begin ext, simp end,
-  right_inv := λ f, funext $ λ x, lift.of f x }
-
-@[simp]
-lemma hom_equiv_apply (f) (x) : ((hom_equiv X G) f) x = f (of x) := rfl
-@[simp]
-lemma hom_equiv_symm_apply (f) (x) : ((hom_equiv X G).symm f) x = (lift f) x := rfl
-
-end
-
 local attribute [instance] quotient_group.left_rel
 
 @[elab_as_eliminator]