Auditable finite group presentations

This file packages a finite group presentation. The generator count fixes the relator index type to Fin generatorCount. Sources, generator names and conventions, and transcription notes belong in the docstring of each concrete presentation. The expected relator count stated by the source is checked against the transcribed data by TauCeti.GroupPresentation.matchesMetadata.

The stored relators are human-readable TauCeti.Relator expressions. They are compiled to Mathlib's signed words and then interpreted by FreeGroup.mk; the resulting finite list of relations, regarded as a set, defines TauCeti.GroupPresentation.Group using Mathlib's PresentedGroup.

Main definitions

• TauCeti.GroupPresentation: finite presentation data and an expected relator count.
• TauCeti.GroupPresentation.relators: the compiled signed words.
• TauCeti.GroupPresentation.relatorLetters: the compiled words with generator indices as naturals, for stating a letter-by-letter comparison with a source.
• TauCeti.GroupPresentation.totalLength: the number of letters in the compiled words, for checking against a published presentation length.
• TauCeti.GroupPresentation.relatorsCyclicallyReduced: the decidable check that every compiled word is cyclically reduced.
• TauCeti.GroupPresentation.relatorSet: the relations as free-group elements.
• TauCeti.GroupPresentation.Group: the group defined by the presentation.
• TauCeti.GroupPresentation.homEquiv: homomorphisms specified by satisfying generator assignments.
• TauCeti.GroupPresentation.matchesMetadata: the decidable relator count check.

Main results

• TauCeti.GroupPresentation.relatorSet_eq_relatorSet_transcribed: the relations of a presentation are the relator set of its transcribed expressions.
• TauCeti.GroupPresentation.range_homEquiv_symm: the range of the homomorphism extending a satisfying assignment is the subgroup generated by the assigned values.
• TauCeti.GroupPresentation.exists_surjective_of_closure_range_eq: a satisfying assignment whose values generate a subgroup gives a surjection onto it.

structure TauCeti.GroupPresentation : Type

A finite group presentation with an expected relator count.

The source must be a full presentation of the abstract group, not a semi-presentation for recognizing generators in a group already constructed elsewhere. Record its citation, generator names and conventions, and any transcription notes in the presentation's docstring. generatorCount determines the relator arity; matchesMetadata checks the relator count against expectedRelatorCount.

• generatorCount : ℕ

  The number of generators stated by the source, fixing the relator index type.

• expectedRelatorCount : ℕ

  The number of relators stated by the source.

• transcribed : List (Relator (Fin self.generatorCount))

  Relators transcribed in the generator order documented for the presentation.

def TauCeti.GroupPresentation.relators (P : GroupPresentation) : List (PresentationWord (Fin P.generatorCount))

The relator expressions compiled to left-to-right signed words.

theorem TauCeti.GroupPresentation.relators_def (P : GroupPresentation) : P.relators = List.map Relator.toWord P.transcribed

The compiled relators are obtained by compiling each transcribed expression.

This is the unfolding lemma for TauCeti.GroupPresentation.relators, whose body is sealed. It is deliberately not @[simp]: the simp normal form of a presentation is the structural description given by length_relators and mem_relators_iff below, not the compiled list.

@[simp]

theorem TauCeti.GroupPresentation.length_relators (P : GroupPresentation) : P.relators.length = P.transcribed.length

Compilation preserves the number of relators.

@[simp]

theorem TauCeti.GroupPresentation.mem_relators_iff (P : GroupPresentation) (w : PresentationWord (Fin P.generatorCount)) : w ∈ P.relators ↔ ∃ t ∈ P.transcribed, t.toWord = w

The compiled words are exactly the compilations of the transcribed expressions.

def TauCeti.GroupPresentation.relatorLetters (P : GroupPresentation) : List (List (ℕ × Bool))

The compiled relator words, with each generator index displayed as a natural number.

A transcription is audited by comparing the compiled letters with the published relators, and this form of them is the one to state such a comparison against: the index type of a word depends on the generator count, whereas the letters here do not, so the comparison needs no arithmetic on that dependency.

theorem TauCeti.GroupPresentation.relatorLetters_def (P : GroupPresentation) : P.relatorLetters = List.map (List.map fun (letter : Fin P.generatorCount × Bool) => (↑letter.1, letter.2)) P.relators

The displayed letters are obtained by forgetting the bounds on the compiled generator indices. This is the unfolding lemma for the sealed body, and like relators_def it is not @[simp].

def TauCeti.GroupPresentation.totalLength (P : GroupPresentation) : ℕ

The total number of letters in the compiled relator words.

Sources for finite presentations customarily publish this figure, usually calling it the length of the presentation, so comparing it with the transcribed data gives a decidable check on a transcription alongside the relator count of TauCeti.GroupPresentation.matchesMetadata. A published length is normally measured after free and cyclic reduction of each relator, so a row using it as a check should also record that its compiled words are reduced.

theorem TauCeti.GroupPresentation.totalLength_def (P : GroupPresentation) : P.totalLength = (List.map List.length P.relators).sum

The total length is the sum of the lengths of the compiled relator words. This is the unfolding lemma for the sealed body, and like relators_def it is not @[simp].

theorem TauCeti.GroupPresentation.map_length_relatorLetters (P : GroupPresentation) : List.map List.length P.relatorLetters = List.map List.length P.relators

The displayed letter words have the same lengths as the compiled relator words, since forgetting the bounds on the generator indices does not change a word's length.

A row that spells its compiled words out letter by letter therefore gets its per-relator length check from that one comparison, rather than by unfolding the relator compiler a second time.

theorem TauCeti.GroupPresentation.sum_map_length_relatorLetters (P : GroupPresentation) : (List.map List.length P.relatorLetters).sum = P.totalLength

The total length is also the sum of the lengths of the displayed letter words.

def TauCeti.GroupPresentation.relatorsCyclicallyReduced (P : GroupPresentation) : Prop

Every compiled relator word of a presentation is cyclically reduced.

A published presentation length is normally measured after free and cyclic reduction of each relator, so this is what makes TauCeti.GroupPresentation.totalLength comparable with such a figure. It is a check on the transcribed data only, and says nothing about the presented group.

@[simp]

theorem TauCeti.GroupPresentation.relatorsCyclicallyReduced_iff (P : GroupPresentation) : P.relatorsCyclicallyReduced ↔ ∀ w ∈ P.relators, FreeGroup.IsCyclicallyReduced w

The cyclic-reduction check unfolds to a statement about each compiled word.

@[instance_reducible]

instance TauCeti.GroupPresentation.instDecidableIsCyclicallyReducedOfDecidableEq {α : Type u_1} [DecidableEq α] (w : PresentationWord α) : Decidable (FreeGroup.IsCyclicallyReduced w)

A word is cyclically reduced exactly when free reduction leaves it alone and its last letter does not cancel against its first, and both halves of that are decidable.

@[instance_reducible]

instance TauCeti.GroupPresentation.instDecidableRelatorsCyclicallyReduced (P : GroupPresentation) : Decidable P.relatorsCyclicallyReduced

def TauCeti.GroupPresentation.relatorSet (P : GroupPresentation) : Set (FreeGroup (Fin P.generatorCount))

The compiled relations, interpreted as elements of the free group.

@[simp]

theorem TauCeti.GroupPresentation.mem_relatorSet_iff (P : GroupPresentation) (r : FreeGroup (Fin P.generatorCount)) : r ∈ P.relatorSet ↔ ∃ t ∈ P.transcribed, t.toFreeGroup = r

The relations are exactly the free-group elements denoted by the transcribed expressions.

This is stated against Relator.toFreeGroup rather than against the compiled words, so a consumer discharging the relations of PresentedGroup never has to unfold the compiler.

theorem TauCeti.GroupPresentation.relatorSet_eq_relatorSet_transcribed (P : GroupPresentation) : P.relatorSet = Relator.relatorSet P.transcribed

The relations of a presentation are the relator set of its transcribed expressions.

This is the bridge between the presentation-level relation set and TauCeti.Relator.relatorSet, the notion in which the relator lists of a transcription are built and reasoned about, so a consumer relating the two never has to re-derive the identification by extensionality.

It is deliberately not @[simp]: mem_relatorSet_iff above is the simp normal form of a membership in relatorSet, and rewriting the set itself would take that lemma's left-hand side out of normal form, which the simpNF linter rejects.

@[reducible, inline]

abbrev TauCeti.GroupPresentation.Group (P : GroupPresentation) : Type

The group defined by the generators and compiled relations of a presentation.

def TauCeti.GroupPresentation.homEquiv (P : GroupPresentation) {G : Type u_1} [_root_.Group G] : (P.Group →* G) ≃ { f : Fin P.generatorCount → G // ∀ t ∈ P.transcribed, (FreeGroup.lift f) t.toFreeGroup = 1 }

Homomorphisms from a finite presentation correspond to generator assignments satisfying its transcribed relators. No generation or injectivity condition is imposed on the assignment.

@[simp]

theorem TauCeti.GroupPresentation.homEquiv_apply (P : GroupPresentation) {G : Type u_1} [_root_.Group G] (φ : P.Group →* G) : ↑(P.homEquiv φ) = fun (i : Fin P.generatorCount) => φ (PresentedGroup.of i)

The assignment associated to a homomorphism consists of its values on the generators.

@[simp]

theorem TauCeti.GroupPresentation.homEquiv_symm_apply_of (P : GroupPresentation) {G : Type u_1} [_root_.Group G] (f : { f : Fin P.generatorCount → G // ∀ t ∈ P.transcribed, (FreeGroup.lift f) t.toFreeGroup = 1 }) (i : Fin P.generatorCount) : (P.homEquiv.symm f) (PresentedGroup.of i) = ↑f i

Extending a satisfying assignment sends each generator to its assigned value.

theorem TauCeti.GroupPresentation.range_homEquiv_symm (P : GroupPresentation) {G : Type u_1} [_root_.Group G] (f : { f : Fin P.generatorCount → G // ∀ t ∈ P.transcribed, (FreeGroup.lift f) t.toFreeGroup = 1 }) : (P.homEquiv.symm f).range = Subgroup.closure (Set.range ↑f)

The range of the homomorphism extending a satisfying assignment is the subgroup generated by the assigned values.

theorem TauCeti.GroupPresentation.exists_surjective_of_closure_range_eq (P : GroupPresentation) {G : Type u_1} [_root_.Group G] {H : Subgroup G} (f : { f : Fin P.generatorCount → G // ∀ t ∈ P.transcribed, (FreeGroup.lift f) t.toFreeGroup = 1 }) (h : Subgroup.closure (Set.range ↑f) = H) : ∃ (g : P.Group →* ↥H), Function.Surjective ⇑g

A satisfying assignment whose values generate a subgroup H gives a surjective homomorphism from the presented group onto H.

def TauCeti.GroupPresentation.matchesMetadata (P : GroupPresentation) : Prop

The recorded relator count agrees with the transcribed data.

This checks transcription metadata only; it makes no claim that the source presents a named group or that the transcription agrees with the source.

@[simp]

theorem TauCeti.GroupPresentation.matchesMetadata_iff (P : GroupPresentation) : P.matchesMetadata ↔ P.transcribed.length = P.expectedRelatorCount

The metadata check unfolds to the relator count equality.

@[instance_reducible]

instance TauCeti.GroupPresentation.instDecidableMatchesMetadata (P : GroupPresentation) : Decidable P.matchesMetadata