lattice-isomorphism-spectrum

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.lattice_isomorphism_induces_homeomorphism

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

An isomorphism $\Phi:L\to K$ of complete lattices induces the canonical homeomorphism of Stone spectra

\Phi_*:Q(L)\longrightarrow Q(K),\qquad \Phi_*(\mathfrak B)=\{\Phi(a):a\in\mathfrak B\}.

No converse from homeomorphic Stone spectra to lattice isomorphism is asserted.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P20

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P20

open Set TopologicalSpace

open QAlgorithms.Papers.Independent.Next46.P33 (Projection)

open scoped Topology

universe u v

/-- lattice-isomorphism-spectrum; de Groote, Observables I, PDF p./pp. 55.
-/
theorem lattice_isomorphism_induces_homeomorphism {L : Type u} {K : Type v} [CompleteLattice L] [CompleteLattice K] (e : L ≃o K) :
    ∃ h : StoneSpectrum L ≃ₜ StoneSpectrum K,
      ∀ B, (h B).val = e '' B.val := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 55, lattice-isomorphism-spectrum

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $L$ and $K$ be complete lattices, and let $e:L\to K$ be an order isomorphism, meaning a bijection satisfying $a\le b$ if and only if $e(a)\le e(b)$ . For either lattice $A$ , let $\mathcal Q(A)$ consist of its inclusion-maximal nonempty subsets that exclude $\bot$ and in which any two members have a common lower bound belonging to the subset, and equip $\mathcal Q(A)$ with the topology generated by $\{B:a\in B\}$ for $a\in A$ . There exists a homeomorphism $h:\mathcal Q(L)\to\mathcal Q(K)$ such that, for every $B\in\mathcal Q(L)$ ,

h(B)=e[B]=\{e(a):a\in B\}.

No nontriviality assumption is imposed on either complete lattice, so empty quasipoint spaces are included.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph