ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.Script

10 Theorems | 16 Definitions | 3 Inductive types

ElementaryTietzeMove records genuine presentation transformations with indexed source and target presentations. VerifiedTietzeScript is the typed sequence of those moves; it evaluates to a semantic PresentationEquivCertificate and exposes an inspectable trace, move count, and weighted cost.

Semantic equivalence constructors live in the Tietze core and operation modules. They are not re-exported here as a parallel family of “script” wrappers.

import

ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.GeneratorDeletion

Imported by

Inductive ReidemeisterSchreier.Discrete.Presentations.ElementaryTietzeMove

inductive ElementaryTietzeMove :
    Presentation.{u} → Presentation.{u} → Type (u + 1) where
  /-- Replace a relator set by another set generating the same normal closure. -/
  | replaceRelators
      {X : Type u} {R S : Set (FreeGroup X)}
      (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)
      (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :
      ElementaryTietzeMove
        (Presentation.ofRelators R) (Presentation.ofRelators S)
  /-- Rename every generator through an equivalence of generator types. -/
  | renameGenerators
      {X Y : Type u} (R : Set (FreeGroup X)) (e : X ≃ Y) :
      ElementaryTietzeMove
        (Presentation.ofRelators R)
        (Presentation.ofRelators (FreeGroup.freeGroupCongr e '' R))
  /-- Adjoin generators together with relators identifying them with prescribed words. -/
  | adjoinGenerators
      {X Y : Type u} (R : Set (FreeGroup X)) (word : Y → FreeGroup X) :
      ElementaryTietzeMove
        (Presentation.ofRelators R)
        (Presentation.ofRelators (Presented.adjoinGeneratorsRelators R word))
  /-- Eliminate a family of generators by substituting their defining words. -/
  | substituteDefinedGenerators
      {X Y : Type u} (R : Set (FreeGroup (Sum X Y)))
      (word : Y → FreeGroup X) :
      ElementaryTietzeMove
        (Presentation.ofRelators
          (Presented.relatorsWithDefinedGenerators R word))
        (Presentation.ofRelators
          (Presented.relatorsAfterSubstitutingDefinedGenerators R word))
  /-- Delete a family of generators whose defining relators make them trivial. -/
  | deleteTrivialGenerators
      {X Y : Type u} (R : Set (FreeGroup (Sum X Y))) :
      ElementaryTietzeMove
        (Presentation.ofRelators (Presented.relatorsWithTrivialGenerators R))
        (Presentation.ofRelators
          (Presented.relatorsAfterDeletingTrivialGenerators R))
  /--
  Transport to a sum decomposition of the generator type and then substitute the defining words.
  -/
  | substituteDefinedGeneratorsAlongEquiv
      {Z X Y : Type u} (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
      (word : Y → FreeGroup X) :
      ElementaryTietzeMove
        (Presentation.ofRelators
          (Presented.relatorsWithDefinedGeneratorsAlongEquiv R e word))
        (Presentation.ofRelators
          (Presented.relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv R e word))
  /-- Transport to a sum decomposition and then delete the generators made trivial by relators. -/
  | deleteTrivialGeneratorsAlongEquiv
      {Z X Y : Type u} (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
      ElementaryTietzeMove
        (Presentation.ofRelators
          (Presented.relatorsWithTrivialGeneratorsAlongEquiv R e))
        (Presentation.ofRelators
          (Presented.relatorsAfterDeletingTrivialGeneratorsAlongEquiv R e))

An inspectable, indexed Tietze move whose endpoints are determined by the mathematical construction which produces its semantic certificate.

In particular, the generator moves do not accept an equivalence or a desired conclusion as an extra field: their certificates are computed from the generator-adjunction and generator-elimination constructions in this library.

Inductive ReidemeisterSchreier.Discrete.Presentations.ElementaryTietzeMove.Kind

inductive Kind where
  /-- A relator-set replacement. -/
  | replaceRelators
  /-- A renaming of generators. -/
  | renameGenerators
  /-- An adjunction of generators with defining relators. -/
  | adjoinGenerators
  /-- A substitution eliminating generators with specified defining words. -/
  | substituteDefinedGenerators
  /-- A deletion of generators made trivial by their defining relators. -/
  | deleteTrivialGenerators
deriving DecidableEq, Repr

Stable tags for script traces and cost functions.

Definition ReidemeisterSchreier.Discrete.Presentations.ElementaryTietzeMove.kind

def kind {P Q : Presentation.{u}} : ElementaryTietzeMove P Q → Kind
  | .replaceRelators _ _ => .replaceRelators
  | .renameGenerators _ _ => .renameGenerators
  | .adjoinGenerators _ _ => .adjoinGenerators
  | .substituteDefinedGenerators _ _ => .substituteDefinedGenerators
  | .deleteTrivialGenerators _ => .deleteTrivialGenerators
  | .substituteDefinedGeneratorsAlongEquiv _ _ _ => .substituteDefinedGenerators
  | .deleteTrivialGeneratorsAlongEquiv _ _ => .deleteTrivialGenerators

Inspect the mathematical kind of an elementary move.

Definition ReidemeisterSchreier.Discrete.Presentations.ElementaryTietzeMove.toCertificate

def toCertificate {P Q : Presentation.{u}}
    (m : ElementaryTietzeMove P Q) : PresentationEquivCertificate P Q := by
  cases m with
  | replaceRelators hR_to_S hS_to_R =>
      exact (Presented.replaceRelatorsTietzeEquiv hR_to_S hS_to_R).toCertificate
  | renameGenerators R e =>
      exact (Presented.renameGeneratorsTietzeEquiv R e).toCertificate
  | adjoinGenerators R word =>
      exact (Presented.adjoinGeneratorsTietzeEquiv R word).toCertificate
  | substituteDefinedGenerators R word =>
      exact (Presented.substituteDefinedGeneratorsTietzeEquiv R word).toCertificate
  | deleteTrivialGenerators R =>
      exact (Presented.deleteTrivialGeneratorsTietzeEquiv R).toCertificate
  | substituteDefinedGeneratorsAlongEquiv R e word =>
      exact
        (Presented.substituteDefinedGeneratorsAlongEquivTietzeEquiv R e word).toCertificate
  | deleteTrivialGeneratorsAlongEquiv R e =>
      exact (Presented.deleteTrivialGeneratorsAlongEquivTietzeEquiv R e).toCertificate

Evaluate one indexed move using its source-producing semantic construction.

Inductive ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript

inductive VerifiedTietzeScript :
    Presentation.{u} → Presentation.{u} → Type (u + 1) where
  /-- The empty script at a presentation. -/
  | nil (P : Presentation.{u}) : VerifiedTietzeScript P P
  /-- Prepend an elementary move to a verified script beginning at its target presentation. -/
  | cons {P Q R : Presentation.{u}}
      (head : ElementaryTietzeMove P Q)
      (tail : VerifiedTietzeScript Q R) : VerifiedTietzeScript P R

A well-typed sequence of genuine Tietze moves. The indexed intermediate presentations make an ill-typed move chain unrepresentable.

Definition ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.singleton

def singleton {P Q : Presentation.{u}} (m : ElementaryTietzeMove P Q) :
    VerifiedTietzeScript P Q :=
  .cons m (.nil Q)

A one-move verified script.

Definition ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.replaceRelators

def replaceRelators
    {X : Type u} {R S : Set (FreeGroup X)}
    (hR_to_S : ∀ r ∈ R, RelatorEquivalent S r 1)
    (hS_to_R : ∀ s ∈ S, RelatorEquivalent R s 1) :
    VerifiedTietzeScript
      (Presentation.ofRelators R) (Presentation.ofRelators S) :=
  singleton (.replaceRelators hR_to_S hS_to_R)

A verified relator-replacement move.

Definition ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.renameGenerators

def renameGenerators
    {X Y : Type u} (R : Set (FreeGroup X)) (e : X ≃ Y) :
    VerifiedTietzeScript
      (Presentation.ofRelators R)
      (Presentation.ofRelators (FreeGroup.freeGroupCongr e '' R)) :=
  singleton (.renameGenerators R e)

Rename the complete generator family by an equivalence.

Definition ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.adjoinGenerators

def adjoinGenerators
    {X Y : Type u} (R : Set (FreeGroup X)) (word : Y → FreeGroup X) :
    VerifiedTietzeScript
      (Presentation.ofRelators R)
      (Presentation.ofRelators (Presented.adjoinGeneratorsRelators R word)) :=
  singleton (.adjoinGenerators R word)

Adjoin a family of generators together with the defining words which make the extension a Tietze equivalence.

Definition ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.substituteDefinedGenerators

def substituteDefinedGenerators
    {X Y : Type u} (R : Set (FreeGroup (Sum X Y)))
    (word : Y → FreeGroup X) :
    VerifiedTietzeScript
      (Presentation.ofRelators (Presented.relatorsWithDefinedGenerators R word))
      (Presentation.ofRelators
        (Presented.relatorsAfterSubstitutingDefinedGenerators R word)) :=
  singleton (.substituteDefinedGenerators R word)

Eliminate a family of generators whose defining words have been included in the relator family.

Definition ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.deleteTrivialGenerators

def deleteTrivialGenerators
    {X Y : Type u} (R : Set (FreeGroup (Sum X Y))) :
    VerifiedTietzeScript
      (Presentation.ofRelators (Presented.relatorsWithTrivialGenerators R))
      (Presentation.ofRelators (Presented.relatorsAfterDeletingTrivialGenerators R)) :=
  singleton (.deleteTrivialGenerators R)

Delete a family of generators carrying the relators y = 1.

Definition ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.substituteDefinedGeneratorsAlongEquiv

def substituteDefinedGeneratorsAlongEquiv
    {Z X Y : Type u} (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y)
    (word : Y → FreeGroup X) :
    VerifiedTietzeScript
      (Presentation.ofRelators
        (Presented.relatorsWithDefinedGeneratorsAlongEquiv R e word))
      (Presentation.ofRelators
        (Presented.relatorsAfterSubstitutingDefinedGeneratorsAlongEquiv R e word)) :=
  singleton (.substituteDefinedGeneratorsAlongEquiv R e word)

Eliminate a family of defined generators after an explicit splitting of an arbitrary generator type.

Definition ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.deleteTrivialGeneratorsAlongEquiv

def deleteTrivialGeneratorsAlongEquiv
    {Z X Y : Type u} (R : Set (FreeGroup Z)) (e : Z ≃ Sum X Y) :
    VerifiedTietzeScript
      (Presentation.ofRelators
        (Presented.relatorsWithTrivialGeneratorsAlongEquiv R e))
      (Presentation.ofRelators
        (Presented.relatorsAfterDeletingTrivialGeneratorsAlongEquiv R e)) :=
  singleton (.deleteTrivialGeneratorsAlongEquiv R e)

Delete trivial generators after an explicit splitting of an arbitrary generator type.

Definition ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.deleteTrivialGeneratorsOfPredicate

def deleteTrivialGeneratorsOfPredicate
    {Z : Type u} (R : Set (FreeGroup Z)) (delete : Z → Prop)
    [DecidablePred delete] :
    VerifiedTietzeScript
      (Presentation.ofRelators
        (Presented.relatorsWithTrivialGeneratorsOfPredicate R delete))
      (Presentation.ofRelators
        (Presented.relatorsAfterDeletingTrivialGeneratorsOfPredicate R delete)) :=
  deleteTrivialGeneratorsAlongEquiv R
    (X := Presented.GeneratorPartition.Kept delete)
    (Y := Presented.GeneratorPartition.Deleted delete)
    (Presented.GeneratorPartition.equiv delete)

Delete exactly the generators selected by a decidable predicate.

Definition ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.trans

def trans {P Q R : Presentation.{u}}
    (s : VerifiedTietzeScript P Q) (t : VerifiedTietzeScript Q R) :
    VerifiedTietzeScript P R :=
  match s with
  | .nil _ => t
  | .cons head tail => .cons head (tail.trans t)

Concatenate two verified scripts.

Definition ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.toCertificate

def toCertificate {P Q : Presentation.{u}}
    (s : VerifiedTietzeScript P Q) : PresentationEquivCertificate P Q :=
  match s with
  | .nil P => PresentationEquivCertificate.refl P
  | .cons head tail =>
      PresentationEquivCertificate.trans head.toCertificate tail.toCertificate

Evaluate a complete move sequence to its semantic certificate.

Definition ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.trace

def trace {P Q : Presentation.{u}}
    (s : VerifiedTietzeScript P Q) : List ElementaryTietzeMove.Kind :=
  match s with
  | .nil _ => []
  | .cons head tail => head.kind :: tail.trace

The inspectable sequence of move kinds.

Definition ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.moveCount

def moveCount {P Q : Presentation.{u}} (s : VerifiedTietzeScript P Q) : ℕ :=
  s.trace.length

The number of elementary moves in a verified script.

Definition ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.cost

def cost {P Q : Presentation.{u}}
    (s : VerifiedTietzeScript P Q)
    (weight : ElementaryTietzeMove.Kind → ℕ) : ℕ :=
  (s.trace.map weight).sum

A customizable additive script cost.

Theorem ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.trace_nil

@[simp] theorem trace_nil (P : Presentation.{u}) :
    (VerifiedTietzeScript.nil P).trace = []

The empty verified script has an empty move trace.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.trace_cons

@[simp] theorem trace_cons
    {P Q R : Presentation.{u}} (head : ElementaryTietzeMove P Q)
    (tail : VerifiedTietzeScript Q R) :
    (VerifiedTietzeScript.cons head tail).trace = head.kind :: tail.trace

The trace of a script begins with the kind of its head move.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.trace_singleton

@[simp] theorem trace_singleton
    {P Q : Presentation.{u}} (move : ElementaryTietzeMove P Q) :
    (singleton move).trace = [move.kind]

A singleton script records exactly the kind of its sole move.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.moveCount_nil

@[simp] theorem moveCount_nil (P : Presentation.{u}) :
    (VerifiedTietzeScript.nil P).moveCount = 0

The empty verified script contains no moves.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.moveCount_cons

@[simp] theorem moveCount_cons
    {P Q R : Presentation.{u}} (head : ElementaryTietzeMove P Q)
    (tail : VerifiedTietzeScript Q R) :
    (VerifiedTietzeScript.cons head tail).moveCount = tail.moveCount + 1

Prepending a move increases the length of a verified script by one.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.moveCount_singleton

@[simp] theorem moveCount_singleton
    {P Q : Presentation.{u}} (move : ElementaryTietzeMove P Q) :
    (singleton move).moveCount = 1

A singleton verified script contains one move.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.moveCount_trans

@[simp] theorem moveCount_trans
    {P Q R : Presentation.{u}} (s : VerifiedTietzeScript P Q)
    (t : VerifiedTietzeScript Q R) :
    (s.trans t).moveCount = s.moveCount + t.moveCount

Concatenating verified scripts adds their move counts.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.cost_nil

@[simp] theorem cost_nil
    (weight : ElementaryTietzeMove.Kind → ℕ) (P : Presentation.{u}) :
    (VerifiedTietzeScript.nil P).cost weight = 0

The empty verified script has zero cost for every weighting.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.cost_cons

@[simp] theorem cost_cons
    (weight : ElementaryTietzeMove.Kind → ℕ)
    {P Q R : Presentation.{u}} (head : ElementaryTietzeMove P Q)
    (tail : VerifiedTietzeScript Q R) :
    (VerifiedTietzeScript.cons head tail).cost weight =
      weight head.kind + tail.cost weight

The cost of a nonempty script is the head move's weight plus the tail cost.

Show Lean proof

Theorem ReidemeisterSchreier.Discrete.Presentations.VerifiedTietzeScript.cost_singleton

@[simp] theorem cost_singleton
    (weight : ElementaryTietzeMove.Kind → ℕ)
    {P Q : Presentation.{u}} (move : ElementaryTietzeMove P Q) :
    (singleton move).cost weight = weight move.kind

The cost of a singleton script is the weight assigned to its sole move.

Show Lean proof

ProCGroups.ReidemeisterSchreier.Discrete.Presentations.Tietze.Script

Declarations