Theorems · Definition · algebraic geometry

PrimeSpectrum.mulZeroAddOneEquivClopens

{R : Type u} →
  [inst : CommSemiring R] → { e // e.1 * e.2 = 0 ∧ e.1 + e.2 = 1 } ≃o TopologicalSpace.Clopens (PrimeSpectrum R)

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.

Defined in

Mathlib.RingTheory.Spectrum.Prime.Topology

Cited by

0 results in Mathlib

Foundations

Depth 92 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiring