ReidemeisterSchreier.Groupoid

1 Theorem | 2 Lemma | 1 Definition

This module formalizes the groupoid version of the spanning-tree basis construction.

import

Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Imported by

ReidemeisterSchreier.Discrete.OpenSubgroups.Words.NielsenSchreierCompat

Definition IsFreeGroupoid.SpanningTree.endBasis GitHub

noncomputable def IsFreeGroupoid.SpanningTree.endBasis
    {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
    (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T] :
    FreeGroupBasis
      (((Quiver.wideSubquiverEquivSetTotal <| Quiver.wideSubquiverSymmetrify T)ᶜ : Set _))
      (End (show G from Quiver.root T)) := by
  classical
  refine FreeGroupBasis.ofUniqueLift
    (((Quiver.wideSubquiverEquivSetTotal <| Quiver.wideSubquiverSymmetrify T)ᶜ : Set _))
    (fun e => IsFreeGroupoid.SpanningTree.loopOfHom T (IsFreeGroupoid.of e.val.hom))
    ?_
  intro X _ f
  let f' : Quiver.Labelling (IsFreeGroupoid.Generators G) X := fun a b e =>
    if h : e ∈ Quiver.wideSubquiverSymmetrify T a b then 1 else f ⟨⟨a, b, e⟩, h⟩
  rcases IsFreeGroupoid.unique_lift f' with ⟨F', hF', uF'⟩
  refine ⟨F'.mapEnd _, ?_, ?_⟩
  · suffices
      ∀ {x y} (q : x ⟶ y),
        F'.map (IsFreeGroupoid.SpanningTree.loopOfHom T q) = (F'.map q : X) by
      rintro ⟨⟨a, b, e⟩, h⟩
      erw [Functor.mapEnd_apply]
      rw [this, hF']
      exact dif_neg h
    intro x y q
    suffices
      ∀ {a} (p : Quiver.Path (Quiver.root T) a),
        F'.map (IsFreeGroupoid.SpanningTree.homOfPath T p) = 1 by
      simp only [this, IsFreeGroupoid.SpanningTree.treeHom,
        CategoryTheory.SingleObj.comp_as_mul, inv_as_inv,
        IsFreeGroupoid.SpanningTree.loopOfHom, inv_one, mul_one, one_mul,
        Functor.map_inv, Functor.map_comp]
    intro a p
    induction p with
    | nil =>
        rw [IsFreeGroupoid.SpanningTree.homOfPath, F'.map_id, id_as_one]
    | cons p e ih =>
        rw [IsFreeGroupoid.SpanningTree.homOfPath, F'.map_comp,
          CategoryTheory.SingleObj.comp_as_mul, ih, mul_one]
        rcases e with ⟨e | e, eT⟩
        · rw [hF']
          have he : e ∈ Quiver.wideSubquiverSymmetrify T _ _ := by
            change T _ _ (Sum.inl e) ∨ T _ _ (Sum.inr e)
            exact Or.inl eT
          simp only [he, ↓reduceDIte, f']
        · rw [F'.map_inv, inv_as_inv, inv_eq_one, hF']
          have he : e ∈ Quiver.wideSubquiverSymmetrify T _ _ := by
            change T _ _ (Sum.inl e) ∨ T _ _ (Sum.inr e)
            exact Or.inr eT
          simp only [he, ↓reduceDIte, f']
  · intro E hE
    ext x
    change E x = F'.map x
    suffices
      (IsFreeGroupoid.SpanningTree.functorOfMonoidHom T E).map x = F'.map x by
      change E (IsFreeGroupoid.SpanningTree.loopOfHom T x) = F'.map x at this
      have hroot : IsFreeGroupoid.SpanningTree.treeHom T (Quiver.root T) = 𝟙 _ := by
        rw [IsFreeGroupoid.SpanningTree.treeHom_eq T Quiver.Path.nil]
        rfl
      have hx : E (IsFreeGroupoid.SpanningTree.loopOfHom T x) = E x := by
        have hloop :
            IsFreeGroupoid.SpanningTree.loopOfHom T x = x ≫ 𝟙 _ := by
          simp only [IsFreeGroupoid.SpanningTree.loopOfHom, hroot, IsIso.inv_id,
            Category.id_comp]
          rfl
        exact (congrArg E hloop).trans (congrArg E (Category.comp_id x))
      exact hx.symm.trans this
    congr
    apply uF'
    intro a b e
    change E (IsFreeGroupoid.SpanningTree.loopOfHom T _) = dite _ _ _
    split_ifs with h
    · rw [IsFreeGroupoid.SpanningTree.loopOfHom_eq_id T e h, ← End.one_def, E.map_one]
    · exact hE ⟨⟨a, b, e⟩, h⟩

The complement of a chosen spanning tree in a free connected groupoid gives an explicit free basis for the root vertex group; equivalently, the non-tree edges form the basis of the fundamental groupoid at the root.

Lemma IsFreeGroupoid.SpanningTree.map_loopOfHom_eq_map GitHub

lemma IsFreeGroupoid.SpanningTree.map_loopOfHom_eq_map
    {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
    (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T]
    {X : Type u} [Group X] (F : G ⥤ CategoryTheory.SingleObj X)
    (hTree : ∀ {a b : IsFreeGroupoid.Generators G} (e : a ⟶ b),
      e ∈ Quiver.wideSubquiverSymmetrify T a b → F.map (IsFreeGroupoid.of e) = 1) :
    ∀ {a b} (q : a ⟶ b), F.map (IsFreeGroupoid.SpanningTree.loopOfHom T q) = (F.map q : X)

The spanning-tree loop map agrees with the corresponding homomorphism map.

Show proof

Theorem FreeGroupBasis.ofUniqueLift_apply GitHub

@[simp] theorem FreeGroupBasis.ofUniqueLift_apply {X G : Type u} [Group G] (of : X → G)
    (h : ∀ {H : Type u} [Group H] (f : X → H), ∃! F : G →* H, ∀ a, F (of a) = f a)
    (x : X) :
    FreeGroupBasis.ofUniqueLift X of h x = of x

The Schreier generator or pair map is evaluated by the chosen section and coset representative.

Show proof

Lemma IsFreeGroupoid.SpanningTree.endBasis_apply GitHub

@[simp] lemma IsFreeGroupoid.SpanningTree.endBasis_apply
    {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
    (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T]
    (e : (((Quiver.wideSubquiverEquivSetTotal <| Quiver.wideSubquiverSymmetrify T)ᶜ : Set _))) :
    IsFreeGroupoid.SpanningTree.endBasis T e =
      IsFreeGroupoid.SpanningTree.loopOfHom T (IsFreeGroupoid.of e.1.hom)

The Schreier generator or pair map is evaluated by the chosen section and coset representative.

Show proof

ReidemeisterSchreier.Groupoid

Declarations