User:Leigh.Samphier/Topology/Equivalence of Definitions of Frame Isomorphism

From ProofWiki
Jump to navigation Jump to search


This page needs proofreading.
Please check it for mathematical errors.
If you believe there are none, please remove {{Proofread}} from the code.
To discuss this page in more detail, feel free to use the talk page.
When this work has been completed, you may remove this instance of {{Proofread}} from the code.


Theorem

Let $\struct {L_1, \vee_1, \wedge_1, \preceq_1}$ and $\struct {L_2, \vee_2, \wedge_2, \preceq_2}$ be frames.


The following definitions of the concept of Frame Isomorphism are equivalent:

Definition 1

Let $\phi: L_1 \to L_2$ be a (frame) homomorphism.


We say $\phi: L_1 \to L_2$ is a frame isomorphism if and only if $\phi : S_1 \to S_2$ is a bijection.


Definition 2

Let $\phi: S_1 \to S_2$ be a mapping.


We say $\phi: L_1 \to L_2$ is a frame isomorphism if and only if $\phi : L_1 \to L_2$ is an order isomorphism


Proof

Definition 1 implies Definition 2

Let $\phi : L_1 \to L_2$ be a bijective frame homomorphism.


From User:Leigh.Samphier/Topology/Inverse of Bijective Frame Homomorphism is Bijective Frame Homomorphism:

$\phi^{-1}: L_2 \to L_1$ is a bijective frame homomorphism.


From User:Leigh.Samphier/Topology/Frame Homomorphism is Lattice Homomorphism:

$\phi : L_1 \to L_2$ and $\phi^{-1} : L_2 \to L_1$ are lattice homomorphisms


From Lattice Homomorphism is Order-Preserving:

$\phi : L_1 \to L_2$ and $\phi^{-1} : L_2 \to L_1$ are order-preserving


Hence $\phi : L_1 \to L_2$ is an order isomorphism by definition.

$\Box$

Definition 2 implies Definition 1

Let $\phi : \struct{A_1, \preceq_1} \to \struct{A_2, \preceq_2}$ be an order isomorphism.


By definition of order isomorphism:

$\phi : L_1 \to L_2$ is an order-preserving bijection


Let $\phi^{-1} : A_2 \to A_1$ be the inverse of $\phi : A_1 \to A_2$.

From Inverse of Order Isomorphism is Order Isomorphism:

$\phi^{-1} : L_2 \to L_1$ is an order isomorphism


$\phi$ is Arbitrary Join Preserving

Let:

$A \subseteq A_1$


We have:

\(\ds \forall a \in A: \, \) \(\ds a\) \(\le\) \(\ds \sup A\) Definition of Supremum
\(\ds \leadsto \ \ \) \(\ds \forall a \in A: \, \) \(\ds \map \phi a\) \(\le\) \(\ds \map \phi {\sup A}\) Definition of Order-Preserving Mapping
\(\ds \leadsto \ \ \) \(\ds \sup \set{\map \phi a : a \in A}\) \(\le\) \(\ds \map \phi {\sup A}\) Definition of Supremum
\(\ds \leadsto \ \ \) \(\ds \map {\phi^{-1} } {\sup \set{\map \phi a : a \in A} }\) \(\le\) \(\ds \map {\phi^{-1} } {\map \phi {\sup A} }\) Definition of Order-Preserving Mapping
\(\text {(1)}: \quad\) \(\ds \leadsto \ \ \) \(\ds \map {\phi^{-1} } {\sup \set{\map \phi a : a \in A} }\) \(\le\) \(\ds {\sup A}\) Definition of Inverse Mapping


Also we have:

\(\ds \forall a \in A: \, \) \(\ds \map \phi a\) \(\le\) \(\ds \sup \set{\map \phi a : a \in A}\) Definition of Supremum
\(\ds \leadsto \ \ \) \(\ds \forall a \in A: \, \) \(\ds \map {\phi^{-1} } {\map \phi a}\) \(\le\) \(\ds \map {\phi^{-1} } {\sup \set{\map \phi a : a \in A} }\) Definition of Order-Preserving Mapping
\(\ds \leadsto \ \ \) \(\ds \forall a \in A: \, \) \(\ds a\) \(\le\) \(\ds \map {\phi^{-1} } {\sup \set{\map \phi a : a \in A} }\) Definition of Inverse Mapping
\(\text {(2)}: \quad\) \(\ds \leadsto \ \ \) \(\ds \sup A\) \(\le\) \(\ds \map {\phi^{-1} } {\sup \set{\map \phi a : a \in A} }\) Definition of Supremum


Hence:

\(\ds \sup A\) \(=\) \(\ds \map {\phi^{-1} } {\sup \set{\map \phi a : a \in A} }\) Ordering Axiom $(3)$: Antisymmetry applied to $(1)$ and $(2)$
\(\ds \leadsto \ \ \) \(\ds \map \phi {\sup A}\) \(=\) \(\ds \map \phi {\map {\phi^{-1} } {\sup \set{\map \phi a : a \in A} } }\)
\(\ds \) \(=\) \(\ds \sup \set{\map \phi a : a \in A}\) Definition of Inverse Mapping


It follows that $\phi$ is arbitrary join preserving.

$\Box$


$\phi$ is Finite Meet Preserving

$\Box$


It follows that $\phi$ is a bijective lattice homomorphism by definition.

$\blacksquare$

Retrieved from "https://proofwiki.org/w/index.php?title=User:Leigh.Samphier/Topology/Equivalence_of_Definitions_of_Frame_Isomorphism&oldid=734173"