FreeBasis.lean

def FreeGroupBasis.actionGroupoidGeneratorTotalEquiv
    {ι G A : Type u} [Group G] [MulAction G A] (b : FreeGroupBasis ι G) :
    letI : IsFreeGroupoid (CategoryTheory.ActionCategory G A) :=
      FreeGroupBasis.actionGroupoidIsFree b
    Quiver.Total (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory G A)) ≃ A × ι := by
  refine
    { toFun := fun e =>
        ((@Quiver.Total.left (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory G A))
            (FreeGroupBasis.actionGroupoidIsFree b).quiverGenerators e).back,
          (@Quiver.Total.hom (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory G A))
            (FreeGroupBasis.actionGroupoidIsFree b).quiverGenerators e).1)
      invFun := fun ai =>
        @Quiver.Total.mk (IsFreeGroupoid.Generators (CategoryTheory.ActionCategory G A))
          (FreeGroupBasis.actionGroupoidIsFree b).quiverGenerators
          (ai.1 : CategoryTheory.ActionCategory G A)
          ((b ai.2 • ai.1 : A) : CategoryTheory.ActionCategory G A) ⟨ai.2, rfl⟩
      left_inv := ?_
      right_inv := ?_ }
  · intro e
    cases e with
    | mk left right hom =>
        induction left with
        | mk a =>
            induction right with
            | mk a' =>
                cases hom with
                | mk i hi =>
                    dsimp
                    cases hi
                    rfl
  · intro ai
    rfl

abbrev schreierComplementEdges
    {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) : Type u

def schreierComplementEdgesBasis
    {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    FreeGroupBasis (schreierComplementEdges (X := X) hT) L

def schreierComplementEdgesEquivNontrivialPairs
    {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    schreierComplementEdges (X := X) hT ≃ NontrivialSchreierPair (X := X) hT

def nontrivialSchreierPairsEquivSchreierGeneratorSet
    {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    NontrivialSchreierPair (X := X) hT ≃ ↥(schreierGeneratorSet (X := X) hT)

def nontrivialSchreierPairBasis
    {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    FreeGroupBasis (NontrivialSchreierPair (X := X) hT) L

def nontrivialSchreierPairBasisEquiv
    {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    FreeGroup (NontrivialSchreierPair (X := X) hT) ≃* L

theorem nontrivialSchreierPairBasisEquiv_of
    {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    (p : NontrivialSchreierPair (X := X) hT) :
    nontrivialSchreierPairBasisEquiv (X := X) hT (FreeGroup.of p) =
      nontrivialSchreierPairBasis (X := X) hT p

theorem nontrivialSchreierPairsEquivSchreierGeneratorSet_apply
    {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T)
    (p : NontrivialSchreierPair (X := X) hT) :
    ((nontrivialSchreierPairsEquivSchreierGeneratorSet (X := X) hT p :
        ↥(schreierGeneratorSet (X := X) hT)) : L) =
      schreierGenerator (X := X) hT ((p.1.1 : T) : FreeGroup X) p.1.2

theorem schreierGenerator_injective_of_nontrivial
    {X : Type u} [DecidableEq X] {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    Function.Injective
      (nontrivialSchreierPairGenerator (X := X) hT)

theorem natCard_schreierTransversal_eq_index
    {X : Type u} [DecidableEq X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    (hT : IsRightSchreierTransversal (X := X) L T) :
    Nat.card T = Nat.card (Quotient (QuotientGroup.rightRel L))

theorem natCard_schreierComplementEdges_eq_rankTransform_direct
    {X : Type u} [DecidableEq X] [Finite X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    [Finite T]
    (hT : IsRightSchreierTransversal (X := X) L T) :
    Nat.card (schreierComplementEdges (X := X) hT) =
      _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card T)

theorem natCard_nontrivialSchreierPairs_eq_rankTransform_direct
    {X : Type u} [DecidableEq X] [Finite X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    [Finite T]
    (hT : IsRightSchreierTransversal (X := X) L T) :
    Nat.card (NontrivialSchreierPair (X := X) hT) =
      _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card T)

theorem natCard_nontrivialSchreierPairs_eq_rankTransform
    {X : Type u} [DecidableEq X] [Finite X]
    {L : Subgroup (FreeGroup X)} {T : Set (FreeGroup X)}
    [Finite (FreeGroup X ⧸ L)]
    (hT : IsRightSchreierTransversal (X := X) L T) :
    Nat.card (NontrivialSchreierPair (X := X) hT) =
      _root_.ReidemeisterSchreier.Schreier.rankTransform (Nat.card X) (Nat.card (FreeGroup X ⧸
          L))

theorem exists_freeBasis_subgroupOfFreeGroup_of_rankTransform
    {X : Type u} {L : Subgroup (FreeGroup X)} [Finite X] [Finite (FreeGroup X ⧸ L)] :
    ∃ Y : Type u, Nonempty (FreeGroupBasis Y L) ∧
      Nat.card Y = _root_.ReidemeisterSchreier.Schreier.rankTransform
        (Nat.card X) (Nat.card (FreeGroup X ⧸ L))