English
Let p be a prime. If P and Q are perfect rings of characteristic p, and R,S are commutative semirings of characteristic p, with ring homomorphisms π: P → R, σ: Q → S and φ: R → S, then there exists a canonical induced ring homomorphism map p m n φ: P → Q making the square commute, i.e. σ ∘ map p m n φ = φ ∘ π.
Русский
Пусть p — простое число. Пусть P и Q — совершенные кольца характеристики p, R и S — коммутативные полугруппы характеристики p, с кольмовыми гомоморфизмами π: P → R, σ: Q → S и φ: R → S. Тогда существует канонический индуцированный гомоморфизм map p m n φ: P → Q, который делает диаграмму равной: σ ∘ map p m n φ = φ ∘ π.
LaTeX
$$$\sigma \circ \big(\mathrm{map}_p\, m\, n\, \varphi\big) = \varphi \circ \pi$$$
Lean4
/-- A ring homomorphism `R →+* S` induces `P →+* Q`, a map of the respective perfections. -/
@[nolint unusedArguments]
noncomputable def map {π : P →+* R} (_ : PerfectionMap p π) {σ : Q →+* S} (n : PerfectionMap p σ) (φ : R →+* S) :
P →+* Q :=
lift p P S Q σ n <| φ.comp π
