toAut_hom_app_apply

Mathlib.CategoryTheory.Galois.IsFundamentalgroup

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

English

For g ∈ G, (toAut F G g).hom.app X x = g • x for any X and x.

Русский

Для элемента g ∈ G выполняется (toAut F G g).hom.app X x = g • x для любых X и x.

LaTeX

$$$(\mathrm{toAut}\ F\ G\ g).hom.app\ X\ x = g \cdot x$$$

Lean4

@[simp]
theorem toAut_hom_app_apply (g : G) {X : C} (x : F.obj X) : (toAut F G g).hom.app X x = g • x :=
  rfl

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

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

Разделы

Аффилиация

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