primeSpectrumOrderEquiv — Mathlib

English

An ordered version of the prime spectrum equivalence, respecting the order between overrings.

Русский

Упорядоченная версия эквивианты прайм-спектра, сохраняющая порядок переобъемов.

LaTeX

$$primeSpectrumOrderEquiv : (PrimeSpectrum A)^{\mathrm{op}} \; \cong_o\; { S // A ≤ S }$$

Lean4

/-- An ordered variant of `primeSpectrumEquiv`. -/
@[simps!]
def primeSpectrumOrderEquiv : (PrimeSpectrum A)ᵒᵈ ≃o { S // A ≤ S } :=
  { OrderDual.ofDual.trans (primeSpectrumEquiv A) with
    map_rel_iff'
      {a
        b} :=
      ⟨a.rec <| fun a =>
          b.rec <| fun b => fun h => by
            simp only [OrderDual.toDual_le_toDual]
            dsimp at h
            have := idealOfLE_le_of_le A _ _ ?_ ?_ h
            · rwa [idealOfLE_ofPrime, idealOfLE_ofPrime] at this
            all_goals exact le_ofPrime A (PrimeSpectrum.asIdeal _),
        fun h => by apply ofPrime_le_of_le; exact h⟩ }

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