ghostEquiv_coe

Mathlib.RingTheory.WittVector.Basic

URI: https://scilib.ai/kg/mathlib#WittVector.ghostEquiv_coe

English

The underlying ring homomorphism of the isomorphism ghostEquiv p R is exactly the ghost map.

Русский

Базовая кольцевая гомоморфная карта изоморфизма ghostEquiv p R совпадает с ghostMap.

LaTeX

$$$$ (ghostEquiv\ p\ R : \mathbb{W}R \to+* (\mathbb{N} \to R)) = ghostMap. $$$$

Lean4

@[simp]
theorem ghostEquiv_coe : (ghostEquiv p R : 𝕎 R →+* ℕ → R) = ghostMap :=
  rfl

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

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

Разделы

Аффилиация

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