English
For any σ, Φ ∈ MvPolynomial idx ℤ, f : idx → σ, and n, the Witt-structure after renaming commutes with renaming on the output: wittStructureInt p (rename f Φ) n = rename (Prod.map f id) (wittStructureInt p Φ n).
Русский
Для произвольного отображения f : idx → σ, переход WittStructureInt через переименование совпадает с переименованием выходной структуры: wittStructureInt p (rename f Φ) n = rename (Prod.map f id) (wittStructureInt p Φ n).
LaTeX
$$$\\forall (σ) (f : idx \\to σ) (n : \\mathbb{N}), \\\\ wittStructureInt p (rename f Φ) n = rename (Prod.map f id) (wittStructureInt p Φ n)$$$
Lean4
theorem wittStructureInt_rename {σ : Type*} (Φ : MvPolynomial idx ℤ) (f : idx → σ) (n : ℕ) :
wittStructureInt p (rename f Φ) n = rename (Prod.map f id) (wittStructureInt p Φ n) :=
by
apply MvPolynomial.map_injective (Int.castRingHom ℚ) Int.cast_injective
simp only [map_rename, map_wittStructureInt, wittStructureRat, rename_bind₁, rename_rename, bind₁_rename]
rfl
