-
Notifications
You must be signed in to change notification settings - Fork 259
/
VertexGroup.lean
94 lines (74 loc) · 3.29 KB
/
VertexGroup.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
/-
Copyright (c) 2022 Rémi Bottinelli. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rémi Bottinelli
-/
import Mathlib.Algebra.Group.Equiv.Basic
import Mathlib.CategoryTheory.Groupoid
import Mathlib.CategoryTheory.PathCategory
import Mathlib.Combinatorics.Quiver.Path
#align_import category_theory.groupoid.vertex_group from "leanprover-community/mathlib"@"47b51515e69f59bca5cf34ef456e6000fe205a69"
/-!
# 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
-/
namespace CategoryTheory
namespace Groupoid
universe u v
variable {C : Type u} [Groupoid C]
/-- The vertex group at `c`. -/
@[simps mul one inv]
instance vertexGroup (c : C) : Group (c ⟶ c) where
mul := fun x y : c ⟶ c => x ≫ y
mul_assoc := Category.assoc
one := 𝟙 c
one_mul := Category.id_comp
mul_one := Category.comp_id
inv := Groupoid.inv
mul_left_inv := inv_comp
#align category_theory.groupoid.vertex_group CategoryTheory.Groupoid.vertexGroup
-- dsimp loops when applying this lemma to its LHS,
-- probably https://github.com/leanprover/lean4/pull/2867
attribute [nolint simpNF] CategoryTheory.Groupoid.vertexGroup_one
/-- The inverse in the group is equal to the inverse given by `CategoryTheory.inv`. -/
theorem vertexGroup.inv_eq_inv (c : C) (γ : c ⟶ c) : γ⁻¹ = CategoryTheory.inv γ :=
Groupoid.inv_eq_inv γ
#align category_theory.groupoid.vertex_group.inv_eq_inv CategoryTheory.Groupoid.vertexGroup.inv_eq_inv
/-- An arrow in the groupoid defines, by conjugation, an isomorphism of groups between
its endpoints.
-/
@[simps]
def vertexGroupIsomOfMap {c d : C} (f : c ⟶ d) : (c ⟶ c) ≃* (d ⟶ d) where
toFun γ := inv f ≫ γ ≫ f
invFun δ := f ≫ δ ≫ inv f
left_inv γ := by
simp_rw [Category.assoc, comp_inv, Category.comp_id, ← Category.assoc, comp_inv,
Category.id_comp]
right_inv δ := by
simp_rw [Category.assoc, inv_comp, ← Category.assoc, inv_comp, Category.id_comp,
Category.comp_id]
map_mul' γ₁ γ₂ := by
simp only [vertexGroup_mul, inv_eq_inv, Category.assoc, IsIso.hom_inv_id_assoc]
#align category_theory.groupoid.vertex_group_isom_of_map CategoryTheory.Groupoid.vertexGroupIsomOfMap
/-- A path in the groupoid defines an isomorphism between its endpoints.
-/
def vertexGroupIsomOfPath {c d : C} (p : Quiver.Path c d) : (c ⟶ c) ≃* (d ⟶ d) :=
vertexGroupIsomOfMap (composePath p)
#align category_theory.groupoid.vertex_group_isom_of_path CategoryTheory.Groupoid.vertexGroupIsomOfPath
/-- A functor defines a morphism of vertex group. -/
@[simps]
def CategoryTheory.Functor.mapVertexGroup {D : Type v} [Groupoid D] (φ : C ⥤ D) (c : C) :
(c ⟶ c) →* (φ.obj c ⟶ φ.obj c) where
toFun := φ.map
map_one' := φ.map_id c
map_mul' := φ.map_comp
#align category_theory.functor.map_vertex_group CategoryTheory.Groupoid.CategoryTheory.Functor.mapVertexGroup
end Groupoid
end CategoryTheory