English
There is a canonical distinguished tensor x := elem(R,S) ∈ S ⊗_R S that encodes the unramified data; it satisfies the relations used in the unramified criterion.
Русский
Существует канонический выделенный тензор x := elem(R,S) ∈ S ⊗_R S, который кодирует данные неразветвленности; он удовлетворяет-relations из критерия неразветвленности.
LaTeX
$$$\\text{elem} \\in S \\otimes_R S \\quad \\text{such that ...}$$$
Lean4
/-- A finite-type `R`-algebra `S` is (formally) unramified iff there exists a `t : S ⊗[R] S` satisfying
1. `t` annihilates every `1 ⊗ s - s ⊗ 1`.
2. the image of `t` is `1` under the map `S ⊗[R] S → S`.
See `Algebra.FormallyUnramified.iff_exists_tensorProduct`.
This is the choice of such a `t`.
-/
noncomputable def elem : S ⊗[R] S :=
(iff_exists_tensorProduct.mp inferInstance).choose
