Outline argument and steps

OrderedSemigroups/Archimedean.lean

@@ -14,7 +14,7 @@ universe u
 variable {α : Type u}
 
 section OrderedSemigroup
-variable [OrderedSemigroup α]
+variable [LeftOrderedSemigroup α]
 
 /-- `a` is Archimedean with respect to `b` if there exists an `N : ℕ+` such that
 for all `n ≥ N`, either `b` is positive and `b < a^n` or `b` is negative and `a^n < b`. -/

OrderedSemigroups/Basic.lean

@@ -83,7 +83,7 @@ theorem le_pow {a b : α} (h : a ≤ b) (n : ℕ+) : a^n ≤ b^n := by
 
 theorem middle_swap {a b c d : α} (h : a ≤ b) : c * a * d ≤ c * b * d := by
   have : a * d ≤ b * d := OrderedSemigroup.mul_le_mul_right a b h d
-  have : c * (a * d) ≤ c * (b * d) := OrderedSemigroup.mul_le_mul_left (a*d) (b*d) this c
+  have : c * (a * d) ≤ c * (b * d) := LeftOrderedSemigroup.mul_le_mul_left (a*d) (b*d) this c
   simp [mul_assoc]
   trivial
 

OrderedSemigroups/Defs.lean

@@ -58,18 +58,23 @@ class Semigroup' (α : Type u) extends Semigroup α where
   nppow_succ : ∀ (n : ℕ+) (x), nppow (n+1) x = nppow n x * x := by intros x; exact nppowRec_succ x
 
 /-- Define the exponentiation notation for the action of ℕ+ on a semigroup' -/
-instance [Semigroup' α]: Pow α ℕ+ :=
+instance [Semigroup' α] : Pow α ℕ+ :=
   ⟨fun x n ↦ Semigroup'.nppow n x⟩
 
-class OrderedSemigroup (α : Type u) extends Semigroup' α, PartialOrder α where
+class LeftOrderedSemigroup (α : Type u) extends Semigroup' α, PartialOrder α where
   mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b
+
+instance [LeftOrderedSemigroup α] : CovariantClass α α (· * ·) (· ≤ ·) where
+  elim a b c bc := LeftOrderedSemigroup.mul_le_mul_left b c bc a
+
+class RightOrderedSemigroup (α : Type u) extends Semigroup' α, PartialOrder α where
   mul_le_mul_right : ∀ a b : α, a ≤ b → ∀ c : α, a * c ≤ b * c
 
-instance [OrderedSemigroup α] : CovariantClass α α (· * ·) (· ≤ ·) where
-  elim a b c bc := OrderedSemigroup.mul_le_mul_left b c bc a
+instance [RightOrderedSemigroup α] : CovariantClass α α (Function.swap (· * ·)) (· ≤ ·) where
+  elim a b c bc := RightOrderedSemigroup.mul_le_mul_right b c bc a
 
-instance [OrderedSemigroup α] : CovariantClass α α (Function.swap (· * ·)) (· ≤ ·) where
-  elim a b c bc := OrderedSemigroup.mul_le_mul_right b c bc a
+class OrderedSemigroup (α : Type u) extends
+  LeftOrderedSemigroup α, RightOrderedSemigroup α, PartialOrder α where
 
 class OrderedCancelSemigroup (α : Type u) extends OrderedSemigroup α where
   le_of_mul_le_mul_left : ∀ a b c : α, a * b ≤ a * c → b ≤ c

OrderedSemigroups/OrderedGroup/Basic.lean

@@ -0,0 +1,56 @@
+import OrderedSemigroups.Defs
+import OrderedSemigroups.OrderedGroup.Defs
+import Mathlib.Data.Set.Basic
+import OrderedSemigroups.SemigroupToMonoid
+import Mathlib.Algebra.Group.Subsemigroup.Basic
+
+
+universe u
+
+variable {α : Type u}
+
+section Cones
+
+variable [Group α] [PartialOrder α]
+
+instance PositiveCone (α : Type u) [Group α] [PartialOrder α] : Subsemigroup α where
+  carrier := {x : α | 1 < x}
+  mul_mem' := sorry
+
+instance NegativeCone (α : Type u) [Group α] [PartialOrder α] : Subsemigroup α where
+  carrier := {x : α | x < 1}
+  mul_mem' := sorry
+
+theorem pos_neg_disjoint : Disjoint (SetLike.coe (PositiveCone α)) (SetLike.coe (NegativeCone α)) := sorry
+
+end Cones
+
+section LeftOrdered
+
+variable [LeftOrderedGroup α]
+
+def archimedean_group (α : Type u) [LeftOrderedGroup α] :=
+    ∀(g h : α), g ≠ 1 → ∃z : ℤ, g^z > h
+
+instance : LeftOrderedSemigroup α where
+  mul_le_mul_left _ _ a b :=  mul_le_mul_left' a b
+
+/--
+  The definition of archimedean for groups and the one for semigroups are equivalent.
+-/
+theorem arch_group_semigroup : archimedean_group α ↔ is_archimedean (α := α) := by sorry
+
+def normal_semigroup {α : Type u} [Group α] (x : Subsemigroup α) :=
+    ∀s : x, ∀g : α, g * s * g⁻¹ ∈ x
+
+/--
+  A left ordered group whose positive cone is a normal semigroup is an ordered group.
+-/
+def pos_normal_ordered (pos_normal : normal_semigroup (PositiveCone α)) : OrderedGroup α := by sorry
+
+/--
+  A left ordered group that is Archimedean is an ordered group.
+-/
+def left_arch_ordered (arch : is_archimedean (α := α)) : OrderedGroup α := by sorry
+
+end LeftOrdered

OrderedSemigroups/OrderedGroup/Defs.lean

@@ -0,0 +1,27 @@
+import Mathlib.Algebra.Order.Group.Basic
+
+universe u
+
+variable {α : Type u}
+
+class LeftOrderedGroup (α : Type u) extends Group α, PartialOrder α where
+  mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b
+
+variable [LeftOrderedGroup α]
+
+instance leftOrderedCovariant [LeftOrderedGroup α] : CovariantClass α α (· * ·) (· ≤ ·) where
+  elim a b c bc := LeftOrderedGroup.mul_le_mul_left b c bc a
+
+instance leftOrderedContravariant [LeftOrderedGroup α] : ContravariantClass α α (· * ·) (· ≤ ·) where
+  elim a b c bc := by simpa using mul_le_mul_left' bc a⁻¹
+
+class RightOrderedGroup (α : Type u) extends Group α, PartialOrder α where
+  mul_le_mul_right : ∀ a b : α, a ≤ b → ∀ c : α, a * c ≤ b * c
+
+instance rightOrderedCovariant [RightOrderedGroup α] : CovariantClass α α (Function.swap (· * ·)) (· ≤ ·) where
+  elim a b c bc := RightOrderedGroup.mul_le_mul_right b c bc a
+
+instance rightOrderedContravariant [RightOrderedGroup α] : ContravariantClass α α (Function.swap (· * ·)) (· ≤ ·) where
+  elim a b c bc := by simpa using mul_le_mul_right' bc a⁻¹
+
+class OrderedGroup (α : Type u) extends LeftOrderedGroup α, RightOrderedGroup α

OrderedSemigroups/SemigroupToMonoid.lean

@@ -112,7 +112,7 @@ end CommSemigroup'
 section LinearOrderedCancelSemigroup
 variable [LinearOrderedCancelCommSemigroup α] [not_one : Fact (∀x : α, ¬is_one x)]
 
-set_option maxHeartbeats 300000
+set_option maxHeartbeats 500000
 instance to_monoid [not_one : Fact (∀x : α, ¬is_one x)] : LinearOrderedCancelCommMonoid (with_one α) where
   le := by
     intro x y

OrderedSemigroups/Sign.lean

@@ -7,8 +7,8 @@ This file defines what it means for an element of an ordered semigroup
 to be positive, negative, or one. It also proves some basic facts about signs.
 -/
 
-section OrderedSemigroup
-variable [OrderedSemigroup α]
+section LeftOrderedSemigroup
+variable [LeftOrderedSemigroup α]
 
 def is_positive (a : α) := ∀x : α, a*x > x
 def is_negative (a : α) := ∀x : α, a*x < x
@@ -50,11 +50,13 @@ theorem one_not_neg {a : α} (is_zer : is_one a) : ¬is_negative a := by
   rw [is_zer a] at is_neg
   exact (lt_self_iff_false a).mp is_neg
 
+/-
 theorem pos_le_pos {a b : α} (pos : is_positive a) (h : a ≤ b) : is_positive b :=
   fun x ↦ lt_mul_of_lt_mul_right (pos x) h
 
 theorem le_neg_neg {a b : α} (neg : is_negative a) (h : b ≤ a) : is_negative b :=
   fun x ↦ mul_lt_of_mul_lt_right (neg x) h
+-/
 
 theorem pos_pow_pos {a : α} (pos : is_positive a) (n : ℕ+) : is_positive (a^n) := by
   intro x
@@ -148,6 +150,17 @@ theorem neg_ppow_le_ppow {a : α} (n m : ℕ+) (neg : is_negative a)
     exact ((neg_pow_neg neg k) (a ^ n)).le
   · simp [h]
 
+end LeftOrderedSemigroup
+
+section OrderedSemigroup
+variable [OrderedSemigroup α]
+
+theorem pos_le_pos {a b : α} (pos : is_positive a) (h : a ≤ b) : is_positive b :=
+  fun x ↦ lt_mul_of_lt_mul_right (pos x) h
+
+theorem le_neg_neg {a b : α} (neg : is_negative a) (h : b ≤ a) : is_negative b :=
+  fun x ↦ mul_lt_of_mul_lt_right (neg x) h
+
 end OrderedSemigroup
 
 section LinearOrderedCancelSemigroup

blueprint/src/content.tex

@@ -288,4 +288,103 @@ \section{Content}
 and so $a$ and $b$ do not form an anomalous pair.
 
 Similalry if $a$ and $b$ are negative.
+\end{proof}
+
+\section{Holder's Theorem}
+We follow the proof from ``Groups, Orders, and Dynamics'' by Deroin, Navas, and Rivas.
+
+\begin{lemma}
+Let $G$ be a left ordered group. 
+If its positive cone is a normal subsemigroup, then $G$ is a bi-ordered group.
+\end{lemma}
+\begin{proof}
+Let $x,y,z \in G$ such that $x \le y$. Since $G$ is a left ordered group, we then know that $zx \le zy$.
+Our goal is to show that $xz \le yz$.
+
+Since $x \le y$, we either have that $x = y$ or $x < y$.
+In the first case, it is true that $xz = yz$ and so $xz \le yz$ and we are done.
+
+In the second case, since $x < y$, we have that $1 < x^{-1}y$.
+So $x^{-1}y$ is in the positive cone. Since the positive cone is normal, we have that
+$1 < z^{-1}x^{-1}yz$. Therefore, $xz < yz$ and we are done.
+\end{proof}
+
+\begin{lemma}
+Let $G$ be a left ordered group.
+If $G$ is Archimedean, then it is bi-ordered.
+\end{lemma}
+\begin{proof}
+By the previous lemma, it suffices to show that its positive cone is a normal semigroup.
+Let $g$ be an element of the positive cone and let $h$ be an element of $G$.
+Our goal is to show that $hgh^{-1}$ is in the positive cone.
+
+Assume for the sake of contradiction that $hgh^{-1}$ is not in the positive cone.
+We then split into two cases based on whether or not $h$ is in the positive or negative cone.
+Notice that since $h \ne 1$, it must be in one of the cones.
+
+Let's first look at the case where $h$ is in the negative cone.
+Since $G$ is Archimedean, there exists a smallest nonnegative integer $n$
+such that $h^{-1} < g^n$ (we can guarantee its nonnegative as both $g$ and $h^{-1}$ are positive).
+Since $h < 1$, $1 < h^{-1}$ and so $n > 0$.
+
+Notice that since $g$ and $h$ are not the identity,
+and $hgh^{-1}$ is not in the positive cone, it must be in the negative cone.
+So $hgh^{-1} < 1$ and thus, we have that $h^{-1} < g^{-1}h^{-1}$. And since
+$h^{-1} < g^n$, we have that $g^{-1}h^{-1} < g^{n-1}$. Therefore,
+we have that $h^{-1} < g^{-1}h^{-1} < g^{n-1}$. So then $h^{-1} < g^{n-1}$.
+Since $n > 0$, $n-1$ is a smaller nonnegative integer such that $h^{-1} < g^{n-1}$. 
+This contradicts the minimality of $n$.
+
+The remaining case is where $h$ is in the positive cone.
+As before, $hgh^{-1}$ must be in the negative cone so
+$hgh^{-1} < 1$. Therefore, $1 < hg^{-1}h^{-1}$.
+
+We have that $h^{-1}$ is in the negative cone
+and so from the first half of this proof, we know that
+$h^{-1}(hg^{-1}h^{-1})h$ is in the positive cone.
+Simplifying, we get that $g^{-1}$ is in the positive cone.
+So then we have that $1 < g^{-1}$ and $1 < g$ which is a contradiction.
+
+So we have shown that the positive cone is a normal subsemigroup
+and thus that the group $G$ is bi-ordered.
+\end{proof}
+
+\begin{theorem}
+A left-ordered group that is Archimedean is isomorphic to a
+subgroup of $\mathbb{R}$.
+\end{theorem}
+\begin{proof}
+The first step is to define the following map:\\ \\
+Let $G$ be a bi-ordered Archimedean group.
+Fix a positive element $f \in G$. Then for each $g \in G$
+we can define a function $q_g\colon \mathbb{N} \to \mathbb{N}$ where
+for each $n \in \mathbb{N}$, $q_g(n)$ is the unique integer satisfying
+\[
+f^{q_g(n)} \le g^n < f^{q_g(n) + 1}
+\]
+
+The second step:\\ \\ 
+We prove that for each $g \in G$,
+the sequence $\frac{q_g(n)}{n}$ converges to a real number as $n$
+goes to infinity.
+Let $n_1$ and $n_2$ be natural numbers. Then
+$f^{q_g(n_1)} \le g^{n_1} < f^{q_g(n_1) + 1}$ and
+$f^{q_g(n_2)} \le g^{n_2} < f^{q_g(n_2) + 1}$.
+Therefore,
+\[
+f^{q_g(n_1)+q_g(n_2)} \le g^{n_1+n_2} < f^{q_g(n_1) + q_g(n_2) + 2}
+\]
+And so it must be that 
+\[
+q_g(n_1) + q_g(n_2) \le q_g(n_1 + n_2) \le q_g(n_1) + q_g(n_2) + 1
+\]
+Then the sequence converges by the exercise already proven as we have that
+$|q_g(n_1+n_2) - q_g(n_1) - q_g(n_2)| \le 1$.
+
+The third step:\\ \\
+We define a map that takes each element $g \in G$ to the real number which is the limit
+of the sequence $\frac{q_g(n)}{n}$. We then check that this map is a group homomorphism.
+
+The fourth step:\\ \\
+We check that the map is injective and order-preserving.
 \end{proof}