From 5d482554ac1608219fd7dd74861a3ae0e5820587 Mon Sep 17 00:00:00 2001 From: Eric P Date: Thu, 22 Aug 2024 11:54:12 -0700 Subject: [PATCH] Show most of not anomalous pair means commutative --- OrderedSemigroups/Archimedean.lean | 94 +++++++++++++++++++++++++++++- OrderedSemigroups/Basic.lean | 33 +++++++++-- OrderedSemigroups/Sign.lean | 3 + 3 files changed, 125 insertions(+), 5 deletions(-) diff --git a/OrderedSemigroups/Archimedean.lean b/OrderedSemigroups/Archimedean.lean index 10077d7..2d79182 100644 --- a/OrderedSemigroups/Archimedean.lean +++ b/OrderedSemigroups/Archimedean.lean @@ -27,6 +27,10 @@ def is_archimedean := ∀a b : α, is_one a ∨ is_one b ∨ (same_sign a b → class Archimedean (α : Type u) [OrderedSemigroup α] where arch : is_archimedean (α := α) +theorem not_has_anomalous_not_pair (not_anomalous : ¬has_anomalous_pair (α := α)) (a b : α) : ¬anomalous_pair a b := by + simp at * + tauto + end OrderedSemigroup section LinearOrderedCancelSemigroup @@ -143,6 +147,94 @@ theorem non_archimedean_anomalous_pair (non_arch : ¬is_archimedean (α := α)) · exact neg_not_archimedean_anomalous_pair neg_a neg_b hab h · exact neg_not_archimedean_anomalous_pair' neg_a neg_b hab h -theorem not_anomalous_pair_commutative (not_anomalous : ¬has_anomalous_pair (α := α)) (a b : α) : a * b = b * a := by sorry +theorem pos_not_comm_anomalous_pair {a b : α} (pos_a : is_positive a) (pos_b : is_positive b) + (h : a * b < b * a) : anomalous_pair (a*b) (b*a) := by + intro n + have : ∀n : ℕ+, (b*a)^n < (a*b)^(n+1) := by + intro n + calc + (b * a) ^ n < (b * a) ^ n * b := pos_right pos_b ((b * a) ^ n) + _ < a * (b * a) ^ n * b := mul_lt_mul_right' (pos_a ((b * a) ^ n)) b + _ = (a * b) ^ (n + 1) := Eq.symm split_first_and_last_factor_of_product + left + exact ⟨comm_swap_lt h n, this n⟩ + +theorem neg_not_comm_anomalous_pair {a b : α} (neg_a : is_negative a) (neg_b : is_negative b) + (h : a * b < b * a) : anomalous_pair (b*a) (a*b) := by + intro n + have : ∀n : ℕ+, (a*b)^n >(b*a)^(n+1) := by + intro n + calc + (a * b) ^ n > (a * b) ^ n * a := neg_right neg_a ((a * b) ^ n) + _ > b * (a * b) ^ n * a := mul_lt_mul_right' (neg_b ((a * b) ^ n)) a + _ = (b * a) ^ (n + 1) := Eq.symm split_first_and_last_factor_of_product + right + exact ⟨comm_swap_lt h n, this n⟩ + +theorem pos_not_anomalous_comm {a b : α} (pos_a : is_positive a) (pos_b : is_positive b) + (not_anomalous : ¬has_anomalous_pair (α := α)): a * b = b * a := by + rcases lt_trichotomy (a*b) (b*a) with h | h | h + · have : has_anomalous_pair (α := α) := by + use (a*b), (b*a) + exact pos_not_comm_anomalous_pair pos_a pos_b h + contradiction + · trivial + · have : has_anomalous_pair (α := α) := by + use (b*a), (a*b) + exact pos_not_comm_anomalous_pair pos_b pos_a h + contradiction + +theorem neg_not_anomalous_comm {a b : α} (neg_a : is_negative a) (neg_b : is_negative b) + (not_anomalous : ¬has_anomalous_pair (α := α)): a * b = b * a := by + rcases lt_trichotomy (a*b) (b*a) with h | h | h + · have : has_anomalous_pair (α := α) := by + use (b*a), (a*b) + exact neg_not_comm_anomalous_pair neg_a neg_b h + contradiction + · trivial + · have : has_anomalous_pair (α := α) := by + use (a*b), (b*a) + exact neg_not_comm_anomalous_pair neg_b neg_a h + contradiction + +theorem not_anomalous_pair_commutative (not_anomalous : ¬has_anomalous_pair (α := α)) (a b : α) : a * b = b * a := by + rcases pos_neg_or_one a with pos_a | neg_a | one_a + <;> rcases pos_neg_or_one b with pos_b | neg_b | one_b + all_goals try simp [one_b a, one_right one_b a] + all_goals try simp [one_a b, one_right one_a b] + · exact pos_not_anomalous_comm pos_a pos_b not_anomalous + · rcases pos_neg_or_one (a*b) with pos_ab | neg_ab | one_ab + · sorry + · sorry + · have : is_one (b * a) := by + apply one_right_one_forall (b := a) + rw [Eq.symm (mul_assoc a b a)] + exact one_ab a + exact one_unique one_ab this + · rcases pos_neg_or_one (b*a) with pos_ba | neg_ba | one_ba + have := pos_not_anomalous_comm pos_ba pos_b not_anomalous + · rcases lt_trichotomy (a*b) (b*a) with h | h | h + · have : a * b * a * b > a * b * a * b := calc + a * b * a * b = a * ((b * a) * b) := by simp [mul_assoc] + _ = a * (b * (b * a)) := by simp [←this] + _ = (a * b) * (b * a) := by simp [mul_assoc] + _ > (a * b) * (a * b) := by exact mul_lt_mul_left' h (a * b) + _ = a * b * a * b := by exact Eq.symm (mul_assoc (a * b) a b) + exact False.elim ((lt_self_iff_false (a * b * a * b)).mp this) + · trivial + · have : a * b * a * b > a * b * a * b := calc + a * b * a * b = a * ((b * a) * b) := by simp [mul_assoc] + _ = a * (b * (b * a)) := by simp [←this] + _ = (a * b) * (b * a) := by simp [mul_assoc] + _ < (a * b) * (a * b) := by exact mul_lt_mul_left' h (a * b) + _ = a * b * a * b := by exact Eq.symm (mul_assoc (a * b) a b) + exact False.elim ((lt_self_iff_false (a * b * a * b)).mp this) + · sorry + · have : is_one (a * b) := by + apply one_right_one_forall (b := b) + rw [Eq.symm (mul_assoc b a b)] + exact one_ba b + exact one_unique this one_ba + · exact neg_not_anomalous_comm neg_a neg_b not_anomalous end LinearOrderedCancelSemigroup diff --git a/OrderedSemigroups/Basic.lean b/OrderedSemigroups/Basic.lean index 1f3c5ba..70814a0 100644 --- a/OrderedSemigroups/Basic.lean +++ b/OrderedSemigroups/Basic.lean @@ -55,8 +55,7 @@ variable [OrderedSemigroup α] theorem le_pow {a b : α} (h : a ≤ b) (n : ℕ+) : a^n ≤ b^n := by induction n using PNat.recOn with | p1 => - simp - assumption + simpa | hp n ih => simp [ppow_succ] exact mul_le_mul' ih h @@ -77,9 +76,9 @@ theorem comm_factor_le {a b : α} (h : a*b ≤ b*a) (n : ℕ+) : a^n * b^n ≤ ( _ ≤ a * (b * a)^n * b := middle_swap (le_pow h n) _ = (a * b)^(n+1) := by rw [←split_first_and_last_factor_of_product] -theorem comm_swap_le [OrderedSemigroup α] {a b : α} (h : a*b ≤ b*a) (n : ℕ+) : (a*b)^n ≤ (b*a)^n := le_pow h n +theorem comm_swap_le {a b : α} (h : a*b ≤ b*a) (n : ℕ+) : (a*b)^n ≤ (b*a)^n := le_pow h n -theorem comm_dist_le [OrderedSemigroup α] {a b : α} (h : a*b ≤ b*a) (n : ℕ+) : (b*a)^n ≤ b^n * a^n := by +theorem comm_dist_le {a b : α} (h : a*b ≤ b*a) (n : ℕ+) : (b*a)^n ≤ b^n * a^n := by induction n using PNat.recOn with | p1 => simp | hp n ih => @@ -91,3 +90,29 @@ theorem comm_dist_le [OrderedSemigroup α] {a b : α} (h : a*b ≤ b*a) (n : ℕ _ = b^(n+1) * a^(n+1) := by simp [ppow_succ, ←ppow_succ'] end OrderedSemigroup + +section OrderedCancelSemigroup +variable [OrderedCancelSemigroup α] + +theorem lt_pow {a b : α} (h : a < b) (n : ℕ+) : a^n < b^n := by + induction n using PNat.recOn with + | p1 => simpa + | hp n ih => + simp [ppow_succ] + exact Left.mul_lt_mul ih h + +theorem comm_swap_lt {a b : α} (h : a*b < b*a) (n : ℕ+) : (a*b)^n < (b*a)^n := lt_pow h n + +/- +theorem comm_dist_lt {a b : α} (h : a*b < b*a) (n : ℕ+) : n > 1 → (b*a)^n < b^n * a^n := by + induction n using PNat.recOn with + | p1 => intro; contradiction + | hp n ih => + calc + (b*a)^(n+1) = b * (a*b)^n * a := by rw [split_first_and_last_factor_of_product] + _ ≤ b * (b*a)^n * a := middle_swap (le_pow h n) + _ ≤ b * (b^n * a^n) * a := middle_swap ih + _ = (b * b^n) * (a^n * a) := by simp [mul_assoc] + _ = b^(n+1) * a^(n+1) := by simp [ppow_succ, ←ppow_succ']-/ + +end OrderedCancelSemigroup diff --git a/OrderedSemigroups/Sign.lean b/OrderedSemigroups/Sign.lean index 6f4478f..52d508b 100644 --- a/OrderedSemigroups/Sign.lean +++ b/OrderedSemigroups/Sign.lean @@ -186,4 +186,7 @@ theorem pos_le_pow_pos {a b : α} (pos : is_positive a) (n : ℕ+) (h : a ≤ b^ theorem pow_le_neg_neg {a b : α} (neg : is_negative a) (n : ℕ+) (h : b^n ≤ a) : is_negative b := pow_neg_neg n (le_neg_neg neg h) +theorem one_unique {a b : α} (one_a : is_one a) (one_b : is_one b) : a = b := by + rw [←one_right one_b a, one_a b] + end LinearOrderedCancelSemigroup