ghostComponent_frobeniusFun — Mathlib

English

The ghost components of the Witt-vector Frobenius functor shift by one index: ghostComponent n (frobeniusFun x) = ghostComponent (n+1) x.

Русский

Гост-компоненты Witt-функторa Фробениуса образуют сдвиг на единицу: ghostComponent n (frobeniusFun x) = ghostComponent (n+1) x.

LaTeX

$$$$\text{ghostComponent}_n(\operatorname{frobeniusFun}(x)) = \text{ghostComponent}_{n+1}(x).$$$$

Lean4

@[ghost_simps]
theorem ghostComponent_frobeniusFun (n : ℕ) (x : 𝕎 R) : ghostComponent n (frobeniusFun x) = ghostComponent (n + 1) x :=
  by simp only [ghostComponent_apply, frobeniusFun, coeff_mk, ← bind₁_frobeniusPoly_wittPolynomial, aeval_bind₁]

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