English
The mapAlgHom {k K L F} sends an algebra hom f: K →ᴬ[k] L to an algebra hom 𝓞K →ᴬ[𝓞k] 𝓞L by restricting scalars to 𝓞k and using mapRingHom on the underlying rings.
Русский
Функция mapAlgHom преобразует алгебра-гомоморфизм f: K →ᴬ[k] L в алгебра-гомоморфизм 𝓞K →ᴬ[𝓞k] 𝓞L за счёт ограничения скаляров к 𝓞k и применения mapRingHom к основанным кольцам.
LaTeX
$$$\\text{mapAlgHom}(f) : (\\mathcal{O}_K) \\to_{\\mathcal{O}_k} (\\mathcal{O}_L)$$$
Lean4
/-- The algebra homomorphism `(𝓞 K) →ₐ[𝓞 k] (𝓞 L)` given by restricting an algebra homomorphism
`f : K →ₐ[k] L` to `𝓞 K`. -/
def mapAlgHom {k K L F : Type*} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] [FunLike F K L]
[AlgHomClass F k K L] (f : F) : (𝓞 K) →ₐ[𝓞 k] (𝓞 L)
where
toRingHom := mapRingHom f
commutes' x := SetCoe.ext (AlgHomClass.commutes ((f : K →ₐ[k] L).restrictScalars (𝓞 k)) x)
