English
A key morphism-level equality showing that applying a renamed and expanded Witt polynomial inside a bind operation equals applying expansion on the WittStructureInt built from Φ, under suitable IH hypothesis.
Русский
Ключевое тождество на уровне отображений: применение переименованного и расширенного Witt-полинома внутри bind равняется применению расширения к WittStructureInt, построенному из Φ, при подходящем IH-гипотезе.
LaTeX
$$$bind₁ (\text{fun } b => rename (fun i => (b,i)) (expand p (W_ ℤ n))) Φ = bind₁ (\text{fun i => expand p (wittStructureInt p Φ i)}) (W_ ℤ n)$$$
Lean4
theorem bind₁_rename_expand_wittPolynomial (Φ : MvPolynomial idx ℤ) (n : ℕ)
(IH :
∀ m : ℕ,
m < n + 1 →
map (Int.castRingHom ℚ) (wittStructureInt p Φ m) = wittStructureRat p (map (Int.castRingHom ℚ) Φ) m) :
bind₁ (fun b => rename (fun i => (b, i)) (expand p (W_ ℤ n))) Φ =
bind₁ (fun i => expand p (wittStructureInt p Φ i)) (W_ ℤ n) :=
by
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
simp only [map_bind₁, map_rename, map_expand, rename_expand, map_wittPolynomial]
have key := (wittStructureRat_prop p (map (Int.castRingHom ℚ) Φ) n).symm
apply_fun expand p at key
simp only [expand_bind₁] at key
rw [key]; clear key
apply eval₂Hom_congr' rfl _ rfl
rintro i hi -
rw [wittPolynomial_vars, Finset.mem_range] at hi
simp only [IH i hi]
