equivSubtype — Mathlib

English

There is a bijection preserving order between PrimeSpectrum R and the subtype { I : Ideal R | I.IsPrime }.

Русский

Существует биекция, сохраняющая порядок, между PrimeSpectrum R и подмножеством { I : Ideal R | I.IsPrime }.

LaTeX

$$$\text{Equiv}(\mathrm{PrimeSpectrum}(R), \{ I : \mathrm{Ideal}(R) \mid I.IsPrime \})$$$

Lean4

/-- The prime spectrum is in bijection with the set of prime ideals. -/
@[simps]
def equivSubtype : PrimeSpectrum R ≃o { I : Ideal R // I.IsPrime }
    where
  toFun I := ⟨I.asIdeal, I.2⟩
  invFun I := ⟨I, I.2⟩
  map_rel_iff' := .rfl

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