of_isIntegrallyClosedIn — Mathlib

English

If R ⊆ A ⊆ B with IsIntegralClosure A R B, then IsIntegrallyClosedIn A B.

Русский

Если R ⊆ A ⊆ B и IsIntegralClosure A R B, то IsIntegrallyClosedIn A B.

LaTeX

$$$IsIntegralClosure\,A\,R\,B \Rightarrow IsIntegrallyClosedIn\,A\,B$$$

Lean4

theorem _root_.IsIntegralClosure.of_isIntegrallyClosedIn [Algebra R B] [Algebra A B] [IsScalarTower R A B]
    [IsIntegrallyClosedIn A B] [Algebra.IsIntegral R A] : IsIntegralClosure A R B :=
  by
  refine
    ⟨IsIntegralClosure.algebraMap_injective _ A _, fun {x} ↦
      ⟨fun hx ↦ IsIntegralClosure.isIntegral_iff.mp (IsIntegral.tower_top (A := A) hx), ?_⟩⟩
  rintro ⟨y, rfl⟩
  exact IsIntegral.map (IsScalarTower.toAlgHom A A B) (Algebra.IsIntegral.isIntegral y)

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