mapIntegralClosure — Mathlib

English

An algebra homomorphism f: A →ₐ[R] S restricts to an algebra homomorphism between the integral closures inside A and S.

Русский

Алгебраическое гомоморфизм f: A →ₐ[R] S ограничивает себя до гомоморфизма между интегральными замыканиями внутри A и S.

LaTeX

$$$\mathrm{mapIntegralClosure} : \text{integralClosure } R A \to_{} \text{integralClosure } R S$$$

Lean4

/-- An `AlgHom` between two rings restrict to an `AlgHom` between the integral closures inside
them. -/
def mapIntegralClosure [Algebra R S] (f : A →ₐ[R] S) : integralClosure R A →ₐ[R] integralClosure R S :=
  (f.restrictDomain (integralClosure R A)).codRestrict (integralClosure R S) (fun ⟨_, h⟩ => h.map f)

Похожие утверждения