English
From a surjective algebra homomorphism f: P →ₐ[R] S one can construct an extension of R by S whose Ring is P and whose σ and algebraMap_σ are induced by a choice of preimage for each x ∈ R.
Русский
Из сюръективного алгебраического однородного отображения f: P →ₐ[R] S строится расширение R над S, где Ring совпадает с P, а σ и algebraMap_σ задаются выбором предобраза для каждого x∈R.
LaTeX
$$$\\text{Ext}_{surj}(R,S; f) : \\exists \\mathcal{E}:\\mathrm{Extension}\\,R\\,S\\text{ с Ring}=P,\\ \\sigma\\text{ и алгMap}_σ\\text{ получены из f}$$$
Lean4
/-- Construct `Extension` from a surjective algebra homomorphism. -/
@[simps -isSimp Ring σ]
noncomputable def ofSurjective {P : Type w} [CommRing P] [Algebra R P] (f : P →ₐ[R] S) (h : Function.Surjective f) :
Extension.{w} R S where
Ring := P
algebra₂ := f.toAlgebra
isScalarTower :=
letI := f.toAlgebra;
IsScalarTower.of_algebraMap_eq' f.comp_algebraMap.symm
σ x := (h x).choose
algebraMap_σ x := (h x).choose_spec
