Coherence of one-relator groups

3 fully proved1 ready to prove

Coherent groups and rings

DefinitionCoherent group#✓fully proved

A group is coherent if all of its finitely generated subgroups are finitely presented.

def Group.Coherent (G : Type*) [Group G] : Prop :=
  ∀ H : Subgroup G, H.FG → Group.IsFinitelyPresented H

Used by 1

Used byJaikin-Zapirain–Linton theorem: one-relator groups are coherent

DefinitionCoherent ring#✓fully proved

A semiring \(R\) is (left) coherent if every finitely generated left ideal of \(R\) is finitely presented as an \(R\)-module.

def Ring.Coherent (R : Type*) [Semiring R] : Prop :=
  ∀ I : Ideal R, I.FG → Module.FinitePresentation R I

Used by 1

Used byJaikin-Zapirain–Linton theorem: one-relator groups are coherent

DefinitionOne-relator group#✓fully proved

A group G is called one-relator if it has a presentation with a single relation.

def Group.OneRelator.{u} (G : Type u) [Group G] : Prop :=
  ∃ n : ℕ, ∃ rel : FreeGroup (Fin n), Nonempty (PresentedGroup {rel} ≃* G)

Used by 1

Used byJaikin-Zapirain–Linton theorem: one-relator groups are coherent

On Coherence Of One Relator Groups

TheoremJaikin-Zapirain–Linton theorem: one-relator groups are coherent#●ready to prove

Let \(G\) be a one-relator group and \(K\) a field. Then \(G\) is a coherent group and the group algebra \(K[G]\) is a (left) coherent ring.

public theorem_wanted theorem_1_1 (G K : Type*) [Group G] [Field K] (hG : Group.OneRelator G) :
    Group.Coherent G ∧ Ring.Coherent (MonoidAlgebra K G)

Sources

• A. Jaikin-Zapirain and M. Linton, On the coherence of one-relator groups and their group algebras, Annals of Math, 201 (3) 2025. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_on_coherence_of_one_relator_groups of the lean-eval benchmark.

Uses 3

Statement usesCoherent group · One-relator group · Coherent ring

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.