English
A variant property asserts that the integer Witt-structure respects the Witt decomposition similarly to the rational case, ensuring canonical integer realizations align with the rational framework after mapping.
Русский
Вариант свойства утверждает, что целочисленная Witt-структура сохраняет разложение Witt аналогично рациональному случаю, обеспечивая канонические целочисленные реализации, согласующиеся с рациональной структурой после отображения.
LaTeX
$$$bind₁ (wittStructureInt p Φ) (W_ ℤ n) = bind₁ (fun i => rename (Prod.mk i) (W_ ℤ n)) Φ$$$
Lean4
@[simp]
theorem map_wittStructureInt (Φ : MvPolynomial idx ℤ) (n : ℕ) :
map (Int.castRingHom ℚ) (wittStructureInt p Φ n) = wittStructureRat p (map (Int.castRingHom ℚ) Φ) n :=
by
induction n using Nat.strong_induction_on with
| h n IH => ?_
rw [wittStructureInt, map_mapRange_eq_iff, Int.coe_castRingHom]
intro c
rw [wittStructureRat_rec, coeff_C_mul, mul_comm, mul_div_assoc', mul_one]
have sum_induction_steps :
map (Int.castRingHom ℚ) (∑ i ∈ range n, C ((p : ℤ) ^ i) * wittStructureInt p Φ i ^ p ^ (n - i)) =
∑ i ∈ range n, C ((p : ℚ) ^ i) * wittStructureRat p (map (Int.castRingHom ℚ) Φ) i ^ p ^ (n - i) :=
by
rw [map_sum]
apply Finset.sum_congr rfl
intro i hi
rw [Finset.mem_range] at hi
simp only [IH i hi, RingHom.map_mul, RingHom.map_pow, map_C]
rfl
simp only [← sum_induction_steps, ← map_wittPolynomial p (Int.castRingHom ℚ), ← map_rename, ← map_bind₁,
← RingHom.map_sub, coeff_map]
rw [show (p : ℚ) ^ n = ((↑(p ^ n) : ℤ) : ℚ) by norm_cast]
rw [← Rat.den_eq_one_iff, eq_intCast, Rat.den_div_intCast_eq_one_iff]
swap; · exact mod_cast pow_ne_zero n hp.1.ne_zero
revert c; rw [← C_dvd_iff_dvd_coeff]
exact C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum Φ n IH
