English
If R[X] → S generates S, T is the localization of S away from g, and f is a preimage of g in R[X], then the R-algebra map compLocalizationAwayAlgHom from the generators to the localization can be described as the unique algebra homomorphism sending each X_i to the corresponding element in S, and the special Y to the inverse of g, i.e., invSelf of the corresponding quotient element.
Русский
Если R[X] → S порождает S, T является локализацией S away по отношению к g, и f является предобразом g в R[X], то R‑алгебровое отображение compLocalizationAwayAlgHom из генераторов в локализацию задаётся как единственное алгебраическое отображение, посылающее каждые X_i в соответствующий элемент S, а специальную переменную Y — в обратное к g, то есть invSelf соответствующего элемента в твердом поле ок.
LaTeX
$$$compLocalizationAwayAlgHom\\ T\\ g\\ P = _$$
Lean4
/-- If `R[X] → S` generates `S`, `T` is the localization of `S` away from `g` and
`f` is a pre-image of `g` in `R[X]`, this is the `R`-algebra map `R[X,Y] →ₐ[R] (R[X]/I²)[1/f]`
defined via mapping `Y` to `1/f`. -/
noncomputable def compLocalizationAwayAlgHom :
((Generators.localizationAway T g).comp P).Ring →ₐ[R] Localization.Away (Ideal.Quotient.mk (P.ker ^ 2) (P.σ g)) :=
aeval (R := R) (S₁ := Localization.Away _)
(Sum.elim (fun _ ↦ IsLocalization.Away.invSelf <| (Ideal.Quotient.mk (P.ker ^ 2) (P.σ g)))
(fun i : ι ↦ algebraMap P.Ring _ (X i)))
