ProCGroups.ReidemeisterSchreier.Groupoid

6 Theorems | 1 Lemma | 5 Definitions | 6 Abbreviations

This module rebuilds the spanning-tree loop construction using public conversion functions between mathlib's vertex type synonyms. No private-root declaration or backward elaboration option enters the public API.

import

Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Imported by

ProCGroups.ReidemeisterSchreier.Discrete.OpenSubgroups.Words.NielsenSchreierCompat

Abbreviation ReidemeisterSchreier.Groupoid.generatorObject

abbrev generatorObject
    {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
    (a : IsFreeGroupoid.Generators G) : G :=
  a

A generator-quiver vertex viewed in the ambient groupoid.

Abbreviation ReidemeisterSchreier.Groupoid.generatorHom

abbrev generatorHom
    {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
    {a b : IsFreeGroupoid.Generators G} (e : a ⟶ b) :
    generatorObject a ⟶ generatorObject b :=
  IsFreeGroupoid.of e

A generating arrow with both endpoints expressed through generatorObject.

Abbreviation ReidemeisterSchreier.Groupoid.treeVertexObject

abbrev treeVertexObject
    {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
    (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G))
    (a : T) : G :=
  generatorObject a

A spanning-tree vertex viewed in the ambient groupoid.

Abbreviation ReidemeisterSchreier.Groupoid.treeVertexOfObject

abbrev treeVertexOfObject
    {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
    (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G))
    (a : G) : T :=
  a

An ambient groupoid vertex viewed as a vertex of the wide spanning subquiver.

Abbreviation ReidemeisterSchreier.Groupoid.rootObject

noncomputable abbrev rootObject
    {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
    (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G))
    [Quiver.Arborescence T] : G :=
  treeVertexObject T (Quiver.root T)

The root vertex of a spanning tree, explicitly returned in the ambient groupoid type.

Abbreviation ReidemeisterSchreier.Groupoid.treeEdgeHom

noncomputable abbrev treeEdgeHom
    {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
    (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G))
    {a b : T} (e : a ⟶ b) : treeVertexObject T a ⟶ treeVertexObject T b :=
  Sum.recOn e.val (fun f => generatorHom f) (fun f => inv (generatorHom f))

A tree edge viewed as an arrow of the ambient groupoid.

Definition ReidemeisterSchreier.Groupoid.rootHomOfPath

noncomputable def rootHomOfPath
    {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
    (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T] :
    ∀ {a : T}, Quiver.Path (Quiver.root T) a →
      (rootObject T ⟶ treeVertexObject T a)
  | _, Quiver.Path.nil => 𝟙 _
  | _, Quiver.Path.cons p e => rootHomOfPath T p ≫ treeEdgeHom T e

A path in the chosen spanning tree gives an arrow from its explicit root.

Definition ReidemeisterSchreier.Groupoid.rootTreeHom

noncomputable def rootTreeHom
    {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
    (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T]
    (a : T) : rootObject T ⟶ treeVertexObject T a :=
  rootHomOfPath T default

The canonical spanning-tree arrow from the explicit root to a tree vertex.

Theorem ReidemeisterSchreier.Groupoid.rootTreeHom_eq

theorem rootTreeHom_eq
    {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
    (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T]
    {a : T} (p : Quiver.Path (Quiver.root T) a) :
    rootTreeHom T a = rootHomOfPath T p

Any spanning-tree path computes the canonical root arrow.

Show Lean proof

Theorem ReidemeisterSchreier.Groupoid.rootTreeHom_root

@[simp] theorem rootTreeHom_root
    {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
    (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T] :
    rootTreeHom T (Quiver.root T) = 𝟙 _

The canonical tree arrow at the explicit root is the identity.

Show Lean proof

Definition ReidemeisterSchreier.Groupoid.rootLoopOfHom

noncomputable def rootLoopOfHom
    {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
    (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T]
    {a b : G} (p : a ⟶ b) : End (rootObject T) :=
  rootTreeHom T (treeVertexOfObject T a) ≫ p ≫
    inv (rootTreeHom T (treeVertexOfObject T b))

The loop associated to a groupoid arrow, based at the explicit spanning-tree root.

Theorem ReidemeisterSchreier.Groupoid.rootLoopOfHom_eq_id

@[simp] theorem rootLoopOfHom_eq_id
    {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
    (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T]
    {a b : IsFreeGroupoid.Generators G} (e : a ⟶ b)
    (h : e ∈ Quiver.wideSubquiverSymmetrify T a b) :
    rootLoopOfHom T (generatorHom e) = 𝟙 (rootObject T)

A tree edge gives the identity explicit-root loop.

Show Lean proof

Definition ReidemeisterSchreier.Groupoid.rootFunctorOfMonoidHom

noncomputable def rootFunctorOfMonoidHom
    {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
    (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T]
    {X : Type u} [Monoid X] (f : End (rootObject T) →* X) :
    G ⥤ CategoryTheory.SingleObj X where
  obj _ := ()
  map p := f (rootLoopOfHom T p)
  map_id := by
    intro a
    dsimp only [rootLoopOfHom]
    rw [Category.id_comp, IsIso.hom_inv_id, ← End.one_def, f.map_one, id_as_one]
  map_comp := by
    intros
    rw [CategoryTheory.SingleObj.comp_as_mul, ← f.map_mul]
    simp only [IsIso.inv_hom_id_assoc, rootLoopOfHom, End.mul_def, Category.assoc]

The functor induced by a homomorphism from the explicit root vertex group.

Theorem ReidemeisterSchreier.Groupoid.rootFunctorOfMonoidHom_map

@[simp] theorem rootFunctorOfMonoidHom_map
    {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
    (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T]
    {X : Type u} [Monoid X] (f : End (rootObject T) →* X)
    {a b : G} (p : a ⟶ b) :
    (rootFunctorOfMonoidHom T f).map p = f (rootLoopOfHom T p)

The explicit-root induced functor applies the supplied homomorphism to the explicit-root loop.

Show Lean proof

Theorem ReidemeisterSchreier.Groupoid.rootLoopOfHom_end

@[simp] theorem rootLoopOfHom_end
    {G : Type u} [Groupoid.{u} G] [IsFreeGroupoid G]
    (T : WideSubquiver (Symmetrify <| IsFreeGroupoid.Generators G)) [Quiver.Arborescence T]
    (p : End (rootObject T)) : rootLoopOfHom T p = p

At the root, turning an endomorphism into a loop does nothing.

Show Lean proof

Lemma ReidemeisterSchreier.Groupoid.map_loopOfHom_eq_map

lemma 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 (generatorHom e) = 1) :
    ∀ {a b} (q : a ⟶ b), F.map (rootLoopOfHom T q) = (F.map q : X)

A functor trivial on the spanning tree maps every explicit-root loop to the original arrow.

Show Lean proof

Definition ReidemeisterSchreier.Groupoid.endBasis

noncomputable def 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 (rootObject T)) := by
  classical
  refine FreeGroupBasis.ofUniqueLift
    (((Quiver.wideSubquiverEquivSetTotal <| Quiver.wideSubquiverSymmetrify T)ᶜ : Set _))
    (fun e => rootLoopOfHom T (generatorHom 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 _, ?_, ?_⟩
  · have hloop :
        ∀ {a b} (q : a ⟶ b), F'.map (rootLoopOfHom T q) = (F'.map q : X) :=
      map_loopOfHom_eq_map T F' (by
        intro a b e he
        rw [hF']
        simp only [f', he, ↓reduceDIte])
    rintro ⟨⟨a, b, e⟩, h⟩
    simp only [Functor.mapEnd, DFunLike.coe, hloop, hF']
    exact dif_neg h
  · intro E hE
    ext x
    change E x = (F'.map x : X)
    suffices (rootFunctorOfMonoidHom T E).map x = F'.map x by
      simpa only [rootFunctorOfMonoidHom_map, rootLoopOfHom_end] using this
    congr
    apply uF'
    intro a b e
    rw [rootFunctorOfMonoidHom_map]
    change E (rootLoopOfHom T (IsFreeGroupoid.of e)) = dite _ _ _
    split_ifs with h
    · rw [rootLoopOfHom_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 group basis of the root vertex group.

Theorem ReidemeisterSchreier.Groupoid.endBasis_apply

@[simp] theorem 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 _))) :
    endBasis T e = rootLoopOfHom T (generatorHom e.1.hom)

The explicit spanning-tree basis evaluates to the corresponding explicit-root loop.

Show Lean proof

ProCGroups.ReidemeisterSchreier.Groupoid

Declarations