From 4cd820506e0fd2a5595a11555fc2a6206757b3cd Mon Sep 17 00:00:00 2001
From: Greg Brown <greg.brown@cl.cam.ac.uk>
Date: Mon, 4 Apr 2022 15:40:31 +0100
Subject: Add group inverse preserves identity.

---
 .../Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda      | 2 ++
 .../Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda   | 4 ++--
 .../Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda      | 4 ++--
 src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda      | 4 ++--
 src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda      | 8 ++++++++
 src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda       | 2 ++
 6 files changed, 18 insertions(+), 6 deletions(-)

(limited to 'src')

diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda
index cad9714..aa37d59 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/AbelianGroup.agda
@@ -63,9 +63,11 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Group group public
 
   ; ⁻¹-anti-cancel-<; ⁻¹-anti-cancel-≤
 
+  ; x≈ε⇒x⁻¹≈ε
   ; x<ε⇒x⁻¹>ε; x>ε⇒x⁻¹<ε
   ; x≤ε⇒x⁻¹≥ε; x≥ε⇒x⁻¹≤ε
 
+  ; x⁻¹≈ε⇒x≈ε
   ; x⁻¹<ε⇒x>ε; x⁻¹>ε⇒x<ε
   ; x⁻¹≤ε⇒x≥ε; x⁻¹≥ε⇒x≤ε
 
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda
index 1ccde6f..37996b0 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/CommutativeRing.agda
@@ -61,8 +61,8 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public
   ; -‿anti-mono-<; -‿anti-mono-≤
   ; -‿anti-cancel-<; -‿anti-cancel-≤
 
-  ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0
-  ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0
+  ; x≈0⇒-x≈0 ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0
+  ; -x≈0⇒x≈0 ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0
 
   ; x<y⇒0<y-x; 0<y-x⇒x<y
 
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
index 3961ca1..03e8ecd 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/DivisionRing.agda
@@ -61,8 +61,8 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.Ring ring public
   ; -‿anti-mono-<; -‿anti-mono-≤
   ; -‿anti-cancel-<; -‿anti-cancel-≤
 
-  ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0
-  ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0
+  ; x≈0⇒-x≈0 ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0
+  ; -x≈0⇒x≈0 ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0
 
   ; x<y⇒0<y-x; 0<y-x⇒x<y
 
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda
index f0ae47d..51a054e 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Field.agda
@@ -61,8 +61,8 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.DivisionRing divisionR
   ; -‿anti-mono-<; -‿anti-mono-≤
   ; -‿anti-cancel-<; -‿anti-cancel-≤
 
-  ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0
-  ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0
+  ; x≈0⇒-x≈0 ; x<0⇒-x>0; x>0⇒-x<0; x≤0⇒-x≥0; x≥0⇒-x≤0
+  ; -x≈0⇒x≈0 ; -x<0⇒x>0; -x>0⇒x<0; -x≤0⇒x≥0; -x≥0⇒x≤0
 
   ; x<y⇒0<y-x; 0<y-x⇒x<y
 
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda
index cf8e4f2..e186c71 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Group.agda
@@ -164,6 +164,14 @@ x⁻¹≥ε⇒x≤ε {x} x⁻¹≥ε = begin
   x ⁻¹ ⁻¹ ≤⟨  x≥ε⇒x⁻¹≤ε x⁻¹≥ε ⟩
   ε       ∎
 
+---- Preserves and respects signs (_≈_)
+
+x≈ε⇒x⁻¹≈ε : ∀ {x} → x ≈ ε → x ⁻¹ ≈ ε
+x≈ε⇒x⁻¹≈ε {x} x≈ε = ≮∧≯⇒≈ (<-irrefl (Eq.sym x≈ε) ∘ x⁻¹<ε⇒x>ε) (<-irrefl x≈ε ∘ x⁻¹>ε⇒x<ε)
+
+x⁻¹≈ε⇒x≈ε : ∀ {x} → x ⁻¹ ≈ ε → x ≈ ε
+x⁻¹≈ε⇒x≈ε {x} x⁻¹≈ε = ≮∧≯⇒≈ (<-irrefl (Eq.sym x⁻¹≈ε) ∘ x<ε⇒x⁻¹>ε) (<-irrefl x⁻¹≈ε ∘ x>ε⇒x⁻¹<ε)
+
 -- ---- Infer signs
 
 -- -- _≈_
diff --git a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda
index db070e0..c83f683 100644
--- a/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda
+++ b/src/Helium/Algebra/Ordered/StrictTotal/Properties/Ring.agda
@@ -105,11 +105,13 @@ open import Helium.Algebra.Ordered.StrictTotal.Properties.AbelianGroup +-abelian
   ; ⁻¹-anti-cancel-< to -‿anti-cancel-<
   ; ⁻¹-anti-cancel-≤ to -‿anti-cancel-≤
 
+  ; x≈ε⇒x⁻¹≈ε to x≈0⇒-x≈0
   ; x<ε⇒x⁻¹>ε to x<0⇒-x>0
   ; x>ε⇒x⁻¹<ε to x>0⇒-x<0
   ; x≤ε⇒x⁻¹≥ε to x≤0⇒-x≥0
   ; x≥ε⇒x⁻¹≤ε to x≥0⇒-x≤0
 
+  ; x⁻¹≈ε⇒x≈ε to -x≈0⇒x≈0
   ; x⁻¹<ε⇒x>ε to -x<0⇒x>0
   ; x⁻¹>ε⇒x<ε to -x>0⇒x<0
   ; x⁻¹≤ε⇒x≥ε to -x≤0⇒x≥0
-- 
cgit v1.2.3