Skip to content

Commit

Permalink
Update blueprint theorem for Theorem 4
Browse files Browse the repository at this point in the history
  • Loading branch information
@ericluap
ericluap committed Aug 22, 2024
1 parent 9ce0954 commit 86513cf
Show file tree
Hide file tree
Showing 5 changed files with 122 additions and 79 deletions.
3 changes: 2 additions & 1 deletion blueprint/lean_decls
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,4 +17,5 @@ comm_dist_le
is_archimedean_wrt
is_archimedean
anomalous_pair
non_archimedean_anomalous_pair
non_archimedean_anomalous_pair
not_anomalous_comm_and_arch
51 changes: 26 additions & 25 deletions blueprint/src/content.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -190,55 +190,56 @@ \section{Content}
The other cases follow similarly.
\end{proof}

\begin{theorem}
\begin{theorem}\label{non_anomalous_comm_and_arch}\lean{not_anomalous_comm_and_arch}\leanok
\uses{def:anomalous_pair, def:arch}
A linear ordered cancel semigroup without anomalous pairs is an Archimedean commutative semigroup.
\end{theorem}
\begin{proof}
Let $a$ and $b$ be elements of an ordered semigroup $S$.
If either $a$ or $b$ is zero, then they commute.
If either $a$ or $b$ is one, then they commute.

We begin with the case that $a$ and $b$ are positive.
If $a + b < b + a$, then for all $n\in \mathbb{N}^+$, we have that
If $a * b < b * a$, then for all $n\in \mathbb{N}^+$, we have that
\begin{align}
(n+1)(a+b) &= a + n(b+a) + b \\
&> n(b+a) + b \\
&> n(b+a) \\
&> n(a+b)
(a*b)^{n+1} &= a * (b*a)^n * b \\
&> (b*a)^n * b \\
&> (b*a)^n \\
&> (a*b)^n
\end{align}
And so $a+b$ and $b+a$ form an anomalous pair.
And so $a*b$ and $b*a$ form an anomalous pair.

The same for the case that $b + a < a + b$.
Therefore, we must have that $a+b = b+a$.
The same for the case that $b * a < a * b$.
Therefore, we must have that $a*b = b*a$.

The case where $a$ and $b$ are negative follows similarly.

We now look at the case where $a$ is negative and $b$ is positive.
If the element $0$ exists and $a+b = 0$, then $a + b + a = a$ and so $b+a = 0$.
If the element $1$ exists and $a*b = 1$, then $a * b * a = a$ and so $b*a = 1$.
Therefore, $a$ and $b$ commute.

If $a + b$ is positive, then
If $a * b$ is positive, then
\begin{align}
(a+b) + (a+b) &> a + b \\
(b + a) + b &> b \\
b + a &> 0
(a*b) * (a*b) &> a * b \\
(b * a) * b &> b \\
b * a &> 0
\end{align}

We already showed that positive elements commute and so
\[ (b+a) + b = b + (b + a)\]
\[ (b*a) * b = b * (b * a)\]

Now we look at the case where $a+b < b+a$.
Now we look at the case where $a*b < b*a$.
Then we have that
\begin{align}
2(a + b) &= a + ((b+a) + b) \\
&= a + (b + (b + a)) \\
&= (a + b) + (b + a) \\
&> (a + b) + (a + b) \\
&= 2(a + b)
(a * b)^2 &= a * ((b*a) * b) \\
&= a * (b * (b * a)) \\
&= (a * b) * (b * a) \\
&> (a * b) * (a * b) \\
&= (a * b)^2
\end{align}
Which is a contradiction.
We get a similar contradiction in the case that $b+a < a+b$.
Therefore, $a+b = b+a$.
We get a similar contradiction in the case that $b*a < a*b$.
Therefore, $a*b = b*a$.

The case where $a+b$ is negative follows similarly.
The case where $a*b$ is negative follows similarly.
The case where $b$ is negative and $a$ is positive is symmetric.
\end{proof}
Binary file modified blueprint/src/web.paux
View file
Binary file not shown.
62 changes: 31 additions & 31 deletions blueprint/web/dep_graph_document.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,36 +61,6 @@ <h1 id="doc_title">Dependencies</h1>
<div id="statements">


<div class="dep-modal-container" id="a0000000014_modal">
<div class="dep-modal-content">
<button class="dep-closebtn">
<svg class="icon icon-cross "><use xlink:href="symbol-defs.svg#icon-cross"></use></svg>
</button>

<div class="thm" id="a0000000014" style="display: none">
<div class="thm_thmheading">
<span class="theorem_thmcaption">
Theorem
</span>
<span class="theorem_thmlabel">4</span></div>
<div class="thm_thmcontent"><p>A linear ordered cancel semigroup without anomalous pairs is an Archimedean commutative semigroup. </p>
</div>

<a class="latex_link" href="index.html#a0000000014">LaTeX</a>







</div>

</div>
</div>



<div class="dep-modal-container" id="def:anomalous_pair_modal">
<div class="dep-modal-content">
<button class="dep-closebtn">
Expand Down Expand Up @@ -439,6 +409,36 @@ <h1 id="doc_title">Dependencies</h1>



</div>

</div>
</div>



<div class="dep-modal-container" id="non_anomalous_comm_and_arch_modal">
<div class="dep-modal-content">
<button class="dep-closebtn">
<svg class="icon icon-cross "><use xlink:href="symbol-defs.svg#icon-cross"></use></svg>
</button>

<div class="thm" id="non_anomalous_comm_and_arch" style="display: none">
<div class="thm_thmheading">
<span class="theorem_thmcaption">
Theorem
</span>
<span class="theorem_thmlabel">4</span></div>
<div class="thm_thmcontent"><p> A linear ordered cancel semigroup without anomalous pairs is an Archimedean commutative semigroup. </p>
</div>

<a class="latex_link" href="index.html#non_anomalous_comm_and_arch">LaTeX</a>


<a class="lean_link lean_decl" href="https://ericluap.github.io/OrderedSemigroups/docs/find/#doc/not_anomalous_comm_and_arch">Lean</a>




</div>

</div>
Expand Down Expand Up @@ -629,7 +629,7 @@ <h1 id="doc_title">Dependencies</h1>
.width(width)
.height(height)
.fit(true)
.renderDot(`strict digraph "" { graph [bgcolor=transparent]; node [label="\N", penwidth=1.8 ]; edge [arrowhead=vee]; split_first_and_last [color=green, fillcolor="#A3D6FF", label=split_first_and_last, shape=ellipse, style=filled]; "lem:right_forall" [color=green, label=right_forall, shape=ellipse]; non_arch_anomalous [color=green, fillcolor="#A3D6FF", label=non_arch_anomalous, shape=ellipse, style=filled]; "thm:pos_neg_or_one" [color=green, fillcolor="#A3D6FF", label=pos_neg_or_one, shape=ellipse, style=filled]; "thm:comm_ineq" [color=green, fillcolor="#A3D6FF", label=comm_ineq, shape=ellipse, style=filled]; a0000000014 [color=blue, fillcolor="#A3D6FF", label=a0000000014, shape=ellipse, style=filled]; "def:OrderedSemigroup" [color=green, fillcolor="#B0ECA3", label=OrderedSemigroup, shape=box, style=filled]; "def:OrderedCancelSemigroup" [color=green, fillcolor="#B0ECA3", label=OrderedCancelSemigroup, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:OrderedCancelSemigroup" [style=dashed]; "def:LinearOrderedSemigroup" [color=green, fillcolor="#B0ECA3", label=LinearOrderedSemigroup, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:LinearOrderedSemigroup" [style=dashed]; "def:positive" [color=green, fillcolor="#B0ECA3", label=positive, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:positive" [style=dashed]; "def:negative" [color=green, fillcolor="#B0ECA3", label=negative, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:negative" [style=dashed]; "def:one" [color=green, fillcolor="#B0ECA3", label=one, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:one" [style=dashed]; "def:LinearOrderedCancelSemigroup" [color=green, fillcolor="#B0ECA3", label=LinearOrderedCancelSemigroup, shape=box, style=filled]; "def:OrderedCancelSemigroup" -> "def:LinearOrderedCancelSemigroup" [style=dashed]; "def:positive" -> "lem:right_forall" [style=dashed]; "def:positive" -> "thm:pos_neg_or_one" [style=dashed]; "def:arch_wrt" [color=green, fillcolor="#B0ECA3", label=arch_wrt, shape=box, style=filled]; "def:positive" -> "def:arch_wrt" [style=dashed]; "thm:neg_lt_pos" [color=green, fillcolor="#A3D6FF", label=neg_lt_pos, shape=ellipse, style=filled]; "def:positive" -> "thm:neg_lt_pos" [style=dashed]; "def:negative" -> "lem:right_forall" [style=dashed]; "def:negative" -> "thm:pos_neg_or_one" [style=dashed]; "def:negative" -> "def:arch_wrt" [style=dashed]; "def:negative" -> "thm:neg_lt_pos" [style=dashed]; "def:one" -> "lem:right_forall" [style=dashed]; "def:one" -> "thm:pos_neg_or_one" [style=dashed]; "def:arch" [color=green, fillcolor="#B0ECA3", label=arch, shape=box, style=filled]; "def:one" -> "def:arch" [style=dashed]; "def:LinearOrderedCancelSemigroup" -> "thm:pos_neg_or_one" [style=dashed]; "def:arch_wrt" -> "def:arch" [style=dashed]; "def:arch" -> non_arch_anomalous [style=dashed]; "def:anomalous_pair" [color=green, fillcolor="#B0ECA3", label=anomalous_pair, shape=box, style=filled]; "def:anomalous_pair" -> non_arch_anomalous [style=dashed];}`)
.renderDot(`strict digraph "" { graph [bgcolor=transparent]; node [label="\N", penwidth=1.8 ]; edge [arrowhead=vee]; split_first_and_last [color=green, fillcolor="#A3D6FF", label=split_first_and_last, shape=ellipse, style=filled]; "lem:right_forall" [color=green, label=right_forall, shape=ellipse]; non_arch_anomalous [color=green, fillcolor="#A3D6FF", label=non_arch_anomalous, shape=ellipse, style=filled]; "thm:pos_neg_or_one" [color=green, fillcolor="#A3D6FF", label=pos_neg_or_one, shape=ellipse, style=filled]; "thm:comm_ineq" [color=green, fillcolor="#A3D6FF", label=comm_ineq, shape=ellipse, style=filled]; non_anomalous_comm_and_arch [color=green, fillcolor="#A3D6FF", label=non_anomalous_comm_and_arch, shape=ellipse, style=filled]; "def:OrderedSemigroup" [color=green, fillcolor="#B0ECA3", label=OrderedSemigroup, shape=box, style=filled]; "def:OrderedCancelSemigroup" [color=green, fillcolor="#B0ECA3", label=OrderedCancelSemigroup, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:OrderedCancelSemigroup" [style=dashed]; "def:LinearOrderedSemigroup" [color=green, fillcolor="#B0ECA3", label=LinearOrderedSemigroup, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:LinearOrderedSemigroup" [style=dashed]; "def:positive" [color=green, fillcolor="#B0ECA3", label=positive, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:positive" [style=dashed]; "def:negative" [color=green, fillcolor="#B0ECA3", label=negative, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:negative" [style=dashed]; "def:one" [color=green, fillcolor="#B0ECA3", label=one, shape=box, style=filled]; "def:OrderedSemigroup" -> "def:one" [style=dashed]; "def:LinearOrderedCancelSemigroup" [color=green, fillcolor="#B0ECA3", label=LinearOrderedCancelSemigroup, shape=box, style=filled]; "def:OrderedCancelSemigroup" -> "def:LinearOrderedCancelSemigroup" [style=dashed]; "def:positive" -> "lem:right_forall" [style=dashed]; "def:positive" -> "thm:pos_neg_or_one" [style=dashed]; "def:arch_wrt" [color=green, fillcolor="#B0ECA3", label=arch_wrt, shape=box, style=filled]; "def:positive" -> "def:arch_wrt" [style=dashed]; "thm:neg_lt_pos" [color=green, fillcolor="#A3D6FF", label=neg_lt_pos, shape=ellipse, style=filled]; "def:positive" -> "thm:neg_lt_pos" [style=dashed]; "def:negative" -> "lem:right_forall" [style=dashed]; "def:negative" -> "thm:pos_neg_or_one" [style=dashed]; "def:negative" -> "def:arch_wrt" [style=dashed]; "def:negative" -> "thm:neg_lt_pos" [style=dashed]; "def:one" -> "lem:right_forall" [style=dashed]; "def:one" -> "thm:pos_neg_or_one" [style=dashed]; "def:arch" [color=green, fillcolor="#B0ECA3", label=arch, shape=box, style=filled]; "def:one" -> "def:arch" [style=dashed]; "def:LinearOrderedCancelSemigroup" -> "thm:pos_neg_or_one" [style=dashed]; "def:arch_wrt" -> "def:arch" [style=dashed]; "def:arch" -> non_arch_anomalous [style=dashed]; "def:arch" -> non_anomalous_comm_and_arch [style=dashed]; "def:anomalous_pair" [color=green, fillcolor="#B0ECA3", label=anomalous_pair, shape=box, style=filled]; "def:anomalous_pair" -> non_arch_anomalous [style=dashed]; "def:anomalous_pair" -> non_anomalous_comm_and_arch [style=dashed];}`)
.on("end", interactive);

latexLabelEscaper = function(label) {
Expand Down
85 changes: 63 additions & 22 deletions blueprint/web/index.html
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1097,7 +1097,7 @@ <h1>Lean declarations</h1>

</div>
</div>
<div class="theorem_thmwrapper theorem-style-plain" id="a0000000014">
<div class="theorem_thmwrapper theorem-style-plain" id="non_anomalous_comm_and_arch">
<div class="theorem_thmheading">
<span class="theorem_thmcaption">
Theorem
Expand All @@ -1108,51 +1108,92 @@ <h1>Lean declarations</h1>
</div>
<div class="thm_header_hidden_extras">

<a class="icon proof" href="index.html#a0000000014">#</a>
<a class="icon proof" href="index.html#non_anomalous_comm_and_arch">#</a>

<a class="icon proof" href="index.html#a0000000015"><svg class="icon icon-cogs "><use xlink:href="symbol-defs.svg#icon-cogs"></use></svg>
<a class="icon proof" href="index.html#a0000000014"><svg class="icon icon-cogs "><use xlink:href="symbol-defs.svg#icon-cogs"></use></svg>
</a>


<button class="modal"><svg class="icon icon-mindmap "><use xlink:href="symbol-defs.svg#icon-mindmap"></use></svg>
</button>
<div class="modal-container">
<div class="modal-content">
<header>
<h1>Uses</h1>
<button class="closebtn"><svg class="icon icon-cross "><use xlink:href="symbol-defs.svg#icon-cross"></use></svg>
</button>
</header>

<ul class="uses">

<li><a href="index.html#def:anomalous_pair">Definition 10</a></li>

<li><a href="index.html#def:arch">Definition 9</a></li>

</ul>

</div>
</div>



<button class="modal lean">L∃∀N</button>
<div class="modal-container">
<div class="modal-content">
<header>
<h1>Lean declarations</h1>
<button class="closebtn"><svg class="icon icon-cross "><use xlink:href="symbol-defs.svg#icon-cross"></use></svg>
</button>
</header>

<ul class="uses">

<li><a href="https://ericluap.github.io/OrderedSemigroups/docs/find/#doc/not_anomalous_comm_and_arch" class="lean_decl">not_anomalous_comm_and_arch</a></li>

</ul>

</div>
</div>


</div>
</div>
<div class="theorem_thmcontent">
<p>A linear ordered cancel semigroup without anomalous pairs is an Archimedean commutative semigroup. </p>
<p> A linear ordered cancel semigroup without anomalous pairs is an Archimedean commutative semigroup. </p>

</div>
</div>
<div class="proof_wrapper" id="a0000000015">
<div class="proof_wrapper" id="a0000000014">
<div class="proof_heading">
<span class="proof_caption">
Proof
</span>
<span class="expand-proof">▶</span>
</div>
<div class="proof_content">
<p>Let \(a\) and \(b\) be elements of an ordered semigroup \(S\). If either \(a\) or \(b\) is zero, then they commute. </p>
<p>We begin with the case that \(a\) and \(b\) are positive. If \(a + b {\lt} b + a\), then for all \(n\in \mathbb {N}^+\), we have that </p>
<div class="displaymath" id="a0000000016">
\begin{align} (n+1)(a+b) & = a + n(b+a) + b \\ & {\gt} n(b+a) + b \\ & {\gt} n(b+a) \\ & {\gt} n(a+b) \end{align}
<p>Let \(a\) and \(b\) be elements of an ordered semigroup \(S\). If either \(a\) or \(b\) is one, then they commute. </p>
<p>We begin with the case that \(a\) and \(b\) are positive. If \(a * b {\lt} b * a\), then for all \(n\in \mathbb {N}^+\), we have that </p>
<div class="displaymath" id="a0000000015">
\begin{align} (a*b)^{n+1} & = a * (b*a)^n * b \\ & {\gt} (b*a)^n * b \\ & {\gt} (b*a)^n \\ & {\gt} (a*b)^n \end{align}
</div>
<p> And so \(a+b\) and \(b+a\) form an anomalous pair. </p>
<p>The same for the case that \(b + a {\lt} a + b\). Therefore, we must have that \(a+b = b+a\). </p>
<p> And so \(a*b\) and \(b*a\) form an anomalous pair. </p>
<p>The same for the case that \(b * a {\lt} a * b\). Therefore, we must have that \(a*b = b*a\). </p>
<p>The case where \(a\) and \(b\) are negative follows similarly. </p>
<p>We now look at the case where \(a\) is negative and \(b\) is positive. If the element \(0\) exists and \(a+b = 0\), then \(a + b + a = a\) and so \(b+a = 0\). Therefore, \(a\) and \(b\) commute. </p>
<p>If \(a + b\) is positive, then </p>
<div class="displaymath" id="a0000000017">
\begin{align} (a+b) + (a+b) & {\gt} a + b \\ (b + a) + b & {\gt} b \\ b + a & {\gt} 0 \end{align}
<p>We now look at the case where \(a\) is negative and \(b\) is positive. If the element \(1\) exists and \(a*b = 1\), then \(a * b * a = a\) and so \(b*a = 1\). Therefore, \(a\) and \(b\) commute. </p>
<p>If \(a * b\) is positive, then </p>
<div class="displaymath" id="a0000000016">
\begin{align} (a*b) * (a*b) & {\gt} a * b \\ (b * a) * b & {\gt} b \\ b * a & {\gt} 0 \end{align}
</div>
<p>We already showed that positive elements commute and so </p>
<div class="displaymath" id="a0000000018">
\[ (b+a) + b = b + (b + a) \]
<div class="displaymath" id="a0000000017">
\[ (b*a) * b = b * (b * a) \]
</div>
<p>Now we look at the case where \(a+b {\lt} b+a\). Then we have that </p>
<div class="displaymath" id="a0000000019">
\begin{align} 2(a + b) & = a + ((b+a) + b) \\ & = a + (b + (b + a)) \\ & = (a + b) + (b + a) \\ & {\gt} (a + b) + (a + b) \\ & = 2(a + b) \end{align}
<p>Now we look at the case where \(a*b {\lt} b*a\). Then we have that </p>
<div class="displaymath" id="a0000000018">
\begin{align} (a * b)^2 & = a * ((b*a) * b) \\ & = a * (b * (b * a)) \\ & = (a * b) * (b * a) \\ & {\gt} (a * b) * (a * b) \\ & = (a * b)^2 \end{align}
</div>
<p> Which is a contradiction. We get a similar contradiction in the case that \(b+a {\lt} a+b\). Therefore, \(a+b = b+a\). </p>
<p>The case where \(a+b\) is negative follows similarly. The case where \(b\) is negative and \(a\) is positive is symmetric. </p>
<p> Which is a contradiction. We get a similar contradiction in the case that \(b*a {\lt} a*b\). Therefore, \(a*b = b*a\). </p>
<p>The case where \(a*b\) is negative follows similarly. The case where \(b\) is negative and \(a\) is positive is symmetric. </p>

</div>
</div>
Expand Down

0 comments on commit 86513cf

Please sign in to comment.