English
If IsAdicComplete I R holds, then the I-adic ideal I is contained in the Jacobson radical of R.
Русский
Пусть выполняется IsAdicComplete I R; тогда I ⊆ jacobson(⊥).
LaTeX
$$$I \le (\perp : \text{Ideal } R).jacobson$$$
Lean4
theorem le_jacobson_bot [IsAdicComplete I R] : I ≤ (⊥ : Ideal R).jacobson :=
by
intro x hx
rw [← Ideal.neg_mem_iff, Ideal.mem_jacobson_bot]
intro y
rw [add_comm]
let f : ℕ → R := fun n => ∑ i ∈ range n, (x * y) ^ i
have hf : ∀ m n, m ≤ n → f m ≡ f n [SMOD I ^ m • (⊤ : Submodule R R)] :=
by
intro m n h
simp only [f, Algebra.id.smul_eq_mul, Ideal.mul_top, SModEq.sub_mem]
rw [← add_tsub_cancel_of_le h, Finset.sum_range_add, ← sub_sub, sub_self, zero_sub, @neg_mem_iff]
apply Submodule.sum_mem
intro n _
rw [mul_pow, pow_add, mul_assoc]
exact Ideal.mul_mem_right _ (I ^ m) (Ideal.pow_mem_pow hx m)
obtain ⟨L, hL⟩ := IsPrecomplete.prec toIsPrecomplete @hf
rw [isUnit_iff_exists_inv]
use L
rw [← sub_eq_zero, neg_mul]
apply IsHausdorff.haus (toIsHausdorff : IsHausdorff I R)
intro n
specialize hL n
rw [SModEq.sub_mem, Algebra.id.smul_eq_mul, Ideal.mul_top] at hL ⊢
rw [sub_zero]
suffices (1 - x * y) * f n - 1 ∈ I ^ n
by
convert Ideal.sub_mem _ this (Ideal.mul_mem_left _ (1 + -(x * y)) hL) using 1
ring
cases n
· simp only [Ideal.one_eq_top, pow_zero, mem_top]
· rw [← neg_sub _ (1 : R), neg_mul, mul_geom_sum, neg_sub, sub_sub, add_comm (_ ^ _), ← sub_sub, sub_self, zero_sub,
@neg_mem_iff, mul_pow]
exact Ideal.mul_mem_right _ (I ^ _) (Ideal.pow_mem_pow hx _)
