English
The isomorphism for compact open subsets through finite-generated ideals asserts that a compact open subset is the complement of the zero locus of a finitely generated ideal.
Русский
Компактно-открытые подмножества корреспондируют через конечносгенерируемые идеалы: подмножество компактно и открыто тогда и только тогда, когда является дополнением к нуль-множеству FG-идеала.
LaTeX
$$$$ \text{IsCompact}(s) \wedge \text{IsOpen}(s) \iff \exists I \ (I \text{ FG}) \wedge (s = ( \operatorname{zeroLocus}(I) )^{c}). $$$$
Lean4
/-- Clopen subsets in the prime spectrum of a commutative semiring are in order-preserving
bijection with pairs of elements with product 0 and sum 1. (By definition, `(e₁, f₁) ≤ (e₂, f₂)`
iff `e₁ * e₂ = e₁`.) Both elements in such pairs must be idempotents, but there may exists
idempotents that do not form such pairs (does not have a "complement"). For example, in the
semiring {0, 0.5, 1} with ⊔ as + and ⊓ as *, 0.5 has no complement. -/
def mulZeroAddOneEquivClopens : { e : R × R // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 } ≃o Clopens (PrimeSpectrum R)
where
toEquiv :=
.ofBijective (fun e ↦ ⟨basicOpen e.1.1, isClopen_iff_mul_add.mpr ⟨_, _, e.2.1, e.2.2, rfl⟩⟩) <|
by
refine ⟨fun ⟨x, hx⟩ ⟨y, hy⟩ eq ↦ mul_eq_zero_add_eq_one_ext_left ?_, fun s ↦ ?_⟩
·
exact
basicOpen_injOn_isIdempotentElem (IsIdempotentElem.of_mul_add hx.1 hx.2).1
(IsIdempotentElem.of_mul_add hy.1 hy.2).1 <|
SetLike.ext' (congr_arg (·.1) eq)
· have ⟨e, f, mul, add, eq⟩ := isClopen_iff_mul_add.mp s.2
exact ⟨⟨(e, f), mul, add⟩, SetLike.ext' eq.symm⟩
map_rel_iff'
{a
b} :=
show basicOpen _ ≤ basicOpen _ ↔ _ by
rw [← inf_eq_left, ← basicOpen_mul]
refine ⟨fun h ↦ ?_, (by rw [·])⟩
rw [← inf_eq_left]
have := (IsIdempotentElem.of_mul_add a.2.1 a.2.2).1
exact
mul_eq_zero_add_eq_one_ext_left
(basicOpen_injOn_isIdempotentElem (this.mul (IsIdempotentElem.of_mul_add b.2.1 b.2.2).1) this h)
