English
Let R be a commutative ring, A and B be R-algebras. If A is integral over R and f: A → B is a surjective R-algebra homomorphism, then B is integral over R.
Русский
Пусть R — коммутативное кольцо, A и B — R-алгебры. Если A интегральна над R и отображение f: A → B является сюръективным гомоморфизмом R-алгебр, то B интегральна над R.
LaTeX
$$$\text{If } A \text{ is integral over } R \text{ and } f: A \to B \text{ is a surjective } R\text{-algebra homomorphism, then } B \text{ is integral over } R.$$$
Lean4
/-- Homomorphic image of an integral algebra is an integral algebra. -/
theorem of_surjective [Algebra.IsIntegral R A] (f : A →ₐ[R] B) (hf : Function.Surjective f) : Algebra.IsIntegral R B :=
isIntegral_def.mpr fun b ↦
let ⟨a, ha⟩ := hf b;
ha ▸ (isIntegral_def.mp ‹_› a).map f
