NYLL
Module

PrefixTree.lean

Nyll.ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.PrefixTree
19 declarations indexed from sourceView source ↗

Module documentation

Reidemeister Schreier / Discrete / Open Subgroups / Prefix Tree

This module constructs the Schreier prefix tree from a right transversal, proves its positive and negative edge criteria, and relates its complement edges to the nontrivial Schreier generators.

Imports4
Imported by2

Declarations

theorem

prefixParentEdge_mem_transversal

L34 ↗
ReidemeisterSchreier.Discrete.OpenSubgroups.prefixParentEdge_mem_transversal
Documentation

The parent vertex of a nontrivial prefix-parent edge of a Schreier transversal again lies in the transversal.

Source context 5 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierPrefixTrees
open scoped Pointwise
open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj
  Quiver _root_.ReidemeisterSchreier.FreeGroup
Lean source · statement
theorem prefixParentEdge_mem_transversal {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    (t : T) (ht1 : (t : FreeGroup X) ≠ 1) :
    (FreeGroup.prefixParentEdgeOfNeOne (X := X) (t := (t : FreeGroup X)) ht1).parent ∈ T
theorem

exists_inverseBasis_edge_of_ne_one

L44 ↗
ReidemeisterSchreier.Discrete.OpenSubgroups.exists_inverseBasis_edge_of_ne_one
Documentation

Every nonidentity transversal representative is reached from its prefix parent by an inverse-basis edge.

Source context 5 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierPrefixTrees
open scoped Pointwise
open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj
  Quiver _root_.ReidemeisterSchreier.FreeGroup
Lean source · full declaration
theorem exists_inverseBasis_edge_of_ne_one {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    (t : T) (ht1 : (t : FreeGroup X) ≠ 1) :
    ∃ x : X,
      letI := schreierTransversalRightCosetAction (X := X) hT
      (FreeGroup.inverseBasis X x •
          (⟨FreeGroup.prefixParent (t : FreeGroup X),
            prefixParent_mem_of_mem (X := X) hT t.property⟩ : T) = t) ∨
      (FreeGroup.inverseBasis X x • t =
          (⟨FreeGroup.prefixParent (t : FreeGroup X),
            prefixParent_mem_of_mem (X := X) hT t.property⟩ : T)) := by
  let edge := FreeGroup.prefixParentEdgeOfNeOne (X := X) (t := (t : FreeGroup X)) ht1
  have hlastEdge :
      FreeGroup.lastLetter? (t : FreeGroup X) = some edge.letter :=
    FreeGroup.prefixParentEdgeOfNeOne_lastLetter? (X := X) (t := (t : FreeGroup X)) ht1
  rcases hletter : edge.letter with ⟨x, b⟩
  cases b with
  | false =>
    have hlast? :
        FreeGroup.lastLetter? (t : FreeGroup X) = some ((x, false) : Internal.SignedLetter X) := by
      simpa [edge, hletter] using hlastEdge
    rcases (Internal.FreeGroupWord.FreeGroup.lastLetter?_eq_some_iff
      (g := (t : FreeGroup X)) (y := ((x, false) : Internal.SignedLetter X))).1 hlast? with
      ⟨hw, hlast⟩
    refine ⟨x, ?_⟩
    refine Or.inr ?_
    let p : T := ⟨FreeGroup.prefixParent (t : FreeGroup X),
      prefixParent_mem_of_mem (X := X) hT t.property⟩
    rw [FreeGroup.inverseBasis_apply,
      schreierTransversalRightCosetAction_smul (X := X) hT (FreeGroup.of x)⁻¹ t]
    simpa [p] using
      schreierRepresentative_eq_prefixParent_of_cancels (X := X) hT t.property hw hlast
  | true =>
    have hlast? :
        FreeGroup.lastLetter? (t : FreeGroup X) = some ((x, true) : Internal.SignedLetter X) := by
      simpa [edge, hletter] using hlastEdge
    rcases (Internal.FreeGroupWord.FreeGroup.lastLetter?_eq_some_iff
      (g := (t : FreeGroup X)) (y := ((x, true) : Internal.SignedLetter X))).1 hlast? with
      ⟨hw, hlast⟩
    refine ⟨x, ?_⟩
    refine Or.inl ?_
    let p : T := ⟨FreeGroup.prefixParent (t : FreeGroup X),
      prefixParent_mem_of_mem (X := X) hT t.property⟩
    rw [FreeGroup.inverseBasis_apply,
      schreierTransversalRightCosetAction_smul (X := X) hT (FreeGroup.of x)⁻¹ p]
    simpa [p] using
      schreierRepresentative_eq_of_prefixParent_last_pos (X := X) hT t.property hw hlast
def

schreierPrefixTree

L97 ↗
ReidemeisterSchreier.Discrete.OpenSubgroups.schreierPrefixTree
Documentation

The canonical prefix tree on the Schreier transversal. Its unique incoming edge for a non-root vertex is determined by the last letter of the reduced word of that vertex.

Source context 5 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierPrefixTrees
open scoped Pointwise
open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj
  Quiver _root_.ReidemeisterSchreier.FreeGroup
Lean source · full declaration
def schreierPrefixTree {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    letI := schreierTransversalRightCosetAction (X := X) hT
    letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
      FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
    WideSubquiver
      (Quiver.Symmetrify <| IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)) := by
  letI := schreierTransversalRightCosetAction (X := X) hT
  exact fun a b =>
    { e |
        ∃ hw : FreeGroup.toWord ((b.back : T) : FreeGroup X) ≠ [],
          let tb : T := b.back
          let pb : T := ⟨FreeGroup.prefixParent (tb : FreeGroup X),
            prefixParent_mem_of_mem (X := X) hT tb.property⟩
          a.back = pb ∧
            match e with
            | Sum.inl g => (FreeGroup.toWord (tb : FreeGroup X)).getLast hw = (g.1, true)
            | Sum.inr g => (FreeGroup.toWord (tb : FreeGroup X)).getLast hw = (g.1, false) }
theorem

mem_schreierPrefixTree_inl_iff

L121 ↗
ReidemeisterSchreier.Discrete.OpenSubgroups.mem_schreierPrefixTree_inl_iff
Documentation

Membership in the left branch of the Schreier prefix tree is equivalent to the displayed prefix condition.

Source context 5 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierPrefixTrees
open scoped Pointwise
open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj
  Quiver _root_.ReidemeisterSchreier.FreeGroup
Lean source · full declaration
theorem mem_schreierPrefixTree_inl_iff {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    {hT : IsRightSchreierTransversal (X := X) L T} :
    letI := schreierTransversalRightCosetAction (X := X) hT
    letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
      FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
    ∀ {a b : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)}
      {g : a ⟶ b},
      (Sum.inl g :
          @Quiver.Hom
            (Quiver.Symmetrify (IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)))
            inferInstance a b) ∈
          schreierPrefixTree (X := X) hT a b ↔
        ∃ hw : FreeGroup.toWord ((b.back : T) : FreeGroup X) ≠ [],
          let tb : T := b.back
          let pb : T := ⟨FreeGroup.prefixParent (tb : FreeGroup X),
            prefixParent_mem_of_mem (X := X) hT tb.property⟩
          a.back = pb ∧
            (FreeGroup.toWord (tb : FreeGroup X)).getLast hw = (g.1, true) := by
  intro a b g
  rfl
theorem

mem_schreierPrefixTree_inr_iff

L147 ↗
ReidemeisterSchreier.Discrete.OpenSubgroups.mem_schreierPrefixTree_inr_iff
Documentation

Membership in the right branch of the Schreier prefix tree is equivalent to the displayed prefix condition.

Source context 5 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierPrefixTrees
open scoped Pointwise
open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj
  Quiver _root_.ReidemeisterSchreier.FreeGroup
Lean source · full declaration
theorem mem_schreierPrefixTree_inr_iff {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    {hT : IsRightSchreierTransversal (X := X) L T} :
    letI := schreierTransversalRightCosetAction (X := X) hT
    letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
      FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
    ∀ {a b : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)}
      {g : b ⟶ a},
      (Sum.inr g :
          @Quiver.Hom
            (Quiver.Symmetrify (IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)))
            inferInstance a b) ∈
          schreierPrefixTree (X := X) hT a b ↔
        ∃ hw : FreeGroup.toWord ((b.back : T) : FreeGroup X) ≠ [],
          let tb : T := b.back
          let pb : T := ⟨FreeGroup.prefixParent (tb : FreeGroup X),
            prefixParent_mem_of_mem (X := X) hT tb.property⟩
          a.back = pb ∧
            (FreeGroup.toWord (tb : FreeGroup X)).getLast hw = (g.1, false) := by
  intro a b g
  rfl
theorem

schreierPrefixTree_edge_of_last_pos

L171 ↗
ReidemeisterSchreier.Discrete.OpenSubgroups.schreierPrefixTree_edge_of_last_pos
Documentation

A positive final letter determines the forward edge from the prefix parent in the Schreier tree.

Source context 5 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierPrefixTrees
open scoped Pointwise
open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj
  Quiver _root_.ReidemeisterSchreier.FreeGroup
Lean source · full declaration
theorem schreierPrefixTree_edge_of_last_pos {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    (t : T) {x : X} (hw : FreeGroup.toWord (t : FreeGroup X) ≠ [])
    (hlast : (FreeGroup.toWord (t : FreeGroup X)).getLast hw = (x, true)) :
    letI := schreierTransversalRightCosetAction (X := X) hT
    letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
      FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
    let p : T := ⟨FreeGroup.prefixParent (t : FreeGroup X),
      prefixParent_mem_of_mem (X := X) hT t.property⟩
    let pA : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) :=
      show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from
        ((p : T) : ActionCategory (FreeGroup X) T)
    let tA : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) :=
      show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from
        ((t : T) : ActionCategory (FreeGroup X) T)
    ∃ e : @Quiver.Hom
        (Quiver.Symmetrify (IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)))
        inferInstance pA tA,
      e ∈ schreierPrefixTree (X := X) hT pA tA := by
  let p : T := ⟨FreeGroup.prefixParent (t : FreeGroup X),
    prefixParent_mem_of_mem (X := X) hT t.property⟩
  refine ⟨Sum.inl ⟨x, ?_⟩, ?_⟩
  · exact (schreierTransversalRightCosetAction_smul (X := X) hT
      (FreeGroup.inverseBasis X x) p).trans (by
        simpa only [FreeGroup.inverseBasis_apply, inv_inv, p, coe_back] using
          schreierRepresentative_eq_of_prefixParent_last_pos (X := X) hT t.property hw hlast)
  · exact (mem_schreierPrefixTree_inl_iff (X := X) (hT := hT)).2
      ⟨hw, rfl, hlast⟩
theorem

schreierPrefixTree_edge_of_last_neg

L202 ↗
ReidemeisterSchreier.Discrete.OpenSubgroups.schreierPrefixTree_edge_of_last_neg
Documentation

A negative final letter determines the oppositely oriented edge from the prefix parent.

Source context 5 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierPrefixTrees
open scoped Pointwise
open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj
  Quiver _root_.ReidemeisterSchreier.FreeGroup
Lean source · full declaration
theorem schreierPrefixTree_edge_of_last_neg {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    (t : T) {x : X} (hw : FreeGroup.toWord (t : FreeGroup X) ≠ [])
    (hlast : (FreeGroup.toWord (t : FreeGroup X)).getLast hw = (x, false)) :
    letI := schreierTransversalRightCosetAction (X := X) hT
    letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
      FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
    let p : T := ⟨FreeGroup.prefixParent (t : FreeGroup X),
      prefixParent_mem_of_mem (X := X) hT t.property⟩
    let pA : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) :=
      show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from
        ((p : T) : ActionCategory (FreeGroup X) T)
    let tA : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) :=
      show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from
        ((t : T) : ActionCategory (FreeGroup X) T)
    ∃ e : @Quiver.Hom
        (Quiver.Symmetrify (IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)))
        inferInstance pA tA,
      e ∈ schreierPrefixTree (X := X) hT pA tA := by
  let p : T := ⟨FreeGroup.prefixParent (t : FreeGroup X),
    prefixParent_mem_of_mem (X := X) hT t.property⟩
  refine ⟨Sum.inr ⟨x, ?_⟩, ?_⟩
  · exact (schreierTransversalRightCosetAction_smul (X := X) hT
      (FreeGroup.inverseBasis X x) t).trans (by
        simpa only [FreeGroup.inverseBasis_apply, inv_inv, p, coe_back] using
          schreierRepresentative_eq_prefixParent_of_cancels (X := X) hT t.property hw hlast)
  · exact (mem_schreierPrefixTree_inr_iff (X := X) (hT := hT)).2
      ⟨hw, rfl, hlast⟩
theorem

schreierPrefixTree_parent_edge_of_ne_one

L233 ↗
ReidemeisterSchreier.Discrete.OpenSubgroups.schreierPrefixTree_parent_edge_of_ne_one
Documentation

Every nonroot vertex has a Schreier-tree edge from its canonical prefix parent.

Source context 5 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierPrefixTrees
open scoped Pointwise
open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj
  Quiver _root_.ReidemeisterSchreier.FreeGroup
Lean source · full declaration
theorem schreierPrefixTree_parent_edge_of_ne_one {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    (t : T) (ht1 : (t : FreeGroup X) ≠ 1) :
    letI := schreierTransversalRightCosetAction (X := X) hT
    letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
      FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
    let p : T := ⟨FreeGroup.prefixParent (t : FreeGroup X),
      prefixParent_mem_of_mem (X := X) hT t.property⟩
    let pA : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) :=
      show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from
        ((p : T) : ActionCategory (FreeGroup X) T)
    let tA : IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) :=
      show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from
        ((t : T) : ActionCategory (FreeGroup X) T)
    ∃ e : @Quiver.Hom
        (Quiver.Symmetrify (IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T)))
        inferInstance pA tA,
      e ∈ schreierPrefixTree (X := X) hT pA tA := by
  let edge := FreeGroup.prefixParentEdgeOfNeOne (X := X) (t := (t : FreeGroup X)) ht1
  have hlastEdge :
      FreeGroup.lastLetter? (t : FreeGroup X) = some edge.letter :=
    FreeGroup.prefixParentEdgeOfNeOne_lastLetter? (X := X) (t := (t : FreeGroup X)) ht1
  rcases hletter : edge.letter with ⟨x, b⟩
  cases b with
  | false =>
      have hlast? :
          FreeGroup.lastLetter? (t : FreeGroup X) = some ((x, false) : Internal.SignedLetter X)
              := by
        simpa [edge, hletter] using hlastEdge
      rcases (Internal.FreeGroupWord.FreeGroup.lastLetter?_eq_some_iff
        (g := (t : FreeGroup X)) (y := ((x, false) : Internal.SignedLetter X))).1 hlast? with
        ⟨hw, hlast⟩
      exact schreierPrefixTree_edge_of_last_neg (X := X) hT t hw hlast
  | true =>
      have hlast? :
          FreeGroup.lastLetter? (t : FreeGroup X) = some ((x, true) : Internal.SignedLetter X) := by
        simpa [edge, hletter] using hlastEdge
      rcases (Internal.FreeGroupWord.FreeGroup.lastLetter?_eq_some_iff
        (g := (t : FreeGroup X)) (y := ((x, true) : Internal.SignedLetter X))).1 hlast? with
        ⟨hw, hlast⟩
      exact schreierPrefixTree_edge_of_last_pos (X := X) hT t hw hlast
lemma

schreierPrefixTree_root_or_arrow

L277 ↗
ReidemeisterSchreier.Discrete.OpenSubgroups.schreierPrefixTree_root_or_arrow
Documentation

Every Schreier-tree vertex is either the identity root or the target of an incoming edge.

Source context 5 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierPrefixTrees
open scoped Pointwise
open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj
  Quiver _root_.ReidemeisterSchreier.FreeGroup
Lean source · full declaration
lemma schreierPrefixTree_root_or_arrow {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    letI := schreierTransversalRightCosetAction (X := X) hT
    letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
      FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
    ∀ b : schreierPrefixTree (X := X) hT,
      b = ((((⟨(1 : FreeGroup X), hT.2.1⟩ : T) : ActionCategory (FreeGroup X) T) :
        schreierPrefixTree (X := X) hT)) ∨
      ∃ a, Nonempty (a ⟶ b) := by
  let _ := schreierTransversalRightCosetAction (X := X) hT
  intro b
  let tb : T := b.back
  by_cases hb1 : (tb : FreeGroup X) = 1
  · left
    apply actionCategory_eq_of_back_eq
    exact Subtype.ext hb1
  · right
    let pb : T := ⟨FreeGroup.prefixParent (tb : FreeGroup X),
      prefixParent_mem_of_mem (X := X) hT tb.property⟩
    refine ⟨((pb : T) : ActionCategory (FreeGroup X) T), ?_⟩
    rcases schreierPrefixTree_parent_edge_of_ne_one (X := X) hT tb hb1 with ⟨e, he⟩
    exact ⟨⟨e, he⟩⟩
lemma

schreierPrefixTree_unique_arrow

L302 ↗
ReidemeisterSchreier.Discrete.OpenSubgroups.schreierPrefixTree_unique_arrow
Documentation

Two Schreier-tree arrows with the same target have equal sources and agree as quiver edges.

Source context 5 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierPrefixTrees
open scoped Pointwise
open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj
  Quiver _root_.ReidemeisterSchreier.FreeGroup
Lean source · full declaration
lemma schreierPrefixTree_unique_arrow {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    letI := schreierTransversalRightCosetAction (X := X) hT
    letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
      FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
    ∀ ⦃a b c : schreierPrefixTree (X := X) hT⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f := by
  let _ := schreierTransversalRightCosetAction (X := X) hT
  intro a b c e f
  rcases e with ⟨e0, hme⟩
  rcases f with ⟨f0, hmf⟩
  have hme0 := hme
  have hmf0 := hmf
  rcases hme with ⟨hwe, hsrca, hlast_e⟩
  rcases hmf with ⟨hwf, hsrcb, hlast_f⟩
  let tc : T := c.back
  let pc : T := ⟨FreeGroup.prefixParent (tc : FreeGroup X),
    prefixParent_mem_of_mem (X := X) hT tc.property⟩
  have ha_back : a.back = pc := by
    simpa [tc, pc] using hsrca
  have hb_back : b.back = pc := by
    simpa [tc, pc] using hsrcb
  have hab : a = b :=
    actionCategory_eq_of_back_eq (ha_back.trans hb_back.symm)
  refine ⟨hab, ?_⟩
  subst hab
  have hUnder : e0 = f0 := by
    cases e0 with
    | inl ge =>
        cases f0 with
        | inl gf =>
            have hxeq : ge.1 = gf.1 := by
              have hlast : (ge.1, true) = (gf.1, true) := by
                calc
                  (ge.1, true) = (FreeGroup.toWord (tc : FreeGroup X)).getLast hwe := by
                    simpa [tc] using hlast_e.symm
                  _ = (gf.1, true) := by simpa [tc] using hlast_f
              exact congrArg Prod.fst hlast
            have hgegf : ge = gf := Subtype.ext hxeq
            subst hgegf
            rfl
        | inr gf =>
            exfalso
            have hlast : (ge.1, true) = (gf.1, false) := by
              calc
                (ge.1, true) = (FreeGroup.toWord (tc : FreeGroup X)).getLast hwe := by
                  simpa [tc] using hlast_e.symm
                _ = (gf.1, false) := by simpa [tc] using hlast_f
            have : (true : Bool) = false := congrArg Prod.snd hlast
            cases this
    | inr ge =>
        cases f0 with
        | inl gf =>
            exfalso
            have hlast : (ge.1, false) = (gf.1, true) := by
              calc
                (ge.1, false) = (FreeGroup.toWord (tc : FreeGroup X)).getLast hwe := by
                  simpa [tc] using hlast_e.symm
                _ = (gf.1, true) := by simpa [tc] using hlast_f
            have : (false : Bool) = true := congrArg Prod.snd hlast
            cases this
        | inr gf =>
            have hxeq : ge.1 = gf.1 := by
              have hlast : (ge.1, false) = (gf.1, false) := by
                calc
                  (ge.1, false) = (FreeGroup.toWord (tc : FreeGroup X)).getLast hwe := by
                    simpa [tc] using hlast_e.symm
                  _ = (gf.1, false) := by simpa [tc] using hlast_f
              exact congrArg Prod.fst hlast
            have hgegf : ge = gf := Subtype.ext hxeq
            subst hgegf
            rfl
  have hEq : (⟨e0, hme0⟩ : a ⟶ c) = ⟨f0, hmf0⟩ := by
    apply Subtype.ext
    exact hUnder
  cases hEq
  rfl
lemma

schreierPrefixTree_height_lt

L381 ↗
ReidemeisterSchreier.Discrete.OpenSubgroups.schreierPrefixTree_height_lt
Documentation

The reduced-word length strictly increases along every oriented Schreier-tree edge.

Source context 5 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierPrefixTrees
open scoped Pointwise
open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj
  Quiver _root_.ReidemeisterSchreier.FreeGroup
Lean source · full declaration
lemma schreierPrefixTree_height_lt {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    letI := schreierTransversalRightCosetAction (X := X) hT
    letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
      FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
    ∀ ⦃a b : schreierPrefixTree (X := X) hT⦄ (_ : a ⟶ b),
      (FreeGroup.toWord ((a.back : T) : FreeGroup X)).length <
      (FreeGroup.toWord ((b.back : T) : FreeGroup X)).length := by
  let _ := schreierTransversalRightCosetAction (X := X) hT
  intro a b e
  rcases e with ⟨_, hmem⟩
  rcases hmem with ⟨hw, hsrc, _⟩
  let tb : T := b.back
  have htb1 : (tb : FreeGroup X) ≠ 1 := by
    exact mt (FreeGroup.toWord_eq_nil_iff.mpr) hw
  have hlt :=
    Internal.FreeGroupWord.FreeGroup.toWord_length_prefixParent_lt (t := (tb : FreeGroup X)) htb1
  have hsrc' : a.back =
      ⟨FreeGroup.prefixParent (tb : FreeGroup X),
        prefixParent_mem_of_mem (X := X) hT tb.property⟩ := by
    simpa [tb] using hsrc
  exact (congrArg (fun t : T => (FreeGroup.toWord (t : FreeGroup X)).length) hsrc').trans_lt hlt
instance

schreierPrefixTree_arborescence

L406 ↗
ReidemeisterSchreier.Discrete.OpenSubgroups.schreierPrefixTree_arborescence
Documentation

The prefix-closed Schreier quiver is an arborescence rooted at the identity representative.

Source context 5 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierPrefixTrees
open scoped Pointwise
open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj
  Quiver _root_.ReidemeisterSchreier.FreeGroup
Lean source · full declaration
instance schreierPrefixTree_arborescence {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    letI := schreierTransversalRightCosetAction (X := X) hT
    letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
      FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
    Quiver.Arborescence (schreierPrefixTree (X := X) hT) := by
  letI := schreierTransversalRightCosetAction (X := X) hT
  refine Quiver.arborescenceMk (V := schreierPrefixTree (X := X) hT)
    ((⟨(1 : FreeGroup X), hT.2.1⟩ : T) : ActionCategory (FreeGroup X) T)
    (fun a =>
      (FreeGroup.toWord ((a.back : T) : FreeGroup X)).length)
    ?_ ?_ ?_
  · intro a b e
    exact schreierPrefixTree_height_lt (X := X) hT e
  · intro a b c e f
    exact schreierPrefixTree_unique_arrow (X := X) hT e f
  · intro b
    exact schreierPrefixTree_root_or_arrow (X := X) hT b
theorem

closure_schreierGeneratorSet_eq_top

L430 ↗
ReidemeisterSchreier.Discrete.OpenSubgroups.closure_schreierGeneratorSet_eq_top
Documentation

The classical Schreier generators attached to a right Schreier transversal algebraically generate the subgroup.

Source context 5 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierPrefixTrees
open scoped Pointwise
open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj
  Quiver _root_.ReidemeisterSchreier.FreeGroup
Lean source · statement
theorem closure_schreierGeneratorSet_eq_top {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    Subgroup.closure (schreierGeneratorSet (X := X) hT : Set L) = ⊤
def

schreierRootEndMulEquiv

L475 ↗
ReidemeisterSchreier.Discrete.OpenSubgroups.schreierRootEndMulEquiv
Documentation

The root vertex group in the Schreier action groupoid is canonically the subgroup L, via the action label of an endomorphism.

Source context 5 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierPrefixTrees
open scoped Pointwise
open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj
  Quiver _root_.ReidemeisterSchreier.FreeGroup
Lean source · full declaration
def schreierRootEndMulEquiv {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    letI := schreierTransversalRightCosetAction (X := X) hT
    CategoryTheory.End
      (show ActionCategory (FreeGroup X) T from ((⟨(1 : FreeGroup X), hT.2.1⟩ : T) :
        ActionCategory (FreeGroup X) T)) ≃* L := by
  let rootT : T := ⟨(1 : FreeGroup X), hT.2.1⟩
  refine
    { toFun := fun g => ⟨g.1, ?_⟩
      invFun := fun l => ⟨l.1, ?_⟩
      left_inv := ?_
      right_inv := ?_
      map_mul' := ?_ }
  · let gF : FreeGroup X := g.1
    have hrep : schreierRepresentative (X := X) hT (gF⁻¹) = rootT := by
      simpa only [rootT, one_mul] using
        (schreierTransversalRightCosetAction_smul (X := X) hT gF rootT).symm.trans g.2
    have hmemInv : gF⁻¹ ∈ L := by
      have hm : gF⁻¹ *
          (((schreierRepresentative (X := X) hT (gF⁻¹) : T) : FreeGroup X))⁻¹ ∈ L :=
        hT.1.mul_inv_toRightFun_mem (gF⁻¹)
      simpa only [hrep, rootT, inv_one, mul_one] using hm
    simpa only [inv_inv] using L.inv_mem hmemInv
  · exact (schreierTransversalRightCosetAction_smul (X := X) hT l.1 rootT).trans
      (by simpa only [rootT, one_mul] using
        schreierRepresentative_eq_one_of_mem (X := X) hT (L.inv_mem l.2))
  · intro g
    rfl
  · intro l
    rfl
  · intro g h
    rfl
def

schreierLabelFunctor

L514 ↗
ReidemeisterSchreier.Discrete.OpenSubgroups.schreierLabelFunctor
Documentation

The cocycle functor on the Schreier action groupoid. It sends a morphism \(a\to b\) labelled by \(g\) to the subgroup element \(b g a^{-1}\), the inverse of the corresponding classical Schreier generator.

Source context 5 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierPrefixTrees
open scoped Pointwise
open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj
  Quiver _root_.ReidemeisterSchreier.FreeGroup
Lean source · full declaration
def schreierLabelFunctor {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    letI := schreierTransversalRightCosetAction (X := X) hT
    ActionCategory (FreeGroup X) T ⥤ CategoryTheory.SingleObj L := by
  letI := schreierTransversalRightCosetAction (X := X) hT
  refine
    { obj := fun _ => ()
      map := fun {a b} p => ?_
      map_id := ?_
      map_comp := ?_ }
  · let g : FreeGroup X := p.1
    refine ⟨Subtype.val b.back * g * (Subtype.val a.back)⁻¹, ?_⟩
    have hp : schreierRepresentative (X := X) hT
        (Subtype.val a.back * g⁻¹) = b.back := by
      simpa only [CategoryTheory.ActionCategory.back] using
        (schreierTransversalRightCosetAction_smul (X := X) hT g
          a.back).symm.trans p.2
    have hmem : Subtype.val a.back * g⁻¹ * (Subtype.val b.back)⁻¹ ∈ L := by
      have hmem0 : Subtype.val a.back * g⁻¹ *
          (((schreierRepresentative (X := X) hT
            (Subtype.val a.back * g⁻¹) : T) : FreeGroup X))⁻¹ ∈ L := by
        simpa [schreierRepresentative] using
          hT.1.mul_inv_toRightFun_mem (Subtype.val a.back * g⁻¹)
      rw [hp] at hmem0
      exact hmem0
    simpa [mul_assoc] using L.inv_mem hmem
  · intro a
    apply Subtype.ext
    change (Subtype.val a.back * (1 : FreeGroup X) * (Subtype.val a.back)⁻¹) = 1
    simp only [mul_one, mul_inv_cancel]
  · intro a b c p q
    let gp : FreeGroup X := p.1
    let gq : FreeGroup X := q.1
    apply Subtype.ext
    change (Subtype.val c.back * (gq * gp) * (Subtype.val a.back)⁻¹) =
        ((Subtype.val c.back * gq * (Subtype.val b.back)⁻¹) *
          (Subtype.val b.back * gp * (Subtype.val a.back)⁻¹))
    simp only [mul_assoc, inv_mul_cancel_left]
theorem

schreierLabelFunctor_map_of

L555 ↗
ReidemeisterSchreier.Discrete.OpenSubgroups.schreierLabelFunctor_map_of
Documentation

The Schreier label functor respects the corresponding map of generators.

Source context 5 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierPrefixTrees
open scoped Pointwise
open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj
  Quiver _root_.ReidemeisterSchreier.FreeGroup
Lean source · full declaration
theorem schreierLabelFunctor_map_of {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    letI := schreierTransversalRightCosetAction (X := X) hT
    letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
      FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
    ∀ {a b : ActionCategory (FreeGroup X) T}
      (e : ((show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from a) ⟶ b)),
      ((schreierLabelFunctor (X := X) hT).map (IsFreeGroupoid.of e) : L) =
        (schreierGenerator (X := X) hT ((a.back : T) : FreeGroup X) e.1)⁻¹ := by
  let _ := schreierTransversalRightCosetAction (X := X) hT
  intro a b e
  have hb : schreierRepresentative (X := X) hT
      (Subtype.val a.back * FreeGroup.of e.1) = b.back := by
    simpa only [FreeGroup.inverseBasis_apply, inv_inv, CategoryTheory.ActionCategory.back] using
      (schreierTransversalRightCosetAction_smul (X := X) hT
        (FreeGroup.inverseBasis X e.1) a.back).symm.trans e.property
  apply Subtype.ext
  change (Subtype.val b.back * (FreeGroup.of e.1)⁻¹ * (Subtype.val a.back)⁻¹) =
      ((((schreierGenerator (X := X) hT (Subtype.val a.back) e.1 : L) :
        FreeGroup X))⁻¹)
  simp only [mul_assoc, schreierGenerator, hb, mul_inv_rev, inv_inv]
lemma

schreierLabelFunctor_map_of_eq_one_of_mem_tree

L579 ↗
ReidemeisterSchreier.Discrete.OpenSubgroups.schreierLabelFunctor_map_of_eq_one_of_mem_tree
Documentation

The corresponding Schreier representative satisfies the stated membership criterion.

Source context 5 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierPrefixTrees
open scoped Pointwise
open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj
  Quiver _root_.ReidemeisterSchreier.FreeGroup
Lean source · full declaration
lemma schreierLabelFunctor_map_of_eq_one_of_mem_tree {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    letI := schreierTransversalRightCosetAction (X := X) hT
    letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
      FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
    ∀ {a b : ActionCategory (FreeGroup X) T}
      (e : ((show IsFreeGroupoid.Generators (ActionCategory (FreeGroup X) T) from a) ⟶ b)),
      e ∈ Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT) a b →
        (schreierLabelFunctor (X := X) hT).map (IsFreeGroupoid.of e) = (1 : L) := by
  let _ := schreierTransversalRightCosetAction (X := X) hT
  intro a b e he
  refine (schreierLabelFunctor_map_of (X := X) hT e).trans ?_
  rcases he with htree | htree
  · rcases htree with ⟨hw, hsrc, hlast⟩
    let tb : T := b.back
    have hsrc' : a.back = ⟨FreeGroup.prefixParent (tb : FreeGroup X),
        prefixParent_mem_of_mem (X := X) hT tb.property⟩ := by
      simpa [tb] using hsrc
    have hgen :
        schreierGenerator (X := X) hT
          (FreeGroup.prefixParent (tb : FreeGroup X)) e.1 = (1 : L) := by
      exact schreierGenerator_eq_one_of_prefixParent_last_pos (X := X) hT
        (t := (tb : FreeGroup X)) tb.property hw hlast
    have hgen' :
        schreierGenerator (X := X) hT (Subtype.val a.back) e.1 = (1 : L) := by
      simpa [hsrc'] using hgen
    exact inv_eq_one.mpr hgen'
  · rcases htree with ⟨hw, hsrc, hlast⟩
    let ta : T := a.back
    have hgen : schreierGenerator (X := X) hT (ta : FreeGroup X) e.1 = (1 : L) := by
      exact schreierGenerator_eq_one_of_cancels (X := X) hT
        (t := (ta : FreeGroup X)) ta.property hw hlast
    exact inv_eq_one.mpr (by simpa [ta] using hgen)
lemma

schreierGenerator_eq_one_implies_mem_prefixTree

L615 ↗
ReidemeisterSchreier.Discrete.OpenSubgroups.schreierGenerator_eq_one_implies_mem_prefixTree
Documentation

The Schreier generator is trivial exactly in the corresponding subgroup-membership case.

Source context 5 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierPrefixTrees
open scoped Pointwise
open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj
  Quiver _root_.ReidemeisterSchreier.FreeGroup
Lean source · full declaration
lemma schreierGenerator_eq_one_implies_mem_prefixTree {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    letI := schreierTransversalRightCosetAction (X := X) hT
    letI : IsFreeGroupoid (CategoryTheory.ActionCategory (FreeGroup X) T) :=
      FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
    ∀ {a b : CategoryTheory.ActionCategory (FreeGroup X) T}
      (e :
        (show IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T) from
          a) ⟶ b),
      schreierGenerator (X := X) hT (a.back : FreeGroup X) e.1 = 1 →
        e ∈ Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT) a b := by
  let _ := schreierTransversalRightCosetAction (X := X) hT
  intro a b e hgen
  let ta : T := a.back
  have hrep : schreierRepresentative (X := X) hT
      ((((ta : T) : FreeGroup X)) * FreeGroup.of e.1) = b.back := by
    simpa only [FreeGroup.inverseBasis_apply, inv_inv, ta,
      CategoryTheory.ActionCategory.back] using
      (schreierTransversalRightCosetAction_smul (X := X) hT
        (FreeGroup.inverseBasis X e.1) a.back).symm.trans e.property
  have hraw :
      (((schreierRepresentative (X := X) hT
          ((((ta : T) : FreeGroup X)) * FreeGroup.of e.1) : T) : FreeGroup X)) =
        ((ta : T) : FreeGroup X) * FreeGroup.of e.1 := by
    exact (schreierGenerator_eq_one_iff (X := X) (hT := hT)
      (t := ((ta : T) : FreeGroup X)) (x := e.1)).mp hgen
  by_cases hcancel : ∃ hw : FreeGroup.toWord ((ta : T) : FreeGroup X) ≠ [],
      (FreeGroup.toWord ((ta : T) : FreeGroup X)).getLast hw = (e.1, false)
  · rcases hcancel with ⟨hw, hlast⟩
    have hb : Subtype.val b.back =
        FreeGroup.prefixParent ((ta : T) : FreeGroup X) := by
      calc
        Subtype.val b.back
            = (((schreierRepresentative (X := X) hT
                ((((ta : T) : FreeGroup X)) * FreeGroup.of e.1) : T) : FreeGroup X)) := by
                  exact congrArg Subtype.val hrep.symm
        _ = ((ta : T) : FreeGroup X) * FreeGroup.of e.1 := hraw
        _ = FreeGroup.prefixParent ((ta : T) : FreeGroup X) :=
              Internal.FreeGroupWord.FreeGroup.mul_of_eq_prefixParent_of_cancels
                ((ta : T) : FreeGroup X) e.1 hw hlast
    refine Or.inr ?_
    refine ⟨hw, ?_⟩
    constructor
    · apply Subtype.ext
      simpa [ta] using hb
    · simpa [ta] using hlast
  · have hword : FreeGroup.toWord (((ta : T) : FreeGroup X) * FreeGroup.of e.1) =
        FreeGroup.toWord ((ta : T) : FreeGroup X) ++ [(e.1, true)] :=
      Internal.FreeGroupWord.FreeGroup.toWord_mul_of_of_not_cancels
        ((ta : T) : FreeGroup X) e.1 hcancel
    have hb : Subtype.val b.back = ((ta : T) : FreeGroup X) * FreeGroup.of e.1 := by
      calc
        Subtype.val b.back
            = (((schreierRepresentative (X := X) hT
                ((((ta : T) : FreeGroup X)) * FreeGroup.of e.1) : T) : FreeGroup X)) := by
                  exact congrArg Subtype.val hrep.symm
        _ = ((ta : T) : FreeGroup X) * FreeGroup.of e.1 := hraw
    have hbw : FreeGroup.toWord (Subtype.val b.back) =
        FreeGroup.toWord ((ta : T) : FreeGroup X) ++ [(e.1, true)] := by
      simpa [hb] using hword
    have hbw_ne : FreeGroup.toWord (Subtype.val b.back) ≠ [] := by
      rw [hbw]
      simp only [ne_eq, List.append_eq_nil_iff, FreeGroup.toWord_eq_nil_iff,
  List.cons_ne_self, and_false, not_false_eq_true]
    have hprefix : FreeGroup.prefixParent (Subtype.val b.back) =
        ((ta : T) : FreeGroup X) := by
      apply FreeGroup.toWord_injective
      rw [Internal.FreeGroupWord.FreeGroup.toWord_prefixParent, hbw]
      simp only [ne_eq, List.cons_ne_self, not_false_eq_true,
          List.dropLast_append_of_ne_nil,
  List.dropLast_singleton, List.append_nil]
    refine Or.inl ?_
    refine ⟨hbw_ne, ?_⟩
    constructor
    · apply Subtype.ext
      exact hprefix.symm
    · simp only [hbw, ne_eq, List.cons_ne_self, not_false_eq_true,
  List.getLast_append_of_ne_nil, List.getLast_singleton]
theorem

schreierGenerator_eq_one_iff_mem_prefixTree

L699 ↗
ReidemeisterSchreier.Discrete.OpenSubgroups.schreierGenerator_eq_one_iff_mem_prefixTree
Documentation

A generator edge lies in the symmetrized prefix tree exactly when the associated Schreier generator is trivial.

Source context 5 commands

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

universe u
namespace ReidemeisterSchreier.Discrete.OpenSubgroups
section SchreierPrefixTrees
open scoped Pointwise
open CategoryTheory CategoryTheory.ActionCategory CategoryTheory.SingleObj
  Quiver _root_.ReidemeisterSchreier.FreeGroup
Lean source · full declaration
theorem schreierGenerator_eq_one_iff_mem_prefixTree {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    {hT : IsRightSchreierTransversal (X := X) L T} :
    letI := schreierTransversalRightCosetAction (X := X) hT
    letI : IsFreeGroupoid (CategoryTheory.ActionCategory (FreeGroup X) T) :=
      FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
    ∀ {a b : CategoryTheory.ActionCategory (FreeGroup X) T}
      {e :
        (show IsFreeGroupoid.Generators (CategoryTheory.ActionCategory (FreeGroup X) T) from
          a) ⟶ b},
      schreierGenerator (X := X) hT (a.back : FreeGroup X) e.1 = 1 ↔
        e ∈ Quiver.wideSubquiverSymmetrify (schreierPrefixTree (X := X) hT) a b := by
  let _ := schreierTransversalRightCosetAction (X := X) hT
  intro a b e
  constructor
  · exact schreierGenerator_eq_one_implies_mem_prefixTree (X := X) hT e
  · intro he
    have hmap :=
      schreierLabelFunctor_map_of_eq_one_of_mem_tree (X := X) hT e he
    exact inv_eq_one.mp
      ((schreierLabelFunctor_map_of (X := X) hT e).symm.trans hmap)

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