frobenius_eq_map_frobenius — Mathlib

English

The Frobenius endomorphism on Witt vectors is equal to the map induced by Frobenius on the base ring when interpreted as a Witt vector endomorphism.

Русский

Эндоморфизм Frobenius на Witt-векторах равен отображению, индуцированному Frobenius на базовом кольце, при трактовке как эндоморфизм Witt.

LaTeX

$$$$@frobenius\, =\, \mathrm{map}(\,\, frobenius_{R,p}\,).$$$$

Lean4

theorem frobenius_eq_map_frobenius : @frobenius p R _ _ = map (_root_.frobenius R p) :=
  by
  ext (x n)
  simp only [coeff_frobenius_charP, map_coeff, frobenius_def]

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