NYLL
Module

Quiver.lean

Nyll.ProCGroups.ReidemeisterSchreier.Quiver
2 declarations indexed from sourceView source ↗

Module documentation

Reidemeister Schreier / Quiver

This module formalizes the quiver and arborescence tools used by the groupoid construction.

Imports2
  • Mathlib.Combinatorics.Quiver.Arborescence
  • Mathlib.Combinatorics.Quiver.ConnectedComponent
Imported by2

Declarations

def

coveredArrowEquivTotal

L22 ↗
ReidemeisterSchreier.Quiver.coveredArrowEquivTotal
Documentation

Forgetting the orientation of a tree edge in a symmetrized quiver identifies the total arrows of the tree with the original arrows covered by its symmetrification.

Source context 2 commands

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

universe u
namespace ReidemeisterSchreier
Lean source · statement
def Quiver.coveredArrowEquivTotal
    {V : Type u} [Quiver V] (T : WideSubquiver (Quiver.Symmetrify V)) [Quiver.Arborescence T] :
    ↥(Quiver.wideSubquiverEquivSetTotal (Quiver.wideSubquiverSymmetrify T)) ≃ Quiver.Total T
def

totalEquivNonRoot

L103 ↗
ReidemeisterSchreier.Quiver.Arborescence.totalEquivNonRoot
Documentation

In an arborescence, the last edge of the unique path to a non-root vertex determines that vertex, and every edge arises this way.

Source context 3 commands

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

universe u
namespace ReidemeisterSchreier
namespace Quiver
Lean source · statement
def Arborescence.totalEquivNonRoot
    (V : Type u) [Quiver V] [Quiver.Arborescence V] :
    Quiver.Total V ≃ {v : V // v ≠ Quiver.root V}

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.