From d1333badf38af7924c9d1899f3430d83fc0a05fe Mon Sep 17 00:00:00 2001
From: Eric <eric.1334@icloud.com>
Date: Tue, 22 Oct 2024 11:34:07 -0700
Subject: [PATCH] Prove that is a semigroup is archimedean, so is its monoid
 with_one

---
 OrderedSemigroups/Basic.lean             |   6 ++
 OrderedSemigroups/Defs.lean              |   4 +
 OrderedSemigroups/SemigroupToMonoid.lean | 117 +++++++++++++++++++++--
 3 files changed, 119 insertions(+), 8 deletions(-)

diff --git a/OrderedSemigroups/Basic.lean b/OrderedSemigroups/Basic.lean
index de6fb0a..3dec0ae 100644
--- a/OrderedSemigroups/Basic.lean
+++ b/OrderedSemigroups/Basic.lean
@@ -15,6 +15,12 @@ variable {α : Type u}
 section Semigroup'
 variable [Semigroup' α]
 
+theorem nppow_eq_nppowRec : Semigroup'.nppow = nppowRec (α := α) := by
+  ext x y
+  induction x using PNat.recOn with
+  | p1 => simp [Semigroup'.nppow_one, nppowRec_one]
+  | hp n ih => simp [Semigroup'.nppow_succ,nppowRec_succ, ih]
+
 theorem nppow_eq_pow (n : ℕ+) (x : α) : Semigroup'.nppow n x = x ^ n := rfl
 
 @[simp]
diff --git a/OrderedSemigroups/Defs.lean b/OrderedSemigroups/Defs.lean
index 146d980..b97b07e 100644
--- a/OrderedSemigroups/Defs.lean
+++ b/OrderedSemigroups/Defs.lean
@@ -23,6 +23,10 @@ def nppowRec [Mul α] : ℕ+ → α → α
     (nppowRec ⟨n+1, by simp⟩ a) * a
 termination_by x => x
 
+theorem nppowRec_eq [Mul α] {n m : ℕ+} (h : n.val = m.val) (x : α) :
+    nppowRec n x = nppowRec m x := by
+  simp only [PNat.eq h]
+
 theorem nppowRec_one [Mul α] (x : α) : nppowRec 1 x = x := by
   unfold nppowRec
   simp
diff --git a/OrderedSemigroups/SemigroupToMonoid.lean b/OrderedSemigroups/SemigroupToMonoid.lean
index 8a6d8e9..26a0f67 100644
--- a/OrderedSemigroups/SemigroupToMonoid.lean
+++ b/OrderedSemigroups/SemigroupToMonoid.lean
@@ -9,6 +9,8 @@ def with_one (α : Type u) := α ⊕ Unit
 section Semigroup
 variable [Semigroup α]
 
+instance {β : Type*} [Semigroup β] : Semigroup' β where
+
 instance : Semigroup (with_one α) where
   mul x y :=
     match x, y with
@@ -74,6 +76,20 @@ noncomputable def iso_without_one : α ≃* without_one (α := α) where
     unfold_projs
     simp
 
+theorem pow_without_one {a : α} (n : ℕ+):
+    (Semigroup'.nppow n (Sum.inl a : with_one α) : with_one α) = (Sum.inl (a ^ n) : with_one α) := by
+  induction n using PNat.recOn with
+  | p1 => simp [Semigroup'.nppow_one]
+  | hp n ih =>
+    simp [Semigroup'.nppow_succ, ih]
+    unfold_projs
+    simp [nppowRec_succ n a]
+    have : Mul.mul (nppowRec n a) a = nppowRec (n+1) a := (nppowRec_succ n a).symm
+    rw [this, Sum.inl.injEq]
+    apply nppowRec_eq
+    simp
+    rfl
+
 end Semigroup
 
 section CommSemigroup'
@@ -94,10 +110,10 @@ instance : CommMonoid (with_one α) where
 end CommSemigroup'
 
 section LinearOrderedCancelSemigroup
-variable [LinearOrderedCancelCommSemigroup α]
+variable [LinearOrderedCancelCommSemigroup α] [not_one : Fact (∀x : α, ¬is_one x)]
 
 set_option maxHeartbeats 300000
-instance to_monoid (not_one : ∀x : α, ¬is_one x) : LinearOrderedCancelCommMonoid (with_one α) where
+instance to_monoid [not_one : Fact (∀x : α, ¬is_one x)] : LinearOrderedCancelCommMonoid (with_one α) where
   le := by
     intro x y
     rcases x with x | _
@@ -130,8 +146,8 @@ instance to_monoid (not_one : ∀x : α, ¬is_one x) : LinearOrderedCancelCommMo
     <;> rcases y with y | one
     <;> simp only [ge_iff_le, reduceCtorEq] at *
     · rw [PartialOrder.le_antisymm x y x_le_y y_le_x]
-    · exact not_one x (one_right_one_forall (PartialOrder.le_antisymm (x*x) x x_le_y y_le_x))
-    · exact not_one y (one_right_one_forall (PartialOrder.le_antisymm (y*y) y y_le_x x_le_y))
+    · exact not_one.out x (one_right_one_forall (PartialOrder.le_antisymm (x*x) x x_le_y y_le_x))
+    · exact not_one.out y (one_right_one_forall (PartialOrder.le_antisymm (y*y) y y_le_x x_le_y))
   mul_le_mul_left := by
     intro x y x_le_y z
     rcases x with x | one
@@ -175,8 +191,6 @@ instance to_monoid (not_one : ∀x : α, ¬is_one x) : LinearOrderedCancelCommMo
     · exact not_neg_iff.1 (not_neg_right_not_neg xy_le_xz)
     all_goals exact xy_le_xz
 
-instance {β : Type*} [Semigroup β] : Semigroup' β where
-
 instance {β : Type*} [OrderedCommMonoid β] : OrderedSemigroup β where
   mul_le_mul_left := fun _ _ a_1 c ↦ mul_le_mul_left' a_1 c
   mul_le_mul_right := fun _ _ a_1 c ↦ mul_le_mul_right' a_1 c
@@ -184,8 +198,95 @@ instance {β : Type*} [OrderedCommMonoid β] : OrderedSemigroup β where
 instance toOrderedSemigroup {β : Type*} (_ : LinearOrderedCancelCommMonoid β) : OrderedSemigroup β :=
   inferInstance
 
-theorem arch_semigroup_arch_monoid (not_one : ∀x : α, ¬is_one x) (arch : is_archimedean (α := α)) :
-    @is_archimedean (with_one α) (toOrderedSemigroup (to_monoid not_one)) := sorry
+theorem inr_is_one : @is_one (with_one α) _ (Sum.inr ()) := by
+  simp only [is_one]
+  intro x
+  rcases x with x | one
+  <;> unfold_projs
+  <;> simp
+
+theorem pos_without_one {a : α} : @is_positive (with_one α) _ (Sum.inl a) ↔ is_positive a := by
+  constructor
+  · simp only [is_positive] at *
+    intro pos x
+    have := pos (Sum.inl x)
+    unfold_projs at this
+    simp at this
+    tauto
+  · simp only [is_positive] at *
+    intro pos x
+    rcases x with x | one
+    · have := pos x
+      unfold_projs
+      simp
+      constructor
+      exact this.le
+      trivial
+    · unfold_projs
+      simp
+      constructor
+      exact (pos a).le
+      exact pos a
+
+theorem neg_without_one {a : α} : @is_negative (with_one α) _ (Sum.inl a) ↔ is_negative a := by
+  constructor
+  · simp only [is_negative] at *
+    intro neg x
+    have := neg (Sum.inl x)
+    unfold_projs at this
+    simp at this
+    tauto
+  · simp only [is_negative] at *
+    intro neg x
+    rcases x with x | one
+    · have := neg x
+      unfold_projs
+      simp
+      constructor
+      exact this.le
+      trivial
+    · unfold_projs
+      simp
+      constructor
+      exact (neg a).le
+      exact neg a
+
+theorem one_without_one {a : α} : @is_one (with_one α) _ (Sum.inl a) ↔ is_one a := by
+  constructor
+  · intro one x
+    have := one (Sum.inl x)
+    simp at this
+  · intro one
+    exact False.elim (not_one.out a one)
+
+theorem same_sign_without_one {a b : α} : @same_sign (with_one α) _ (Sum.inl a) (Sum.inl b) ↔ same_sign a b := by
+  simp [same_sign, neg_without_one, pos_without_one, one_without_one] at *
+
+theorem arch_wrt_without_one {a b : α} : @is_archimedean_wrt (with_one α) _ (Sum.inl a) (Sum.inl b) ↔ is_archimedean_wrt a b := by
+  simp [is_archimedean_wrt, pos_without_one, neg_without_one, HPow.hPow, Pow.pow, pow_without_one, nppow_eq_nppowRec]
+  unfold_projs
+  have {a b : α} : a ≤ b ∧ a < b ↔ a < b := by
+    constructor
+    · rintro ⟨-, this⟩
+      exact this
+    · intro h
+      exact ⟨h.le, h⟩
+  simp [this]
 
+theorem arch_semigroup_arch_monoid (arch : is_archimedean (α := α)) :
+    @is_archimedean (with_one α) _ := by
+  simp [is_archimedean] at *
+  intro x y
+  rcases x with x | one
+  <;> rcases y with y | one'
+  <;> simp [same_sign_without_one, one_without_one, arch_wrt_without_one]
+  · exact arch x y
+  · right
+    left
+    exact inr_is_one
+  · left
+    exact inr_is_one
+  · left
+    exact inr_is_one
 
 end LinearOrderedCancelSemigroup