Module

Groupoid.lean

Nyll.ProCGroups.ReidemeisterSchreier.Groupoid

18 declarations indexed from sourceView source ↗

Module documentation

Reidemeister Schreier / Groupoid

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.

Imports1

Mathlib.GroupTheory.FreeGroup.NielsenSchreier

Imported by2

abbrev

generatorObject

L24 ↗

ReidemeisterSchreier.Groupoid.generatorObject

Documentation

A generator-quiver vertex viewed in the ambient groupoid.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.SingleObj Quiver
universe u
namespace ReidemeisterSchreier.Groupoid

Lean source · statement

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

abbrev

generatorHom

L30 ↗

ReidemeisterSchreier.Groupoid.generatorHom

Documentation

A generating arrow with both endpoints expressed through generatorObject.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.SingleObj Quiver
universe u
namespace ReidemeisterSchreier.Groupoid

Lean source · statement

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

abbrev

treeVertexObject

L37 ↗

ReidemeisterSchreier.Groupoid.treeVertexObject

Documentation

A spanning-tree vertex viewed in the ambient groupoid.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.SingleObj Quiver
universe u
namespace ReidemeisterSchreier.Groupoid

Lean source · statement

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

abbrev

treeVertexOfObject

L44 ↗

ReidemeisterSchreier.Groupoid.treeVertexOfObject

Documentation

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

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.SingleObj Quiver
universe u
namespace ReidemeisterSchreier.Groupoid

Lean source · statement

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

abbrev

rootObject

L51 ↗

ReidemeisterSchreier.Groupoid.rootObject

Documentation

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

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.SingleObj Quiver
universe u
namespace ReidemeisterSchreier.Groupoid

Lean source · statement

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

abbrev

treeEdgeHom

L58 ↗

ReidemeisterSchreier.Groupoid.treeEdgeHom

Documentation

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

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.SingleObj Quiver
universe u
namespace ReidemeisterSchreier.Groupoid

Lean source · statement

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

def

rootHomOfPath

L65 ↗

ReidemeisterSchreier.Groupoid.rootHomOfPath

Documentation

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

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.SingleObj Quiver
universe u
namespace ReidemeisterSchreier.Groupoid

Lean source · full declaration

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

def

rootTreeHom

L74 ↗

ReidemeisterSchreier.Groupoid.rootTreeHom

Documentation

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

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.SingleObj Quiver
universe u
namespace ReidemeisterSchreier.Groupoid

Lean source · statement

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

theorem

rootTreeHom_eq

L81 ↗

ReidemeisterSchreier.Groupoid.rootTreeHom_eq

Documentation

Any spanning-tree path computes the canonical root arrow.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.SingleObj Quiver
universe u
namespace ReidemeisterSchreier.Groupoid

Lean source · statement

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

theorem

rootTreeHom_root

L89 ↗

ReidemeisterSchreier.Groupoid.rootTreeHom_root

Documentation

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

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.SingleObj Quiver
universe u
namespace ReidemeisterSchreier.Groupoid

Lean source · statement

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) = 𝟙 _

def

rootLoopOfHom

L96 ↗

ReidemeisterSchreier.Groupoid.rootLoopOfHom

Documentation

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

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.SingleObj Quiver
universe u
namespace ReidemeisterSchreier.Groupoid

Lean source · statement

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)

theorem

rootLoopOfHom_eq_id

L104 ↗

ReidemeisterSchreier.Groupoid.rootLoopOfHom_eq_id

Documentation

A tree edge gives the identity explicit-root loop.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.SingleObj Quiver
universe u
namespace ReidemeisterSchreier.Groupoid

Lean source · statement

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)

def

rootFunctorOfMonoidHom

L138 ↗

ReidemeisterSchreier.Groupoid.rootFunctorOfMonoidHom

Documentation

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

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.SingleObj Quiver
universe u
namespace ReidemeisterSchreier.Groupoid

Lean source · full declaration

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]

theorem

rootFunctorOfMonoidHom_map

L157 ↗

ReidemeisterSchreier.Groupoid.rootFunctorOfMonoidHom_map

Documentation

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

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.SingleObj Quiver
universe u
namespace ReidemeisterSchreier.Groupoid

Lean source · statement

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)

theorem

rootLoopOfHom_end

L165 ↗

ReidemeisterSchreier.Groupoid.rootLoopOfHom_end

Documentation

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

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.SingleObj Quiver
universe u
namespace ReidemeisterSchreier.Groupoid

Lean source · statement

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

lemma

map_loopOfHom_eq_map

L173 ↗

ReidemeisterSchreier.Groupoid.map_loopOfHom_eq_map

Documentation

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

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.SingleObj Quiver
universe u
namespace ReidemeisterSchreier.Groupoid

Lean source · statement

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)

def

endBasis

L198 ↗

ReidemeisterSchreier.Groupoid.endBasis

Documentation

The complement of a chosen spanning tree in a free connected groupoid gives an explicit free group basis of the root vertex group.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.SingleObj Quiver
universe u
namespace ReidemeisterSchreier.Groupoid

Lean source · statement

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))

theorem

endBasis_apply

L239 ↗

ReidemeisterSchreier.Groupoid.endBasis_apply

Documentation

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

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open CategoryTheory CategoryTheory.SingleObj Quiver
universe u
namespace ReidemeisterSchreier.Groupoid

Lean source · statement

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)

Module documentation

Reidemeister Schreier / Groupoid

Declarations