English
Let A ⊆ B be domains with a domain extension, and let K,L be their respective fraction fields with compatible algebras. There exists a canonical extension map extendedHom_A,B: FractionalIdeal A⁰ K → FractionalIdeal B⁰ L, defined by extending along the injection using nonZeroDivisors to compare the zero divisors properly.
Русский
Пусть A ⊆ B — области интегрирования, и пусть K, L — их поля дробных и соответствующие алгебры. Существует каноническое отображение расширения extendedHom_A,B: FractionalIdeal A⁰ K → FractionalIdeal B⁰ L, задающееся расширением вдоль включения с учетом nonZeroDivisors для корректного сравнения нулевых делителей.
LaTeX
$$$$\exists \phi: \mathrm{FractionalIdeal}(A^{0}K) \to \mathrm{FractionalIdeal}(B^{0}L)\; \text{ring hom},\quad \phi(I)=\mathrm{extendedHom}\,L\ hf\,(I)\text{ with }hf=\text{nonZeroDivisors-le-comap-nonZeroDivisors-of-injective}.$$$$
Lean4
/-- The ring homomorphisme that extends a fractional ideal of `A` to a fractional ideal of `B` for
`A ⊆ B` an extension of domains.
-/
abbrev extendedHomₐ : FractionalIdeal A⁰ K →+* FractionalIdeal B⁰ L :=
extendedHom L <| nonZeroDivisors_le_comap_nonZeroDivisors_of_injective _ (FaithfulSMul.algebraMap_injective _ _)
