English
The basic open sets separate idempotents: if e is idempotent, the map to basicOpen is injective on {e | IsIdempotentElem e}.
Русский
Базовые opens разделяют идемпотентные элементы: отображение в basicOpen инъективно на множество идемпотентных элементов.
LaTeX
$$$<{e: R | IsIdempotentElem e}>.InjOn\\;\\text{basicOpen}$$$
Lean4
theorem basicOpen_injOn_isIdempotentElem : {e : R | IsIdempotentElem e}.InjOn basicOpen := fun x hx y hy eq ↦
by
by_contra! ne
wlog ne' : x * y ≠ x generalizing x y
· apply this y hy x hx eq.symm ne.symm
rwa [mul_comm, of_not_not ne']
have : x ∉ Ideal.span { y } := fun mem ↦
ne' <| by
obtain ⟨r, rfl⟩ := Ideal.mem_span_singleton'.mp mem
rw [mul_assoc, hy]
have ⟨p, prime, le, notMem⟩ := Ideal.exists_le_prime_notMem_of_isIdempotentElem _ x hx this
exact ne_of_mem_of_not_mem' (a := ⟨p, prime⟩) notMem (not_not.mpr <| p.span_singleton_le_iff_mem.mp le) eq
