English
There is an Equiv between the root sets of expand R(p^n) f and f not dependent on chosen representatives.
Русский
Существует эквивалентность между множестами корней expand_R(p^n) f и f без привязки к конкретным представителям.
LaTeX
$$$\operatorname{RootsExpandPowEquivRoots}(p,f,n)\;:\; (\mathrm{roots}(\operatorname{expand}_R(p^n,f)))^{\text{toFinset}} \simeq (\mathrm{roots}(f))^{\text{toFinset}}$$$
Lean4
/-- If `f` is a polynomial over a perfect integral domain `R` of characteristic `p`, then there is
a bijection from the set of roots of `Polynomial.expand R (p ^ n) f` to the set of roots of `f`.
It's given by `x ↦ x ^ (p ^ n)`, see `rootsExpandPowEquivRoots_apply`. -/
noncomputable def rootsExpandPowEquivRoots (n : ℕ) : (expand R (p ^ n) f).roots.toFinset ≃ f.roots.toFinset :=
((iterateFrobeniusEquiv R p n).image _).trans <|
.setCongr <|
show _ '' (setOf (· ∈ _)) = setOf (· ∈ _) by
classical
simp_rw [← roots_expand_image_iterateFrobenius (p := p) (f := f) (n := n), Finset.mem_val, Finset.setOf_mem,
Finset.coe_image, RingEquiv.toEquiv_eq_coe, EquivLike.coe_coe, iterateFrobeniusEquiv_apply]
