English
Let A, B be commutative rings with a ring hom f: A → B, and let M ⊆ A and N ⊆ B be multiplicative submonoids such that M ≤ f^{-1}(N). Let K be the localization of A at M and L the localization of B at N. Then there exists a ring homomorphism extending along the localization, from fractional ideals over (M, K) to fractional ideals over (N, L), whose action on an ideal I is given by the extension along L with hf.
Русский
Пусть A, B — кольца с коммутативной структурой, есть кольцевое отображение f: A → B, и пусть M ⊆ A, N ⊆ B являются мультипликативными подмонойдами так, что M ≤ Submonoid.comap f N. Пусть K — локализация A по M, L — локализация B по N. Тогда существует группа гомоморфизма, расширяющего вдоль локализации, от дробных идеалов на (M, K) к дробным идеалам на (N, L), действующий на идеале I как расширение along L с hf.
LaTeX
$$$$\exists \phi: \mathrm{FractionalIdeal}(M,K) \to \mathrm{FractionalIdeal}(N,L)\; \text{ring hom},\quad \forall I \in \mathrm{FractionalIdeal}(M,K),\ \phi(I)=\mathrm{extended}(L,hf)(I).$$$$
Lean4
/-- The ring homomorphism version of `FractionalIdeal.extended`.
-/
@[simps]
def extendedHom : FractionalIdeal M K →+* FractionalIdeal N L
where
toFun := extended L hf
map_one' := extended_one L hf
map_zero' := extended_zero L hf
map_mul' := extended_mul L hf
map_add' := extended_add L hf
