Vertex group #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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
category_theory.Aut.groupor usingcategory_theory.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
category_theory.groupoid.vertex_group_mul
{C : Type u}
[category_theory.groupoid C]
(c : C)
(x y : c ⟶ c) :
@[simp]
theorem
category_theory.groupoid.vertex_group_npow
{C : Type u}
[category_theory.groupoid C]
(c : C)
(ᾰ : ℕ)
(ᾰ_1 : c ⟶ c) :
group.npow ᾰ ᾰ_1 = div_inv_monoid.npow._default (𝟙 c) (λ (x y : c ⟶ c), x ≫ y) _ _ ᾰ ᾰ_1
@[simp]
theorem
category_theory.groupoid.vertex_group_one
{C : Type u}
[category_theory.groupoid C]
(c : C) :
@[protected, instance]
The vertex group at c.
Equations
- category_theory.groupoid.vertex_group c = {mul := λ (x y : c ⟶ c), x ≫ y, mul_assoc := _, one := 𝟙 c, one_mul := _, mul_one := _, npow := div_inv_monoid.npow._default (𝟙 c) (λ (x y : c ⟶ c), x ≫ y) _ _, npow_zero' := _, npow_succ' := _, inv := category_theory.groupoid.inv c, div := div_inv_monoid.div._default (λ (x y : c ⟶ c), x ≫ y) _ (𝟙 c) _ _ (div_inv_monoid.npow._default (𝟙 c) (λ (x y : c ⟶ c), x ≫ y) _ _) _ _ category_theory.groupoid.inv, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default (λ (x y : c ⟶ c), x ≫ y) _ (𝟙 c) _ _ (div_inv_monoid.npow._default (𝟙 c) (λ (x y : c ⟶ c), x ≫ y) _ _) _ _ category_theory.groupoid.inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
@[simp]
theorem
category_theory.groupoid.vertex_group_div
{C : Type u}
[category_theory.groupoid C]
(c : C)
(ᾰ ᾰ_1 : c ⟶ c) :
@[simp]
theorem
category_theory.groupoid.vertex_group_inv
{C : Type u}
[category_theory.groupoid C]
(c : C)
(ᾰ : c ⟶ c) :
@[simp]
theorem
category_theory.groupoid.vertex_group_zpow
{C : Type u}
[category_theory.groupoid C]
(c : C)
(ᾰ : ℤ)
(ᾰ_1 : c ⟶ c) :
group.zpow ᾰ ᾰ_1 = div_inv_monoid.zpow._default (λ (x y : c ⟶ c), x ≫ y) _ (𝟙 c) _ _ (div_inv_monoid.npow._default (𝟙 c) (λ (x y : c ⟶ c), x ≫ y) _ _) _ _ category_theory.groupoid.inv ᾰ ᾰ_1
theorem
category_theory.groupoid.vertex_group.inv_eq_inv
{C : Type u}
[category_theory.groupoid C]
(c : C)
(γ : c ⟶ c) :
The inverse in the group is equal to the inverse given by category_theory.inv.
@[simp]
theorem
category_theory.groupoid.vertex_group_isom_of_map_apply
{C : Type u}
[category_theory.groupoid C]
{c d : C}
(f : c ⟶ d)
(γ : c ⟶ c) :
def
category_theory.groupoid.vertex_group_isom_of_map
{C : Type u}
[category_theory.groupoid C]
{c d : C}
(f : c ⟶ d) :
An arrow in the groupoid defines, by conjugation, an isomorphism of groups between its endpoints.
@[simp]
theorem
category_theory.groupoid.vertex_group_isom_of_map_symm_apply
{C : Type u}
[category_theory.groupoid C]
{c d : C}
(f : c ⟶ d)
(δ : d ⟶ d) :
def
category_theory.groupoid.vertex_group_isom_of_path
{C : Type u}
[category_theory.groupoid C]
{c d : C}
(p : quiver.path c d) :
A path in the groupoid defines an isomorphism between its endpoints.
@[simp]
theorem
category_theory.functor.map_vertex_group_apply
{C : Type u}
[category_theory.groupoid C]
{D : Type v}
[category_theory.groupoid D]
(φ : C ⥤ D)
(c : C)
(ᾰ : c ⟶ c) :
⇑(φ.map_vertex_group c) ᾰ = φ.map ᾰ
def
category_theory.functor.map_vertex_group
{C : Type u}
[category_theory.groupoid C]
{D : Type v}
[category_theory.groupoid D]
(φ : C ⥤ D)
(c : C) :
A functor defines a morphism of vertex group.