Add properties of almost groups.

1 files changed, 118 insertions, 0 deletions

diff --git a/src/Helium/Algebra/Properties/AlmostGroup.agda b/src/Helium/Algebra/Properties/AlmostGroup.agda
new file mode 100644
index 0000000..a21d218
--- /dev/null
+++ b/src/Helium/Algebra/Properties/AlmostGroup.agda
@@ -0,0 +1,118 @@
+------------------------------------------------------------------------
+--  Agda Helium
+--
+-- Properties of almost groups
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Helium.Algebra.Bundles
+
+module Helium.Algebra.Properties.AlmostGroup
+  {g₁ g₂}
+  (almostGroup : AlmostGroup g₁ g₂)
+  where
+
+open AlmostGroup almostGroup
+open import Algebra.Definitions _≈_
+open import Relation.Binary.Reasoning.Setoid setoid
+open import Function
+open import Data.Product
+
+1≉0⇒1⁻¹≈1 : (1≉0 : 1# ≉ 0#) → 1≉0 ⁻¹ ≈ 1#
+1≉0⇒1⁻¹≈1 1≉0 = begin
+  1≉0 ⁻¹      ≈˘⟨ identityʳ (1≉0 ⁻¹) ⟩
+  1≉0 ⁻¹ ∙ 1# ≈⟨ inverseˡ 1≉0 ⟩
+  1#          ∎
+
+⁻¹-irrelevant : ∀ {x} → (x≉0 x≉0′ : x ≉ 0#) → x≉0 ⁻¹ ≈ x≉0′ ⁻¹
+⁻¹-irrelevant {x} x≉0 x≉0′ = begin
+  x≉0 ⁻¹                 ≈˘⟨ identityˡ (x≉0 ⁻¹) ⟩
+  1# ∙ x≉0 ⁻¹            ≈˘⟨ ∙-congʳ (inverseˡ x≉0′) ⟩
+  x≉0′ ⁻¹ ∙ x ∙ x≉0 ⁻¹   ≈⟨  assoc (x≉0′ ⁻¹) x (x≉0 ⁻¹) ⟩
+  x≉0′ ⁻¹ ∙ (x ∙ x≉0 ⁻¹) ≈⟨  ∙-congˡ (inverseʳ x≉0) ⟩
+  x≉0′ ⁻¹ ∙ 1#           ≈⟨  identityʳ (x≉0′ ⁻¹) ⟩
+  x≉0′ ⁻¹                ∎
+
+private
+
+  left-helper : ∀ x {y} (y≉0 : y ≉ 0#) → (x ∙ y) ∙ y≉0 ⁻¹ ≈ x
+  left-helper x {y} y≉0 = begin
+    x ∙ y ∙ y≉0 ⁻¹   ≈⟨ assoc x y (y≉0 ⁻¹) ⟩
+    x ∙ (y ∙ y≉0 ⁻¹) ≈⟨ ∙-congˡ (inverseʳ y≉0) ⟩
+    x ∙ 1#           ≈⟨ identityʳ x ⟩
+    x                ∎
+
+  right-helper : ∀ {x} (x≉0 : x ≉ 0#) y → x≉0 ⁻¹ ∙ (x ∙ y) ≈ y
+  right-helper {x} x≉0 y = begin
+    x≉0 ⁻¹ ∙ (x ∙ y) ≈˘⟨ assoc (x≉0 ⁻¹) x y ⟩
+    x≉0 ⁻¹ ∙ x ∙ y   ≈⟨  ∙-congʳ (inverseˡ x≉0) ⟩
+    1# ∙ y           ≈⟨  identityˡ y ⟩
+    y                ∎
+
+x≉0⇒∙-cancelˡ : ∀ {x} → x ≉ 0# → Injective _≈_ _≈_ (x ∙_)
+x≉0⇒∙-cancelˡ {x} x≉0 {y} {z} x∙y≈x∙z = begin
+  y                ≈˘⟨ right-helper x≉0 y ⟩
+  x≉0 ⁻¹ ∙ (x ∙ y) ≈⟨  ∙-congˡ x∙y≈x∙z ⟩
+  x≉0 ⁻¹ ∙ (x ∙ z) ≈⟨  right-helper x≉0 z ⟩
+  z                ∎
+
+x≉0⇒∙-cancelʳ : ∀ {x} → x ≉ 0# → Injective _≈_ _≈_ (_∙ x)
+x≉0⇒∙-cancelʳ {x} x≉0 {y} {z} y∙x≈z∙x = begin
+  y              ≈˘⟨ left-helper y x≉0 ⟩
+  y ∙ x ∙ x≉0 ⁻¹ ≈⟨  ∙-congʳ y∙x≈z∙x ⟩
+  z ∙ x ∙ x≉0 ⁻¹ ≈⟨  left-helper z x≉0 ⟩
+  z              ∎
+
+⁻¹-involutive : ∀ {x} → (x≉0 : x ≉ 0#) → (x⁻¹≉0 : x≉0 ⁻¹ ≉ 0#) → x⁻¹≉0 ⁻¹ ≈ x
+⁻¹-involutive {x} x≉0 x⁻¹≉0 = begin
+  x⁻¹≉0 ⁻¹                ≈˘⟨ identityʳ (x⁻¹≉0 ⁻¹) ⟩
+  x⁻¹≉0 ⁻¹ ∙ 1#           ≈˘⟨ ∙-congˡ (inverseˡ x≉0) ⟩
+  x⁻¹≉0 ⁻¹ ∙ (x≉0 ⁻¹ ∙ x) ≈⟨  right-helper x⁻¹≉0 x ⟩
+  x                       ∎
+
+⁻¹-injective : ∀ {x y} {x≉0 : x ≉ 0#} {y≉0 : y ≉ 0#} → x≉0 ⁻¹ ≈ y≉0 ⁻¹ → x ≈ y
+⁻¹-injective {x} {y} {x≉0} {y≉0} x⁻¹≈y⁻¹ = begin
+  x                ≈˘⟨ identityˡ x ⟩
+  1# ∙ x           ≈˘⟨ ∙-congʳ (inverseʳ y≉0) ⟩
+  y ∙ y≉0 ⁻¹ ∙ x   ≈˘⟨ ∙-congʳ (∙-congˡ x⁻¹≈y⁻¹) ⟩
+  y ∙ x≉0 ⁻¹ ∙ x   ≈⟨  assoc y (x≉0 ⁻¹) x ⟩
+  y ∙ (x≉0 ⁻¹ ∙ x) ≈⟨  ∙-congˡ (inverseˡ x≉0) ⟩
+  y ∙ 1#           ≈⟨  identityʳ y ⟩
+  y                ∎
+
+⁻¹-anti-homo-∙ : ∀ {x y} (x≉0 : x ≉ 0#) (y≉0 : y ≉ 0#) (x∙y≉0 : x ∙ y ≉ 0#) → x∙y≉0 ⁻¹ ≈ y≉0 ⁻¹ ∙ x≉0 ⁻¹
+⁻¹-anti-homo-∙ {x} {y} x≉0 y≉0 x∙y≉0 = x≉0⇒∙-cancelˡ x∙y≉0 (begin
+  x ∙ y ∙ x∙y≉0 ⁻¹          ≈⟨  inverseʳ x∙y≉0 ⟩
+  1#                        ≈˘⟨ inverseʳ x≉0 ⟩
+  x ∙ x≉0 ⁻¹                ≈˘⟨ ∙-congʳ (left-helper x y≉0) ⟩
+  x ∙ y ∙ y≉0 ⁻¹ ∙ x≉0 ⁻¹   ≈⟨  assoc (x ∙ y) (y≉0 ⁻¹) (x≉0 ⁻¹) ⟩
+  x ∙ y ∙ (y≉0 ⁻¹ ∙ x≉0 ⁻¹) ∎)
+
+identityˡ-unique : ∀ {x} {y} → y ≉ 0# → x ∙ y ≈ y → x ≈ 1#
+identityˡ-unique {x} {y} y≉0 x∙y≈y = begin
+  x              ≈˘⟨ left-helper x y≉0 ⟩
+  x ∙ y ∙ y≉0 ⁻¹ ≈⟨  ∙-congʳ x∙y≈y ⟩
+  y ∙ y≉0 ⁻¹     ≈⟨  inverseʳ y≉0 ⟩
+  1#             ∎
+
+identityʳ-unique : ∀ {x} {y} → y ≉ 0# → y ∙ x ≈ y → x ≈ 1#
+identityʳ-unique {x} {y} y≉0 y∙x≈y = begin
+  x                ≈˘⟨ right-helper y≉0 x ⟩
+  y≉0 ⁻¹ ∙ (y ∙ x) ≈⟨  ∙-congˡ y∙x≈y ⟩
+  y≉0 ⁻¹ ∙ y       ≈⟨  inverseˡ y≉0 ⟩
+  1#               ∎
+
+inverseˡ-unique : ∀ {x} {y} (y≉0 : y ≉ 0#) → x ∙ y ≈ 1# → x ≈ y≉0 ⁻¹
+inverseˡ-unique {x} {y} y≉0 x∙y≈1 = begin
+  x              ≈˘⟨ left-helper x y≉0 ⟩
+  x ∙ y ∙ y≉0 ⁻¹ ≈⟨  ∙-congʳ x∙y≈1 ⟩
+  1# ∙ y≉0 ⁻¹    ≈⟨  identityˡ (y≉0 ⁻¹) ⟩
+  y≉0 ⁻¹         ∎
+
+inverseʳ-unique : ∀ {x} {y} (y≉0 : y ≉ 0#) → y ∙ x ≈ 1# → x ≈ y≉0 ⁻¹
+inverseʳ-unique {x} {y} y≉0 y∙x≈1 = begin
+  x                ≈˘⟨ right-helper y≉0 x ⟩
+  y≉0 ⁻¹ ∙ (y ∙ x) ≈⟨  ∙-congˡ y∙x≈1 ⟩
+  y≉0 ⁻¹ ∙ 1#      ≈⟨  identityʳ (y≉0 ⁻¹) ⟩
+  y≉0 ⁻¹           ∎