map_eq_map — Mathlib

English

The induced map on perfections via the canonical inclusions is equal to the universal perfection map: map p (of p R) (of p S) φ = Perfection.map p φ.

Русский

Индуцированное отображение на перфекциях через канонические вложения равно универсальному отображению перфекции: map p (of p R) (of p S) φ = Perfection.map p φ.

LaTeX

$$$\mathrm{map}_p(\mathrm{of}_p R, \mathrm{of}_p S, \varphi) = \mathrm{Perfection.map}_p(\varphi)$$$

Lean4

theorem map_eq_map (φ : R →+* S) : map p (of p R) (of p S) φ = Perfection.map p φ :=
  hom_ext _ (of p S) fun f => by rw [map_map, Perfection.coeff_map]

Похожие утверждения