English
There is a map IsFractionRing.map that, given rings A,B with IsDomain B, and j : A →+* B, provides K →+* L under injectivity of j, compatible with localization.
Русский
Существует отображение IsFractionRing.map, которое при дании кольца A,B с областью B дает отображение K →+* L и совместимо с локализацией через инъекцию j.
LaTeX
$$$\text{noncomputable def map }{A B K L} \{...\} (j : A →+* B) (hj : Injective j) : K →+* L$$$
Lean4
/-- Given commutative rings `A, B` where `B` is an integral domain, with fraction rings `K`, `L`
and an injective ring hom `j : A →+* B`, we get a ring hom
sending `z : K` to `g (j x) * (g (j y))⁻¹`, where `(x, y) : A × (NonZeroDivisors A)` are
such that `z = f x * (f y)⁻¹`. -/
noncomputable def map {A B K L : Type*} [CommRing A] [CommRing B] [IsDomain B] [CommRing K] [Algebra A K]
[IsFractionRing A K] [CommRing L] [Algebra B L] [IsFractionRing B L] {j : A →+* B} (hj : Injective j) : K →+* L :=
IsLocalization.map L j
(show nonZeroDivisors A ≤ (nonZeroDivisors B).comap j from
nonZeroDivisors_le_comap_nonZeroDivisors_of_injective j hj)
