English
The ring homomorphism mapRingHom f: 𝓞 K → 𝓞 L is defined by sending ⟨x,hx⟩ to ⟨f x, map_isIntegral_int f x hx⟩, preserving ring operations.
Русский
Кольцо отображение mapRingHom f: 𝓞K → 𝓞L определяется отображением ⟨x,hx⟩ ↦ ⟨f(x), map_isIntegral_int f x hx⟩ и сохраняет операции кольца.
LaTeX
$$$\\mathrm{mapRingHom}(f)(\\langle x,hx\\rangle) = \\langle f(x), map\\_isIntegral\\_int f x hx\\rangle$$$
Lean4
/-- The ring homomorphism `(𝓞 K) →+* (𝓞 L)` given by restricting a ring homomorphism
`f : K →+* L` to `𝓞 K`. -/
def mapRingHom {K L : Type*} [Field K] [Field L] (f : K →+* L) : (𝓞 K) →+* (𝓞 L)
where
toFun k := ⟨f k.val, map_isIntegral_int f k.2⟩
map_zero' := by ext; simp only [map_mk, map_zero]
map_one' := by ext; simp only [map_mk, map_one]
map_add' x y := by ext; simp only [map_mk, map_add]
map_mul' x y := by ext; simp only [map_mk, map_mul]
