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

@[instance_reducible]

instance CategoryTheory.Groupoid.vertexGroup {C : Type u} [Groupoid C] (c : C) : Group (c ⟶ c)

The vertex group at c.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Groupoid.vertexGroup_inv {C : Type u} [Groupoid C] (c : C) (a✝ : c ⟶ c) : a✝⁻¹ = inv a✝

@[simp]

theorem CategoryTheory.Groupoid.vertexGroup_one {C : Type u} [Groupoid C] (c : C) : 1 = CategoryStruct.id c

@[simp]

theorem CategoryTheory.Groupoid.vertexGroup_mul {C : Type u} [Groupoid C] (c : C) (x y : c ⟶ c) : x * y = CategoryStruct.comp x y

theorem CategoryTheory.Groupoid.vertexGroup.inv_eq_inv {C : Type u} [Groupoid C] (c : C) (γ : c ⟶ c) : γ⁻¹ = CategoryTheory.inv γ

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

def CategoryTheory.Groupoid.vertexGroupIsomOfMap {C : Type u} [Groupoid 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.

@[simp]

theorem CategoryTheory.Groupoid.vertexGroupIsomOfMap_apply {C : Type u} [Groupoid C] {c d : C} (f : c ⟶ d) (γ : c ⟶ c) : (vertexGroupIsomOfMap f) γ = CategoryStruct.comp (inv f) (CategoryStruct.comp γ f)

@[simp]

theorem CategoryTheory.Groupoid.vertexGroupIsomOfMap_symm_apply {C : Type u} [Groupoid C] {c d : C} (f : c ⟶ d) (δ : d ⟶ d) : (vertexGroupIsomOfMap f).symm δ = CategoryStruct.comp f (CategoryStruct.comp δ (inv f))

def CategoryTheory.Groupoid.vertexGroupIsomOfPath {C : Type u} [Groupoid C] {c d : C} (p : Quiver.Path c d) : (c ⟶ c) ≃* (d ⟶ d)

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

Equations

• CategoryTheory.Groupoid.vertexGroupIsomOfPath p = CategoryTheory.Groupoid.vertexGroupIsomOfMap (CategoryTheory.composePath p)

def CategoryTheory.Functor.mapVertexGroup {C : Type u} [Groupoid C] {D : Type v} [Groupoid D] (φ : Functor C D) (c : C) : (c ⟶ c) →* (φ.obj c ⟶ φ.obj c)

A functor defines a morphism of vertex groups.

Equations

• φ.mapVertexGroup c = { toFun := φ.map, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem CategoryTheory.Functor.mapVertexGroup_apply {C : Type u} [Groupoid C] {D : Type v} [Groupoid D] (φ : Functor C D) (c : C) (a✝ : c ⟶ c) : (φ.mapVertexGroup c) a✝ = φ.map a✝

@[deprecated CategoryTheory.Functor.mapVertexGroup (since := "2026-05-24")]

def CategoryTheory.Groupoid.CategoryTheory.Functor.mapVertexGroup {C : Type u} [Groupoid C] {D : Type v} [Groupoid D] (φ : Functor C D) (c : C) : (c ⟶ c) →* (φ.obj c ⟶ φ.obj c)

Alias of CategoryTheory.Functor.mapVertexGroup.

---

A functor defines a morphism of vertex groups.

Equations

• @CategoryTheory.Groupoid.CategoryTheory.Functor.mapVertexGroup = @CategoryTheory.Functor.mapVertexGroup

@[deprecated CategoryTheory.Functor.mapVertexGroup_apply (since := "2026-05-24")]

theorem CategoryTheory.Groupoid.CategoryTheory.Functor.mapVertexGroup_apply {C : Type u} [Groupoid C] {D : Type v} [Groupoid D] (φ : Functor C D) (c : C) (a✝ : c ⟶ c) : (φ.mapVertexGroup c) a✝ = φ.map a✝

Alias of CategoryTheory.Functor.mapVertexGroup_apply.