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 usingCategoryTheory.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]
@[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_inv
{C : Type u}
[CategoryTheory.Groupoid C]
(c : C)
:
∀ (a : c ⟶ c), a⁻¹ = CategoryTheory.Groupoid.inv a
The vertex group at c
.
Equations
theorem
CategoryTheory.Groupoid.vertexGroup.inv_eq_inv
{C : Type u}
[CategoryTheory.Groupoid C]
(c : C)
(γ : c ⟶ c)
:
The inverse in the group is equal to the inverse given by CategoryTheory.inv
.
@[simp]
theorem
CategoryTheory.Groupoid.vertexGroupIsomOfMap_apply
{C : Type u}
[CategoryTheory.Groupoid C]
{c : C}
{d : C}
(f : c ⟶ d)
(γ : c ⟶ c)
:
@[simp]
theorem
CategoryTheory.Groupoid.vertexGroupIsomOfMap_symm_apply
{C : Type u}
[CategoryTheory.Groupoid C]
{c : C}
{d : C}
(f : c ⟶ d)
(δ : d ⟶ d)
:
def
CategoryTheory.Groupoid.vertexGroupIsomOfMap
{C : Type u}
[CategoryTheory.Groupoid C]
{c : C}
{d : C}
(f : c ⟶ 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.
Instances For
def
CategoryTheory.Groupoid.vertexGroupIsomOfPath
{C : Type u}
[CategoryTheory.Groupoid C]
{c : C}
{d : C}
(p : Quiver.Path c d)
:
A path in the groupoid defines an isomorphism between its endpoints.
Equations
Instances For
@[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 = φ.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)
:
A functor defines a morphism of vertex group.
Equations
- CategoryTheory.Groupoid.CategoryTheory.Functor.mapVertexGroup φ c = { toFun := φ.map, map_one' := ⋯, map_mul' := ⋯ }