instIsStandardOpenImmersionTensorProduct

English

If IsStandardOpenImmersion holds for R and T, then it holds for S and TensorProduct R, S, T.

Русский

Если IsStandardOpenImmersion выполняется для R и T, то она выполняется и для S и TensorProduct R,S,T.

LaTeX

$$$\operatorname{IsStandardOpenImmersion}(R,T) \Rightarrow \operatorname{IsStandardOpenImmersion}(S, \mathrm{TensorProduct}_R(S,T)).$$$

Lean4

instance [IsStandardOpenImmersion R T] : IsStandardOpenImmersion S (S ⊗[R] T) :=
  let ⟨r, _⟩ := exists_away R T
  ⟨algebraMap R S r, inferInstance⟩

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