integralClosure_idem — Mathlib

English

The integral closure operation is idempotent in the sense that applying it twice yields the bottom subalgebra inside A.

Русский

Операция интегрального замыкания идиоматически идемпотентна: двойное замыкание внутри A даёт нижнее подалгебру.

LaTeX

$$$integralClosure(integralClosure(R,A),A) = \\bot$$$

Lean4

theorem integralClosure_idem {R A : Type*} [CommRing R] [CommRing A] [Algebra R A] :
    integralClosure (integralClosure R A) A = ⊥ :=
  letI := (integralClosure R A).algebra
  eq_bot_iff.2 fun x hx ↦ Algebra.mem_bot.2 ⟨⟨x, isIntegral_trans (A := integralClosure R A) x hx⟩, rfl⟩

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