English
For any ring hom φ: R →+* S and any f in Ring.Perfection R p, the coefficient map commutes with map p φ: coeff S p n (map p φ f) = φ (coeff R p n f).
Русский
Для любого гомоморфизма φ: R →+* S и любого f из Ring.Perfection R p коэффициент сохраняется при применении φ: coeff S p n (map p φ f) = φ (coeff R p n f).
LaTeX
$$$\\operatorname{coeff} S p n (\\text{map } p \\varphi f) = \\varphi(\\operatorname{coeff} R p n f)$$$
Lean4
/-- A ring homomorphism `R →+* S` induces `Perfection R p →+* Perfection S p`. -/
@[simps]
def map (φ : R →+* S) : Ring.Perfection R p →+* Ring.Perfection S p
where
toFun f := ⟨fun n => φ (coeff R p n f), fun n => by rw [← φ.map_pow, coeff_pow_p']⟩
map_one' := Subtype.eq <| funext fun _ => φ.map_one
map_mul' _ _ := Subtype.eq <| funext fun _ => φ.map_mul _ _
map_zero' := Subtype.eq <| funext fun _ => φ.map_zero
map_add' _ _ := Subtype.eq <| funext fun _ => φ.map_add _ _
