English
A propagation lemma showing how map_wittStructureInt interacts with the underlying structure, reinforcing the equivalence with map_wittStructureRat through the rationalization map.
Русский
Лемма распространения показывает, как map_wittStructureInt взаимодействует с базовой структурой, усиливая эквивалентность map_wittStructureRat через рационализацию.
LaTeX
$$$map_wittStructureInt\ p\ Φ\ n = wittStructureRat p (map (Int.castRingHom ℚ) Φ) n$$$
Lean4
theorem wittStructureInt_prop (Φ : MvPolynomial idx ℤ) (n) :
bind₁ (wittStructureInt p Φ) (wittPolynomial p ℤ n) = bind₁ (fun i => rename (Prod.mk i) (W_ ℤ n)) Φ :=
by
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
have := wittStructureRat_prop p (map (Int.castRingHom ℚ) Φ) n
simpa only [map_bind₁, ← eval₂Hom_map_hom, eval₂Hom_C_left, map_rename, map_wittPolynomial, AlgHom.coe_toRingHom,
map_wittStructureInt]
