From 36d83d35aa66d05d8dac81a6faebc231606e6bb4 Mon Sep 17 00:00:00 2001
From: Eric P <eric.1334@icloud.com>
Date: Tue, 8 Oct 2024 11:43:42 -0700
Subject: [PATCH] Convert monoid to group

---
 OrderedSemigroups.lean                        |   2 +-
 OrderedSemigroups/Defs.lean                   |  37 ++++++-
 ...migroupToGroup.lean => MonoidToGroup.lean} |   0
 OrderedSemigroups/SemigroupToMonoid.lean      | 100 ++++++++++++++++++
 OrderedSemigroups/Sign.lean                   |  72 ++++++++++++-
 5 files changed, 205 insertions(+), 6 deletions(-)
 rename OrderedSemigroups/{SemigroupToGroup.lean => MonoidToGroup.lean} (100%)
 create mode 100644 OrderedSemigroups/SemigroupToMonoid.lean

diff --git a/OrderedSemigroups.lean b/OrderedSemigroups.lean
index 75adac0..22eddbe 100644
--- a/OrderedSemigroups.lean
+++ b/OrderedSemigroups.lean
@@ -1,4 +1,4 @@
 -- This module serves as the root of the `OrderedSemigroups` library.
 -- Import modules here that should be built as part of the library.
 import «OrderedSemigroups».Archimedean
-import «OrderedSemigroups».SemigroupToGroup
+import «OrderedSemigroups».MonoidToGroup
diff --git a/OrderedSemigroups/Defs.lean b/OrderedSemigroups/Defs.lean
index 23821a8..146d980 100644
--- a/OrderedSemigroups/Defs.lean
+++ b/OrderedSemigroups/Defs.lean
@@ -15,7 +15,7 @@ universe u
 variable {α : Type u}
 
 /-- The action of ℕ+ on a type with Mul where
-  nppowRec n a = a * a ⋯ * a (aka a^n)-/
+  `nppowRec n a = a * a ⋯ * a` (aka `a^n`)-/
 def nppowRec [Mul α] : ℕ+ → α → α
   | 1, a => a
   | ⟨n+2, hnp⟩, a =>
@@ -23,11 +23,35 @@ def nppowRec [Mul α] : ℕ+ → α → α
     (nppowRec ⟨n+1, by simp⟩ a) * a
 termination_by x => x
 
+theorem nppowRec_one [Mul α] (x : α) : nppowRec 1 x = x := by
+  unfold nppowRec
+  simp
+
+theorem nppowRec_succ [Mul α] (n : ℕ+) (x : α) : nppowRec (n + 1) x = nppowRec n x * x := by
+  induction n using PNat.recOn with
+  | p1 =>
+    unfold nppowRec
+    simp [nppowRec_one]
+  | hp n ih =>
+    unfold nppowRec
+    have : (n + 1) = ⟨↑n + 1, nppowRec.proof_1 ↑n⟩ := by rfl
+    simp
+    erw [←this]
+    split
+    · rename_i x y w z
+      have : (n : Nat) = 0 := Eq.symm ((fun {n m} ↦ Nat.succPNat_inj.mp) (id (Eq.symm z)))
+      exact False.elim (PNat.ne_zero n this)
+    · rename_i x y w z h g
+      simp at *
+      have : n = z + 1 := by exact Nat.succPNat_inj.mp g
+      have : n = ⟨z + 1, nppowRec.proof_1 z⟩ := by exact PNat.eq this
+      simp [←this, ih]
+
 /-- 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
+  nppow_one : ∀ x, nppow 1 x = x := by intros x; exact nppowRec_one x
+  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 α ℕ+ :=
@@ -75,3 +99,10 @@ instance [LinearOrderedCancelSemigroup α] : LinearOrderedSemigroup α where
   min_def := LinearOrderedCancelSemigroup.min_def
   max_def := LinearOrderedCancelSemigroup.max_def
   compare_eq_compareOfLessAndEq := LinearOrderedCancelSemigroup.compare_eq_compareOfLessAndEq
+
+class CommSemigroup' (G : Type u) extends Semigroup' G, CommMagma G where
+
+class LinearOrderedCancelCommSemigroup (α : Type u) extends LinearOrderedCancelSemigroup α, CommSemigroup' α where
+
+instance [LinearOrderedCancelCommSemigroup α] : LinearOrderedCancelSemigroup α :=
+  inferInstance
diff --git a/OrderedSemigroups/SemigroupToGroup.lean b/OrderedSemigroups/MonoidToGroup.lean
similarity index 100%
rename from OrderedSemigroups/SemigroupToGroup.lean
rename to OrderedSemigroups/MonoidToGroup.lean
diff --git a/OrderedSemigroups/SemigroupToMonoid.lean b/OrderedSemigroups/SemigroupToMonoid.lean
new file mode 100644
index 0000000..44d7285
--- /dev/null
+++ b/OrderedSemigroups/SemigroupToMonoid.lean
@@ -0,0 +1,100 @@
+import Mathlib.Algebra.Order.Group.Basic
+import OrderedSemigroups.Sign
+
+universe u
+variable {α : Type u}
+
+def with_one (α : Type u) := α ⊕ Unit
+
+section Semigroup
+variable [Semigroup α]
+
+instance : Semigroup (with_one α) where
+  mul x y :=
+    match x, y with
+    | .inl x, .inl y => .inl (x * y)
+    | .inl x, .inr _ => .inl x
+    | .inr _, .inl y => .inl y
+    | .inr one, .inr _ => .inr one
+  mul_assoc := by
+    intro x y z
+    rcases x with x | _ <;> rcases y with y | _ <;> rcases z with z | _
+    <;> try simp [HMul.hMul]
+    · exact congrArg Sum.inl (mul_assoc x y z)
+
+instance : Monoid (with_one α) where
+  one := .inr ()
+  one_mul := by
+    intro x
+    cases x
+    <;> unfold_projs
+    <;> simp
+  mul_one := by
+    intro x
+    cases x
+    <;> unfold_projs
+    <;> simp
+
+end Semigroup
+
+section CommSemigroup'
+variable [CommSemigroup' α]
+
+instance : CommMonoid (with_one α) where
+  mul_comm := by
+    intro x y
+    cases x <;> cases y
+    <;> unfold_projs
+    <;> simp [mul_comm]
+    · apply congrArg
+      rename_i x y
+      have := mul_comm x y
+      unfold_projs at this
+      simpa
+
+end CommSemigroup'
+
+section LinearOrderedCancelSemigroup
+variable [LinearOrderedCancelCommSemigroup α]
+
+instance : OrderedCommMonoid (with_one α) where
+  le := by
+    intro x y
+    rcases x with x | one
+    <;> rcases y with y | one
+    · exact x ≤ y
+    · exact x*x ≤ x
+    · exact y*y ≥ y
+    · exact True
+  le_refl := by
+    intro x
+    rcases x with x | one
+    <;> simp
+  le_trans := by
+    intro x y z x_le_y y_le_z
+    rcases x with x | one
+    <;> rcases y with y | one
+    <;> rcases z with z | one
+    <;> simp at *
+    · exact Preorder.le_trans x y z x_le_y y_le_z
+    · rw [←not_pos_iff]
+      exact le_not_pos_not_pos (not_pos_iff.mpr y_le_z) x_le_y
+    · exact not_pos_le_not_neg (not_pos_iff.mpr x_le_y) (not_neg_iff.mpr y_le_z)
+    · trivial
+    · rw [←not_neg_iff]
+      exact ge_not_neg_not_neg (not_neg_iff.mpr x_le_y) y_le_z
+    · trivial
+  le_antisymm := by
+    intro x y x_le_y y_le_x
+    rcases x with x | one
+    <;> rcases y with y | one
+    <;> simp at *
+    · rw [PartialOrder.le_antisymm x y x_le_y y_le_x]
+    · sorry
+    · sorry
+  mul_le_mul_left := sorry
+
+
+
+
+end LinearOrderedCancelSemigroup
diff --git a/OrderedSemigroups/Sign.lean b/OrderedSemigroups/Sign.lean
index 673bb28..4b76117 100644
--- a/OrderedSemigroups/Sign.lean
+++ b/OrderedSemigroups/Sign.lean
@@ -153,10 +153,10 @@ end OrderedSemigroup
 section LinearOrderedCancelSemigroup
 variable [LinearOrderedCancelSemigroup α]
 
-theorem pos_gt_one {a b : α} (one : is_one a) (h : a < b) : is_positive b :=
+theorem gt_one_pos {a b : α} (one : is_one a) (h : a < b) : is_positive b :=
   fun x ↦ lt_of_eq_of_lt (id (Eq.symm (one x))) (mul_lt_mul_right' h x)
 
-theorem neg_lt_one {a b : α} (one : is_one a) (h : b < a) : is_negative b :=
+theorem lt_one_neg {a b : α} (one : is_one a) (h : b < a) : is_negative b :=
   fun x ↦ lt_of_lt_of_eq (mul_lt_mul_right' h x) (one x)
 
 theorem neg_lt_pos {a b : α} (neg : is_negative a) (pos : is_positive b) : a < b :=
@@ -198,6 +198,12 @@ theorem one_right {a : α} (one : is_one a) : ∀x : α, x * a = x := by
   · trivial
   · exact False.elim (pos_not_one (pos_right_pos_forall h) one)
 
+theorem neg_lt_one {a b : α} (neg : is_negative a) (one : is_one b) : a < b :=
+  lt_of_eq_of_lt (id (Eq.symm (one_right one a))) (neg b)
+
+theorem one_lt_pos {a b : α} (one : is_one a) (pos : is_positive b) : a < b :=
+  lt_of_lt_of_eq (pos a) (one_right one b)
+
 /-- 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
@@ -229,4 +235,66 @@ theorem pow_le_neg_neg {a b : α} (neg : is_negative a) (n : ℕ+) (h : b^n ≤
 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]
 
+theorem not_pos_iff {a : α} : ¬is_positive a ↔ a * a ≤ a := by
+  constructor
+  · intro _
+    obtain pos | neg | one := pos_neg_or_one a
+    · contradiction
+    · exact le_of_lt (neg a)
+    · exact le_of_eq (one a)
+  · intro _
+    simp [is_positive]
+    use a
+
+theorem not_neg_iff {a : α} : ¬is_negative a ↔ a ≤ a * a := by
+  constructor
+  · intro _
+    obtain pos | neg | one := pos_neg_or_one a
+    · exact le_of_lt (pos a)
+    · contradiction
+    · exact Eq.ge (one a)
+  · intro _
+    simp [is_negative]
+    use a
+
+theorem not_pos_or {a : α} (not_pos : ¬is_positive a) : is_negative a ∨ is_one a := by
+  obtain pos | neg | one := pos_neg_or_one a
+  · contradiction
+  · exact Or.symm (Or.inr neg)
+  · exact Or.inr one
+
+theorem not_neg_or {a : α} (not_neg : ¬is_negative a) : is_positive a ∨ is_one a := by
+  obtain pos | neg | one := pos_neg_or_one a
+  · exact Or.symm (Or.inr pos)
+  · contradiction
+  · exact Or.inr one
+
+theorem le_not_pos_not_pos {a b : α} (not_pos : ¬is_positive a) (h : b ≤ a) : ¬is_positive b := by
+  obtain h | h := eq_or_lt_of_le h
+  <;> obtain pos | neg | one := pos_neg_or_one a
+  · contradiction
+  · simpa [h]
+  · simpa [h]
+  · exact fun _ ↦ not_pos pos
+  · exact neg_not_pos (le_neg_neg neg h.le)
+  · exact neg_not_pos (lt_one_neg one h)
+
+theorem ge_not_neg_not_neg {a b : α} (not_neg : ¬is_negative a) (h : a ≤ b) : ¬is_negative b := by
+  obtain h | h := eq_or_lt_of_le h
+  <;> obtain pos | neg | one := pos_neg_or_one a
+  · simpa [←h]
+  · simpa [←h]
+  · simpa [←h]
+  · exact pos_not_neg (pos_le_pos pos h.le)
+  · contradiction
+  · exact pos_not_neg (gt_one_pos one h)
+
+theorem not_pos_le_not_neg {a b : α} (not_pos : ¬is_positive a) (not_neg : ¬is_negative b) : a ≤ b := by
+  obtain neg_a | one_a := not_pos_or not_pos
+  <;> obtain pos_b | one_b := not_neg_or not_neg
+  · exact (neg_lt_pos neg_a pos_b).le
+  · exact (neg_lt_one neg_a one_b).le
+  · exact (one_lt_pos one_a pos_b).le
+  · exact (one_unique one_a one_b).le
+
 end LinearOrderedCancelSemigroup