isIntegral_iff_isIntegral_closure_finite

English

Equivalence for IsIntegral and existence of finite subring closures; IsIntegral R r iff ∃ finite S with IsIntegral (Subring.closure S) r.

Русский

Эквивалентность интегральности: IsIntegral R r эквивалентно существованию конечного подкольца, для которого r интегрален.

LaTeX

$$$\\text{IsIntegral}_R(r) \\iff \\exists s, s.Finite \\land \\text{IsIntegral}(\\operatorname{Subring.closure}(s), r)$$$

Lean4

theorem isIntegral_iff_isIntegral_closure_finite {r : B} :
    IsIntegral R r ↔ ∃ s : Set R, s.Finite ∧ IsIntegral (Subring.closure s) r :=
  by
  constructor <;> intro hr
  · rcases hr with ⟨p, hmp, hpr⟩
    refine ⟨_, Finset.finite_toSet _, p.restriction, monic_restriction.2 hmp, ?_⟩
    rw [← aeval_def, ← aeval_map_algebraMap R r p.restriction, map_restriction, aeval_def, hpr]
  rcases hr with ⟨s, _, hsr⟩
  exact hsr.of_subring _

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