Documentation

Mathlib.CategoryTheory.Groupoid.VertexGroup

Vertex group #

This file defines the vertex group (aka isotropy group) of a groupoid at a vertex.

Implementation notes #

Tags #

isotropy, vertex group, groupoid

The vertex group at c.

The inverse in the group is equal to the inverse given by CategoryTheory.inv.

def CategoryTheory.Groupoid.vertexGroupIsomOfMap {C : Type u} [CategoryTheory.Groupoid C] {c : C} {d : C} (f : c d) :
(c c) ≃* (d d)

An arrow in the groupoid defines, by conjugation, an isomorphism of groups between its endpoints.

Instances For

    A path in the groupoid defines an isomorphism between its endpoints.

    Instances For

      A functor defines a morphism of vertex group.

      Instances For