add group and ring rational properties (#1072)

Author: jake

CHANGELOG.md

@@ -277,6 +277,9 @@ Other major additions
 
 * Added new modules:
   ```agda
+  Algebra.Morphism.GroupMonomorphism
+  Algebra.Morphism.RingMonomorphism
+  
   Codata.Cowriter.Bisimilarity
 
   Data.Erased
@@ -406,6 +409,20 @@ Other major additions
 Other minor additions
 ---------------------
 
+* Added new record to `Algebra.Bundles`:
+  ```
+  +-rawGroup : RawGroup c ℓ
+  ```
+  
+* Added new records to `Algebra.Morphism.Structures`:
+  ```
+  IsGroupHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂)
+  IsGroupMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂)
+  IsGroupIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
+  IsRingHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂)
+  IsRingMonomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂)
+  IsRingIsomorphism (⟦_⟧ : A → B) : Set (a ⊔ b ⊔ ℓ₁ ⊔ ℓ₂)
+
 * Added new proof to `Data.Fin.Properties`:
   ```agda
   inject+-raise-splitAt : [ inject+ n , raise {n} m ] (splitAt m i) ≡ i
@@ -734,23 +751,44 @@ Other minor additions
   toℚᵘ-isMagmaHomomorphism-*  : IsMagmaHomomorphism *-rawMagma ℚᵘ.*-rawMagma toℚᵘ
   toℚᵘ-isMonoidHomomorphism-* : IsMonoidHomomorphism *-rawMonoid ℚᵘ.*-rawMonoid toℚᵘ
   toℚᵘ-isMonoidMonomorphism-* : IsMonoidMonomorphism *-rawMonoid ℚᵘ.*-rawMonoid toℚᵘ
+  toℚᵘ-homo‿- : Homomorphic₁ toℚᵘ (-_) (ℚᵘ.-_)
+  toℚᵘ-isGroupHomomorphism-+  : IsGroupHomomorphism +-0-rawGroup ℚᵘ.+-0-rawGroup toℚᵘ
+  toℚᵘ-isGroupMonomorphism-+  : IsGroupMonomorphism +-0-rawGroup ℚᵘ.+-0-rawGroup toℚᵘ
+  toℚᵘ-isRingHomomorphism-|-* : IsRingHomomorphism +-*-rawRing ℚᵘ.+-*-rawRing toℚᵘ
+  toℚᵘ-isRingMonomorphism-|-* : IsRingMonomorphism +-*-rawRing ℚᵘ.+-*-rawRing toℚᵘ
 
   *-assoc     : Associative _*_
   *-comm      : Commutative _*_
   *-identityˡ : LeftIdentity 1ℚ _*_
   *-identityʳ : RightIdentity 1ℚ _*_
   *-identity  : Identity 1ℚ _*_
-
+  +-inverseˡ  : LeftInverse 0ℚ -_ _+_
+  +-inverseʳ  : RightInverse 0ℚ -_ _+_
+  +-inverse   : Inverse 0ℚ -_ _+_
+  -‿cong      :  Congruent₁ (-_)
+  
   *-isMagma               : IsMagma _*_
   *-isSemigroup           : IsSemigroup _*
   *-1-isMonoid            : IsMonoid _*_ 1ℚ
   *-1-isCommutativeMonoid : IsCommutativeMonoid _*_ 1ℚ
   *-rawMagma              : RawMagma 0ℓ 0ℓ
   *-rawMonoid             : RawMonoid 0ℓ 0ℓ
+  +-0-rawGroup            : RawGroup 0ℓ 0ℓ
+  +-*-rawRing             : RawRing 0ℓ 0ℓ
+  +-0-isGroup             : IsGroup _+_ 0ℚ (-_)
+  +-0-isAbelianGroup      : IsAbelianGroup _+_ 0ℚ (-_)
+  +-0-isRing              : IsRing _+_ _*_ -_ 0ℚ 1ℚ
+  +-0-group               : Group 0ℓ 0ℓ
+  +-0-abelianGroup        : AbelianGroup 0ℓ 0ℓ
+  *-distribˡ-+            : _*_ DistributesOverˡ _+_
+  *-distribʳ-+            : _*_ DistributesOverʳ _+_
+  *-distrib-+             : _*_ DistributesOver _+_
   *-magma                 : Magma 0ℓ 0ℓ
   *-semigroup             : Semigroup 0ℓ 0ℓ
   *-1-monoid              : Monoid 0ℓ 0ℓ
   *-1-commutativeMonoid   : CommutativeMonoid 0ℓ 0ℓ
+  +-*-isRing              : IsRing _+_ _*_ -_ 0ℚ 1ℚ
+  +-*-ring                : Ring 0ℓ 0ℓ
   ```
 
 * Added new proofs to `Data.Rational.Unnormalised.Properties`:
@@ -763,12 +801,69 @@ Other minor additions
   +-0-group          : Group 0ℓ 0ℓ
   +-0-isAbelianGroup : IsAbelianGroup _≃_ _+_ 0ℚᵘ (-_)
   +-0-abelianGroup   : AbelianGroup 0ℓ 0ℓ
-  *-zeroˡ : LeftZero _≃_ 0ℚᵘ _*_
-  *-zeroʳ : RightZero _≃_ 0ℚᵘ _*_
-  *-zero : Zero _≃_ 0ℚᵘ _*_
-  *-distribˡ-+ : _DistributesOverˡ_ _≃_ _*_ _+_
-  *-distribʳ-+ : _DistributesOverʳ_ _≃_ _*_ _+_
-  *-distrib-+ : _DistributesOver_ _≃_ _*_ _+_
-  +-*-isRing : IsRing _≃_ _+_ _*_ -_ 0ℚᵘ 1ℚ 
-  +-*-ring : Ring 0ℓ 0ℓ
+  *-zeroˡ            : LeftZero _≃_ 0ℚᵘ _*_
+  *-zeroʳ            : RightZero _≃_ 0ℚᵘ _*_
+  *-zero             : Zero _≃_ 0ℚᵘ _*_
+  *-distribˡ-+       : _DistributesOverˡ_ _≃_ _*_ _+_
+  *-distribʳ-+       : _DistributesOverʳ_ _≃_ _*_ _+_
+  *-distrib-+        : _DistributesOver_ _≃_ _*_ _+_
+  +-*-isRing         : IsRing _≃_ _+_ _*_ -_ 0ℚᵘ 1ℚ 
+  +-*-ring           : Ring 0ℓ 0ℓ
+  +-0-rawGroup       : RawGroup 0ℓ 0ℓ
+  +-*-rawRing        : RawRing 0ℓ 0ℓ
+  +-*-isCommutativeRing : IsCommutativeRing _≃_ _+_ _*_ -_ 0ℚᵘ 1ℚᵘ
+  +-*-commutativeRing : CommutativeRing 0ℓ 0ℓ
+  ```
+
+* Added convenience functions to `Data.String.Base`:
+  ```agda
+  parens : String → String
+  braces : String → String
+  intersperse : String → List String → String
+  unwords : List String → String
+  _<+>_ : String → String → String -- space-introducing append
   ```
+  
+Version 2.6.1 changes
+=====================
+
+* New modules
+  ```agda
+  Data.Float.Base
+  Data.Float.Properties
+
+  Data.Word.Base
+  Data.Word.Properties
+
+  Reflection.Abstraction
+  Reflection.Argument
+  Reflection.Argument.Information
+  Reflection.Argument.Relevance
+  Reflection.Argument.Visibility
+  Reflection.Definition
+  Reflection.Literal
+  Reflection.Meta
+  Reflection.Name
+  Reflection.Pattern
+  Reflection.Term
+  ```
+
+* The modules `Data.Word.Unsafe` and `Data.Float.Unsafe` have been removed
+  as there are no longer any unsafe operations.
+
+* Decidable equality over floating point numbers has been made safe and
+  so  `_≟_` has been moved from `Data.Float.Unsafe` to `Data.Float.Properties`.
+
+* Added new definitions to `Data.Word.Base`:
+  ```agda
+  _≈_ : Rel Word64 zero
+  _<_ : Rel Word64 zero
+  ```
+
+* Decidable equality over words has been made safe and so `_≟_` has been
+  moved from `Data.Word.Unsafe` to `Data.Word.Properties`.
+
+* Added new definitions in `Relation.Binary.Core`:
+  ```agda
+  DecidableEquality A = Decidable {A = A} _≡_
+  ```

src/Algebra/Bundles.agda

@@ -267,7 +267,6 @@ record Group c ℓ : Set (suc (c ⊔ ℓ)) where
 
   open Monoid monoid public using (rawMagma; magma; semigroup; rawMonoid)
 
-
 record AbelianGroup c ℓ : Set (suc (c ⊔ ℓ)) where
   infix  8 _⁻¹
   infixl 7 _∙_
@@ -603,6 +602,20 @@ record RawRing c ℓ : Set (suc (c ⊔ ℓ)) where
     0#      : Carrier
     1#      : Carrier
 
+  +-rawGroup : RawGroup c ℓ
+  +-rawGroup = record
+    { _≈_ = _≈_
+    ; _∙_ = _+_
+    ; ε   = 0#
+    ; _⁻¹ = -_
+    }
+
+  *-rawMonoid : RawMonoid c ℓ
+  *-rawMonoid = record
+    { _≈_     = _≈_
+    ; _∙_     = _*_
+    ; ε       = 1#
+    }
 
 record Ring c ℓ : Set (suc (c ⊔ ℓ)) where
   infix  8 -_

src/Algebra/Morphism/GroupMonomorphism.agda

@@ -0,0 +1,83 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Consequences of a monomorphism between group-like structures
+------------------------------------------------------------------------
+
+-- See Data.Nat.Binary.Properties for examples of how this and similar
+-- modules can be used to easily translate properties between types.
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Algebra.Bundles
+open import Algebra.Morphism.Structures
+open import Relation.Binary.Core
+
+module Algebra.Morphism.GroupMonomorphism
+  {a b ℓ₁ ℓ₂} {G₁ : RawGroup a ℓ₁} {G₂ : RawGroup b ℓ₂} {⟦_⟧}
+  (isGroupMonomorphism : IsGroupMonomorphism G₁ G₂ ⟦_⟧)
+  where
+
+open IsGroupMonomorphism isGroupMonomorphism
+open RawGroup G₁ renaming
+  (Carrier to A; _≈_ to _≈₁_; _∙_ to _∙_; _⁻¹ to _⁻¹₁; ε to ε₁)
+open RawGroup G₂ renaming
+  (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; _⁻¹ to _⁻¹₂; ε to ε₂)
+
+open import Algebra.Definitions
+open import Algebra.Structures
+open import Data.Product
+import Relation.Binary.Reasoning.Setoid as SetoidReasoning
+
+------------------------------------------------------------------------
+-- Re-export all properties of monoid monomorphisms
+
+open import Algebra.Morphism.MonoidMonomorphism
+  isMonoidMonomorphism public
+
+------------------------------------------------------------------------
+-- Properties
+
+module _ (◦-isMagma : IsMagma _≈₂_ _◦_) where
+
+  open IsMagma ◦-isMagma renaming (∙-cong to ◦-cong)
+  open SetoidReasoning setoid
+
+  inverseˡ : LeftInverse _≈₂_ ε₂ _⁻¹₂ _◦_ → LeftInverse _≈₁_ ε₁ _⁻¹₁  _∙_
+  inverseˡ invˡ x = injective (begin
+    ⟦ x ⁻¹₁ ∙ x ⟧     ≈⟨ ∙-homo (x ⁻¹₁ ) x ⟩
+    ⟦ x ⁻¹₁ ⟧ ◦ ⟦ x ⟧ ≈⟨ ◦-cong (⁻¹-homo x) refl ⟩
+    ⟦ x ⟧ ⁻¹₂ ◦ ⟦ x ⟧ ≈⟨ invˡ ⟦ x ⟧ ⟩
+    ε₂                ≈˘⟨ ε-homo ⟩
+    ⟦ ε₁ ⟧ ∎)
+
+  inverseʳ : RightInverse _≈₂_ ε₂ _⁻¹₂ _◦_ → RightInverse _≈₁_ ε₁ _⁻¹₁  _∙_
+  inverseʳ invʳ x = injective (begin
+    ⟦ x ∙ x ⁻¹₁ ⟧     ≈⟨ ∙-homo x (x ⁻¹₁) ⟩
+    ⟦ x ⟧ ◦ ⟦ x ⁻¹₁ ⟧ ≈⟨ ◦-cong refl (⁻¹-homo x) ⟩
+    ⟦ x ⟧ ◦ ⟦ x ⟧ ⁻¹₂ ≈⟨ invʳ ⟦ x ⟧ ⟩
+    ε₂                ≈˘⟨ ε-homo ⟩
+    ⟦ ε₁ ⟧ ∎)
+
+  inverse : Inverse _≈₂_ ε₂ _⁻¹₂ _◦_ → Inverse _≈₁_ ε₁ _⁻¹₁  _∙_
+  inverse (invˡ , invʳ) = inverseˡ invˡ , inverseʳ invʳ
+
+  ⁻¹-cong : Congruent₁ _≈₂_ _⁻¹₂ → Congruent₁ _≈₁_ _⁻¹₁
+  ⁻¹-cong  ⁻¹-cong {x} {y} x≈y = injective (begin
+    ⟦ x ⁻¹₁ ⟧ ≈⟨ ⁻¹-homo x ⟩
+    ⟦ x ⟧ ⁻¹₂ ≈⟨ ⁻¹-cong (⟦⟧-cong x≈y) ⟩
+    ⟦ y ⟧ ⁻¹₂ ≈˘⟨ ⁻¹-homo y ⟩
+    ⟦ y ⁻¹₁ ⟧ ∎)
+
+isGroup : IsGroup _≈₂_ _◦_ ε₂ _⁻¹₂ → IsGroup _≈₁_ _∙_ ε₁ _⁻¹₁
+isGroup isGroup = record
+  { isMonoid = isMonoid G.isMonoid
+  ; inverse  = inverse  G.isMagma G.inverse
+  ; ⁻¹-cong  = ⁻¹-cong  G.isMagma G.⁻¹-cong
+  } where module G = IsGroup isGroup
+
+isAbelianGroup : IsAbelianGroup _≈₂_ _◦_ ε₂ _⁻¹₂ → IsAbelianGroup _≈₁_ _∙_ ε₁ _⁻¹₁
+isAbelianGroup isAbelianGroup = record
+  { isGroup = isGroup G.isGroup
+  ; comm    = comm G.isMagma G.comm
+  } where module G = IsAbelianGroup isAbelianGroup

src/Algebra/Morphism/MonoidMonomorphism.agda

@@ -25,7 +25,6 @@ open RawMonoid M₂ renaming (Carrier to B; _≈_ to _≈₂_; _∙_ to _◦_; 
 open import Algebra.Definitions
 open import Algebra.Structures
 open import Data.Product using (map)
-open import Relation.Binary
 import Relation.Binary.Reasoning.Setoid as SetoidReasoning
 
 ------------------------------------------------------------------------