Transversals.lean

def IsRightSchreierTransversal {X : Type u} [DecidableEq X]
    (L : Subgroup (FreeGroup X)) (T : Set (FreeGroup X)) : Prop

def IsRightPartialSchreierTransversal {X : Type u} [DecidableEq X]
    (L : Subgroup (FreeGroup X)) (T : Set (FreeGroup X)) : Prop

theorem IsRightSchreierTransversal.isComplement {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    Subgroup.IsComplement (L : Set (FreeGroup X)) T

theorem IsRightSchreierTransversal.one_mem {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    (1 : FreeGroup X) ∈ T

theorem IsRightSchreierTransversal.prefix_closed {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    {t : FreeGroup X} (ht : t ∈ T) :
    freeGroupInitialSegments t ⊆ T

theorem IsRightPartialSchreierTransversal.one_mem {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightPartialSchreierTransversal (X := X) L T) :
    (1 : FreeGroup X) ∈ T

theorem IsRightPartialSchreierTransversal.prefix_closed {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightPartialSchreierTransversal (X := X) L T)
    {t : FreeGroup X} (ht : t ∈ T) :
    freeGroupInitialSegments t ⊆ T

theorem IsRightPartialSchreierTransversal.eq_of_rightQuotient_eq
    {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightPartialSchreierTransversal (X := X) L T)
    {a b : FreeGroup X} (ha : a ∈ T) (hb : b ∈ T)
    (hEq :
      (Quotient.mk'' a : Quotient (QuotientGroup.rightRel L)) =
        Quotient.mk'' b) :
    a = b

theorem prefixParent_mem_of_partial {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightPartialSchreierTransversal (X := X) L T)
    {t : FreeGroup X} (ht : t ∈ T) :
    FreeGroup.prefixParent t ∈ T

theorem chain_sUnion_isRightPartialSchreierTransversal
    {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {c : Set (Set (FreeGroup X))}
    (hcn : c.Nonempty)
    (hc :
      ∀ ⦃s⦄, s ∈ c → ∀ ⦃t⦄, t ∈ c → s ≠ t → s ⊆ t ∨ t ⊆ s)
    (hcPartial :
      ∀ ⦃s⦄, s ∈ c → IsRightPartialSchreierTransversal (X := X) L s) :
    IsRightPartialSchreierTransversal (X := X) L (⋃₀ c)

theorem exists_rightSchreierTransversal_of_partial {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T₀ : Set (FreeGroup X)}
    (hT₀ : IsRightPartialSchreierTransversal (X := X) L T₀) :
    ∃ T : Set (FreeGroup X), T₀ ⊆ T ∧ IsRightSchreierTransversal (X := X) L T

theorem exists_rightSchreierTransversal {X : Type u} [DecidableEq X]
    (L : Subgroup (FreeGroup X)) :
    ∃ T : Set (FreeGroup X), IsRightSchreierTransversal (X := X) L T

theorem generatorPower_sub_mem_of_rightQuotient_eq {X : Type u}
    {L : Subgroup (FreeGroup X)} (x : X) {m n : ℕ} (hmn : m ≤ n)
    (hEq :
      (Quotient.mk'' ((FreeGroup.of x) ^ m) : Quotient (QuotientGroup.rightRel L)) =
        Quotient.mk'' ((FreeGroup.of x) ^ n)) :
    (FreeGroup.of x) ^ (n - m) ∈ L

theorem isRightPartialSchreierTransversal_generatorPowers_of_minimalPower
    {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} (x : X) {N : ℕ}
    (hN : 0 < N)
    (hmin : ∀ m : ℕ, 0 < m → m < N → (FreeGroup.of x) ^ m ∉ L) :
    IsRightPartialSchreierTransversal (X := X) L
      (Set.range fun i : Fin N => (FreeGroup.of x) ^ (i : ℕ)) := by
  refine ⟨?_, ?_, ?_⟩
  · exact ⟨⟨0, hN⟩, by simp only [pow_zero]⟩
  · intro t ht u hu
    rcases ht with ⟨i, rfl⟩
    rcases hu with ⟨m, hm, rfl⟩
    have hm' : m ≤ (i : ℕ) := by
      simpa [FreeGroup.toWord_of_pow, List.length_replicate] using hm
    refine ⟨⟨m, lt_of_le_of_lt hm' i.2⟩, ?_⟩
    rw [FreeGroup.toWord_of_pow, List.take_replicate, min_eq_left hm',
      ← FreeGroup.toWord_of_pow, FreeGroup.mk_toWord]
  · intro a b ha hb hEq
    rcases ha with ⟨i, rfl⟩
    rcases hb with ⟨j, rfl⟩
    have hij : (i : ℕ) = j := by
      by_contra hij
      rcases lt_or_gt_of_ne hij with hijlt | hjilt
      · have hmem : (FreeGroup.of x) ^ ((j : ℕ) - i) ∈ L :=
          generatorPower_sub_mem_of_rightQuotient_eq (X := X) (L := L) x
            (Nat.le_of_lt hijlt) hEq
        exact hmin ((j : ℕ) - i) (Nat.sub_pos_of_lt hijlt)
          (lt_of_le_of_lt (Nat.sub_le _ _) j.2) hmem
      · have hmem : (FreeGroup.of x) ^ ((i : ℕ) - j) ∈ L :=
          generatorPower_sub_mem_of_rightQuotient_eq (X := X) (L := L) x
            (Nat.le_of_lt hjilt) hEq.symm
        exact hmin ((i : ℕ) - j) (Nat.sub_pos_of_lt hjilt)
          (lt_of_le_of_lt (Nat.sub_le _ _) i.2) hmem
    have hij' : i = j := Fin.ext hij
    subst hij'
    rfl

instance rightCosetLeftMulActionByInverse {X : Type u} (L : Subgroup (FreeGroup X)) :
    MulAction (FreeGroup X) (Quotient (QuotientGroup.rightRel L))

theorem rightCosetLeftMulActionByInverse_mk_smul {X : Type u}
    (L : Subgroup (FreeGroup X)) (g a : FreeGroup X) :
    g • (Quotient.mk'' a : Quotient (QuotientGroup.rightRel L)) =
      Quotient.mk'' (a * g⁻¹)