le_integralClosure_iff_isIntegral

English

For a subalgebra S ≤ A, S is contained in integralClosure R A iff S is integral over R.

Русский

Для подалгебры S ≤ A, S ≤ integralClosure R A тогда и только тогда, когда S интегральна над R.

LaTeX

$$$S \\leq integralClosure\\ R\\ A \\iff Algebra.IsIntegral\\ R S$$$

Lean4

theorem le_integralClosure_iff_isIntegral {S : Subalgebra R A} : S ≤ integralClosure R A ↔ Algebra.IsIntegral R S :=
  SetLike.forall.symm.trans <|
    (forall_congr' fun x =>
          show IsIntegral R (algebraMap S A x) ↔ IsIntegral R x from
            isIntegral_algebraMap_iff Subtype.coe_injective).trans
      Algebra.isIntegral_def.symm

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