closedsEmbedding — Mathlib

English

The antitone order embedding sends closed subsets of Spec R to ideals of R via the vanishing ideal.

Русский

Анти-порядковое вложение отображает замкнутые подмножества Spec R в идеалы R через vanishingIdeal.

LaTeX

$$$\\text{closedsEmbedding}(R) : (\\operatorname{TopologicalSpace.Closeds}(\\operatorname{PrimeSpectrum}(R)))^{\\mathrm{op}} \\hookrightarrow \\operatorname{Ideal}(R)$$$

Lean4

/-- The antitone order embedding of closed subsets of `Spec R` into ideals of `R`. -/
def closedsEmbedding (R : Type*) [CommSemiring R] : (TopologicalSpace.Closeds <| PrimeSpectrum R)ᵒᵈ ↪o Ideal R :=
  OrderEmbedding.ofMapLEIff (fun s => vanishingIdeal ↑(OrderDual.ofDual s)) fun s _ =>
    (vanishingIdeal_anti_mono_iff s.2).symm

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