Skip to content

Commit

Permalink
Prove that a left ordered Archimedean group is right ordered
Browse files Browse the repository at this point in the history
  • Loading branch information
ericluap committed Nov 7, 2024
1 parent 1dd7a52 commit 1ba7ee9
Show file tree
Hide file tree
Showing 2 changed files with 78 additions and 6 deletions.
78 changes: 72 additions & 6 deletions OrderedSemigroups/OrderedGroup/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,7 @@ theorem pos_arch {x y : α} (pos_x : 1 < x) (pos_y : 1 < y) :
If x and y are both positive, then by Archimedneaness
we have a least z such that x^z > y.
-/
theorem pos_min_arch {x y : α} (pos_x : 1 < x) (pos_y : 1 < y) :
theorem pos_min_arch {x y : α} (arch : archimedean_group α) (pos_x : 1 < x) (pos_y : 1 < y) :
∃z : ℤ, x^z > y ∧ z > 0 ∧ (∀t : ℤ, x^t > y → z < t) := sorry

/--
Expand All @@ -110,11 +110,77 @@ def normal_semigroup {α : Type u} [Group α] (x : Subsemigroup α) :=
/--
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
def pos_normal_ordered (pos_normal : normal_semigroup (PositiveCone α)) :
∀ a b : α, a ≤ b → ∀ c : α, a * c ≤ b * c := by sorry

end LeftOrdered

section LeftLinearOrderedGroup

variable [LeftLinearOrderedGroup α]

theorem neg_case_left_arch_false {g h : α} (arch : is_archimedean (α := α)) (pos_g : 1 < g) (neg_h : h < 1)
(conj_lt_one : h * g * h⁻¹ < 1) : False := by
simp [←arch_group_semigroup] at arch
have pos_hinv : 1 < h⁻¹ := one_lt_inv_of_inv neg_h
obtain ⟨z, gz_gt_hinv, _, z_maximum⟩ := pos_min_arch arch pos_g pos_hinv
have hinv_lt : h⁻¹ < g⁻¹ * h⁻¹ := by
have : h⁻¹ * (h * g * h⁻¹) < h⁻¹ * 1 := mul_lt_mul_left' conj_lt_one (h⁻¹)
simp [mul_assoc] at this
have : g⁻¹ * (g * h⁻¹) < g⁻¹ * h⁻¹ := mul_lt_mul_left' this g⁻¹
simpa [mul_assoc]
have : g⁻¹ * h⁻¹ < g⁻¹ * g^z := mul_lt_mul_left' gz_gt_hinv g⁻¹
have hinv_lt : h⁻¹ < g⁻¹ * g^z := by exact gt_trans this hinv_lt
have : g^z = g * g^((-1) + z) := by
have : g^z = g^(1 + ((-1) + z)) := by simp
have : g^(1 + ((-1) + z)) = g^(1 : ℤ) * g^((-1) + z) := by
simp only [zpow_add g 1 (-1 + z)]
simpa
simp [this] at hinv_lt
have := z_maximum (-1 + z) hinv_lt
omega

theorem neg_case_conj_pos {g h : α} (arch : is_archimedean (α := α)) (pos_g : 1 < g) (neg_h : h < 1)
: 1 < h * g * h⁻¹ := by
by_contra not_pos_conj
simp at not_pos_conj
rcases not_pos_conj.eq_or_lt with conj_eq_one | conj_lt_one
· have : g = 1 := by exact conj_eq_one_iff.mp conj_eq_one
rw [this] at pos_g
exact (lt_self_iff_false 1).mp pos_g
exact False.elim (neg_case_left_arch_false arch pos_g neg_h conj_lt_one)

/--
A left ordered group that is Archimedean is an ordered group.
A left ordered group that is Archimedean is right ordered.
-/
def left_arch_ordered (arch : is_archimedean (α := α)) : OrderedGroup α := by sorry

end LeftOrdered
theorem left_arch_ordered (arch : is_archimedean (α := α)) :
∀ a b : α, a ≤ b → ∀ c : α, a * c ≤ b * c := by
apply pos_normal_ordered
simp [normal_semigroup, PositiveCone]
intro g pos_g h
-- Assume that `h * g * h⁻¹` is negative for contradiction
by_contra not_pos_conj
simp at not_pos_conj
rcases not_pos_conj.eq_or_lt with conj_eq_one | conj_lt_one
· have : g = 1 := by exact conj_eq_one_iff.mp conj_eq_one
rw [this] at pos_g
exact (lt_self_iff_false 1).mp pos_g
by_cases pos_h : 1 < h
case neg =>
simp at pos_h
rcases pos_h.eq_or_lt with h_eq_one | neg_h
-- The case where `h = 1`
· simp [h_eq_one] at *
exact (lt_self_iff_false 1).mp (lt_imp_lt_of_le_imp_le (fun a ↦ not_pos_conj) pos_g)
-- The case where `h` is in the negative cone
· exact False.elim (neg_case_left_arch_false arch pos_g neg_h conj_lt_one)
case pos =>
-- The case where `h` is in the positive cone
have conjinv_pos : 1 < (h * g * h⁻¹)⁻¹ := one_lt_inv_of_inv conj_lt_one
simp at conjinv_pos
have hinv_neg : h⁻¹ < 1 := Left.inv_lt_one_iff.mpr pos_h
have := neg_case_conj_pos arch conjinv_pos hinv_neg
simp at this
exact (lt_self_iff_false g).mp (gt_trans pos_g this)

end LeftLinearOrderedGroup
6 changes: 6 additions & 0 deletions OrderedSemigroups/OrderedGroup/Defs.lean
Original file line number Diff line number Diff line change
Expand Up @@ -25,3 +25,9 @@ instance rightOrderedContravariant [RightOrderedGroup α] : ContravariantClass
elim a b c bc := by simpa using mul_le_mul_right' bc a⁻¹

class OrderedGroup (α : Type u) extends LeftOrderedGroup α, RightOrderedGroup α

class LeftLinearOrderedGroup (α : Type u) extends LeftOrderedGroup α, LinearOrder α

class RightLinearOrderedGroup (α : Type u) extends RightOrderedGroup α, LinearOrder α

class LinearOrderedgroup (α : Type u) extends LeftLinearOrderedGroup α, RightLinearOrderedGroup α

0 comments on commit 1ba7ee9

Please sign in to comment.