English
For f ∈ Ring.Perfection R p and n,m ∈ ℕ with m ≤ n, coeff R p n ((frobenius _ p)^[m] f) = coeff R p (n-m) f.
Русский
Для f ∈ Ring.Perfection R p и n,m ∈ ℕ с условием m ≤ n, coeff R p n ((frobenius _ p)^[m] f) = coeff R p (n-m) f.
LaTeX
$$$\\operatorname{coeff} R p n\\big((\\mathrm{frobenius}_{p})^{[m]} f\\big) = \\operatorname{coeff} R p (n-m) f$$$
Lean4
/-- Create a `PerfectionMap` from an isomorphism to the perfection. -/
@[simps]
theorem mk' {f : P →+* R} (g : P ≃+* Ring.Perfection R p) (hfg : Perfection.lift p P R f = g) : PerfectionMap p f :=
{ injective := fun x y hxy =>
g.injective <|
(RingHom.ext_iff.1 hfg x).symm.trans <|
Eq.symm <| (RingHom.ext_iff.1 hfg y).symm.trans <| Perfection.ext fun n => (hxy n).symm
surjective := fun y hy =>
let ⟨x, hx⟩ := g.surjective ⟨y, hy⟩
⟨x, fun n =>
show Perfection.coeff R p n (Perfection.lift p P R f x) = Perfection.coeff R p n ⟨y, hy⟩ by simp [hfg, hx]⟩ }
