Projects: Finitely Presented Groups

Stream: ItaLean 2025

[Lorenzo Luccioli]

This thread is dedicated to the Finitely Presented Groups project:

• Repository: ?
• Informal Manager: @Hang Lu Su
• Formal Manager: @Riccardo Brasca

[Hang Lu Su]

Repo: https://github.com/homeowmorphism/FinitelyPresentedGroups

[Valerio Proietti]

Hi, went to the repo but the proof we wrote today is not there? I can see is 2 sorrys and one unfinished lemma with ‘constructor’ as last line

[Riccardo Brasca]

I guess @Hang Lu Su forgot to push. There was definitely something in her computer

[Riccardo Brasca]

wait no, the definition is there. You have to do git pull (in VS Code click on the little circle in the bottom left part of the window)

[Riccardo Brasca]

Ah sorry, I misunderstood you message. She probably forgot to push

[Kevin Buzzard]

Looks like a good start! Is there a dream theorem you're working towards?

[Valerio Proietti]

Hang Lu Su mentioned the Reidemeister-Schreier Theorem

[Hang Lu Su]

@Valerio Thanks for the notice! I just pushed again and the latest changes should be in the repo now. Sorry about that.

The Reidemeister-Schreier theorem would be really cool to be able to make good progress on this week indeed :).

Edit: I should mention I wrote an introductory chapter on it in my thesis https://arxiv.org/abs/2512.07035 p. 169-177 in case someone finds this useful.

[Riccardo Brasca]

I don't know how difficult it is, but since it seems it is an algorithm that actually gives the presentation of the subgroup, the next step is probably to link our definition to docs#PresentedGroup

[Riccardo Brasca]

anyway since this is also the topic of the conference I am throwing the first sorry to aristotle

[Lawrence Wu (llllvvuu)]

I don't really know the math, but this is what I've cooked up so far:

open scoped Pointwise

def IsFinitelyPresented.{u} (G : Type u) [Group G] : Prop :=
  Nonempty ((ι : Type u) × (_ : Fintype ι) × (FinitePresentation G ι))

def ReidemeisterSchreierMethod.{u} {ι : Type u} [Fintype ι] {G : Type u} [Group G]
    (H : Subgroup G)
    (P : FinitePresentation G ι) -- G is presented by generators ι
    (T : Finset G) -- The transversal
    -- These are from `Subgroup.closure_mul_image_mul_eq_top`
    (hT : Subgroup.IsComplement H (T : Set G)) -- T is a right transversal
    -- TODO: should be Hg, not gH?
    (hT_covers : ⋃ g ∈ T, (g : G) • (H : Set G) = ⊤) -- T covers H
    (hT1 : (1 : G) ∈ T) -- 1 is in T
    -- Definition: T is a Schreier transversal if it is prefix-closed with respect to generators of P.
    -- TODO: we need some order relation to prevent cycles, i.e. t' < t.
    (hT_is_schreier : ∀ t ∈ T, t ≠ 1 → ∃ t' ∈ T, ∃ i : ι, t = t' * P.val i ∨ t = t' * (P.val i)⁻¹)
    : FinitePresentation H (T × ι) := by -- H is presented by T × ι
  sorry

theorem reidemeister_schreier {G : Type*} [Group G] (H : Subgroup G) [H.FiniteIndex]
    (hG : IsFinitelyPresented G) : IsFinitelyPresented H := by
  -- obtain a *Finset* *Schreier* right transversal somehow
  -- and then call ReidemeisterSchreierMethod
  sorry

[Valerio Proietti]

Hi, with some help from GPT, I added a new file (didn’t make a PR) which compares our definition and the notion of PresentedGroup already in Mathlib. It’s probably rough, but I hope it’s a start.

[Hang Lu Su]

I added the ReidemeisterSchreier.lean that combines the improvements that @Francesco Milizia and @Lawrence Wu (llllvvuu) made today, plus some edits.

In the end, I felt like it might be easier for now (given the timing of the presentation being tomorrow) to just offload the requirement of being a Schreier transversal as a "sorry".

[Lawrence Wu (llllvvuu)]

Indeed the design of IsSchreierTransversal seems tricky. It is possible that we would actually want a structure SchreierTransversal that contains not only the data T but some additional data parent which tells you exactly what the "parent" / prefix of each element is instead of just asserting that one exists. Otherwise, ReidemeisterSchreierMethod may have to use axiom of choice e.g. Exists.choose and hence be noncomputable.

An interesting design for the ordering thing could be to have T be a Fin n -> G instead of Finset G, then Fin n gives an ordering i.e. it could be asserted that parent has a lower index in Fin n.

[Lawrence Wu (llllvvuu)]

Aristotle did prove a version of the theorem yesterday: https://github.com/homeowmorphism/FinitelyPresentedGroups/pull/2

Maybe possible that it can also do it with the new definitions and prompted to make it computable as mentioned above

[Riccardo Brasca]

This is great! Did Aristotle find the proof by itself or did you help it?

[Lawrence Wu (llllvvuu)]

It formalized everything itself including the statement

[Hang Lu Su]

Hi everyone! I hope travel home went smoothly for those who attended the conference in-person.

I made a mathlib fork for this project. https://github.com/homeowmorphism/mathlib4

My intention is to upstream it to mathlib in small PRs, and I would appreciate guidance on how to go about it and on the credit conventions. (For context I'm new to the community, so extra guidance is very welcome!)

From what I can tell, there's a group of separate files with some overlaps and some different features, which need to be merged and polished together and separated into different PRs. Does the following rough plan seem reasonable from a maintainer/reviewer perspective?

1. add to, polish and submit the IsFinitelyPresented-related statements/proofs we developed with @Riccardo Brasca, since this appears minimally invasive.
   Edit: I'm currently working on this and the branch can be found here: https://github.com/leanprover-community/mathlib4/compare/master...homeowmorphism:mathlib4:FinitelyPresentedGroup

2. add Presentation and FinitePresentation we did with @Fabrizio Barroero , and then adjust so that PresentedGroup (a 2019 package we did not work on) and FinitelyPresentedGroup are groups obtained from a presentation.
   Edit: @Valerio Proietti is working on this, and his branch can be found here: https://github.com/leanprover-community/mathlib4/compare/master...jazzits:mathlib4:finitely-presented-groups

3. Work on the Reidemeister-Schreier method/theorem on a different branch. Many thanks to @Lawrence Wu (llllvvuu) for helping with this and the Aristotle workflow.

Credit questions:

Copyright: Who should I put for that? I'm not sure what that's supposed to do :sweat_smile:.

Authors: I added everyone who worked on this in alphabetic order in the header of the file I'm working on (I got the names from the Google Sheet). I was wondering if that's ok with everyone, or if anyone would like to be excluded? @Riccardo Brasca @Fabrizio Barroero @Francesco Milizia @Valerio @Lawrence Wu (llllvvuu) (I'm not sure what Stefano Francaviglia's username is so I didn't tag him.)

[Riccardo Brasca]

Starting with a small PR is surely a good idea. Put your name in the copyright header and everybody else as author. It a good idea to read the doc page before opening the PR, and don't hesitate to ask questions here!

[Valerio Proietti]

I made a PR addressing point 2 above. First time doing this so I hope I am doing things right, perhaps somebody knowledgeable can review it.

[Kevin Buzzard]

Can you post the PR number eg #12345 ?

[Riccardo Brasca]

Can you link the PR here? You can write # 12345 (without the space and with the correct number)

[Valerio Proietti]

Sorry, I meant I made a PR to Hang's repo, not to mathlib (I guess the one to mathlib should be much smaller)

[Hang Lu Su]

I think Valerio means this one: https://github.com/homeowmorphism/FinitelyPresentedGroups/pull/3.

[Riccardo Brasca]

@Hang Lu Su this is your repo, so it's really up to you :)

[Riccardo Brasca]

In my experience anything that compiles is fine for repository whose goal is to end up in mathlib. The mathlib PR process is already long enough, we probably don't want to have two reviews

[Valerio Proietti]

Okay, so I will try to extract something and make a PR to mathlib in the following days. Thanks

[Hang Lu Su]

Thanks @Valerio Proietti for the contribution! I'm currently working on PR 1 and this code looks pretty advanced for me, but I'll merge it as part of the project and I agree with you probably best if you PR it directly to mathlib since I'm probably not the reviewer needed here :sweat_smile: .

[Riccardo Brasca]

it's still fine to have one repo to point out to show what we want to do

[Hang Lu Su]

Is it ok to use classical for isFinitelyPresented_iff, defined as

lemma isFinitelyPresented_iff {G : Type*} [Group G] :
  IsFinitelyPresented G ↔ ∃ (S : Finset G) (f : FreeGroup S →* G),
  Function.Surjective f ∧ normalClosureIsFG (MonoidHom.ker f) := by

to get rid of the DecidableEq Gproblem when using Finset G? I was stuck and it was proposed by an LLM, but it seems strange since group element equality isn't actually decidable.

Or maybe Finset isn't the right thing to use for finitely presented groups for this reason?

Edit: I'm thinking of the context where we are using finitely presented groups algorithmically, which is common in geometric group theory.

[Bhavik Mehta]

Putting classical inside the proof is the usual pattern for this kind of thing, yeah

[Hang Lu Su]

I double-checked with Group.FG and it looks like it's using Set and S.Finite

theorem Group.fg_iff : Group.FG G ↔ ∃ S : Set G, Subgroup.closure S = (⊤ : Subgroup G) ∧ S.Finite :=

Source: https://github.com/leanprover-community/mathlib4/blob/8fc0483a875e84b83c6cdb6f5c124bcbb3530370/Mathlib/GroupTheory/Finiteness.lean#L376-L378

it seems to get rid of the DecidableEq problem as well, but not sure if there's actually a difference philosophically?

[Hang Lu Su]

Nevermind, it also uses Finset right after :sweat_smile:, so seems like both are fine. It doesn't seem to use classical to show the proof though.

theorem Group.fg_iff' :
    Group.FG G ↔ ∃ (n : _) (S : Finset G), S.card = n ∧ Subgroup.closure (S : Set G) = ⊤ :=
  Group.fg_def.trans ⟨fun ⟨S, hS⟩ => ⟨S.card, S, rfl, hS⟩, fun ⟨_n, S, _hn, hS⟩ => ⟨S, hS⟩⟩

[Kevin Buzzard]

Hang Lu Su said:

lemma isFinitelyPresented_iff {G : Type*} [Group G] :
  IsFinitelyPresented G ↔ ∃ (S : Finset G) (f : FreeGroup S →* G),
  Function.Surjective f ∧ normalClosureIsFG (MonoidHom.ker f) := by

Note that the fact that $S$ is a finite subset of $G$ is completely spurious here: $f$ is an arbitrary function, so $S$ may as well be an arbitrary finite type here (and you should change it to a finite type) rather than a finite subset of $G$ being used in a way which is unrelated to the inclusion $S\subseteq G$.

[Kevin Buzzard]

I don't know if you mean for $f$ to be the function induced by the inclusion $S\subseteq G$ but that's not what the code says.

[Valerio Proietti]

Hi, so I made the PR to mathlib. It is #33233. As I said, first time doing this so high chance I did something silly. I'd appreciate any guidance.

[Valerio Proietti]

(I can already see one check has failed, and github tells me it's because I should put the word "module" at the beginning?)

[Riccardo Brasca]

Just start with

public import Mathlib.GroupTheory.Presentation
public import Mathlib.GroupTheory.Finiteness

/-!
# Finitely presented groups
...
-/

@[expose] public section

namespace Group

[Riccardo Brasca]

(we are in a transition period where mathlib and projects depending on mathlib behave differently)

[Valerio Proietti]

Ok, I got the green check mark now!

[Hang Lu Su]

Kevin Buzzard said:

Hang Lu Su said:

lemma isFinitelyPresented_iff {G : Type*} [Group G] :
  IsFinitelyPresented G ↔ ∃ (S : Finset G) (f : FreeGroup S →* G),
  Function.Surjective f ∧ normalClosureIsFG (MonoidHom.ker f) := by

Note that the fact that $S$ is a finite subset of $G$ is completely spurious here: $f$ is an arbitrary function, so $S$ may as well be an arbitrary finite type here (and you should change it to a finite type) rather than a finite subset of $G$ being used in a way which is unrelated to the inclusion $S\subseteq G$.

I think the context for this (if I'm understanding correctly) is that we have already defined IsFinitelyPresented there existing a surjective function from a FreeGroup on some arbitrary set of cardinality n to G such that the kernel has a finitely generated normal closure, and the isFinitelyPresented_iff lemma is there to offer an alternative to the potential user in case they're working with a Finset of G. It's modeled after @Riccardo Brasca 's code for Group.FG https://github.com/leanprover-community/mathlib4/blob/8fc0483a875e84b83c6cdb6f5c124bcbb3530370/Mathlib/GroupTheory/Finiteness.lean#L376-L378, but perhaps in the context of FinitelyPresentedGroup there is a way to do this differently that would be less spurious? I've included the code below for full context.

open Subgroup

def normalClosureIsFG {G : Type*} [Group G] (H : Subgroup G) : Prop :=
  ∃ S : Finset G, Subgroup.normalClosure S = H

class IsFinitelyPresented (G : Type*) [Group G] : Prop where
  out : ∃ (n : ℕ) (f : (FreeGroup (Fin n)) →* G),
    Function.Surjective f ∧ normalClosureIsFG (MonoidHom.ker f)

lemma isFinitelyPresented_iff_finset {G : Type*} [Group G] :
  IsFinitelyPresented G ↔ ∃ (S : Finset G) (f : FreeGroup S →* G),
  Function.Surjective f ∧ normalClosureIsFG (MonoidHom.ker f) := by
sorry

If I remember correctly, this is part of why @Valerio Proietti championed doing this in terms of presentations (which would indeed be more general), but I wasn't sure about the implementation tradeoffs to mathlib.

Edit 1: accidentally copy-pasted the wrong isFinitelyPresented_iff statement in the full context as I had replaced it with Set and Set.Finite in my own editor. To avoid future confusion, I've changed the old function name to isFinitelyPresented_iff_finset as it appears in my editor now.

Edit 2: I think I'm starting to see the point more clearly, so let me say it in my own words: we want to avoid using concrete elements of G as generators since they live in the FreeGroup lift, and so Fintype provides the correct level of abstraction to do that, whereas Finset G is taking generators of G, using them to generate the FreeGroup lift and then sending them back using the quotient map, which does indeed seem spurious. I've made the change from Finset to Fintype in my code as Kevin suggested in my fork. The branch can be found here: https://github.com/leanprover-community/mathlib4/compare/master...homeowmorphism:mathlib4:FinitelyPresentedGroup.

[Hang Lu Su]

I think perhaps I'm missing some context to have an intuition for what's best to do and it's part of why I'm having trouble figuring out what needs to be done to add a good FinitelyPresentedGroupimplementation to mathlib. Maybe someone more senior could weight in on this?

[Valerio Proietti]

@Hang Lu Su Perhaps it's worth waiting to see what happens to my PR? The PR also adds a file Mathlib/GroupTheory/FinitelyPresented.lean which defines the notion more or less based off what Francesco had started writing during ItaLean. The feedback we get there might clear up your doubts too.

[Riccardo Brasca]

I am busy with family/Christmas things these days, but I may have some time to have a look tomorrow

[Hang Lu Su]

No rush on my end! I'll be busy with Christmas things as well. And thanks for the help with all this.

[Francesco Milizia]

Thanks Valerio for your work! I will also have a look when I have time. I wish a good break to you all

[Hang Lu Su]

Hey @Valerio Proietti, I came back to check on the updates for your PR and noticed that your latest commit fin n approach has been significantly overlapping with PR 1 while we had previously agreed (both in DMs and implicitly here) I'd be doing point 1 while you do 2?

This is my branch: https://github.com/leanprover-community/mathlib4/compare/master...homeowmorphism:mathlib4:FinitelyPresentedGroup

And this is your latest commit: https://github.com/leanprover-community/mathlib4/pull/33233/commits/a1a99f5d04a5e08e065b43f2d6cf7307837c004c

I’d like to keep point 1 as the part I'm in charge of and complete since this is a beginner-friendly mathlib project I proposed and want to learn from. Maybe my progress seems slow, but I've been spending a lot of time reading the docs and trying to understand what I'm doing as a first-timer. It would help a lot if you could focus on point 2 (or leave feedback on my code) rather than implementing point 1 in parallel.

This might be a misunderstanding, but I just wanted to make my intentions clear.

[Valerio Proietti]

@Hang Lu Su this is completely fine, I'm sorry I never meant to "steal your thunder". Following a request to allow the group and the generating set to live in different universes, I made some other changes that led me to define some things wrong, and so before stopping with my edits I wanted to push one last commit to fix those, and to check whether the definition of "finite presentation" would work well with "finitely presented group". In any case, I am not planning any other edits now, and I absolutely don't mind if the progress is slow, so we can coordinate better from now on.

[Hang Lu Su]

Thanks for the clarification Valerio. I can see how that happened, and happy to move forward and better coordinate in the future.

I think I could have been clearer about my ideas on how to do this. For the FinitelyPresentedGroup vs FinitePresentation files, I was thinking something along the lines of what GAP has done, where they are two separate things can be bridged together:

FpGroups: https://docs.gap-system.org/doc/ref/chap47.html
Presentations: https://docs.gap-system.org/doc/ref/chap48.html

Not sure if that would be the best way to do it for mathlib and happy to get feedback on this, but I figured I should put the idea out there so that we can be on the same page.

Anyhow, I agree with your proposed coordination plans and let's wait a bit for me to finish working on Part 1 so we can coordinate the next step together. Thanks for your patience and understanding!

[Hang Lu Su]

Hi everyone!

I'm starting to feel stuck so I thought I'd give an update. Essentially, I took @Kevin Buzzard feedback and rewrote the isFinitelyPresented_iff lemma using a Fintype (and Type*). (I followed @Riccardo Brasca 's advice to throw it into Aristotle, then rewrote it to be prettier once I understood what was going on). The full progress can be found here but the relevant code so far is this:

import Mathlib

/-- The kernel of a homomorphism composed with an isomorphism is equal to the kernel of
the homomorphism mapped by the inverse isomorphism. -/
-- TODO not sure if this is the right abstraction / right name for this.
@[simp]
lemma MonoidHom.ker_comp_mulEquiv {G H K : Type*} [Group G] [Group H] [Group K]
    (f : H →* K) (e : G ≃* H) : (f.comp e).ker = (Subgroup.map (e.symm.toMonoidHom) f.ker) := by
  rw [← MonoidHom.comap_ker, Subgroup.comap_equiv_eq_map_symm]
  rfl

def FinitelyPresentedGroup (n : ℕ) (rels : Set (FreeGroup (Fin n))) (_h : rels.Finite) : Type :=
  FreeGroup (Fin n) ⧸ Subgroup.normalClosure (rels : Set (FreeGroup (Fin n)))

open Subgroup

/-- Definition of subgroup that is given by the normal closure of finitely many elements. -/
def IsNormalClosureFG {G : Type*} [Group G] (H : Subgroup G) : Prop :=
  ∃ S : Set G, S.Finite ∧ Subgroup.normalClosure S = H

/-- The above property is invariant under surjective homomorphism. -/
lemma IsNormalClosureFG.map {G H : Type*} [Group G] [Group H]
  (f : G →* H) (hf : Function.Surjective f) (K : Subgroup G) (hK : IsNormalClosureFG K)
  : IsNormalClosureFG (K.map f) := by
  obtain ⟨ S, hSfinite, hSclosure ⟩ := hK
  use f '' S
  constructor
  · exact hSfinite.image _
  · rw [ ← hSclosure, Subgroup.map_normalClosure _ _ hf]

/-- A finitely presented group is given by a surjective homomorphism from a free group on n
elements whose normal closure of its kernel is finitely generated. -/
class IsFinitelyPresented (G : Type*) [Group G] : Prop where
  out : ∃ (n : ℕ) (f : (FreeGroup (Fin n)) →* G),
    Function.Surjective f ∧ IsNormalClosureFG (MonoidHom.ker f)

-- TODO calls to IsNormalClosureFG.map could be simplified? Like maybe using the iso functions.
  -- seems like we apply a lot of `MonoidHom.ker_comp_mulEquiv + IsNormalClosureFG.map`.
lemma isFinitelyPresented_iff_fintype {G : Type*} [Group G] :
    IsFinitelyPresented G ↔ ∃ (α : Type*) (_ : Fintype α) (f : FreeGroup α →* G),
    Function.Surjective f ∧ IsNormalClosureFG (f.ker) := by
  constructor
  · intro ⟨n, f, hfsurj, hfker⟩
    let iso : FreeGroup (ULift (Fin n)) ≃* FreeGroup (Fin n) :=
      FreeGroup.freeGroupCongr Equiv.ulift
    refine ⟨ULift (Fin n), inferInstance, f.comp iso, hfsurj.comp iso.surjective, ?_⟩
    simp only [MonoidHom.ker_comp_mulEquiv]
    exact IsNormalClosureFG.map iso.symm.toMonoidHom iso.symm.surjective f.ker hfker
  · intro ⟨α, _, f, hfsurj, hfker⟩
    let iso : FreeGroup (Fin (Fintype.card α)) ≃* FreeGroup α :=
      FreeGroup.freeGroupCongr (Fintype.equivFin α).symm
    refine ⟨Fintype.card α, f.comp iso, hfsurj.comp iso.surjective, ?_⟩
    simp only [MonoidHom.ker_comp_mulEquiv]
    exact IsNormalClosureFG.map iso.symm.toMonoidHom iso.symm.surjective f.ker hfker

I wanted to recover IsFinitelyPresented is an instance of Group.FG and to do so, we originally had to use the fact that an FG group admits a surjective homorphism from a FreeGroup on a finite type. Originally, I was using Group.fg_iff_exists_freeGroup_hom_surjective, but this uses that the surjection is from FreeGroup S where S: Set G which took me back in the "spurious" direction of showing isFinitelyPresented_iff using a surjection FreeGroup S where S: Set G, so I wrote two versions using Fintype which seems to avoid this problem. The difference between version 1 and 2 is that α : Type and α : Type*.

theorem Group.fg_iff_exists_freeGroup_hom_surjective_fintype_ARISTOTLE1 {G : Type*} [Group G] :
    Group.FG G ↔ ∃ (α : Type) (_ : Fintype α) (φ : FreeGroup α →* G), Function.Surjective φ := by
sorry

theorem Group.fg_iff_exists_freeGroup_hom_surjective_fintype_ARISTOTLE2 {G : Type*} [Group G] :
    Group.FG G ↔ ∃ (α : Type*) (_ : Fintype α) (φ : FreeGroup α →* G), Function.Surjective φ := by
sorry

Aristotle was able to find proofs for both of them, but the thing I'm stuck on is that while this compiles

instance {G : Type*} [Group G] [h : IsFinitelyPresented G] : Group.FG G := by
  rw [Group.fg_iff_exists_freeGroup_hom_surjective_fintype_ARISTOTLE1]
  rw [isFinitelyPresented_iff_fintype] at h
  obtain ⟨S, hSfinite, f, hfsurj, hkernel⟩ := h
  use S, hSfinite, f, hfsurj

the ARISTOTLE2 version gives me the following error message:

declaration `instFGOfIsFinitelyPresented` contains universe level metavariables at the expression
  ∃ (α : Type ?u.29684),
    ∃ (x : Fintype.{?u.29684} α), ∃ (φ : MonoidHom.{?u.29684, u_1} (FreeGroup.{?u.29684} α) G), Function.Surjective ⇑φ
in the declaration body
  fun {G} [Group G] [h : IsFinitelyPresented G] ↦
    Eq.mpr
      (id
        (congrArg (fun _a ↦ _a)
          (propext Group.fg_iff_exists_freeGroup_hom_surjective_fintype_ARISTOTLE2.{u_1, ?u.29684})))
      (Exists.casesOn (Eq.mp (congrArg (fun _a ↦ _a) (propext isFinitelyPresented_iff_fintype.{u_1, ?u.29684})) h)
        fun (S : Type ?u.29684)
          (h :
            ∃ (x : Fintype.{?u.29684} S),
              ∃ (f : MonoidHom.{?u.29684, u_1} (FreeGroup.{?u.29684} S) G),
                Function.Surjective ⇑f ∧ IsNormalClosureFG.{?u.29684} (MonoidHom.ker.{?u.29684, u_1} f)) ↦
        Exists.casesOn h
          fun (hSfinite : Fintype.{?u.29684} S)
            (h :
              ∃ (f : MonoidHom.{?u.29684, u_1} (FreeGroup.{?u.29684} S) G),
                Function.Surjective ⇑f ∧ IsNormalClosureFG.{?u.29684} (MonoidHom.ker.{?u.29684, u_1} f)) ↦
          Exists.casesOn h
            fun (f : MonoidHom.{?u.29684, u_1} (FreeGroup.{?u.29684} S) G)
              (h : Function.Surjective ⇑f ∧ IsNormalClosureFG.{?u.29684} (MonoidHom.ker.{?u.29684, u_1} f)) ↦
            And.casesOn h
              fun (hfsurj : Function.Surjective ⇑f)
                (hkernel : IsNormalClosureFG.{?u.29684} (MonoidHom.ker.{?u.29684, u_1} f)) ↦
              Exists.intro S (Exists.intro hSfinite (Exists.intro f hfsurj)))

Overall, I think the main thing now that's slowly me down is struggling on how to understand the universe levels and how Lean infers from context which makes it hard to work with Type* (edit: not Fintype). (I first wrote isFinitelyPresented_iff_fintype with \a: Type as well and found it pretty painful to figure out how to adapt it to \a: Type* with ULift).

If anyone has advice or references they could point me towards dealing with the above problem better that would be greatly appreciated!

Incidentally, if anyone would like to give me some feedback my approach, refactoring, and whether the coding style matches that of mathlib, that would be greatly appreciated also.

[Kevin Buzzard]

Yikes that's a terrifying error message :-)

I think I would be tempted to write ∃ (α : Type) (_ : Finite α) (f : FreeGroup α →* G). It's kind of scary to quantify over all universes, and typically I avoid Fintype when I can get away with Finite although maybe Fintype is easier, I'm not sure. Fintype X basically means "a fixed bijection X <-> {1,2,...,n}" (in particular it's data) whereas Finite X just means "there exists a bijection...".

[Kevin Buzzard]

It's much easier for someone to give feedback on code if they can get the code compiling. Your code does not compile as it stands without other stuff before it, so people have to read it, they can't play with it, which is much more fun. Are you able to post the code which you want people to look at as a #mwe ?

[Hang Lu Su]

Oops, seems like I forgot to include the import Mathlib statement at the top. I edited the code to include it. When I copy-paste it now it should compile in the editor, but please let me know if it doesn't. (The later code snippets can just be pasted sequentially).

Ok, understood for the Finite vs Fintype. The reason I chose α : Type* (edit: not Fintype) was for compatibility as PresentedGroup is defined using \a: Type*, but maybe that's not quite the right way to think about it?

variable {α : Type*}

/-- Given a set of relations, `rels`, over a type `α`, `PresentedGroup` constructs the group with
generators `x : α` and relations `rels` as a quotient of `FreeGroup α`. -/
def PresentedGroup (rels : Set (FreeGroup α)) :=
  FreeGroup α ⧸ Subgroup.normalClosure rels
```

[Hang Lu Su]

I just realized that I was saying I was struggling to work with Fintype when really I meant I was struggling to work with Type* and I think that was probably confusing. I've fixed the above comments for clarity.

[Valerio Proietti]

@Hang Lu Su I don't know if this helps, but I can get this to compile (I am using an explicit universe in the ARISTOTLE2 theorem). The last theorem is an alternative shorter approach but maybe not what you want?

module

public import Mathlib.GroupTheory.Presentation
public import Mathlib.GroupTheory.Finiteness

@[expose] public section

namespace Group

universe u

variable {G : Type*} [Group G]

/-- The kernel of a homomorphism composed with an isomorphism is equal to the kernel of
the homomorphism mapped by the inverse isomorphism. -/
-- TODO not sure if this is the right abstraction / right name for this.
@[simp]
lemma MonoidHom.ker_comp_mulEquiv {G H K : Type*} [Group G] [Group H] [Group K]
    (f : H →* K) (e : G ≃* H) : (f.comp e).ker = (Subgroup.map (e.symm.toMonoidHom) f.ker) := by
  rw [← MonoidHom.comap_ker, Subgroup.comap_equiv_eq_map_symm]
  rfl

/-- Definition of subgroup that is given by the normal closure of finitely many elements. -/
def IsNormalClosureFG {G : Type*} [Group G] (H : Subgroup G) : Prop :=
  ∃ S : Set G, S.Finite ∧ Subgroup.normalClosure S = H

/-- The above property is invariant under surjective homomorphism. -/
lemma IsNormalClosureFG.map {G H : Type*} [Group G] [Group H]
  (f : G →* H) (hf : Function.Surjective f) (K : Subgroup G) (hK : IsNormalClosureFG K)
  : IsNormalClosureFG (K.map f) := by
  obtain ⟨ S, hSfinite, hSclosure ⟩ := hK
  use f '' S
  constructor
  · exact hSfinite.image _
  · rw [ ← hSclosure, Subgroup.map_normalClosure _ _ hf]

/-- A finitely presented group is given by a surjective homomorphism from a free group on n
elements whose normal closure of its kernel is finitely generated. -/
class IsFinitelyPresented (G : Type*) [Group G] : Prop where
  out : ∃ (n : ℕ) (f : (FreeGroup (Fin n)) →* G),
    Function.Surjective f ∧ IsNormalClosureFG (MonoidHom.ker f)

-- TODO calls to IsNormalClosureFG.map could be simplified? Like maybe using the iso functions.
  -- seems like we apply a lot of `MonoidHom.ker_comp_mulEquiv + IsNormalClosureFG.map`.
lemma isFinitelyPresented_iff_fintype {G : Type*} [Group G] :
    IsFinitelyPresented G ↔ ∃ (α : Type*) (_ : Fintype α) (f : FreeGroup α →* G),
    Function.Surjective f ∧ IsNormalClosureFG (f.ker) := by
  constructor
  · intro ⟨n, f, hfsurj, hfker⟩
    let iso : FreeGroup (ULift (Fin n)) ≃* FreeGroup (Fin n) :=
      FreeGroup.freeGroupCongr Equiv.ulift
    refine ⟨ULift (Fin n), inferInstance, f.comp iso, hfsurj.comp iso.surjective, ?_⟩
    simp only [MonoidHom.ker_comp_mulEquiv]
    exact IsNormalClosureFG.map iso.symm.toMonoidHom iso.symm.surjective f.ker hfker
  · intro ⟨α, _, f, hfsurj, hfker⟩
    let iso : FreeGroup (Fin (Fintype.card α)) ≃* FreeGroup α :=
      FreeGroup.freeGroupCongr (Fintype.equivFin α).symm
    refine ⟨Fintype.card α, f.comp iso, hfsurj.comp iso.surjective, ?_⟩
    simp only [MonoidHom.ker_comp_mulEquiv]
    exact IsNormalClosureFG.map iso.symm.toMonoidHom iso.symm.surjective f.ker hfker

theorem fg_iff_exists_freeGroup_hom_surjective_fintype_ARISTOTLE2 {G : Type u} [Group G] :
    Group.FG G ↔ ∃ (α : Type u) (_ : Fintype α) (φ : FreeGroup α →* G), Function.Surjective φ := by
  constructor
  · intro h
    rcases
        (Group.fg_iff_exists_freeGroup_hom_surjective (G := G)).1 h with
      ⟨S, hS, φ, hφ⟩
    haveI : Fintype S := hS.fintype
    refine ⟨Subtype fun x => x ∈ S, inferInstance, ?_, ?_⟩
    · simpa using φ
    · simpa using hφ
  · rintro ⟨α, hα, φ, hφ⟩
    let val : α → G := fun i => φ (FreeGroup.of i)
    have hlift : FreeGroup.lift val = φ := by ext i; simp [val]
    have hsurj' : Function.Surjective (FreeGroup.lift val) := by
      simpa [hlift] using hφ
    have hcl : Subgroup.closure (Set.range val) = ⊤ := by
      simpa [FreeGroup.range_lift_eq_closure] using
        (MonoidHom.range_eq_top).2 hsurj'
    refine (Group.fg_iff).2 ?_
    refine ⟨Set.range val, ?_, ?_⟩
    · simpa using hcl
    · simpa using (Set.finite_range val)

instance {G : Type*} [Group G] [h : IsFinitelyPresented G] : Group.FG G := by
  rw [Group.fg_iff_exists_freeGroup_hom_surjective_fintype_ARISTOTLE2]
  rw [isFinitelyPresented_iff_fintype] at h
  obtain ⟨S, hSfinite, f, hfsurj, hkernel⟩ := h
  use S, hSfinite, f, hfsurj

theorem fg_of_finitelyPresented' :
    Group.IsFinitelyPresented (G := G) → Group.FG G := by
  rintro ⟨n, f, hsurj, -⟩
  let val : Fin n → G := fun i => f (FreeGroup.of i)
  have hlift : FreeGroup.lift val = f := by ext i; simp [val]
  have hsurj' : Function.Surjective (FreeGroup.lift val) := by
    simpa [hlift] using hsurj
  have hcl : Subgroup.closure (Set.range val) = ⊤ := by
    simpa [FreeGroup.range_lift_eq_closure] using
      (MonoidHom.range_eq_top).2 hsurj'
  refine (Group.fg_iff).2 ?_
  refine ⟨Set.range val, ?_, ?_⟩
  · simpa using hcl
  · simpa using (Set.finite_range val)

end Group

[Hang Lu Su]

Thanks @Valerio Proietti !

Do you mind explaining why G and \a should live in the same type universe?
(Edit: is it because FreeGroup \a is Type u and so is G its quotient?)

instance {G : Type*} [Group G] [h : IsFinitelyPresented G] could totally be made simpler! Aristotle had even come up with a more elementary proof, but I figured it would be a good test of my already written lemmas if they work as intended.

[Hang Lu Su]

Ok, I think I answered by own question above! Let me spell out the reasoning because this is new to me:

Starting with variable {α : Type u}, we have:

• FreeGroup (α : Type u) : Type u from #FreeGroup
• The quotient can be traced back to Quot {\b : Sort v} (r : \b → \b → Prop) : Sort v. from #Quot
• Therefore, since G = FreeGroup α / rels where rels are a Set: (α : Type u) : Type u (#Set), G: Type u.

So yeah actually I think this helps a lot @Valerio Proietti ! I think I now have a better idea on how to reason about types :grinning_face_with_smiling_eyes: .

[Hang Lu Su]

Ok, maybe I'm overthinking it, but now I'm wondering if what I wrote above really stands when you have isomorphism instead of equality? As in, if G ≃* FreeGroup α / rels, thenMulEquiv : {M : Type u} → {N : Type v} → [Mul M] → [Mul N] → Type (max u v) so α and G are allowed to be from different type universes.

The reason I'm wondering this is that if I have the following MWE.

We have IsFinitelyPresented group as an instance of IsPresentedGroup which I define as admitting an isomorphism from G to a PresentedGroup, but such an isomorphism doesn't force \a to be of the same type as G.

If I'm thinking of the iffstatements above now as isomorphisms from FreeGroup / \a / rels to G instead of straight equalities (which seems more flexible and general), it's not clear to me that \a and G have to live in the same universe?

However, in addition to the above iff statements breaking the (very wip) proof of instance {G : Type*} [Group G] [h : IsFinitelyPresented G] : IsPresentedGroup G breaks if I write `G: Type* and \a: Type* instead of forcing them to live in the same universe (there's probably a way around that, but just wanted to point it out).

import Mathlib

universe u

@[simp]
lemma MonoidHom.ker_comp_mulEquiv {G H K : Type*} [Group G] [Group H] [Group K]
    (f : H →* K) (e : G ≃* H) : (f.comp e).ker = (Subgroup.map (e.symm.toMonoidHom) f.ker) := by
  rw [← MonoidHom.comap_ker, Subgroup.comap_equiv_eq_map_symm]
  rfl

open Subgroup

/-- Definition of subgroup that is given by the normal closure of finitely many elements. -/
def IsNormalClosureFG {G : Type*} [Group G] (H : Subgroup G) : Prop :=
  ∃ S : Set G, S.Finite ∧ Subgroup.normalClosure S = H

lemma IsNormalClosureFG.invariant_surj_hom {G H : Type*} [Group G] [Group H]
  (f : G →* H) (hf : Function.Surjective f) (K : Subgroup G) (hK : IsNormalClosureFG K)
  : IsNormalClosureFG (K.map f) := by
  obtain ⟨ S, hSfinite, hSclosure ⟩ := hK
  use f '' S
  constructor
  · exact hSfinite.image _
  · rw [ ← hSclosure, Subgroup.map_normalClosure _ _ hf]

class IsFinitelyPresented (G : Type*) [Group G] : Prop where
  out : ∃ (n : ℕ) (f : (FreeGroup (Fin n)) →* G),
    Function.Surjective f ∧ IsNormalClosureFG (MonoidHom.ker f)

lemma isFinitelyPresented_iff_finite {G : Type u} [Group G] :
    IsFinitelyPresented G ↔ ∃ (α : Type u) (_ : Finite α) (f : FreeGroup α →* G),
    Function.Surjective f ∧ IsNormalClosureFG (f.ker) := by
    constructor
    · intro ⟨n, f, hfsurj, hfker⟩
      let iso : FreeGroup (ULift (Fin n)) ≃* FreeGroup (Fin n) :=
      FreeGroup.freeGroupCongr Equiv.ulift
      refine ⟨ULift (Fin n), inferInstance, f.comp iso, hfsurj.comp iso.surjective, ?_⟩
      simp only [MonoidHom.ker_comp_mulEquiv]
      exact IsNormalClosureFG.invariant_surj_hom
        iso.symm.toMonoidHom iso.symm.surjective f.ker hfker
    · intro ⟨α, _, f, hfsurj, hfker⟩
      let n := Nat.card α
      let iso : FreeGroup (Fin (Nat.card α)) ≃* FreeGroup α :=
        FreeGroup.freeGroupCongr (Finite.equivFin α).symm
      refine ⟨Nat.card α, f.comp iso, hfsurj.comp iso.surjective, ?_⟩
      simp only [MonoidHom.ker_comp_mulEquiv]
      exact IsNormalClosureFG.invariant_surj_hom
        iso.symm.toMonoidHom iso.symm.surjective f.ker hfker

def IsPresentedGroup (G : Type u) [Group G] : Prop :=
  ∃ (α : Type u) (rels : Set (FreeGroup α)), Nonempty (G ≃* PresentedGroup rels)

instance {G : Type*} [Group G] [h : IsFinitelyPresented G] : IsPresentedGroup G := by
  rw [isFinitelyPresented_iff_finite] at h
  obtain ⟨α, _, f, hfsurj, hfkernel⟩ := h
  obtain ⟨S, hSfinite, hSclosure⟩ := hfkernel
  unfold IsPresentedGroup
  use α, S
  let iso := (QuotientGroup.quotientKerEquivOfSurjective f hfsurj).symm
  refine ⟨?_⟩
  unfold PresentedGroup
  let hSclosure_equiv := QuotientGroup.quotientMulEquivOfEq hSclosure
  let iso' := iso.trans hSclosure_equiv.symm
  exact iso'

TLDR: I'm still unsure as to what should be left flexible in terms of universe levels vs what should be forced when defining isomorphism statements for FinitelyPresentedGroups.

It seems like #Group.FG deals with this by defining everything inside the group itself, such as the statement Group.fg_iff_exists_freeGroup_hom_surjective using a surjection FreeGroup S where S: Set G, whereas #PresentedGroup defines a group in terms of a FreeGroup \a where \a : Type* and I'm not sure where FinitelyPresentedGroup.lean should sit in terms of flexibility of universe levels. Both have that the FreeGroup generators are of the same type as the group G though.

[Valerio Proietti]

I agree with you that isomorphism (unlike equality) should not force the same universe (this goes against my code where I did fix the same universe, however that was just so that it compiles). In these cases, as far as I understand (which is not much), it would be preferable to find an alternative proof which does not require fixing universes. In the specific case of proving FP implies FG, I suppose the theorem fg_of_finitelyPresented' would do the job. I will also note that, in the case of FP groups, because of the finiteness assumption, one can always have generators be of Type 0, so that overall the different universes level don't matter too much in this case.
What I mean is one can prove

variable {α : Type*} (rels : Set (FreeGroup α))

/-- If `α` and `rels` are finite, then `PresentedGroup rels` is finitely presented. -/
theorem finitelyPresented_of_finite
    [Finite α] (hrels : rels.Finite) :
    Group.IsFinitelyPresented (G := PresentedGroup rels) := by
  -- Choose `Fin n` equivalent to `α`.
  rcases Finite.exists_equiv_fin α with ⟨n, ⟨eα⟩⟩
  let e : Fin n ≃ α := eα.symm
  let E : FreeGroup (Fin n) ≃* FreeGroup α := FreeGroup.freeGroupCongr e
-- Continues...

So you can have α : Type u and Fin n : Type 0 and still form α ≃ Fin n

[Hang Lu Su]

In these cases, as far as I understand (which is not much), it would be preferable to find an alternative proof which does not require fixing universes. In the specific case of proving FP implies FG, I suppose the theorem fg_of_finitelyPresented' would do the job.

It's a nice proof! My concern is that if the current statements can't be used to prove simple desired facts about FP groups, then there is a problem with the statements which need to be fixed before PR'ing to mathlib since other people might run into the same issues in the future, which is why I prefer to use them to show other simple statements and see if something breaks.

I will also note that, in the case of FP groups, because of the finiteness assumption, one can always have generators be of Type 0, so that overall the different universes level don't matter too much in this case.

Mhm, this is going in line with what Kevin was saying about using \a: Type. I think I'll go with this for now since it seems like it might fix the problem in a way that makes the statements more robust to use.

Thanks a lot for the discussion @Valerio Proietti! This really helped me get a better sense of what to do next.

[Bhavik Mehta]

I agree with Kevin that the universe polymorphism was the scary bit here; essentially the error is happening because in

lemma isFinitelyPresented_iff_fintype {G : Type*} [Group G] :
    IsFinitelyPresented G ↔ ∃ (α : Type*) (_ : Fintype α) (f : FreeGroup α →* G)

when you try to apply this lemma from the left to right, Lean will know what G should be and therefore which universe it should be in. But it doesn't know what the universe variable corresponding to α should be, so you get the error "contains universe level metavariables"

[Kevin Buzzard]

Perhaps the simplest fix for this is just ...↔ ∃ (n : \N) (f : FreeGroup (Fin n) →* G)

[Hang Lu Su]

Hi everyone! Thanks for the help. I've made some significant changes to the code since which I believe makes everything feel "smoother" and at the same time is more in line with what @Valerio Proietti and I were thinking mathematically. Of course, feel free to chime in if you have feedback / reservations on this approach.

Here's how the code looks like now MWE, also found here: https://github.com/leanprover-community/mathlib4/compare/master...homeowmorphism:mathlib4:FinitelyPresentedGroup

Basically, I decided to define a FinitelyPresentedGroup using the existing PresentedGroup with finiteness conditions on \a: Type and the relations. Then, a group IsFinitelyPresented and IsPresented if you can find an isomorphism to the appropriate (Finitely)Presented group. (This is the literal definition of (finitely) presented group I'm used to in geometric group theory).

def FinitelyPresentedGroup {α : Type} [Finite α] (rels : Set (FreeGroup α))
(_h : rels.Finite) := PresentedGroup (rels)

class IsFinitelyPresented (G : Type*) [Group G] : Prop where
  out: ∃ (α : Type) (_: Finite α) (rels : Set (FreeGroup α)) (h : rels.Finite),
  Nonempty (G ≃* (FinitelyPresentedGroup rels h))

def IsPresented (G : Type*) [Group G] : Prop :=
 ∃ (α : Type*) (rels : Set (FreeGroup α)), Nonempty (G ≃* PresentedGroup rels)

Using this, you can recover that a group that IsFinitelyPresented is also a Group.FG, and also IsFinitelyPresented is IsPresented via using a ULift on \a since PresentedGroup was defined using \a: Type* instead of \a: Type. #PresentedGroup

instance {G : Type*} [Group G] [h : IsFinitelyPresented G] : Group.FG G := by
  rw [Group.fg_iff_exists_freeGroup_hom_surjective_finite]
  obtain ⟨α, hα, rels, hrels, ⟨iso⟩⟩ := h
  unfold FinitelyPresentedGroup at iso
  unfold PresentedGroup at iso
  use α, hα
  -- TODO probably a nicer way to do this.
  let iso' := iso.symm.toMonoidHom.comp (QuotientGroup.mk' (Subgroup.normalClosure rels))
  use iso'
  simpa [iso'] using
    (Function.Surjective.comp iso.symm.surjective (QuotientGroup.mk'_surjective (Subgroup.normalClosure rels)))

instance {G : Type*} [Group G] [h : IsFinitelyPresented G] : IsPresented G := by
  obtain ⟨α, hα, rels, hrels, ⟨iso⟩⟩ := h
  use ULift α, Set.image (FreeGroup.map ULift.up) rels
  let e : ULift α ≃ α := Equiv.ulift
  refine ⟨iso.trans (PresentedGroup.equivPresentedGroup rels e.symm)⟩

Finally, it was easy to recover the lemma that a PresentedGroup IsFinitelyPresented, which was the last lemma that we wrote with @Riccardo Brasca during the workshop!

lemma FPgroup {α : Type} [Finite α] (rels : Set (FreeGroup α)) (h : rels.Finite) :
  IsFinitelyPresented (FinitelyPresentedGroup rels h) := by
  refine ⟨α, inferInstance, rels, h, ?_⟩
  exact ⟨MulEquiv.refl _⟩

Overall, this code felt a lot easier to write and work with due to the notion of isomorphism being natural here (although this might also be due that I'm getting more in the flow of things now), and thanks to \a: Type, I haven't had to use universe constraints unlike the previous version (although given @Bhavik Mehta 's insight, maybe it isn't so bad to use that \a and G are in the same type universe?)

Edit: I thought a bit further about why the isomorphism to a FinitelyPresentedGroup approach for IsFinitelyPresented seems to work better apart from being more literal, and I think it's because when a FinitelyPresentedGroup G is defined as a PresentedGroup G, it naturally acquires the type \a since G = FreeGroup \a / normalClosure rels where rels : Set (FreeGroup \a). On the other hand, when we write IsFinitelyPresented as \exists \a: Type and a surjective map f: FreeGroup \a to* G such that f.ker is finitely generated, since MonoidHom allows FreeGroup \a and G to be different types, we have to specify that \a and G live in the same type universe to get the same result.

What I would like to do next (if the above seems reasonable) is work out some more simple examples of FinitelyPresentedGroups and then write a FinitelyPresentedGroup.toPresentation function with @Valerio Proietti and then pass it along to him.

[Hang Lu Su]

More update:

The latest commit (which can also be found here) has compiling proofs of the following statements:

/- Every FP group is FP -/
lemma FPgroup {α : Type} [Finite α] (rels : Set (FreeGroup α)) (h : rels.Finite) :
  IsFinitelyPresented (FinitelyPresentedGroup rels h) := by

/- Trivial group is FP -/
instance instTrivial : IsFinitelyPresented (Unit) := by

/- ℤ is finitely presented -/
instance Int.instFinitelyPresented : IsFinitelyPresented (Multiplicative ℤ) := by

/- FP groups are closed under isomorphism -/
lemma of_mulEquiv {G H : Type*} [Group G] [Group H]
(iso : G ≃* H) (h : IsFinitelyPresented G) :
    IsFinitelyPresented H := by

[Hang Lu Su]

Random idea after not sleeping, but would a classification on of PresentedGroups based on their presentations be something welcome in mathlib? Something like this (here is a MWE)

class IsOneRelator (G : Type*) [Group G] : Prop where
  out : ∃ (α : Type*) (rels : Set (FreeGroup α)) (hrels : rels.Finite),
      Nonempty (G ≃* PresentedGroup rels) ∧
      hrels.toFinset.card = 1

but replace other types of classes of groups from presentation with OneRelator (ex: Artin).

[Riccardo Brasca]

Can you prove that a group G if finitely presented if and only if there is a surjective morphism FreeGroup (Fin n) →* G?If you can prove this I think that the actual definition doesn't matter.

[Kevin Buzzard]

That's not true right? That's finitely generated

[Riccardo Brasca]

Sorry, plus the condition on the kernel.

[Kevin Buzzard]

Yes, all that matters is that you can prove that the definition coincides with any sensible characterisation

[Riccardo Brasca]

I see three equivalent formulations for a group G:

• there is a n and a surjective FreeGroup (Fin n) →* G with kernel finitely presented (in the sense of normal closure)
• There is a S : Finset G and a surjective FreeGroup S →* G with kernel finitely presented
• There is a type T with Fintype T and a surjective FreeGroup T →* G with kernel finitely presented. Here it would be nice to prove one direction with T : Type (just take Fin n), but the other one should hold for T : Type u.

@Hang Lu Su once we have these characterizations we can forget about what is the actual definition.

[Kevin Buzzard]

• There is a S : Finset G and a surjective FreeGroup S →* G with kernel finitely presented

I don't think you want this. It is not "a random map FreeGroup S →* G", it is "the canonical map FreeGroup S →* G". And also you don't want the kernel finitely presented, you want the kernel finitely-generated.

[Riccardo Brasca]

Ah yes, we surely want the canonical map. And I mean finitely generated yes, sorry (but using the normal closure, not the notion in mathlib).

[Hang Lu Su]

there is a n and a surjective FreeGroup (Fin n) →* G with kernel finitely presented (in the sense of normal closure)

I managed to prove this first one! The latest commit is here and it compiles!

Edit: For clarity, the two added iff statements for which the proofs compile are:

theorem iff_hom_surj_finite {G : Type*} [Group G] :
IsFinitelyPresented G ↔ ∃ (α : Type) (_ : Finite α) (f : (FreeGroup α) →* G),
  Function.Surjective f ∧ IsNormalClosureFG (MonoidHom.ker f)  := by
  sorry

theorem iff_hom_surj_fin_n {G : Type*} [Group G] :
IsFinitelyPresented G ↔ ∃ (n : ℕ) (f : (FreeGroup (Fin n)) →* G),
  Function.Surjective f ∧ IsNormalClosureFG (MonoidHom.ker f)  := by
  sorry

[Riccardo Brasca]

This is great! Can you prove the right to left arrow in the first theorem for α in Type*? It shouldn't be hard since α is finite.

[Hang Lu Su]

Done! This compile in context and I made the commit.

theorem implied_by_hom_surj_finite {G : Type*} [Group G] :
(∃ (α : Type*) (_ : Finite α) (f : (FreeGroup α) →* G),
  Function.Surjective f ∧ IsNormalClosureFG (MonoidHom.ker f)) → IsFinitelyPresented G := by
  rintro ⟨α, hα, f, hfsurj, hfker⟩
  rw [iff_hom_surj_fin_n]
  -- TODO considering refactoring this since it seems used for the second time.
  let n := Nat.card α
  let iso : FreeGroup (Fin n) ≃* FreeGroup α :=
    FreeGroup.freeGroupCongr (Finite.equivFin α).symm
  let f' : FreeGroup (Fin n) →* G := f.comp iso
  let hf'surj := hfsurj.comp iso.surjective
  have hf'ker : IsNormalClosureFG f'.ker := by
    unfold f'
    simp only [MonoidHom.ker_comp_mulEquiv]
    exact
    IsNormalClosureFG.invariant_surj_hom iso.symm.toMonoidHom iso.symm.surjective f.ker hfker
  exact ⟨n, f', hf'surj, hf'ker⟩

[Hang Lu Su]

Onto the last of Riccardo's statements!

• There is a S : Finset G and a surjective FreeGroup S →* G with kernel finitely presented

I don't think you want this. It is not "a random map FreeGroup S →* G", it is "the canonical map FreeGroup S →* G". And also you don't want the kernel finitely presented, you want the kernel finitely-generated.

Could someone confirm to me if there's already a usual mathlib way to write the canonical map FreeGroup S →* G?

Edit: Is it FreeGroup.lift (fun s => (s : G))?

[Kevin Buzzard]

docs#FreeGroup.lift

[Kevin Buzzard]

Yes that looks like the canonical group homomorphism (although usually we use \mapsto rather than => in mathlib)

[Hang Lu Su]

Just had a very productive Zoom meeting with @Valerio Proietti about what we're planning next! We concluded FinitelyPresented and Presentation can work independently with bridge functions between them so one can pass from a PresentedGroup to a Presentation and vice-versa.

As for the PR plan, it's now as follows:

• I will PR my FinitelyPresentedGroup.lean file with the statements about finitely presented groups from my branch.
• Valerio will PR his Presentation.lean file with the statements about presentations from his branch.
• As a third PR, we will submit code which bridges the two. This code is pretty minimal and Valerio has mostly already done the work in this regard, which can be found in his FinitelyPresented.lean file on his branch.

We thought this might be better as we can work mostly independently of one another which seems easier to coordinate since we are in different locations. Moreover, that way it is clear who has technical ownership of what in case we need to make a call on how to do something (although obviously we welcome the feedback on the maintainers to guide us).

[Hang Lu Su]

Hi! After encouragement by @Kevin Buzzard, I finally went ahead and made the draft PR for my part of the project. https://github.com/leanprover-community/mathlib4/pull/34236

This PR includes the notion of IsPresented and IsFinitelyPresented via isomorphism with a (Finitely)PresentedGroup and satisfies the three equivalent formulations posed by @Riccardo Brasca . I've also included some auxiliary results for this and some instances of finitely presented groups.

I included some comments within the code of what's still a work in progress imo. It's nothing that doesn't compile, but little notes to myself on what I'd like to do better in the future. I must also admit that while I did the mathematical reasoning by myself and tried to write code that is transparent in terms of human understanding, in terms of being able to write code more efficiently I did resort to vibe-coding when it came to some of the substatements in the proofs (with this context, please feel free to question my code as it will probably help me improve a lot).

I would really welcome feedback on this. Specifically, I would appreciate feedback on:

• I'm not sure why my code is failing the tests :sweat_smile:. It says

Error: error: Mathlib.lean:1:0: cannot import non-`module` Mathlib.GroupTheory.FinitelyPresentedGroup from `module`

but I'm not sure why it tried to auto-import this as a module in the first place? (in the file Mathlib.lean)

• Factoring this PR. I was told the average length of a PR is usually 100 lines (this clearly got out of hand). There are auxiliary results that I'm happy to factor into other PR dependencies.
• Factoring proofs sub-steps. I found many proofs had a repetitive pattern.
• Code clarity and mathlib best practices.
• More 1-1 discussion on \a: Type* vs \a: Type in terms of usability now that I (think) I understand what went wrong in terms of type inference.
• Anything else you can think of.

PS: sorry for disappearing last week right after having a wind of productivity and announcing the PR. I had the flu but I'm recovered.

[Kevin Buzzard]

I think all the CI errors can be fixed as follows:

1) The second line should start Copyright (c) 2025 Hang Lu Su... (the error says "you wrote Hang but I was expecting a number")

2) The file should start

[copyright notice]
module

public import Mathlib.blah
public import Mathlib.blah.blah

/-!

[module docstring]

-/

@[expose] public section

Just look at any other file in mathlib to see the correct syntax.

[Hang Lu Su]

It now passes more checks but still has the following error

Error: error: Mathlib.lean:1:0: cannot import non-`module` Mathlib.GroupTheory.FinitelyPresentedGroup from `module`

I tried a commit where I changed the public import Mathlib.Algebra.Group.Defsin to

public import Mathlib.GroupTheory.Exponent
public import Mathlib.GroupTheory.FiniteAbelian.Basic
public import Mathlib.GroupTheory.FiniteAbelian.Duality
public import Mathlib.GroupTheory.Finiteness
public import Mathlib.GroupTheory.FixedPointFree
public import Mathlib.GroupTheory.Frattini

and it solved the problem in the file containing that import statement, but then returned the same error in another file containing the importing definitions line.

Is there a better way to get rid of the error than to repeat this process in every file containing the def import?

[Henrik Böving]

You need to put the module keyword at the top of your Mathlib/GroupTheory/FinitelyPresentedGroup.lean file as Kevin showed in his template.

[Riccardo Brasca]

The error is about the file FinitelyPresentedGroup.lean, that should start with module, have the import public and have then @[expose] public section. You can copy any other file, they are all more or less the same (ignore non public import for the moment).

[Riccardo Brasca]

There is no need to touch any other file (except Mathlib.lean), you should revert that changes

[Hang Lu Su]

Thank you Kevin, Henrik and Riccardo for the help! And sorry I did not the first line of instruction properly in the first place.

The errors have now disappeared with the exception of this

/- The `unusedArguments` linter reports:
UNUSED ARGUMENTS. -/
-- Mathlib.GroupTheory.FinitelyPresentedGroup
Error: /home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/Mathlib/GroupTheory/FinitelyPresentedGroup.lean:197:1: error: @FinitelyPresentedGroup argument 2 inst✝ : Finite
  α, argument 4 x✝ : rels.Finite
+ status=1
+ grep -q 'cannot parse arguments' .lake/lint_output_attempt_1.txt
+ '[' 1 -eq 124 ']'
+ exit 1
Error: Process completed with exit code 1.

I think the problem is that the linter doesn't like the way I've defined FinitelyPresentedGroup in my code:

/-- A finitely presented group is defined as a presented group with generators of a finite type
and finite relations. -/
def FinitelyPresentedGroup {α : Type} [Finite α] (rels : Set (FreeGroup α))
(_ : rels.Finite)
:= PresentedGroup (rels)

I defined a finitely presented group as a presented group with generators \a of finite type and a finite hypothesis on the set of relations _ : rels.Finite. In the info view, it didn't like when I wrote the hypothesis as h : rels.Finite but the error went away when I changed it to _. However, it seems like the CI still has a problem with this.

Is there a different formulation that could get rid of this error? I'm happy to define FinitelyPresentedGroup apart from PresentedGroup separately if needs be as the definition is quite straightforward. My thought process was just to try and make compatible what's already existing.

/-- Given a set of relations, `rels`, over a type `α`, `PresentedGroup` constructs the group with
generators `x : α` and relations `rels` as a quotient of `FreeGroup α`. -/
def PresentedGroup (rels : Set (FreeGroup α)) :=
  FreeGroup α ⧸ Subgroup.normalClosure rels

[Riccardo Brasca]

You can just tell the linter to ignore this. I don't remember exactly the syntax, isn't it written in the error?

[Riccardo Brasca]

Something like "this linter can be turned off by..."

[Hang Lu Su]

The linter doesn't say anything is wrong in the infoView when I use _ for the hypothesis just the CI when I try to PR the code. Do you mean I should use the error I get with h as the hypothesis?

unused variable `h`

Note: This linter can be disabled with `set_option linter.unusedVariables false`

[Riccardo Brasca]

The linter is telling you that the definition makes sense without assuming that rels is finite and usually we prefer to make definition as general as possible. In this case I think you can just write

set_option linter.unusedVariables false in

before the declaration.

[Riccardo Brasca]

It is like if you say "a finite group is simple if it has no nontrivial normal subgroups". The linter would say "well, you can make the same definition for any group, no need to assume that is finite".

[Hang Lu Su]

This fix still returns the same error for some reason?

https://github.com/leanprover-community/mathlib4/pull/34236/commits/1968c14113204786dbc74b8e4e215e110bc6be70

[Riccardo Brasca]

Mmm, I am not at the computer at the moment, but you can try to not name the argument (use an underscore). Otherwise just do Ctrl + shift + f and look for the line set_option blahblahlinter false in mathlib and copy the syntax.

[Kevin Buzzard]

Why do you want this definition anyway?

The point of docs#PresentedGroup is "I have a bunch of relations in a free group on some generators and I want to make the corresponding group defined by these generators and relations".

So the point of your FinitelyPresentedGroup must be "I have a finite bunch of relations in a free group on finitely many generators and I want to make the corresponding group defined by these generators and relations" -- but you can already do this, just using docs#PresentedGroup.

That's what the linter is telling you. It's saying "the thing you're trying to make is something you can already make".

[Hang Lu Su]

Why do you want this definition anyway?

I guess there are two answers to this question, which may or may not be "good" reasons:

1. Because finitely presented groups are "special" in geometric group theory, so being able to have a constructor for this specifically seems nice in the sense that it's a guarantee the user has defined a finitely presented group, and not just a presented group (but perhaps not necessary).
2. Because the way that I defined IsFinitelyPresented is by saying that a group is finitely presented if it admits an isomorphism to a finitely presented group

class IsFinitelyPresented (G : Type*) [Group G] : Prop where
  out: ∃ (α : Type) (_: Finite α) (rels : Set (FreeGroup α)) (h : rels.Finite),
  Nonempty (G ≃* (FinitelyPresentedGroup rels h))

I suppose I can try defining IsFinitelyPresented as a presented group with the finiteness conditions as well. Let me try that and see what happens.

[Hang Lu Su]

It breaks a lot of proofs but it isn't unfixable of course. It will just take more time to PR, and I sort of believe in point 1, but if someone strongly believes there shouldn't be a special constructor for FinitelyPresentedGroup I can make a commit where I fix this problem.

[Riccardo Brasca]

This is exactly the same, right?

class IsFinitelyPresented (G : Type*) [Group G] : Prop where
  out: ∃ (α : Type) (_: Finite α) (rels : Set (FreeGroup α)) (h : rels.Finite),
  Nonempty (G ≃* (PresentedGroup rels))

[Hang Lu Su]

This has the same issue that now h is unused.

I tried with

/-- A group is finitely presented if it admits an isomorphism to a finitely presented group. -/
class IsFinitelyPresented (G : Type*) [Group G] : Prop where
  out: ∃ (α : Type) (_: Finite α) (rels : Set (FreeGroup α)),
  Nonempty (G ≃* (PresentedGroup rels)) ∧ rels.Finite

which is what breaks the proofs.

[Riccardo Brasca]

Don't worry about the unused variable linter, it is just a warning and we can turn it off.

[Kevin Buzzard]

Surely in Riccardo's definition h is being used!

[Hang Lu Su]

Well I tried this first but it returned this in the infoView

unused variable `h`

Note: This linter can be disabled with `set_option linter.unusedVariables false`

But I can try to commit this and see what the CI thinks.

[Riccardo Brasca]

this is just about the name

[Riccardo Brasca]

anyway, if only need FinitelyPresentedGroup to define IsFinitelyPresented I agree with Kevin that you go directly with IsFinitelyPresented.

[Kevin Buzzard]

Objection 1: I know finitely presented groups are special but that specialness comes up in the proofs, not in the definition itself. It's like how we define a group ring R[G] but when you look at the definition of a group ring in lean, G isn't assumed to be a group and R isn't assumed to be a ring, those assumptions come later on in the code. This is the formalisation philosophy.

The solution to 2 is given by Riccardo.

[Hang Lu Su]

Thank you both for the help and explaining the philosophy behind this.

I made the commit using Riccardo's solution with the _ variable name and it now passes the checks! :tada:

[Hang Lu Su]

I've been factoring this project into dependencies and I GOT MY FIRST PR MERGED!!!

https://github.com/leanprover-community/mathlib4/pull/34580

:dancer:

A big thank you again to everyone for continued support. :smiling_face_with_tear:

[Valerio Proietti]

Following the redistribution of tasks, I changed my (draft) PR #33233 accordingly. Now it only deals with the notion of presentations and the Tietze transformations. I have implemented 2/4 Tietze moves (adding/removing a relator). I have working code for the remaining two but probably not super polished now so perhaps it's for another PR. If anybody wants to have a look, I'd appreciate it as I am new to this process.