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

def CategoryTheory.Groupoid.vertexGroup {C : Type u} [Groupoid C] (c : C) : Group (Quiver.Hom c c)

The vertex group at c.

Equations

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

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

theorem CategoryTheory.Groupoid.vertexGroup_mul {C : Type u} [Groupoid C] (c : C) (x y : Quiver.Hom c c) : Eq (HMul.hMul x y) (CategoryStruct.comp x y)

theorem CategoryTheory.Groupoid.vertexGroup_inv {C : Type u} [Groupoid C] (c : C) (a✝ : Quiver.Hom c c) : Eq (Inv.inv a✝) (inv a✝)

theorem CategoryTheory.Groupoid.vertexGroup.inv_eq_inv {C : Type u} [Groupoid C] (c : C) (γ : Quiver.Hom c c) : Eq (Inv.inv γ) (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 : Quiver.Hom c d) : MulEquiv (Quiver.Hom c c) (Quiver.Hom 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.

theorem CategoryTheory.Groupoid.vertexGroupIsomOfMap_apply {C : Type u} [Groupoid C] {c d : C} (f : Quiver.Hom c d) (γ : Quiver.Hom c c) : Eq (DFunLike.coe (vertexGroupIsomOfMap f) γ) (CategoryStruct.comp (inv f) (CategoryStruct.comp γ f))

theorem CategoryTheory.Groupoid.vertexGroupIsomOfMap_symm_apply {C : Type u} [Groupoid C] {c d : C} (f : Quiver.Hom c d) (δ : Quiver.Hom d d) : Eq (DFunLike.coe (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) : MulEquiv (Quiver.Hom c c) (Quiver.Hom d d)

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

Equations

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

def CategoryTheory.Groupoid.CategoryTheory.Functor.mapVertexGroup {C : Type u} [Groupoid C] {D : Type v} [Groupoid D] (φ : Functor C D) (c : C) : MonoidHom (Quiver.Hom c c) (Quiver.Hom (φ.obj c) (φ.obj c))

A functor defines a morphism of vertex group.

Equations

• Eq (CategoryTheory.Groupoid.CategoryTheory.Functor.mapVertexGroup φ c) { toFun := φ.map, map_one' := ⋯, map_mul' := ⋯ }

theorem CategoryTheory.Groupoid.CategoryTheory.Functor.mapVertexGroup_apply {C : Type u} [Groupoid C] {D : Type v} [Groupoid D] (φ : Functor C D) (c : C) (a✝ : Quiver.Hom c c) : Eq (DFunLike.coe (mapVertexGroup φ c) a✝) (φ.map a✝)