Auditable relator expressions

Finite group presentations in print use expressions such as powers and commutators, while FreeGroup consumes flat words. This file provides a small expression language for transcribing those published relators and compiles it to Mathlib's canonical signed-word representation List (α × Bool). In that representation true denotes a generator and false its inverse.

The central result, TauCeti.Relator.toWord_toFreeGroup, proves that compilation agrees with direct structural interpretation in the free group. This makes the compiler a checked link between a human-readable transcription and the relator used to define a presented group.

The representation and its interpretation reuse FreeGroup.mk, FreeGroup.invRev, commutatorElement, and their compatibility with multiplication, inversion, and natural powers from Mathlib.

Main definitions

• TauCeti.PresentationWord: Mathlib's left-to-right list of signed generators.
• TauCeti.Relator: expressions built from generators, inverse, product, power, and commutator.
• TauCeti.Relator.map: renaming generators while preserving the expression structure.
• TauCeti.Relator.toWord: compilation of an expression to a signed word.
• TauCeti.Relator.length: the length of that word, computed from the expression without expanding powers.
• TauCeti.Relator.eval: structural evaluation under a generator assignment in any group.
• TauCeti.Relator.toFreeGroup: evaluation at the canonical free-group generators.
• TauCeti.Relator.conj and TauCeti.Relator.div: the conjugate s⁻¹ r s and the relator r s⁻¹ by which a source states an equation between two words.
• TauCeti.Relator.commInvInv: the commutator r⁻¹ s⁻¹ r s of the presentation literature.
• TauCeti.Relator.relatorSet: the free-group elements denoted by a list of expressions.

Main results

• TauCeti.Relator.toWord_toFreeGroup: compilation preserves the free-group element denoted by an expression.
• TauCeti.Relator.relatorSet_eq_of_mem_map_toWord_iff: relator lists with the same compiled-word membership denote the same relations.

@[reducible, inline]

abbrev TauCeti.PresentationWord (α : Type u_1) : Type u_1

A left-to-right word in generators of α and their formal inverses. The Boolean convention is the one used by FreeGroup.mk: true is a generator and false is its inverse.

inductive TauCeti.Relator (α : Type u_1) : Type u_1

A human-readable relator expression.

The commutator constructor is Mathlib's commutatorElement, that is, the convention ⁅r, s⁆ = r * s * r⁻¹ * s⁻¹. A source using the convention [r, s] = r⁻¹ * s⁻¹ * r * s should be transcribed as comm (inv r) (inv s).

• gen {α : Type u_1} (x : α) : Relator α

  A generator.

• inv {α : Type u_1} (r : Relator α) : Relator α

  The inverse of a relator expression.

• mul {α : Type u_1} (r s : Relator α) : Relator α

  The product of two relator expressions.

• pow {α : Type u_1} (r : Relator α) (n : ℕ) : Relator α

  A relator expression raised to a natural power.

• comm {α : Type u_1} (r s : Relator α) : Relator α

  The commutator ⁅r, s⁆ = r * s * r⁻¹ * s⁻¹.

@[instance_reducible]

instance TauCeti.instDecidableEqRelator {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (Relator α✝)

def TauCeti.instDecidableEqRelator.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : Relator α✝) : Decidable (x✝ = x✝¹)

def TauCeti.Relator.map {α : Type u_1} {β : Type u_2} (f : α → β) : Relator α → Relator β

Rename the generators of an expression without changing its operations or exponents. The renaming function need not be injective.

@[simp]

theorem TauCeti.Relator.map_gen {α : Type u_1} {β : Type u_2} (f : α → β) (x : α) : map f (gen x) = gen (f x)

Renaming a generator applies the given function.

@[simp]

theorem TauCeti.Relator.map_inv {α : Type u_1} {β : Type u_2} (f : α → β) (r : Relator α) : map f r.inv = (map f r).inv

Renaming preserves inversion.

@[simp]

theorem TauCeti.Relator.map_mul {α : Type u_1} {β : Type u_2} (f : α → β) (r s : Relator α) : map f (r.mul s) = (map f r).mul (map f s)

Renaming preserves products.

@[simp]

theorem TauCeti.Relator.map_pow {α : Type u_1} {β : Type u_2} (f : α → β) (r : Relator α) (n : ℕ) : map f (r.pow n) = (map f r).pow n

Renaming preserves natural powers, including their exponents.

@[simp]

theorem TauCeti.Relator.map_comm {α : Type u_1} {β : Type u_2} (f : α → β) (r s : Relator α) : map f (r.comm s) = (map f r).comm (map f s)

Renaming preserves commutators.

@[simp]

theorem TauCeti.Relator.map_id {α : Type u_1} (r : Relator α) : map id r = r

Renaming each generator to itself leaves the expression unchanged.

@[simp]

theorem TauCeti.Relator.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ) (r : Relator α) : map g (map f r) = map (g ∘ f) r

Successive generator renamings compose.

def TauCeti.Relator.toWord {α : Type u_1} : Relator α → PresentationWord α

Compile a relator expression to a flat signed word.

Inversion uses Mathlib's FreeGroup.invRev, which reverses the word and flips every sign. Powers are compiled by repeating the whole word, rather than by expanding the expression recursively. The five equation lemmas below are the public interface: the body itself is not exposed.

@[simp]

theorem TauCeti.Relator.toWord_gen {α : Type u_1} (x : α) : (gen x).toWord = [(x, true)]

Compilation of a generator.

@[simp]

theorem TauCeti.Relator.toWord_inv {α : Type u_1} (r : Relator α) : r.inv.toWord = FreeGroup.invRev r.toWord

Compilation of an inverse.

@[simp]

theorem TauCeti.Relator.toWord_mul {α : Type u_1} (r s : Relator α) : (r.mul s).toWord = r.toWord ++ s.toWord

Compilation of a product.

@[simp]

theorem TauCeti.Relator.toWord_pow {α : Type u_1} (r : Relator α) (n : ℕ) : (r.pow n).toWord = (List.replicate n r.toWord).flatten

Compilation of a natural power.

theorem TauCeti.Relator.isCyclicallyReduced_toWord_pow {α : Type u_1} {r : Relator α} (h : FreeGroup.IsCyclicallyReduced r.toWord) (n : ℕ) : FreeGroup.IsCyclicallyReduced (r.pow n).toWord

A power of a relator compiles to a cyclically reduced word as soon as its base does.

Published relators are often a single large power, and checking the base is much cheaper than checking the expansion: the base of the longest TauCeti.Sporadic.co1Presentation relator has nine letters where its expansion has three hundred and fifty-one. TauCeti.isCyclicallyReduced_toWord_coxeterRelator is the case of a base with two letters.

@[simp]

theorem TauCeti.Relator.toWord_comm {α : Type u_1} (r s : Relator α) : (r.comm s).toWord = r.toWord ++ s.toWord ++ FreeGroup.invRev r.toWord ++ FreeGroup.invRev s.toWord

Compilation of a commutator.

def TauCeti.Relator.length {α : Type u_1} : Relator α → ℕ

The number of signed letters in the compiled word of a relator expression, read off the expression itself rather than from the compiled list.

A transcribed presentation checks its published letter count against TauCeti.GroupPresentation.totalLength. Computing that count through Relator.toWord alone forces every power to be expanded, which for a relator such as (adefcefgh)³⁹ is hundreds of signed-letter constructors; this function multiplies instead of repeating, and TauCeti.Relator.length_toWord certifies that the two agree.

The five equations below are the interface: a module carrying transcribed relators rewrites with them rather than unfolding this definition.

@[simp]

theorem TauCeti.Relator.length_gen {α : Type u_1} (x : α) : (gen x).length = 1

The structural length of a generator.

@[simp]

theorem TauCeti.Relator.length_inv {α : Type u_1} (r : Relator α) : r.inv.length = r.length

The structural length of an inverse.

@[simp]

theorem TauCeti.Relator.length_mul {α : Type u_1} (r s : Relator α) : (r.mul s).length = r.length + s.length

The structural length of a product.

@[simp]

theorem TauCeti.Relator.length_pow {α : Type u_1} (r : Relator α) (n : ℕ) : (r.pow n).length = n * r.length

The structural length of a natural power.

@[simp]

theorem TauCeti.Relator.length_comm {α : Type u_1} (r s : Relator α) : (r.comm s).length = r.length + s.length + r.length + s.length

The structural length of a commutator.

@[simp]

theorem TauCeti.Relator.length_toWord {α : Type u_1} (r : Relator α) : List.length r.toWord = r.length

The structural length is the length of the compiled word.

This is stated in the direction that rewrites away Relator.toWord, so a letter count of a transcribed presentation reduces to arithmetic on the transcribed expressions.

def TauCeti.Relator.eval {α : Type u_1} {G : Type u_2} [Group G] (f : α → G) : Relator α → G

Evaluate a relator expression under an assignment of its generators to a group. This structural interpretation is independent of compilation to a signed word.

@[simp]

theorem TauCeti.Relator.eval_gen {α : Type u_1} {G : Type u_2} [Group G] (f : α → G) (x : α) : eval f (gen x) = f x

Evaluation of a generator is its assigned value.

@[simp]

theorem TauCeti.Relator.eval_inv {α : Type u_1} {G : Type u_2} [Group G] (f : α → G) (r : Relator α) : eval f r.inv = (eval f r)⁻¹

Evaluation preserves inversion.

@[simp]

theorem TauCeti.Relator.eval_mul {α : Type u_1} {G : Type u_2} [Group G] (f : α → G) (r s : Relator α) : eval f (r.mul s) = eval f r * eval f s

Evaluation preserves products.

@[simp]

theorem TauCeti.Relator.eval_pow {α : Type u_1} {G : Type u_2} [Group G] (f : α → G) (r : Relator α) (n : ℕ) : eval f (r.pow n) = eval f r ^ n

Evaluation preserves natural powers.

@[simp]

theorem TauCeti.Relator.eval_comm {α : Type u_1} {G : Type u_2} [Group G] (f : α → G) (r s : Relator α) : eval f (r.comm s) = ⁅eval f r, eval f s⁆

Evaluation preserves Mathlib's commutator convention.

@[simp]

theorem TauCeti.Relator.eval_map {α : Type u_1} {β : Type u_2} {G : Type u_3} [Group G] (f : β → G) (g : α → β) (r : Relator α) : eval f (map g r) = eval (f ∘ g) r

Evaluating after renaming generators is evaluation at the composed assignment. The renaming function need not be injective.

def TauCeti.Relator.toFreeGroup {α : Type u_1} : Relator α → FreeGroup α

Evaluate an expression at the canonical free-group generators. This remains independent of Relator.toWord: the comparison theorem below checks that compilation preserves meaning. The five equation lemmas below are the public interface.

@[simp]

theorem TauCeti.Relator.toFreeGroup_gen {α : Type u_1} (x : α) : (gen x).toFreeGroup = FreeGroup.of x

Interpretation of a generator.

@[simp]

theorem TauCeti.Relator.toFreeGroup_inv {α : Type u_1} (r : Relator α) : r.inv.toFreeGroup = r.toFreeGroup⁻¹

Interpretation of an inverse.

@[simp]

theorem TauCeti.Relator.toFreeGroup_mul {α : Type u_1} (r s : Relator α) : (r.mul s).toFreeGroup = r.toFreeGroup * s.toFreeGroup

Interpretation of a product.

@[simp]

theorem TauCeti.Relator.toFreeGroup_pow {α : Type u_1} (r : Relator α) (n : ℕ) : (r.pow n).toFreeGroup = r.toFreeGroup ^ n

Interpretation of a natural power.

@[simp]

theorem TauCeti.Relator.toFreeGroup_comm {α : Type u_1} (r s : Relator α) : (r.comm s).toFreeGroup = ⁅r.toFreeGroup, s.toFreeGroup⁆

Interpretation of a commutator.

@[simp]

theorem TauCeti.Relator.map_eval {α : Type u_1} {G : Type u_2} {H : Type u_3} {F : Type u_4} [Group G] [Group H] [FunLike F G H] [MonoidHomClass F G H] (φ : F) (f : α → G) (r : Relator α) : φ (eval f r) = eval (⇑φ ∘ f) r

Group homomorphisms commute with evaluation of relator expressions.

@[simp]

theorem TauCeti.Relator.lift_toFreeGroup {α : Type u_1} {G : Type u_2} [Group G] (f : α → G) (r : Relator α) : (FreeGroup.lift f) r.toFreeGroup = eval f r

The free-group universal map evaluates the expression at the assigned generators.

def TauCeti.Relator.conj {α : Type u_1} (r s : Relator α) : Relator α

The conjugate s⁻¹ * r * s, written r ^ s by most of the presentation literature.

Published presentations of the larger sporadic groups state many of their relators as conjugates, so this is the shape a transcription of such a source needs. It is a derived form rather than a sixth constructor: Relator.toWord and Relator.toFreeGroup therefore stay total on the five constructors, and Relator.toWord_toFreeGroup covers it with no extra case.

The body is exposed because a module carrying transcribed relators checks properties of its list by kernel reduction, which needs the transcription combinators to reduce.

def TauCeti.Relator.div {α : Type u_1} (r s : Relator α) : Relator α

The relator r * s⁻¹, by which a source states the equation r = s.

A published presentation freely mixes relators with relations, writing for instance a = (cd)⁴ alongside a²; Relator.toFreeGroup_div computes what this denotes, so Mathlib's div_eq_one says that imposing r s⁻¹ as a relator is imposing the source's equation r = s.

The body is exposed for the same reason as that of TauCeti.Relator.conj.

def TauCeti.Relator.commInvInv {α : Type u_1} (r s : Relator α) : Relator α

The commutator r⁻¹ s⁻¹ r s, written [r, s] by most of the presentation literature.

Mathlib's bracket is ⁅r, s⁆ = r s r⁻¹ s⁻¹, carried by Relator.comm, so the presentation literature's commutator is Relator.comm applied to the two inverses, which is what this abbreviates; Relator.toFreeGroup_commInvInv computes what it denotes.

The body is exposed for the same reason as that of TauCeti.Relator.conj.

@[simp]

theorem TauCeti.Relator.eval_conj {α : Type u_1} {G : Type u_2} [Group G] (f : α → G) (r s : Relator α) : eval f (r.conj s) = (eval f s)⁻¹ * eval f r * eval f s

Evaluation of a conjugate uses the convention s⁻¹ * r * s.

@[simp]

theorem TauCeti.Relator.eval_div {α : Type u_1} {G : Type u_2} [Group G] (f : α → G) (r s : Relator α) : eval f (r.div s) = eval f r / eval f s

Evaluation of an equation expression is the quotient of the assigned values.

@[simp]

theorem TauCeti.Relator.eval_commInvInv {α : Type u_1} {G : Type u_2} [Group G] (f : α → G) (r s : Relator α) : eval f (r.commInvInv s) = (eval f r)⁻¹ * (eval f s)⁻¹ * eval f r * eval f s

Evaluation of the presentation-literature commutator gives r⁻¹ * s⁻¹ * r * s.

@[simp]

theorem TauCeti.Relator.toFreeGroup_conj {α : Type u_1} (r s : Relator α) : (r.conj s).toFreeGroup = s.toFreeGroup⁻¹ * r.toFreeGroup * s.toFreeGroup

The conjugate expression denotes the conjugate free-group element.

@[simp]

theorem TauCeti.Relator.toFreeGroup_div {α : Type u_1} (r s : Relator α) : (r.div s).toFreeGroup = r.toFreeGroup / s.toFreeGroup

The equation expression denotes the quotient of the two free-group elements.

@[simp]

theorem TauCeti.Relator.toWord_conj {α : Type u_1} (r s : Relator α) : (r.conj s).toWord = FreeGroup.invRev s.toWord ++ (r.toWord ++ s.toWord)

The compiled word of a conjugate expression.

@[simp]

theorem TauCeti.Relator.toWord_div {α : Type u_1} (r s : Relator α) : (r.div s).toWord = r.toWord ++ FreeGroup.invRev s.toWord

The compiled word of an equation expression.

@[simp]

theorem TauCeti.Relator.toFreeGroup_commInvInv {α : Type u_1} (r s : Relator α) : (r.commInvInv s).toFreeGroup = r.toFreeGroup⁻¹ * s.toFreeGroup⁻¹ * r.toFreeGroup * s.toFreeGroup

The commutator expression of the presentation literature denotes r⁻¹ s⁻¹ r s: the expanded word a reviewer compares against the printed source.

@[simp]

theorem TauCeti.Relator.toWord_commInvInv {α : Type u_1} (r s : Relator α) : (r.commInvInv s).toWord = FreeGroup.invRev r.toWord ++ FreeGroup.invRev s.toWord ++ r.toWord ++ s.toWord

The compiled word of a commutator expression of the presentation literature.

def TauCeti.Relator.relatorSet {α : Type u_1} (l : List (Relator α)) : Set (FreeGroup α)

The free-group elements denoted by a list of relator expressions.

@[simp]

theorem TauCeti.Relator.mem_relatorSet {α : Type u_1} {l : List (Relator α)} {r : FreeGroup α} : r ∈ relatorSet l ↔ ∃ t ∈ l, t.toFreeGroup = r

Membership in a relator set: being denoted by some expression of the list.

@[simp]

theorem TauCeti.Relator.relatorSet_append {α : Type u_1} (l l' : List (Relator α)) : relatorSet (l ++ l') = relatorSet l ∪ relatorSet l'

Appending relator lists unions their relator sets.

@[simp]

theorem TauCeti.Relator.toWord_toFreeGroup {α : Type u_1} (r : Relator α) : FreeGroup.mk r.toWord = r.toFreeGroup

The compiled word denotes the direct interpretation of the relator expression.

Consequently, a reviewer may check the structured Relator against a published presentation while a PresentedGroup safely uses FreeGroup.mk r.toWord as its defining relation.

@[simp]

theorem TauCeti.Relator.toWord_map {α : Type u_1} {β : Type u_2} (f : α → β) (r : Relator α) : (map f r).toWord = List.map (Prod.map f id) r.toWord

Renaming commutes with compilation: each signed letter keeps its sign.

@[simp]

theorem TauCeti.Relator.length_map {α : Type u_1} {β : Type u_2} (f : α → β) (r : Relator α) : (map f r).length = r.length

Renaming preserves the compiled length even when distinct generators are identified.

@[simp]

theorem TauCeti.Relator.toFreeGroup_map {α : Type u_1} {β : Type u_2} (f : α → β) (r : Relator α) : (map f r).toFreeGroup = (FreeGroup.map f) r.toFreeGroup

Structural interpretation commutes with the induced free-group homomorphism.

theorem TauCeti.Relator.relatorSet_eq_of_mem_map_toWord_iff {α : Type u_1} {l l' : List (Relator α)} (h : ∀ (w : PresentationWord α), w ∈ List.map toWord l ↔ w ∈ List.map toWord l') : relatorSet l = relatorSet l'

Two relator lists with the same compiled-word membership denote the same relations.

A source may present the same relation in two shapes: an involution relation is written sᵢ ^ 2 by one source and (sᵢ sᵢ) ^ 1 by another, and a list of relations carries no order. Neither difference reaches the presented group, because the relations are the free-group elements of the compiled words and these agree. A transcription can therefore be compared with a generated relator list letter by letter, which is decidable, rather than expression by expression, which would see both differences. Multiplicity is irrelevant because relatorSet is a set.