[Merged by Bors] - feat(FinitelyPresentedGroup): Additivize everything and add ℤ instance

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -846,6 +846,7 @@ instance (priority := 100) normal_subgroupOf {H N : Subgroup G} [N.Normal] :
     (N.subgroupOf H).Normal :=
   Subgroup.normal_comap _
 
+@[to_additive]
 theorem map_normalClosure (s : Set G) (f : G →* N) (hf : Surjective f) :
     (normalClosure s).map f = normalClosure (f '' s) := by
   have : Normal (map f (normalClosure s)) := Normal.map inferInstance f hf
@@ -854,6 +855,7 @@ theorem map_normalClosure (s : Set G) (f : G →* N) (hf : Surjective f) :
       ← Set.image_subset_iff, subset_normalClosure]
   · exact normalClosure_le_normal (Set.image_mono subset_normalClosure)
 
+@[to_additive]
 theorem comap_normalClosure (s : Set N) (f : G ≃* N) :
     normalClosure (f ⁻¹' s) = (normalClosure s).comap f := by
   have := f.toEquiv.image_symm_eq_preimage s

Mathlib/GroupTheory/FinitelyPresentedGroup.lean

@@ -33,51 +33,70 @@ finitely presented group, finitely generated normal closure
 
 variable {G H α β : Type*} [Group G] [Group H]
 
-/--
-`IsNormalClosureFG N` says that the subgroup `N` is the normal closure of a finitely-generated
-subgroup.
--/
+/-- `IsNormalClosureFG N` says that the subgroup `N` is the normal closure of a finitely-generated
+subgroup. -/
+@[to_additive /-- `IsNormalClosureFG N` says that the additive subgroup `N` is the normal closure
+of an additive finitely-generated subgroup. -/]
 def Subgroup.IsNormalClosureFG (N : Subgroup G) : Prop :=
   ∃ S : Set G, S.Finite ∧ Subgroup.normalClosure S = N
 
 namespace Subgroup.IsNormalClosureFG
 
 /-- Being the normal closure of a finite set is invariant under surjective homomorphism. -/
+@[to_additive /-- Being the additive normal closure of a finite set is invariant under
+surjective homomorphism. -/]
 protected theorem map {N : Subgroup G} (hN : IsNormalClosureFG N)
     {f : G →* H} (hf : Function.Surjective f) : (N.map f).IsNormalClosureFG := by
   obtain ⟨S, hSfinite, hSclosure⟩ := hN
   refine ⟨f '' S, hSfinite.image _, ?_⟩
   rw [← hSclosure, Subgroup.map_normalClosure _ _ hf]
 
 /-- The trivial group is the normal closure of a finite set of relations. -/
+@[to_additive /-- The trivial additive group is the normal closure of a finite set of relations. -/]
 protected theorem bot : IsNormalClosureFG (⊥ : Subgroup G) :=
   ⟨∅, Finite.of_subsingleton, normalClosure_empty⟩
 
 end Subgroup.IsNormalClosureFG
 
+/-- An additive group is finitely presented if it has a finite generating set such that the kernel
+of the induced map from the free additive group on that set is the normal closure
+of finitely many relations. -/
+class AddGroup.IsFinitelyPresented (G : Type*) [AddGroup G] : Prop where
+  out : ∃ (n : ℕ) (φ : FreeAddGroup (Fin n) →+ G), Function.Surjective φ ∧ φ.ker.IsNormalClosureFG
+
 /-- A group is finitely presented if it has a finite generating set such that the kernel
 of the induced map from the free group on that set is the normal closure of finitely many
 relations. -/
-@[mk_iff]
+@[mk_iff, to_additive existing]
 class Group.IsFinitelyPresented (G : Type*) [Group G] : Prop where
   out : ∃ (n : ℕ) (φ : FreeGroup (Fin n) →* G), Function.Surjective φ ∧ φ.ker.IsNormalClosureFG
 
 namespace Group.IsFinitelyPresented
 
 /-- Finitely presented groups are closed under isomorphism. -/
+@[to_additive /-- Finitely presented additive groups are closed under additive isomorphism. -/
+]
 theorem equiv (iso : G ≃* H) (h : IsFinitelyPresented G) : IsFinitelyPresented H := by
   obtain ⟨n, φ, hφsurj, hNC⟩ := h
   refine ⟨n, (iso : G →* H).comp φ, iso.surjective.comp hφsurj, ?_⟩
   rwa [MonoidHom.ker_mulEquiv_comp φ iso]
 
-/-- A free group (with a finite number of generators) is finitely presented. -/
-instance [Finite α] : Group.IsFinitelyPresented (FreeGroup α) := by
+/-- A free group with a finite number of generators is finitely presented. -/
+@[to_additive /-- A free additive group with a finite number of generators is finitely presented. -/
+]
+instance [Finite α] : IsFinitelyPresented (FreeGroup α) := by
   have ⟨n, _, f, hf_surj, hf_inj⟩ := Finite.exists_equiv_fin α
   refine ⟨n, FreeGroup.map f, FreeGroup.map_surjective hf_surj.surjective, ?_⟩
   · rw [(FreeGroup.map f).ker_eq_bot_iff.mpr (FreeGroup.map_injective hf_inj.injective)]
     exact Subgroup.IsNormalClosureFG.bot
 
+/-- `Multiplicative ℤ` is finitely presented. -/
 instance : IsFinitelyPresented (Multiplicative ℤ) :=
   equiv (FreeGroup.mulEquivIntOfUnique : FreeGroup Unit ≃* Multiplicative ℤ) inferInstance
 
+/-- ℤ is finitely presented -/
+instance : AddGroup.IsFinitelyPresented ℤ :=
+  AddGroup.IsFinitelyPresented.equiv
+    (FreeAddGroup.addEquivIntOfUnique : FreeAddGroup Unit ≃+ ℤ) inferInstance
+
 end Group.IsFinitelyPresented