English
The main property of wittStructureRat is that applying bind₁ with the Witt polynomial recovers the renaming composition with W_ℚ n, ensuring the canonical behavior of the Witt structure in the rational setting.
Русский
Основное свойство wittStructureRat: применение bind₁ с Witt-полином восстанавливает переименование и композицию с W_ℚ n, обеспечивая каноническое поведение Witt-структуры в рациональной настройке.
LaTeX
$$$bind_₁ wittStructureRat p Φ (W_ ℚ n) = bind₁ (\lambda i. rename (Prod.mk i) (W_ ℚ n)) Φ$$$
Lean4
/-- Write `wittStructureRat p φ n` in terms of `wittStructureRat p φ i` for `i < n`. -/
theorem wittStructureRat_rec (Φ : MvPolynomial idx ℚ) (n : ℕ) :
wittStructureRat p Φ n =
C (1 / (p : ℚ) ^ n) *
(bind₁ (fun b => rename (fun i => (b, i)) (W_ ℚ n)) Φ -
∑ i ∈ range n, C ((p : ℚ) ^ i) * wittStructureRat p Φ i ^ p ^ (n - i)) :=
by
calc
wittStructureRat p Φ n = C (1 / (p : ℚ) ^ n) * (wittStructureRat p Φ n * C ((p : ℚ) ^ n)) := ?_
_ = _ := by rw [wittStructureRat_rec_aux]
rw [mul_left_comm, ← C_mul, div_mul_cancel₀, C_1, mul_one]
exact pow_ne_zero _ (Nat.cast_ne_zero.2 hp.1.ne_zero)
