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

  • One or more equations did not get rendered due to their size.
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