# mathlib3documentation

category_theory.groupoid.vertex_group

# Vertex group #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 category_theory.Aut.group or using category_theory.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 category_theory.groupoid.vertex_group_mul {C : Type u} (c : C) (x y : c c) :
x * y = x y
@[simp]
theorem category_theory.groupoid.vertex_group_npow {C : Type u} (c : C) (ᾰ : ) (ᾰ_1 : c c) :
ᾰ_1 = div_inv_monoid.npow._default (𝟙 c) (λ (x y : c c), x y) _ _ ᾰ_1
@[simp]
theorem category_theory.groupoid.vertex_group_one {C : Type u} (c : C) :
1 = 𝟙 c
@[protected, instance]
def category_theory.groupoid.vertex_group {C : Type u} (c : C) :
group (c c)

The vertex group at c.

Equations
@[simp]
theorem category_theory.groupoid.vertex_group_div {C : Type u} (c : C) (ᾰ ᾰ_1 : c c) :
/ ᾰ_1 = div_inv_monoid.div._default (λ (x y : c c), x y) _ (𝟙 c) _ _ (div_inv_monoid.npow._default (𝟙 c) (λ (x y : c c), x y) _ _) _ _ category_theory.groupoid.inv ᾰ_1
@[simp]
theorem category_theory.groupoid.vertex_group_inv {C : Type u} (c : C) (ᾰ : c c) :
@[simp]
theorem category_theory.groupoid.vertex_group_zpow {C : Type u} (c : C) (ᾰ : ) (ᾰ_1 : c c) :
ᾰ_1 = div_inv_monoid.zpow._default (λ (x y : c c), x y) _ (𝟙 c) _ _ (div_inv_monoid.npow._default (𝟙 c) (λ (x y : c c), x y) _ _) _ _ category_theory.groupoid.inv ᾰ_1
theorem category_theory.groupoid.vertex_group.inv_eq_inv {C : Type u} (c : C) (γ : c c) :

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

@[simp]
theorem category_theory.groupoid.vertex_group_isom_of_map_apply {C : Type u} {c d : C} (f : c d) (γ : c c) :
def category_theory.groupoid.vertex_group_isom_of_map {C : Type u} {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
@[simp]
theorem category_theory.groupoid.vertex_group_isom_of_map_symm_apply {C : Type u} {c d : C} (f : c d) (δ : d d) :
def category_theory.groupoid.vertex_group_isom_of_path {C : Type u} {c d : C} (p : d) :
(c c) ≃* (d d)

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

Equations
@[simp]
theorem category_theory.functor.map_vertex_group_apply {C : Type u} {D : Type v} (φ : C D) (c : C) (ᾰ : c c) :
(φ.map_vertex_group c) = φ.map
def category_theory.functor.map_vertex_group {C : Type u} {D : Type v} (φ : C D) (c : C) :
(c c) →* (φ.obj c φ.obj c)

A functor defines a morphism of vertex group.

Equations