diff --git a/OrderedSemigroups/Archimedean.lean b/OrderedSemigroups/Archimedean.lean index d63edf1..95e0392 100644 --- a/OrderedSemigroups/Archimedean.lean +++ b/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`. -/ diff --git a/OrderedSemigroups/Basic.lean b/OrderedSemigroups/Basic.lean index 3dec0ae..2eedc0e 100644 --- a/OrderedSemigroups/Basic.lean +++ 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 diff --git a/OrderedSemigroups/Defs.lean b/OrderedSemigroups/Defs.lean index b97b07e..dff45eb 100644 --- a/OrderedSemigroups/Defs.lean +++ b/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 diff --git a/OrderedSemigroups/OrderedGroup/Basic.lean b/OrderedSemigroups/OrderedGroup/Basic.lean new file mode 100644 index 0000000..951cce8 --- /dev/null +++ b/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 diff --git a/OrderedSemigroups/OrderedGroup/Defs.lean b/OrderedSemigroups/OrderedGroup/Defs.lean new file mode 100644 index 0000000..d654424 --- /dev/null +++ b/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 α diff --git a/OrderedSemigroups/SemigroupToMonoid.lean b/OrderedSemigroups/SemigroupToMonoid.lean index 26a0f67..8432d53 100644 --- a/OrderedSemigroups/SemigroupToMonoid.lean +++ b/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 diff --git a/OrderedSemigroups/Sign.lean b/OrderedSemigroups/Sign.lean index 96c29a5..e3a847d 100644 --- a/OrderedSemigroups/Sign.lean +++ b/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 diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index 4f55553..005e922 100644 --- a/blueprint/src/content.tex +++ b/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} \ No newline at end of file