NYLL
Module

WordCertificates.lean

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.ReidemeisterSchreier.FiniteQuotient.WordCertificates
11 declarations indexed from sourceView source ↗

Module documentation

Reidemeister Schreier / Discrete / Reidemeister Schreier / Finite Quotient / Word Certificates

This module records checkable prefix-closure conditions for quotient-section words and proves the reduced-word and state-transition facts required by the finite tau presentation.

Imports1
Imported by2

Declarations

def

prefixClosedAlongList

L34 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.prefixClosedAlongList
Documentation

Prefix-closedness along a concrete word list, starting at quotient state \(q\). Positive letters require the next representative to be obtained by appending \(x\); negative letters require the current representative to be obtained by appending \(x\) to the previous state.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · full declaration
def prefixClosedAlongList (D : FiniteQuotientSchreierData X Q) :
    Q → List (X × Bool) → Prop
  | _q, [] => True
  | q, (x, true) :: xs =>
      D.quotientSection (D.transition q x) =
        D.quotientSection q * FreeGroup.of x ∧
      prefixClosedAlongList D (D.transition q x) xs
  | q, (x, false) :: xs =>
      D.quotientSection q =
        D.quotientSection (D.inverseTransition q x) * FreeGroup.of x ∧
      prefixClosedAlongList D (D.inverseTransition q x) xs
def

prefixClosedQuotientSectionWordAlongList

L50 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.prefixClosedQuotientSectionWordAlongList
Documentation

Word-level prefix-closedness certificate for a chosen representative-word function. This is easier to produce from a finite search tree than group equalities of representatives.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · full declaration
def prefixClosedQuotientSectionWordAlongList
    (D : FiniteQuotientSchreierData X Q)
    (quotientSectionWord : Q → List (X × Bool)) :
    Q → List (X × Bool) → Prop
  | _q, [] => True
  | q, (x, true) :: xs =>
      quotientSectionWord (D.transition q x) =
        quotientSectionWord q ++ [(x, true)] ∧
      prefixClosedQuotientSectionWordAlongList D quotientSectionWord
        (D.transition q x) xs
  | q, (x, false) :: xs =>
      quotientSectionWord q =
        quotientSectionWord (D.inverseTransition q x) ++ [(x, true)] ∧
      prefixClosedQuotientSectionWordAlongList D quotientSectionWord
        (D.inverseTransition q x) xs
theorem

prefixClosedAlongList_of_prefixClosedQuotientSectionWordAlongList

L68 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.prefixClosedAlongList_of_prefixClosedQuotientSectionWordAlongList
Documentation

A prefix-closed quotient-section word along a list gives prefix-closedness along that list.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem prefixClosedAlongList_of_prefixClosedQuotientSectionWordAlongList
    {quotientSectionWord : Q → List (X × Bool)}
    (hsection :
      ∀ q : Q, D.quotientSection q = FreeGroup.mk (quotientSectionWord q))
    {q : Q} {xs : List (X × Bool)}
    (hprefix :
      D.prefixClosedQuotientSectionWordAlongList quotientSectionWord q xs) :
    D.prefixClosedAlongList q xs
def

IsPrefixClosedQuotientSection

L98 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.IsPrefixClosedQuotientSection
Documentation

The chosen quotient section is prefix closed on its own representative words.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
def IsPrefixClosedQuotientSection : Prop
theorem

isPrefixClosedQuotientSection_of_prefixClosedQuotientSectionWord

L102 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.isPrefixClosedQuotientSection_of_prefixClosedQuotientSectionWord
Documentation

A prefix-closed quotient-section word certificate gives a prefix-closed quotient section.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
Lean source · statement
theorem isPrefixClosedQuotientSection_of_prefixClosedQuotientSectionWord
    {quotientSectionWord : Q → List (X × Bool)}
    (hsection :
      ∀ q : Q, D.quotientSection q = FreeGroup.mk (quotientSectionWord q))
    (hreduced :
      ∀ q : Q, FreeGroup.reduce (quotientSectionWord q) = quotientSectionWord q)
    (hprefix :
      ∀ q : Q,
        D.prefixClosedQuotientSectionWordAlongList quotientSectionWord 1
          (quotientSectionWord q)) :
    D.IsPrefixClosedQuotientSection
theorem

prefixClosedQuotientSectionWordAlongList_of_positive_prefixStates_from_acc

L120 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.prefixClosedQuotientSectionWordAlongList_of_positive_prefixStates_from_acc
Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · full declaration
theorem prefixClosedQuotientSectionWordAlongList_of_positive_prefixStates_from_acc
    {quotientSectionWord : Q → List (X × Bool)}
    (hsection :
      ∀ q : Q, D.quotientSection q = FreeGroup.mk (quotientSectionWord q))
    (hpositive :
      ∀ q : Q, ∀ xb ∈ quotientSectionWord q, xb.2 = true)
    (hprefixState :
      ∀ q : Q, ∀ acc rest : List (X × Bool),
        acc ++ rest = quotientSectionWord q →
          quotientSectionWord (D.quotientMap (FreeGroup.mk acc)) = acc)
    (target : Q) :
    ∀ acc rest : List (X × Bool),
      acc ++ rest = quotientSectionWord target →
      quotientSectionWord (D.quotientMap (FreeGroup.mk acc)) = acc →
      D.prefixClosedQuotientSectionWordAlongList quotientSectionWord
        (D.quotientMap (FreeGroup.mk acc)) rest
  | _acc, [], _hcat, _hacc => by
      trivial
  | acc, (x, eps) :: xs, hcat, hacc => by
      have heps : eps = true := by
        exact hpositive target (x, eps) (by
          rw [← hcat]
          exact List.mem_append_right acc (by simp only [List.mem_cons, true_or]))
      cases eps
      · cases heps
      · have hnext :
              quotientSectionWord
                  (D.quotientMap (FreeGroup.mk (acc ++ [(x, true)]))) =
                acc ++ [(x, true)] :=
            hprefixState target (acc ++ [(x, true)]) xs (by
              simpa [List.append_assoc] using hcat)
        have htransition :
              D.transition (D.quotientMap (FreeGroup.mk acc)) x =
                D.quotientMap (FreeGroup.mk (acc ++ [(x, true)])) := by
          simp only [transition, hsection, hacc, map_mul]
          rw [← D.quotientMap.map_mul]
          change
            D.quotientMap (FreeGroup.mk acc * FreeGroup.mk [(x, true)]) =
              D.quotientMap (FreeGroup.mk (acc ++ [(x, true)]))
          rw [FreeGroup.mul_mk]
        refine ⟨?_, ?_⟩
        · calc
            quotientSectionWord (D.transition (D.quotientMap (FreeGroup.mk acc)) x) =
                quotientSectionWord
                  (D.quotientMap (FreeGroup.mk (acc ++ [(x, true)]))) := by
                  rw [htransition]
            _ = acc ++ [(x, true)] := hnext
            _ = quotientSectionWord (D.quotientMap (FreeGroup.mk acc)) ++
                [(x, true)] := by rw [hacc]
        · have htail :=
            prefixClosedQuotientSectionWordAlongList_of_positive_prefixStates_from_acc
              hsection hpositive hprefixState target
              (acc ++ [(x, true)]) xs
              (by simpa [List.append_assoc] using hcat)
              (hprefixState target (acc ++ [(x, true)]) xs (by
                simpa [List.append_assoc] using hcat))
          change D.prefixClosedQuotientSectionWordAlongList quotientSectionWord
            (D.transition (D.quotientMap (FreeGroup.mk acc)) x) xs
          rw [htransition]
          exact htail
theorem

prefixClosedQuotientSectionWordAlongList_of_positive_prefixStates

L185 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.prefixClosedQuotientSectionWordAlongList_of_positive_prefixStates
Documentation

Positive prefix states along a word give a prefix-closed quotient-section word along the list.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem prefixClosedQuotientSectionWordAlongList_of_positive_prefixStates
    {quotientSectionWord : Q → List (X × Bool)}
    (hsection :
      ∀ q : Q, D.quotientSection q = FreeGroup.mk (quotientSectionWord q))
    (hpositive :
      ∀ q : Q, ∀ xb ∈ quotientSectionWord q, xb.2 = true)
    (hprefixState :
      ∀ q : Q, ∀ acc rest : List (X × Bool),
        acc ++ rest = quotientSectionWord q →
          quotientSectionWord (D.quotientMap (FreeGroup.mk acc)) = acc)
    (q : Q) :
    D.prefixClosedQuotientSectionWordAlongList quotientSectionWord 1
      (quotientSectionWord q)
theorem

isReduced_of_forall_snd_eq_true

L213 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.isReduced_of_forall_snd_eq_true
Documentation

A word list whose letters all have positive sign is reduced.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · full declaration
theorem isReduced_of_forall_snd_eq_true :
    ∀ {word : List (X × Bool)},
      (∀ xb ∈ word, xb.2 = true) → FreeGroup.IsReduced word
  | [], _hpositive => by
      simp only [FreeGroup.IsReduced.nil]
  | [_x], _hpositive => by
      simp only [FreeGroup.IsReduced.singleton]
  | x :: y :: xs, hpositive => by
      rw [FreeGroup.isReduced_cons_cons]
      refine ⟨?_, ?_⟩
      · intro _hxy
        rw [hpositive x (by simp only [List.mem_cons, true_or]), hpositive y (by simp only
            [List.mem_cons, true_or, or_true])]
      · exact isReduced_of_forall_snd_eq_true (by
          intro xb hxb
          exact hpositive xb (by simp only [List.mem_cons, hxb, or_true]))
theorem

reduce_eq_of_forall_snd_eq_true

L232 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.reduce_eq_of_forall_snd_eq_true
Documentation

A word list whose letters all have positive sign is unchanged by free reduction.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit D [Group Q] [Fintype Q] in
Lean source · statement
theorem reduce_eq_of_forall_snd_eq_true
    {word : List (X × Bool)}
    (hpositive : ∀ xb ∈ word, xb.2 = true) :
    FreeGroup.reduce word = word
theorem

snd_eq_true_of_prefixClosedQuotientSectionWordAlongList_of_isReduced_append

L243 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.snd_eq_true_of_prefixClosedQuotientSectionWordAlongList_of_isReduced_append
Documentation

In a reduced appended prefix-closed quotient-section word, each letter in the added part has positive sign.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem snd_eq_true_of_prefixClosedQuotientSectionWordAlongList_of_isReduced_append
    {quotientSectionWord : Q → List (X × Bool)}
    {q : Q} {xs : List (X × Bool)}
    (hprefix :
      D.prefixClosedQuotientSectionWordAlongList quotientSectionWord q xs)
    (hreduced : FreeGroup.IsReduced (quotientSectionWord q ++ xs)) :
    ∀ xb ∈ xs, xb.2 = true
theorem

quotientSectionWord_positive_of_prefixClosed_reduced

L282 ↗
ReidemeisterSchreier.Discrete.FiniteQuotientSchreierData.quotientSectionWord_positive_of_prefixClosed_reduced
Documentation

A reduced prefix-closed quotient-section word has only positive signed letters.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace ReidemeisterSchreier.Discrete
open ReidemeisterSchreier.Discrete.Presentations
variable {X Q : Type*} [Group Q] [Fintype Q]
namespace FiniteQuotientSchreierData
variable (D : FiniteQuotientSchreierData X Q)
variable [DecidableEq X]
omit [DecidableEq X] in
Lean source · statement
theorem quotientSectionWord_positive_of_prefixClosed_reduced
    {quotientSectionWord : Q → List (X × Bool)}
    (hOne : quotientSectionWord 1 = [])
    (hreduced : ∀ q : Q, FreeGroup.IsReduced (quotientSectionWord q))
    (hprefix :
      ∀ q : Q,
        D.prefixClosedQuotientSectionWordAlongList quotientSectionWord 1
          (quotientSectionWord q)) :
    ∀ q : Q, ∀ xb ∈ quotientSectionWord q, xb.2 = true

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.