Split files

OrderedSemigroups/Archimedean.lean

@@ -0,0 +1,32 @@
+import OrderedSemigroups.Sign
+
+/-!
+# Archimedean Ordered Semigroups and Anomalous Pairs
+
+This file defines Archimedean ordered semigroups and anomalous pairs
+and proves theorems about how they interact.
+
+-/
+
+universe u
+
+variable {α : Type u} [OrderedSemigroup α]
+
+def is_archimedean_wrt (a b : α) :=
+  is_one a ∨ is_one b ∨
+  ∃n : ℕ+, (is_positive b ∧ b < a^n) ∨ (is_negative b ∧ a^n < b)
+
+theorem arhimedean_same_sign {a b : α} (h : is_archimedean_wrt a b) : same_sign a b := by
+  sorry
+
+def anomalous_pair (a b : α) := ∀n : ℕ+, (a^n < b^n ∧ b^n < a^(n+1)) ∨ (a^n > b^n ∧ b^n > a^(n+1))
+
+def has_anomalous_pair := ∃a b : α, anomalous_pair a b
+
+class Archimedean (α : Type u) [OrderedSemigroup α] where
+  arch : ∀a b : α, is_archimedean_wrt a b
+
+section Archimedean
+variable [Archimedean α]
+
+end Archimedean

OrderedSemigroups/Defs.lean

@@ -0,0 +1,77 @@
+import Mathlib.Algebra.Order.Group.Basic
+import Mathlib.Algebra.Order.Monoid.Unbundled.Basic
+import Mathlib.Data.PNat.Basic
+
+/-!
+# Ordered Semigroups
+
+This file defines ordered semigroups and provides some basic instances.
+It also defines the action of `ℕ+` on a semigroup.
+
+-/
+
+universe u
+
+variable {α : Type u}
+
+/-- The action of ℕ+ on a type with Mul where
+  nppowRec n a = a * a ⋯ * a (aka a^n)-/
+def nppowRec [Mul α] : ℕ+ → α → α
+  | 1, a => a
+  | ⟨n+2, hnp⟩, a =>
+    have: (⟨n+1, by simp⟩ : ℕ+) < ⟨n+2, hnp⟩ := by simp
+    (nppowRec ⟨n+1, by simp⟩ a) * a
+termination_by x => x
+
+/-- A semigroup with an action of ℕ+ on it, by default it is exponentiation -/
+class Semigroup' (α : Type u) extends Semigroup α where
+  nppow : ℕ+ → α → α := nppowRec
+  nppow_one : ∀ x, nppow 1 x = x := by intros; rfl
+  nppow_succ : ∀ (n : ℕ+) (x), nppow (n+1) x = nppow n x * x
+
+/-- Define the exponentiation notation for the action of ℕ+ on a semigroup' -/
+instance [Semigroup' α]: Pow α ℕ+ :=
+  ⟨fun x n ↦ Semigroup'.nppow n x⟩
+
+class OrderedSemigroup (α : Type u) extends Semigroup' α, PartialOrder α where
+  mul_le_mul_left : ∀ a b : α, a ≤ b → ∀ c : α, c * a ≤ c * b
+  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 [OrderedSemigroup α] : CovariantClass α α (Function.swap (· * ·)) (· ≤ ·) where
+  elim a b c bc := OrderedSemigroup.mul_le_mul_right b c bc a
+
+class OrderedCancelSemigroup (α : Type u) extends OrderedSemigroup α where
+  le_of_mul_le_mul_left : ∀ a b c : α, a * b ≤ a * c → b ≤ c
+  le_of_mul_le_mul_right : ∀ a b c : α, b * a ≤ c * a → b ≤ c
+
+instance [OrderedCancelSemigroup α] : ContravariantClass α α (· * ·) (· ≤ ·) where
+  elim a b c bc := OrderedCancelSemigroup.le_of_mul_le_mul_left a b c bc
+
+instance [OrderedCancelSemigroup α] : ContravariantClass α α (Function.swap (· * ·)) (· ≤ ·) where
+  elim a b c bc := OrderedCancelSemigroup.le_of_mul_le_mul_right a b c bc
+
+instance [OrderedCancelSemigroup α] : LeftCancelSemigroup α where
+  mul_left_cancel a b c habc := by
+    have b_le_c : b ≤ c := OrderedCancelSemigroup.le_of_mul_le_mul_left a b c (le_of_eq habc)
+    have c_le_b : c ≤ b := OrderedCancelSemigroup.le_of_mul_le_mul_left a c b (le_of_eq (id (Eq.symm habc)))
+    exact (le_antisymm b_le_c c_le_b)
+
+instance [OrderedCancelSemigroup α] : RightCancelSemigroup α where
+  mul_right_cancel a b c habc := by
+    have a_le_c : a ≤ c := OrderedCancelSemigroup.le_of_mul_le_mul_right b a c (le_of_eq habc)
+    have c_le_a : c ≤ a := OrderedCancelSemigroup.le_of_mul_le_mul_right b c a (le_of_eq (id (Eq.symm habc)))
+    exact (le_antisymm a_le_c c_le_a)
+
+class LinearOrderedSemigroup (α : Type u) extends OrderedSemigroup α, LinearOrder α
+
+class LinearOrderedCancelSemigroup (α : Type u) extends OrderedCancelSemigroup α, LinearOrder α
+
+instance [LinearOrderedCancelSemigroup α] : LinearOrderedSemigroup α where
+  le_total := LinearOrderedCancelSemigroup.le_total
+  decidableLE := LinearOrderedCancelSemigroup.decidableLE
+  min_def := LinearOrderedCancelSemigroup.min_def
+  max_def := LinearOrderedCancelSemigroup.max_def
+  compare_eq_compareOfLessAndEq := LinearOrderedCancelSemigroup.compare_eq_compareOfLessAndEq

OrderedSemigroups/Sign.lean

@@ -0,0 +1,88 @@
+import OrderedSemigroups.Basic
+
+/-!
+# Sign of element in Ordered Semigroup
+
+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 α]
+
+def is_positive (a : α) := ∀x : α, a*x > x
+def is_negative (a : α) := ∀x : α, a*x < x
+def is_one (a : α) := ∀x : α, a*x = x
+
+theorem pos_not_neg {a : α} (is_pos : is_positive a) : ¬is_negative a := by
+  intro is_neg
+  rw [is_positive, is_negative] at *
+  exact (lt_self_iff_false (a * a)).mp (lt_trans (is_neg a) (is_pos a))
+
+theorem pos_not_one {a : α} (is_pos : is_positive a) : ¬is_one a := by
+  intro is_zer
+  rw [is_positive, is_one] at *
+  have is_pos := is_pos a
+  simp [is_zer a] at is_pos
+
+theorem neg_not_pos {a : α} (is_neg : is_negative a) : ¬is_positive a := by
+  intro is_pos
+  rw [is_positive, is_negative] at *
+  exact (lt_self_iff_false a).mp (lt_trans (is_pos a) (is_neg a))
+
+theorem neg_not_one {a : α} (is_neg : is_negative a) : ¬is_one a := by
+  intro is_zer
+  rw [is_negative, is_one] at *
+  have is_neg := is_neg a
+  simp [is_zer a] at is_neg
+
+theorem one_not_pos {a : α} (is_zer : is_one a) : ¬is_positive a := by
+  intro is_pos
+  rw [is_positive, is_one] at *
+  have is_pos := is_pos a
+  rw [is_zer a] at is_pos
+  exact (lt_self_iff_false a).mp is_pos
+
+theorem one_not_neg {a : α} (is_zer : is_one a) : ¬is_negative a := by
+  intro is_neg
+  rw [is_negative, is_one] at *
+  have is_neg := is_neg a
+  rw [is_zer a] at is_neg
+  exact (lt_self_iff_false a).mp is_neg
+
+def same_sign (a b : α) :=
+  (is_positive a ∧ is_positive b) ∨
+  (is_negative a ∧ is_negative b) ∨
+  (is_one a ∧ is_one b)
+
+end OrderedSemigroup
+
+section LinearOrderedCancelSemigroup
+variable [LinearOrderedCancelSemigroup α]
+
+lemma pos_right_pos_forall {a b : α} (h : b * a > b) : is_positive a := by
+  intro x
+  have : b * a * x > b * x := mul_lt_mul_right' h x
+  simpa [mul_assoc]
+
+lemma neg_right_neg_forall {a b : α} (h : b * a < b) : is_negative a := by
+  intro x
+  have : b * a * x < b * x := mul_lt_mul_right' h x
+  simpa [mul_assoc]
+
+lemma one_right_one_forall {a b : α} (h : b * a = b) : is_one a := by
+  intro x
+  have : b * a * x = b * x := congrFun (congrArg HMul.hMul h) x
+  simpa [mul_assoc]
+
+/-- Every element of a LinearOrderedCancelSemigroup is either positive, negative, or one. -/
+theorem pos_neg_or_one : ∀a : α, is_positive a ∨ is_negative a ∨ is_one a := by
+  intro a
+  rcases le_total (a*a) a with ha | ha
+  <;> rcases LE.le.lt_or_eq ha with ha | ha
+  · right; left; exact neg_right_neg_forall ha
+  · right; right; exact one_right_one_forall ha
+  · left; exact pos_right_pos_forall ha
+  · right; right; exact one_right_one_forall ha.symm
+
+end LinearOrderedCancelSemigroup