mathlib3 documentation

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 #

Tags #

isotropy, vertex group, groupoid

@[simp]
theorem category_theory.groupoid.vertex_group_mul {C : Type u} [category_theory.groupoid C] (c : C) (x y : c c) :
x * y = x y
@[simp]
theorem category_theory.groupoid.vertex_group_npow {C : Type u} [category_theory.groupoid C] (c : C) (ᾰ : ) (ᾰ_1 : c c) :
group.npow ᾰ_1 = div_inv_monoid.npow._default (𝟙 c) (λ (x y : c c), x y) _ _ ᾰ_1
@[protected, instance]

The vertex group at c.

Equations
@[simp]
theorem category_theory.groupoid.vertex_group_div {C : Type u} [category_theory.groupoid C] (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_zpow {C : Type u} [category_theory.groupoid C] (c : C) (ᾰ : ) (ᾰ_1 : c c) :
group.zpow ᾰ_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

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

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

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

A functor defines a morphism of vertex group.

Equations