continuous_tensorProductTo — Mathlib

English

Let R,S,T be commutative rings with S and T endowed with R-algebra structures. Then the canonical map tensorProductTo R S T on prime spectra is a continuous map.

Русский

Пусть R,S,T — коммутативные кольца, S и T являются R-алгебрами. Тогда каноническое отображение tensorProductTo R S T между спектрами примар непрерывно.

LaTeX

$$$\\mathrm{Continuous}\\bigl(\\mathrm{tensorProductTo}(R,S,T)\\bigr)$$$

Lean4

@[fun_prop]
theorem continuous_tensorProductTo : Continuous (tensorProductTo R S T) :=
  (comap _).2.prodMk (comap _).2

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