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} [CategoryTheory.Groupoid C] (c : C) : ∀ (a : c ⟶ c), a⁻¹ = CategoryTheory.Groupoid.inv a

@[simp]

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

@[simp]

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

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

The vertex group at c.

Equations

• CategoryTheory.Groupoid.vertexGroup c = Group.mk (_ : ∀ (f : c ⟶ c), CategoryTheory.CategoryStruct.comp (CategoryTheory.Groupoid.inv f) f = CategoryTheory.CategoryStruct.id c)

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

A functor defines a morphism of vertex group.

Equations

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