instCoeDep

Mathlib.CategoryTheory.Galois.Prorepresentability

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

English

The projection π F A from AutGalois F to Aut(A) is surjective for every pointed Galois object A.

Русский

Проекция π F A: AutGalois F → Aut(A) сюръективна для каждого точечного Galois-объекта A.

LaTeX

$$$\forall A\; AutGalois.\pi F A\;\text{is surjective}$$$

Lean4

instance (X : PointedGaloisObject F) : CoeDep (PointedGaloisObject F) X C where coe := X.obj

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

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

Разделы

Аффилиация

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