English
There exists a canonical algebra homomorphism lift: S → A that sends each s ∈ S to the integral closure element corresponding to algebraMap(S,B) of s via mk'.
Русский
Существует каноническое алгебраическое отображение lift: S → A, отправляющее каждое s ∈ S в соответствующий элемент интегрального замыкания через mk'.
LaTeX
$$$\text{lift} : S \to_R A \text{ is an } R\text{-algebra homomorphism with } \text{toFun}(x) = \mathrm{mk'}\ A (\mathrm{algebraMap}\ S B\ x) (\text{IsIntegral.algebraMap}...)$$$
Lean4
/-- If `B / S / R` is a tower of ring extensions where `S` is integral over `R`,
then `S` maps (uniquely) into an integral closure `B / A / R`. -/
noncomputable def lift : S →ₐ[R] A
where
toFun x := mk' A (algebraMap S B x) (IsIntegral.algebraMap (Algebra.IsIntegral.isIntegral (R := R) x))
map_one' := by simp only [RingHom.map_one, mk'_one]
map_zero' := by simp only [RingHom.map_zero, mk'_zero]
map_add' x y := by simp_rw [← mk'_add, map_add]
map_mul' x y := by simp_rw [← mk'_mul, RingHom.map_mul]
commutes' x := by simp_rw [← IsScalarTower.algebraMap_apply, mk'_algebraMap]
