toAutHomeo_apply

Mathlib.CategoryTheory.Galois.IsFundamentalgroup

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PreGaloisCategory.toAutHomeo_apply

English

Two automorphisms of AutF are equal if all their projections π F A on pointed Galois objects agree.

Русский

Два автоморфизма AutF равны, если их все проекции π F A на точечных Galois-объектах совпадают.

LaTeX

$$$\forall A\; AutGalois.\pi F A\ f = AutGalois.\pi F A\ g \Rightarrow f = g$$$

Lean4

@[simp]
theorem toAutHomeo_apply (g : G) : toAutHomeo F G g = toAut F G g :=
  rfl

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru