π_apply

Mathlib.CategoryTheory.Galois.Prorepresentability

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PreGaloisCategory.AutGalois.π_apply

English

The projection π F A sends an automorphism to its restriction to A.

Русский

Проекция π F A отправляет автоморфизм к его ограничению на A.

LaTeX

$$$\pi F A(x) = x|_A$$$

Lean4

theorem π_apply (A : PointedGaloisObject F) (x : AutGalois F) : AutGalois.π F A x = x.val A :=
  rfl

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

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

Разделы

Аффилиация

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