equivSubtype — Mathlib

English

The equivalence between MaximalSpectrum and maximal ideals has a constructive proof via an explicit pair of maps forming inverses.

Русский

Эквивалентность между спектром максимальных идеалов и максимальными идеалами имеет конструктивное доказательство через явные отображения, образующие обратные.

LaTeX

$$equivSubtype is an Equiv between MaximalSpectrum and { I : Ideal R // I.IsMaximal } with toFun and invFun defined as in the statement.$$

Lean4

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

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