English
For Φ ∈ MvPolynomial idx ℤ and n, the evaluation of wittStructureInt via the appropriate cast maps equals the evaluation of Φ under the renamed Witt components: aeval (i ↦ map (Int.castRingHom R) (wittStructureInt p Φ i)) (wittPolynomial p ℤ n) equals aeval (i ↦ rename (Prod.mk i) (W n)) Φ.
Русский
Для Φ ∈ MvPolynomial idx ℤ и для каждого n, вычисление wittStructureInt через соответствующее отображение эквивалентно вычислению ψ(Φ) с переименованными компонентами Witt: aeval (i ↦ map (Int.castRingHom R) (wittStructureInt p Φ i)) (wittPolynomial p ℤ n) = aeval (i ↦ rename (Prod.mk i) (W n)) Φ.
LaTeX
$$$\\forall (n)\\; aeval (\\lambda i. {\\map{Int.castRingHom} (wittStructureInt p \\ Φ i)}) (\\mathrm{wittPolynomial} p \\mathbb{Z} n) = aeval (\\lambda i. rename(\\mathrm{Prod.mk} i) (W n)) Φ$$$
Lean4
theorem witt_structure_prop (Φ : MvPolynomial idx ℤ) (n) :
aeval (fun i => map (Int.castRingHom R) (wittStructureInt p Φ i)) (wittPolynomial p ℤ n) =
aeval (fun i => rename (Prod.mk i) (W n)) Φ :=
by
convert congr_arg (map (Int.castRingHom R)) (wittStructureInt_prop p Φ n) using 1 <;> rw [hom_bind₁] <;>
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
· rfl
· simp only [map_rename, map_wittPolynomial]
