equiv — Mathlib

English

All integral closures in towers are mutually isomorphic via the lift maps.

Русский

Все интегральные замыкания в башнях взаимно изоморфны через отображения lift.

LaTeX

$$IsIntegralClosure.equiv : A ≃ₐ[R] A'$$

Lean4

/-- Integral closures are all isomorphic to each other. -/
noncomputable def equiv : A ≃ₐ[R] A' :=
  AlgEquiv.ofAlgHom (lift R A' B (isIntegral := isIntegral_algebra R B))
    (lift R A B (isIntegral := isIntegral_algebra R B)) (by ext x; apply algebraMap_injective A' R B; simp)
    (by ext x; apply algebraMap_injective A R B; simp)

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