English
An equality showing how the bind operation with a renamed Witt polynomial interacts with the expansion map, leading to a standard renaming of the Witt polynomial under the W-structure map.
Русский
Равенство, показывающее, как операция bind с переименованным Witt-полином взаимодействует с отображением расширения, приводя к стандартному переименованию Witt-полинома под структурой W.
LaTeX
$$$bind_₁ (fun b => rename (fun i => (b,i)) (expand p (W_ ℤ n))) Φ = bind_₁ (fun i => expand p (wittStructureInt p Φ i)) (W_ ℤ n)$$$
Lean4
theorem wittStructureRat_prop (Φ : MvPolynomial idx ℚ) (n : ℕ) :
bind₁ (wittStructureRat p Φ) (W_ ℚ n) = bind₁ (fun i => rename (Prod.mk i) (W_ ℚ n)) Φ :=
calc
bind₁ (wittStructureRat p Φ) (W_ ℚ n) =
bind₁ (fun k => bind₁ (fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (bind₁ (xInTermsOfW p ℚ) (W_ ℚ n)) :=
by rw [bind₁_bind₁]; exact eval₂Hom_congr (RingHom.ext_rat _ _) rfl rfl
_ = bind₁ (fun i => rename (Prod.mk i) (W_ ℚ n)) Φ := by rw [bind₁_xInTermsOfW_wittPolynomial p _ n, bind₁_X_right]
