map_map — Mathlib

English

For all elements x in P and φ: R → S, the image under the perfection-map equals the value of φ on the original element, i.e., σ(map p m n φ x) = φ(π x).

Русский

Для каждого x ∈ P и φ: R → S, образ через отображение перфекции равен значению φ на исходный элемент: σ(map p m n φ x) = φ(π x).

LaTeX

$$$\sigma\big(\mathrm{map}_p\, m\, n\, \varphi\, x\big) = \varphi\big(\pi x\big)$$$

Lean4

theorem map_map {π : P →+* R} (m : PerfectionMap p π) {σ : Q →+* S} (n : PerfectionMap p σ) (φ : R →+* S) (x : P) :
    σ (map p m n φ x) = φ (π x) :=
  RingHom.ext_iff.1 (comp_map p m n φ) x

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