# Vertex group #

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

## Implementation notes #

• The instance is defined "manually", instead of relying on CategoryTheory.Aut.group or using CategoryTheory.inv.
• The multiplication order therefore matches the categorical one: x * y = x ≫ y.
• The inverse is directly defined in terms of the groupoidal inverse: x ⁻¹ = Groupoid.inv x.

## Tags #

isotropy, vertex group, groupoid

@[simp]
theorem CategoryTheory.Groupoid.vertexGroup_inv {C : Type u} (c : C) :
∀ (a : c c),
@[simp]
theorem CategoryTheory.Groupoid.vertexGroup_mul {C : Type u} (c : C) (x : c c) (y : c c) :
@[simp]
instance CategoryTheory.Groupoid.vertexGroup {C : Type u} (c : C) :
Group (c c)

The vertex group at c.

Equations
theorem CategoryTheory.Groupoid.vertexGroup.inv_eq_inv {C : Type u} (c : C) (γ : c c) :

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

@[simp]
theorem CategoryTheory.Groupoid.vertexGroupIsomOfMap_symm_apply {C : Type u} {c : C} {d : C} (f : c d) (δ : d d) :
@[simp]
theorem CategoryTheory.Groupoid.vertexGroupIsomOfMap_apply {C : Type u} {c : C} {d : C} (f : c d) (γ : c c) :
def CategoryTheory.Groupoid.vertexGroupIsomOfMap {C : Type u} {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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
def CategoryTheory.Groupoid.vertexGroupIsomOfPath {C : Type u} {c : C} {d : C} (p : ) :
(c c) ≃* (d d)

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

Equations
Instances For
@[simp]
theorem CategoryTheory.Groupoid.CategoryTheory.Functor.mapVertexGroup_apply {C : Type u} {D : Type v} (φ : ) (c : C) :
∀ (a : c c),
def CategoryTheory.Groupoid.CategoryTheory.Functor.mapVertexGroup {C : Type u} {D : Type v} (φ : ) (c : C) :
(c c) →* (φ.obj c φ.obj c)

A functor defines a morphism of vertex group.

Equations
• = { toFun := φ.map, map_one' := , map_mul' := }
Instances For