English
For hy: M ≤ T.comap g, the map map Q g hy sends algebraMap_R_S x to algebraMap_P_Q (g x).
Русский
При гипотезе hy: M ≤ T.comap g отображение map Q g hy отправляет algebraMap_R_S x в algebraMap_P_Q (g x).
LaTeX
$$$ map\\ Q\\ g\\ hy\\ ((\\mathrm{algebraMap}_{R,S})\\, x) = (\\mathrm{algebraMap}_{P,Q})\\,(g\\,x). $$$
Lean4
/-- Map a homomorphism `g : R →+* P` to `S →+* Q`, where `S` and `Q` are
localizations of `R` and `P` at `M` and `T` respectively,
such that `g(M) ⊆ T`.
We send `z : S` to `algebraMap P Q (g x) * (algebraMap P Q (g y))⁻¹`, where
`(x, y) : R × M` are such that `z = f x * (f y)⁻¹`. -/
noncomputable def map (g : R →+* P) (hy : M ≤ T.comap g) : S →+* Q :=
lift (M := M) (g := (algebraMap P Q).comp g) fun y => map_units _ ⟨g y, hy y.2⟩
