English
The map version equates the composed map of WittStructureInt with rational Witt polynomials to WittStructureRat under the corresponding map, establishing a bridge between integral and rational constructions.
Русский
Совместимость отображения демонстрирует, что композиция WittStructureInt в сочетании с рациональными Witt-полиномами эквивалентна WittStructureRat при соответствующем отображении, устанавливая мост между целочисленной и рациональной конструкциями.
LaTeX
$$$map (Int.castRingHom ℚ) (wittStructureInt p Φ n) = wittStructureRat p (map (Int.castRingHom ℚ) Φ) n$$$
Lean4
theorem C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum (Φ : MvPolynomial idx ℤ) (n : ℕ)
(IH :
∀ m : ℕ,
m < n → map (Int.castRingHom ℚ) (wittStructureInt p Φ m) = wittStructureRat p (map (Int.castRingHom ℚ) Φ) m) :
(C ((p ^ n :) : ℤ) : MvPolynomial (idx × ℕ) ℤ) ∣
bind₁ (fun b : idx => rename (fun i => (b, i)) (wittPolynomial p ℤ n)) Φ -
∑ i ∈ range n, C ((p : ℤ) ^ i) * wittStructureInt p Φ i ^ p ^ (n - i) :=
by
rcases n with - | n
·
simp only [isUnit_one, pow_zero, C_1, IsUnit.dvd, Nat.cast_one]
-- prepare a useful equation for rewriting
have key := bind₁_rename_expand_wittPolynomial Φ n IH
apply_fun map (Int.castRingHom (ZMod (p ^ (n + 1)))) at key
conv_lhs at key =>
simp only [map_bind₁, map_rename, map_expand, map_wittPolynomial]
-- clean up and massage
rw [C_dvd_iff_zmod, RingHom.map_sub, sub_eq_zero, map_bind₁]
simp only [map_rename, map_wittPolynomial, wittPolynomial_zmod_self]
rw [key]; clear key IH
rw [bind₁, aeval_wittPolynomial, map_sum, map_sum, Finset.sum_congr rfl]
intro k hk
rw [Finset.mem_range, Nat.lt_succ_iff] at hk
rw [← sub_eq_zero, ← RingHom.map_sub, ← C_dvd_iff_zmod, C_eq_coe_nat, ← Nat.cast_pow, ← Nat.cast_pow, C_eq_coe_nat, ←
mul_sub]
have : p ^ (n + 1) = p ^ k * p ^ (n - k + 1) := by rw [← pow_add, ← add_assoc]; congr 2;
rw [add_comm, ← tsub_eq_iff_eq_add_of_le hk]
rw [this]
rw [Nat.cast_mul, Nat.cast_pow, Nat.cast_pow]
apply mul_dvd_mul_left ((p : MvPolynomial (idx × ℕ) ℤ) ^ k)
rw [show p ^ (n + 1 - k) = p * p ^ (n - k) by rw [← pow_succ', ← tsub_add_eq_add_tsub hk]]
rw [pow_mul]
-- the machine!
apply dvd_sub_pow_of_dvd_sub
rw [← C_eq_coe_nat, C_dvd_iff_zmod, RingHom.map_sub, sub_eq_zero, map_expand, RingHom.map_pow,
MvPolynomial.expand_zmod]
