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]

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]

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]

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.

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.

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!