English
A morphism f: c ⟶ d induces a group isomorphism between the vertex groups at c and at d by conjugation: γ ↦ f⁻¹ γ f.
Русский
Стрела f: c ⟶ d задаёт изоморфизм групп вершинных групп c и d по конъюгации: γ ↦ f⁻¹ γ f.
LaTeX
$$$\\forall f : c \\to d,\\; (c \\to c) \\cong_* (d \\to d),\\; \\gamma \\mapsto f^{-1} \\gamma f$$$
Lean4
/-- 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]
