ReidemeisterSchreier.Discrete.OpenSubgroups.PrefixTree

noncomputable 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
  letI : IsFreeGroupoid (ActionCategory (FreeGroup X) T) :=
    FreeGroupBasis.actionGroupoidIsFree (FreeGroup.inverseBasis X)
  exact fun a b =>
    { e |
        ∃ hw : FreeGroup.toWord (((show ActionCategory (FreeGroup X) T from b).back : T) :
            FreeGroup X) ≠ [],
          let tb : T := (show ActionCategory (FreeGroup X) T from b).back
          let pb : T := ⟨FreeGroup.prefixParent (tb : FreeGroup X),
            prefixParent_mem_of_mem (X := X) hT tb.property⟩
          (show ActionCategory (FreeGroup X) T from 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) }

noncomputable 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
  letI := schreierTransversalRightCosetAction (X := X) hT
  let rootT : T := ⟨(1 : FreeGroup X), hT.2.1⟩
  let eStab : MulAction.stabilizer (FreeGroup X) rootT ≃* L := by
    refine MulEquiv.subgroupCongr ?_
    ext g
    constructor
    · intro hg
      have hfix : g • rootT = rootT := hg
      have hrep : schreierRepresentative (X := X) hT (g⁻¹) = rootT := by
        simpa [rootT] using (schreierTransversalRightCosetAction_smul (X := X) hT g rootT).symm.trans hfix
      have hmemInv : g⁻¹ ∈ L := by
        have hm : g⁻¹ *
            (((schreierRepresentative (X := X) hT (g⁻¹) : T) : FreeGroup X))⁻¹ ∈ L :=
          hT.1.mul_inv_toRightFun_mem (g⁻¹)
        simpa [hrep, rootT] using hm
      simpa using L.inv_mem hmemInv
    · intro hg
      change g • rootT = rootT
      rw [schreierTransversalRightCosetAction_smul (X := X) hT g rootT]
      simpa [rootT] using schreierRepresentative_eq_one_of_mem (X := X) hT (L.inv_mem hg)
  let eSubmonoid : MulAction.stabilizerSubmonoid (FreeGroup X) rootT ≃* L :=
    { toFun := fun g => eStab ⟨g.1, g.2⟩
      invFun := fun l => ⟨(eStab.symm l).1, (eStab.symm l).2⟩
      left_inv := by intro g; rfl
      right_inv := by intro l; rfl
      map_mul' := by intro g h; rfl }
  exact (CategoryTheory.ActionCategory.stabilizerIsoEnd (FreeGroup X) rootT).symm.trans eSubmonoid

noncomputable 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 ⟨((b.back : T) : FreeGroup X) * g * (((a.back : T) : FreeGroup X))⁻¹, ?_⟩
    have hp : schreierRepresentative (X := X) hT
        ((((a.back : T) : FreeGroup X)) * g⁻¹) = b.back := by
      rw [← schreierTransversalRightCosetAction_smul (X := X) hT g a.back]
      exact p.2
    have hmem : (((a.back : T) : FreeGroup X)) * g⁻¹ *
        (((b.back : T) : FreeGroup X))⁻¹ ∈ L := by
      have hmem0 : (((a.back : T) : FreeGroup X)) * g⁻¹ *
          (((schreierRepresentative (X := X) hT
            ((((a.back : T) : FreeGroup X)) * g⁻¹) : T) : FreeGroup X))⁻¹ ∈ L := by
        simpa [schreierRepresentative] using
          hT.1.mul_inv_toRightFun_mem ((((a.back : T) : FreeGroup X)) * g⁻¹)
      rw [hp] at hmem0
      exact hmem0
    simpa [mul_assoc] using L.inv_mem hmem
  · intro a
    apply Subtype.ext
    change (((a.back : T) : FreeGroup X) * (1 : FreeGroup X) *
        (((a.back : T) : FreeGroup X))⁻¹) = 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 (((c.back : T) : FreeGroup X) * (gq * gp) *
        (((a.back : T) : FreeGroup X))⁻¹) =
        ((((c.back : T) : FreeGroup X) * gq * (((b.back : T) : FreeGroup X))⁻¹) *
          (((b.back : T) : FreeGroup X) * gp * (((a.back : T) : FreeGroup X))⁻¹))
    simp only [mul_assoc, inv_mul_cancel_left]