SelfInverse operations on Algebras and their properties (#1914)

Author: jamesmckinna

CHANGELOG.md

@@ -1591,8 +1591,23 @@ Other minor changes
   ```
   and their corresponding algebraic subbundles.
 
+* Added new proofs to `Algebra.Consequences.Base`:
+  ```agda
+  reflexive+selfInverse⇒involutive : Reflexive _≈_ →
+                                     SelfInverse _≈_ f →
+                                     Involutive _≈_ f
+  ```
+
 * Added new proofs to `Algebra.Consequences.Setoid`:
   ```agda
+  involutive⇒surjective  : Involutive f  → Surjective f
+  selfInverse⇒involutive : SelfInverse f → Involutive f
+  selfInverse⇒congruent  : SelfInverse f → Congruent f
+  selfInverse⇒inverseᵇ   : SelfInverse f → Inverseᵇ f f
+  selfInverse⇒surjective : SelfInverse f → Surjective f
+  selfInverse⇒injective  : SelfInverse f → Injective f
+  selfInverse⇒bijective  : SelfInverse f → Bijective f
+
   comm+idˡ⇒id              : Commutative _•_ → LeftIdentity  e _•_ → Identity e _•_
   comm+idʳ⇒id              : Commutative _•_ → RightIdentity e _•_ → Identity e _•_
   comm+zeˡ⇒ze              : Commutative _•_ → LeftZero      e _•_ → Zero     e _•_
@@ -1683,6 +1698,8 @@ Other minor changes
 
 * Added new definition to `Algebra.Definitions`:
   ```agda
+  SelfInverse : Op₁ A → Set _
+  
   LeftDividesˡ  : Op₂ A → Op₂ A → Set _
   LeftDividesʳ  : Op₂ A → Op₂ A → Set _
   RightDividesˡ : Op₂ A → Op₂ A → Set _

src/Algebra/Consequences/Base.agda

@@ -2,7 +2,7 @@
 -- The Agda standard library
 --
 -- Lemmas relating algebraic definitions (such as associativity and
--- commutativity) that don't the equality relation to be a setoid.
+-- commutativity) that don't require the equality relation to be a setoid.
 ------------------------------------------------------------------------
 
 {-# OPTIONS --without-K --safe #-}
@@ -14,9 +14,19 @@ open import Algebra.Core
 open import Algebra.Definitions
 open import Data.Sum.Base
 open import Relation.Binary.Core
+open import Relation.Binary.Definitions using (Reflexive)
+
+module _ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) where
+
+  sel⇒idem : Selective _≈_ _•_ → Idempotent _≈_ _•_
+  sel⇒idem sel x with sel x x
+  ... | inj₁ x•x≈x = x•x≈x
+  ... | inj₂ x•x≈x = x•x≈x
+
+module _ {ℓ} {f : Op₁ A} (_≈_ : Rel A ℓ) where
+
+  reflexive+selfInverse⇒involutive : Reflexive _≈_ →
+                                     SelfInverse _≈_ f →
+                                     Involutive _≈_ f
+  reflexive+selfInverse⇒involutive refl inv _ = inv refl
 
-sel⇒idem : ∀ {ℓ} {_•_ : Op₂ A} (_≈_ : Rel A ℓ) →
-           Selective _≈_ _•_ → Idempotent _≈_ _•_
-sel⇒idem _ sel x with sel x x
-... | inj₁ x•x≈x = x•x≈x
-... | inj₂ x•x≈x = x•x≈x

src/Algebra/Consequences/Setoid.agda

@@ -17,6 +17,7 @@ open import Algebra.Definitions _≈_
 open import Data.Sum.Base using (inj₁; inj₂)
 open import Data.Product using (_,_)
 open import Function.Base using (_$_)
+import Function.Definitions as FunDefs
 import Relation.Binary.Consequences as Bin
 open import Relation.Binary.Reasoning.Setoid S
 open import Relation.Unary using (Pred)
@@ -28,6 +29,48 @@ open import Relation.Unary using (Pred)
 
 open import Algebra.Consequences.Base public
 
+------------------------------------------------------------------------
+-- Involutive/SelfInverse functions
+
+module _ {f : Op₁ A} (inv : Involutive f) where
+
+  open FunDefs _≈_ _≈_
+
+  involutive⇒surjective : Surjective f
+  involutive⇒surjective y = f y , inv y
+
+module _ {f : Op₁ A} (self : SelfInverse f) where
+
+  selfInverse⇒involutive : Involutive f
+  selfInverse⇒involutive = reflexive+selfInverse⇒involutive _≈_ refl self
+
+  private
+
+    inv = selfInverse⇒involutive
+
+  open FunDefs _≈_ _≈_
+
+  selfInverse⇒congruent : Congruent f
+  selfInverse⇒congruent {x} {y} x≈y = sym (self (begin
+    f (f x) ≈⟨ inv x ⟩
+    x       ≈⟨ x≈y ⟩
+    y       ∎))
+
+  selfInverse⇒inverseᵇ : Inverseᵇ f f
+  selfInverse⇒inverseᵇ = inv , inv
+
+  selfInverse⇒surjective : Surjective f
+  selfInverse⇒surjective = involutive⇒surjective inv
+
+  selfInverse⇒injective : Injective f
+  selfInverse⇒injective {x} {y} x≈y = begin
+    x       ≈˘⟨ self x≈y ⟩
+    f (f y) ≈⟨ inv y ⟩
+    y       ∎
+
+  selfInverse⇒bijective : Bijective f
+  selfInverse⇒bijective = selfInverse⇒injective , selfInverse⇒surjective
+
 ------------------------------------------------------------------------
 -- Magma-like structures
 

src/Algebra/Definitions.agda

@@ -126,6 +126,9 @@ _∙_ Absorbs _∘_ = ∀ x y → (x ∙ (x ∘ y)) ≈ x
 Absorptive : Op₂ A → Op₂ A → Set _
 Absorptive ∙ ∘ = (∙ Absorbs ∘) × (∘ Absorbs ∙)
 
+SelfInverse : Op₁ A → Set _
+SelfInverse f = ∀ {x y} → f x ≈ y → f y ≈ x
+
 Involutive : Op₁ A → Set _
 Involutive f = ∀ x → f (f x) ≈ x
 

src/Data/Parity/Properties.agda

@@ -25,8 +25,8 @@ open import Relation.Nullary using (yes; no)
 
 open import Algebra.Structures {A = Parity} _≡_
 open import Algebra.Definitions {A = Parity} _≡_
-
-open import Algebra.Consequences.Propositional using (comm+distrˡ⇒distrʳ)
+open import Algebra.Consequences.Propositional
+  using (selfInverse⇒involutive; selfInverse⇒injective; comm+distrˡ⇒distrʳ)
 open import Algebra.Morphism.Structures
 
 ------------------------------------------------------------------------
@@ -52,22 +52,24 @@ _≟_ : DecidableEquality Parity
 ------------------------------------------------------------------------
 -- _⁻¹
 
-p≢p⁻¹ : ∀ p → p ≢ p ⁻¹
-p≢p⁻¹ 1ℙ ()
-p≢p⁻¹ 0ℙ ()
+-- Algebraic properties of _⁻¹
+
+⁻¹-selfInverse : SelfInverse _⁻¹
+⁻¹-selfInverse { 1ℙ } { 0ℙ } refl = refl
+⁻¹-selfInverse { 0ℙ } { 1ℙ } refl = refl
 
-⁻¹-inverts : ∀ {p q} → p ⁻¹ ≡ q → q ⁻¹ ≡ p
-⁻¹-inverts { 1ℙ } { 0ℙ } refl = refl
-⁻¹-inverts { 0ℙ } { 1ℙ } refl = refl
+⁻¹-involutive : Involutive _⁻¹
+⁻¹-involutive = selfInverse⇒involutive ⁻¹-selfInverse
 
-⁻¹-involutive : ∀ p → (p ⁻¹) ⁻¹ ≡ p
-⁻¹-involutive p = ⁻¹-inverts refl
+⁻¹-injective : Injective _≡_ _≡_ _⁻¹
+⁻¹-injective = selfInverse⇒injective ⁻¹-selfInverse
 
-⁻¹-injective : ∀ {p q} → p ⁻¹ ≡ q ⁻¹ → p ≡ q
-⁻¹-injective {p} {q} eq = begin
-  p         ≡⟨ sym (⁻¹-inverts eq) ⟩
-  (q ⁻¹) ⁻¹ ≡⟨ ⁻¹-involutive q ⟩
-  q         ∎ where open ≡-Reasoning
+------------------------------------------------------------------------
+-- other properties of _⁻¹
+
+p≢p⁻¹ : ∀ p → p ≢ p ⁻¹
+p≢p⁻¹ 1ℙ ()
+p≢p⁻¹ 0ℙ ()
 
 ------------------------------------------------------------------------
 -- ⁻¹ and _+_
@@ -480,7 +482,7 @@ toSign-isGroupIsomorphism = record
 
 suc-homo-⁻¹ : ∀ n → (parity (suc n)) ⁻¹ ≡ parity n
 suc-homo-⁻¹ zero    = refl
-suc-homo-⁻¹ (suc n) = ⁻¹-inverts (suc-homo-⁻¹ n)
+suc-homo-⁻¹ (suc n) = ⁻¹-selfInverse (suc-homo-⁻¹ n)
 
 -- parity is a _+_ homomorphism
 

src/Data/Sign/Properties.agda

@@ -21,6 +21,8 @@ open import Relation.Nullary.Decidable using (yes; no)
 
 open import Algebra.Structures {A = Sign} _≡_
 open import Algebra.Definitions {A = Sign} _≡_
+open import Algebra.Consequences.Propositional
+  using (selfInverse⇒involutive; selfInverse⇒injective)
 
 ------------------------------------------------------------------------
 -- Equality
@@ -45,14 +47,26 @@ _≟_ : DecidableEquality Sign
 ------------------------------------------------------------------------
 -- opposite
 
+-- Algebraic properties of opposite
+
+opposite-selfInverse : SelfInverse opposite
+opposite-selfInverse { - } { + } refl = refl
+opposite-selfInverse { + } { - } refl = refl
+
+opposite-involutive : Involutive opposite
+opposite-involutive = selfInverse⇒involutive opposite-selfInverse
+
+opposite-injective : Injective _≡_ _≡_ opposite
+opposite-injective = selfInverse⇒injective opposite-selfInverse
+
+
+------------------------------------------------------------------------
+-- other properties of opposite
+
 s≢opposite[s] : ∀ s → s ≢ opposite s
 s≢opposite[s] - ()
 s≢opposite[s] + ()
 
-opposite-injective : ∀ {s t} → opposite s ≡ opposite t → s ≡ t
-opposite-injective { - } { - } refl = refl
-opposite-injective { + } { + } refl = refl
-
 ------------------------------------------------------------------------
 -- _*_