feat(algebra/category/Group/epi_mono): (mono)epimorphisms and (in)sur…

…jections are the same in `(Add)(Comm)Group` (#15496)

src/algebra/category/Group/epi_mono.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Jujian Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jujian Zhang
 -/
-import algebra.category.Group.basic
+import algebra.category.Group.equivalence_Group_AddGroup
 import category_theory.epi_mono
 import group_theory.quotient_group
 
@@ -23,13 +23,36 @@ open quotient_group
 
 variables {A : Type u} {B : Type v}
 
+section
 variables [group A] [group B]
 
 @[to_additive add_monoid_hom.ker_eq_bot_of_cancel]
 lemma ker_eq_bot_of_cancel {f : A →* B} (h : ∀ (u v : f.ker →* A), f.comp u = f.comp v → u = v) :
   f.ker = ⊥ :=
 by simpa using _root_.congr_arg range (h f.ker.subtype 1 (by tidy))
 
+end
+
+section
+variables [comm_group A] [comm_group B]
+
+@[to_additive add_monoid_hom.range_eq_top_of_cancel]
+lemma range_eq_top_of_cancel {f : A →* B}
+  (h : ∀ (u v : B →* B ⧸ f.range), u.comp f = v.comp f → u = v) :
+  f.range = ⊤ :=
+begin
+  specialize h 1 (quotient_group.mk' _) _,
+  { ext1,
+    simp only [one_apply, coe_comp, coe_mk', function.comp_app],
+    rw [show (1 : B ⧸ f.range) = (1 : B), from quotient_group.coe_one _, quotient_group.eq,
+     inv_one, one_mul],
+    exact ⟨x, rfl⟩, },
+  replace h : (quotient_group.mk' _).ker = (1 : B →* B ⧸ f.range).ker := by rw h,
+  rwa [ker_one, quotient_group.ker_mk] at h,
+end
+
+end
+
 end monoid_hom
 
 section
@@ -281,4 +304,58 @@ iff.trans (epi_iff_surjective _) (subgroup.eq_top_iff' f.range).symm
 
 end Group
 
+namespace AddGroup
+variables {A B : AddGroup.{u}} (f : A ⟶ B)
+
+lemma epi_iff_surjective : epi f ↔ function.surjective f :=
+begin
+  have i1 : epi f ↔ epi (Group_AddGroup_equivalence.inverse.map f),
+  { refine ⟨_, Group_AddGroup_equivalence.inverse.epi_of_epi_map⟩,
+    introsI e',
+    apply Group_AddGroup_equivalence.inverse.map_epi },
+  rwa Group.epi_iff_surjective at i1,
+end
+
+lemma epi_iff_range_eq_top : epi f ↔ f.range = ⊤ :=
+iff.trans (epi_iff_surjective _) (add_subgroup.eq_top_iff' f.range).symm
+
+end AddGroup
+
+namespace CommGroup
+variables {A B : CommGroup.{u}} (f : A ⟶ B)
+
+@[to_additive AddCommGroup.ker_eq_bot_of_mono]
+lemma ker_eq_bot_of_mono [mono f] : f.ker = ⊥ :=
+monoid_hom.ker_eq_bot_of_cancel $ λ u v,
+  (@cancel_mono _ _ _ _ _ f _ (show CommGroup.of f.ker ⟶ A, from u) _).1
+
+@[to_additive AddCommGroup.mono_iff_ker_eq_bot]
+lemma mono_iff_ker_eq_bot : mono f ↔ f.ker = ⊥ :=
+⟨λ h, @@ker_eq_bot_of_mono f h,
+ λ h, concrete_category.mono_of_injective _ $ (monoid_hom.ker_eq_bot_iff f).1 h⟩
+
+@[to_additive AddCommGroup.mono_iff_injective]
+lemma mono_iff_injective : mono f ↔ function.injective f :=
+iff.trans (mono_iff_ker_eq_bot f) $ monoid_hom.ker_eq_bot_iff f
+
+@[to_additive]
+lemma range_eq_top_of_epi [epi f] : f.range = ⊤ :=
+monoid_hom.range_eq_top_of_cancel $ λ u v h,
+  (@cancel_epi _ _ _ _ _ f _ (show B ⟶ ⟨B ⧸ monoid_hom.range f⟩, from u) v).1 h
+
+@[to_additive]
+lemma epi_iff_range_eq_top : epi f ↔ f.range = ⊤ :=
+⟨λ hf, by exactI range_eq_top_of_epi _,
+ λ hf, concrete_category.epi_of_surjective _ $ monoid_hom.range_top_iff_surjective.mp hf⟩
+
+@[to_additive]
+lemma epi_iff_surjective : epi f ↔ function.surjective f :=
+by rw [epi_iff_range_eq_top, monoid_hom.range_top_iff_surjective]
+
+@[to_additive]
+instance : functor.preserves_epimorphisms (forget₂ CommGroup Group) :=
+{ preserves := λ X Y f e, by rwa [epi_iff_surjective, ←@Group.epi_iff_surjective ⟨X⟩ ⟨Y⟩ f] at e }
+
+end CommGroup
+
 end

src/algebra/category/Group/equivalence_Group_AddGroup.lean

@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2022 Jujian Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jujian Zhang
+-/
+import algebra.category.Group.basic
+
+/-!
+# Equivalence between `Group` and `AddGroup`
+
+This file contains two equivalences:
+* `Group_AddGroup_equivalence` : the equivalence between `Group` and `AddGroup` by sending
+  `X : Group` to `additive X` and `Y : AddGroup` to `multiplicative Y`.
+* `CommGroup_AddCommGroup_equivlance` : the equivalence between `CommGroup` and `AddCommGroup` by
+  sending `X : CommGroup` to `additive X` and `Y : AddCommGroup` to `multiplicative Y`.
+-/
+
+open category_theory
+
+namespace Group
+
+/--
+The functor `Group ⥤ AddGroup` by sending `X ↦ additive X` and `f ↦ f`.
+-/
+@[simps] def to_AddGroup : Group ⥤ AddGroup :=
+{ obj := λ X, AddGroup.of (additive X),
+  map := λ X Y, monoid_hom.to_additive }
+
+end Group
+
+namespace CommGroup
+
+/--
+The functor `CommGroup ⥤ AddCommGroup` by sending `X ↦ additive X` and `f ↦ f`.
+-/
+@[simps] def to_AddCommGroup : CommGroup ⥤ AddCommGroup :=
+{ obj := λ X, AddCommGroup.of (additive X),
+  map := λ X Y, monoid_hom.to_additive }
+
+end CommGroup
+
+namespace AddGroup
+
+/--
+The functor `AddGroup ⥤ Group` by sending `X ↦ multiplicative Y` and `f ↦ f`.
+-/
+@[simps] def to_Group : AddGroup ⥤ Group :=
+{ obj := λ X, Group.of (multiplicative X),
+  map := λ X Y, add_monoid_hom.to_multiplicative }
+
+end AddGroup
+
+namespace AddCommGroup
+
+/--
+The functor `AddCommGroup ⥤ CommGroup` by sending `X ↦ multiplicative Y` and `f ↦ f`.
+-/
+@[simps] def to_CommGroup : AddCommGroup ⥤ CommGroup :=
+{ obj := λ X, CommGroup.of (multiplicative X),
+  map := λ X Y, add_monoid_hom.to_multiplicative }
+
+end AddCommGroup
+
+/--
+The equivalence of categories between `Group` and `AddGroup`
+-/
+@[simps] def Group_AddGroup_equivalence : Group ≌ AddGroup :=
+equivalence.mk Group.to_AddGroup AddGroup.to_Group
+  (nat_iso.of_components
+    (λ X, mul_equiv.to_Group_iso (mul_equiv.multiplicative_additive X))
+    (λ X Y f, rfl))
+  (nat_iso.of_components
+    (λ X, add_equiv.to_AddGroup_iso (add_equiv.additive_multiplicative X))
+    (λ X Y f, rfl))
+
+/--
+The equivalence of categories between `CommGroup` and `AddCommGroup`.
+-/
+@[simps] def CommGroup_AddCommGroup_equivalence : CommGroup ≌ AddCommGroup :=
+equivalence.mk CommGroup.to_AddCommGroup AddCommGroup.to_CommGroup
+  (nat_iso.of_components
+    (λ X, mul_equiv.to_CommGroup_iso (mul_equiv.multiplicative_additive X))
+    (λ X Y f, rfl))
+  (nat_iso.of_components
+    (λ X, add_equiv.to_AddCommGroup_iso (add_equiv.additive_multiplicative X))
+    (λ X Y f, rfl))

src/algebra/hom/equiv.lean

@@ -729,3 +729,16 @@ def mul_equiv.to_additive'' [add_zero_class G] [mul_one_class H] :
 add_equiv.to_multiplicative''.symm
 
 end type_tags
+
+section
+variables (G) (H)
+
+/-- `additive (multiplicative G)` is just `G`. -/
+def add_equiv.additive_multiplicative [add_zero_class G] : additive (multiplicative G) ≃+ G :=
+mul_equiv.to_additive'' (mul_equiv.refl (multiplicative G))
+
+/-- `multiplicative (additive H)` is just `H`. -/
+def mul_equiv.multiplicative_additive [mul_one_class H] : multiplicative (additive H) ≃* H :=
+add_equiv.to_multiplicative'' (add_equiv.refl (additive H))
+
+end