opposite of a Ring

CHANGELOG.md

@@ -1587,6 +1587,13 @@ Other minor changes
   moufangLoop : MoufangLoop a ℓ₁ → MoufangLoop b ℓ₂ → MoufangLoop (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
  ```
 
+* Added new proofs to `Algebra.Construct.Flip.Op`:
+  ```agda
+  zero : Zero ≈ ε ∙ → Zero ≈ ε (flip ∙)
+  distributes : (≈ DistributesOver ∙) + → (≈ DistributesOver (flip ∙)) +
+  isRing : IsRing ≈ + * - 0# 1# → IsRing ≈ + (flip *) - 0# 1#
+  ```
+
 * Added new definition to `Algebra.Definitions`:
   ```agda
   LeftDividesˡ  : Op₂ A → Op₂ A → Set _

src/Algebra/Construct/Flip/Op.agda

@@ -9,7 +9,10 @@
 
 module Algebra.Construct.Flip.Op where
 
-open import Algebra
+open import Algebra.Core
+open import Algebra.Bundles
+import Algebra.Definitions as Def
+import Algebra.Structures as Str
 import Data.Product as Prod
 import Data.Sum as Sum
 open import Function.Base using (flip)
@@ -33,136 +36,171 @@ preserves₂ : (∼ ≈ ≋ : Rel A ℓ) →
              ∙ Preserves₂ ∼ ⟶ ≈ ⟶ ≋ → (flip ∙) Preserves₂ ≈ ⟶ ∼ ⟶ ≋
 preserves₂ _ _ _ pres = flip pres
 
-module _ (≈ : Rel A ℓ) (∙ : Op₂ A) where
+module ∙-Properties (≈ : Rel A ℓ) (∙ : Op₂ A) where
 
-  associative : Symmetric ≈ → Associative ≈ ∙ → Associative ≈ (flip ∙)
+  open Def ≈
+
+  associative : Symmetric ≈ → Associative ∙ → Associative (flip ∙)
   associative sym assoc x y z = sym (assoc z y x)
 
-  identity : Identity ≈ ε ∙ → Identity ≈ ε (flip ∙)
+  identity : Identity ε ∙ → Identity ε (flip ∙)
   identity id = Prod.swap id
 
-  commutative : Commutative ≈ ∙ → Commutative ≈ (flip ∙)
+  commutative : Commutative ∙ → Commutative (flip ∙)
   commutative comm = flip comm
 
-  selective : Selective ≈ ∙ → Selective ≈ (flip ∙)
+  selective : Selective ∙ → Selective (flip ∙)
   selective sel x y = Sum.swap (sel y x)
 
-  idempotent : Idempotent ≈ ∙ → Idempotent ≈ (flip ∙)
+  idempotent : Idempotent ∙ → Idempotent (flip ∙)
   idempotent idem = idem
 
-  inverse : Inverse ≈ ε ⁻¹ ∙ → Inverse ≈ ε ⁻¹ (flip ∙)
+  inverse : Inverse ε ⁻¹ ∙ → Inverse ε ⁻¹ (flip ∙)
   inverse inv = Prod.swap inv
 
+  zero : Zero ε ∙ → Zero ε (flip ∙)
+  zero zer = Prod.swap zer
+
+module *-Properties (≈ : Rel A ℓ) (* + : Op₂ A) where
+
+  open Def ≈
+
+  distributes : * DistributesOver + → (flip *) DistributesOver +
+  distributes distrib = Prod.swap distrib
+
 ------------------------------------------------------------------------
 -- Structures
 
 module _ {≈ : Rel A ℓ} {∙ : Op₂ A} where
 
-  isMagma : IsMagma ≈ ∙ → IsMagma ≈ (flip ∙)
+  open Def ≈
+  open Str ≈
+  open ∙-Properties ≈ ∙
+
+  isMagma : IsMagma ∙ → IsMagma (flip ∙)
   isMagma m = record
     { isEquivalence = isEquivalence
     ; ∙-cong        = preserves₂ ≈ ≈ ≈ ∙-cong
     }
     where open IsMagma m
 
-  isSelectiveMagma : IsSelectiveMagma ≈ ∙ → IsSelectiveMagma ≈ (flip ∙)
+  isSelectiveMagma : IsSelectiveMagma ∙ → IsSelectiveMagma (flip ∙)
   isSelectiveMagma m = record
     { isMagma = isMagma m.isMagma
-    ; sel     = selective ≈ ∙ m.sel
+    ; sel     = selective m.sel
     }
     where module m = IsSelectiveMagma m
 
-  isCommutativeMagma : IsCommutativeMagma ≈ ∙ → IsCommutativeMagma ≈ (flip ∙)
+  isCommutativeMagma : IsCommutativeMagma ∙ → IsCommutativeMagma (flip ∙)
   isCommutativeMagma m = record
     { isMagma = isMagma m.isMagma
-    ; comm    = commutative ≈ ∙ m.comm
+    ; comm    = commutative m.comm
     }
     where module m = IsCommutativeMagma m
 
-  isSemigroup : IsSemigroup ≈ ∙ → IsSemigroup ≈ (flip ∙)
+  isSemigroup : IsSemigroup ∙ → IsSemigroup (flip ∙)
   isSemigroup s = record
     { isMagma = isMagma s.isMagma
-    ; assoc   = associative ≈ ∙ s.sym s.assoc
+    ; assoc   = associative s.sym s.assoc
     }
     where module s = IsSemigroup s
 
-  isBand : IsBand ≈ ∙ → IsBand ≈ (flip ∙)
+  isBand : IsBand ∙ → IsBand (flip ∙)
   isBand b = record
     { isSemigroup = isSemigroup b.isSemigroup
     ; idem        = b.idem
     }
     where module b = IsBand b
 
-  isCommutativeSemigroup : IsCommutativeSemigroup ≈ ∙ →
-                           IsCommutativeSemigroup ≈ (flip ∙)
+  isCommutativeSemigroup : IsCommutativeSemigroup ∙ →
+                           IsCommutativeSemigroup (flip ∙)
   isCommutativeSemigroup s = record
     { isSemigroup = isSemigroup s.isSemigroup
-    ; comm        = commutative ≈ ∙ s.comm
+    ; comm        = commutative s.comm
     }
     where module s = IsCommutativeSemigroup s
 
-  isUnitalMagma : IsUnitalMagma ≈ ∙ ε → IsUnitalMagma ≈ (flip ∙) ε
+  isUnitalMagma : IsUnitalMagma ∙ ε → IsUnitalMagma (flip ∙) ε
   isUnitalMagma m = record
     { isMagma  = isMagma m.isMagma
-    ; identity = identity ≈ ∙ m.identity
+    ; identity = identity m.identity
     }
     where module m = IsUnitalMagma m
 
-  isMonoid : IsMonoid ≈ ∙ ε → IsMonoid ≈ (flip ∙) ε
+  isMonoid : IsMonoid ∙ ε → IsMonoid (flip ∙) ε
   isMonoid m = record
     { isSemigroup = isSemigroup m.isSemigroup
-    ; identity    = identity ≈ ∙ m.identity
+    ; identity    = identity m.identity
     }
     where module m = IsMonoid m
 
-  isCommutativeMonoid : IsCommutativeMonoid ≈ ∙ ε →
-                        IsCommutativeMonoid ≈ (flip ∙) ε
+  isCommutativeMonoid : IsCommutativeMonoid ∙ ε →
+                        IsCommutativeMonoid (flip ∙) ε
   isCommutativeMonoid m = record
     { isMonoid = isMonoid m.isMonoid
-    ; comm     = commutative ≈ ∙ m.comm
+    ; comm     = commutative m.comm
     }
     where module m = IsCommutativeMonoid m
 
-  isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid ≈ ∙ ε →
-                                  IsIdempotentCommutativeMonoid ≈ (flip ∙) ε
+  isIdempotentCommutativeMonoid : IsIdempotentCommutativeMonoid ∙ ε →
+                                  IsIdempotentCommutativeMonoid (flip ∙) ε
   isIdempotentCommutativeMonoid m = record
     { isCommutativeMonoid = isCommutativeMonoid m.isCommutativeMonoid
-    ; idem                = idempotent ≈ ∙ m.idem
+    ; idem                = idempotent m.idem
     }
     where module m = IsIdempotentCommutativeMonoid m
 
-  isInvertibleMagma : IsInvertibleMagma ≈ ∙ ε ⁻¹ →
-                      IsInvertibleMagma ≈ (flip ∙) ε ⁻¹
+  isInvertibleMagma : IsInvertibleMagma ∙ ε ⁻¹ →
+                      IsInvertibleMagma (flip ∙) ε ⁻¹
   isInvertibleMagma m = record
     { isMagma = isMagma m.isMagma
-    ; inverse = inverse ≈ ∙ m.inverse
+    ; inverse = inverse m.inverse
     ; ⁻¹-cong = m.⁻¹-cong
     }
     where module m = IsInvertibleMagma m
 
-  isInvertibleUnitalMagma : IsInvertibleUnitalMagma ≈ ∙ ε ⁻¹ →
-                            IsInvertibleUnitalMagma ≈ (flip ∙) ε ⁻¹
+  isInvertibleUnitalMagma : IsInvertibleUnitalMagma ∙ ε ⁻¹ →
+                            IsInvertibleUnitalMagma (flip ∙) ε ⁻¹
   isInvertibleUnitalMagma m = record
     { isInvertibleMagma = isInvertibleMagma m.isInvertibleMagma
-    ; identity          = identity ≈ ∙ m.identity
+    ; identity          = identity m.identity
     }
     where module m = IsInvertibleUnitalMagma m
 
-  isGroup : IsGroup ≈ ∙ ε ⁻¹ → IsGroup ≈ (flip ∙) ε ⁻¹
+  isGroup : IsGroup ∙ ε ⁻¹ → IsGroup (flip ∙) ε ⁻¹
   isGroup g = record
     { isMonoid = isMonoid g.isMonoid
-    ; inverse  = inverse ≈ ∙ g.inverse
+    ; inverse  = inverse g.inverse
     ; ⁻¹-cong  = g.⁻¹-cong
     }
     where module g = IsGroup g
 
-  isAbelianGroup : IsAbelianGroup ≈ ∙ ε ⁻¹ → IsAbelianGroup ≈ (flip ∙) ε ⁻¹
+  isAbelianGroup : IsAbelianGroup ∙ ε ⁻¹ → IsAbelianGroup (flip ∙) ε ⁻¹
   isAbelianGroup g = record
     { isGroup = isGroup g.isGroup
-    ; comm    = commutative ≈ ∙ g.comm
+    ; comm    = commutative g.comm
     }
     where module g = IsAbelianGroup g
 
+module _ {≈ : Rel A ℓ} {+ * : Op₂ A} { - : Op₁ A} {0# 1# : A} where
+
+  open Str ≈
+  open ∙-Properties ≈ *
+  open *-Properties ≈ * +
+
+  isRing : IsRing + * - 0# 1# → IsRing + (flip *) - 0# 1#
+  isRing r = record
+    { +-isAbelianGroup = r.+-isAbelianGroup
+    ; *-cong = preserves₂ ≈ ≈ ≈ r.*-cong
+    ; *-assoc = associative r.sym r.*-assoc
+    ; *-identity = identity r.*-identity
+    ; distrib = distributes r.distrib
+    ; zero = zero r.zero
+    }
+    where
+      module r = IsRing r
+
+
 ------------------------------------------------------------------------
 -- Bundles
 
@@ -239,3 +277,7 @@ group g = record { isGroup = isGroup g.isGroup }
 abelianGroup : AbelianGroup a ℓ → AbelianGroup a ℓ
 abelianGroup g = record { isAbelianGroup = isAbelianGroup g.isAbelianGroup }
   where module g = AbelianGroup g
+
+ring : Ring a ℓ → Ring a ℓ
+ring r = record { isRing = isRing r.isRing }
+  where module r = Ring r

src/Algebra/Construct/Initial.agda

@@ -0,0 +1,97 @@
+------------------------------------------------------------------------
+-- The Agda standard library
+--
+-- Instances of algebraic structures where the carrier is ⊥.
+-- In mathematics, this is usually called 0.
+--
+-- From monoids up, these are zero-objects – i.e, the initial
+-- object is the terminal object in the relevant category.
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+open import Level using (Level)
+
+module Algebra.Construct.Initial {c ℓ : Level} where
+
+open import Algebra.Bundles
+  using (Magma; Semigroup; Band)
+open import Algebra.Bundles.Raw
+  using (RawMagma)
+open import Algebra.Core using (Op₂)
+open import Algebra.Definitions using (Congruent₂)
+open import Algebra.Structures using (IsMagma; IsSemigroup; IsBand)
+open import Data.Empty.Polymorphic
+open import Relation.Binary using (Rel; Reflexive; Symmetric; Transitive; IsEquivalence)
+
+
+------------------------------------------------------------------------
+-- re-export those algebras which are also terminal
+
+open import Algebra.Construct.Terminal {c} {ℓ} public
+  hiding (rawMagma; magma; semigroup; band)
+
+------------------------------------------------------------------------
+-- gather all the functionality in one place
+
+private module ℤero where
+
+  infixl 7 _∙_
+  infix  4 _≈_
+
+  Carrier : Set c
+  Carrier = ⊥
+
+  _≈_     : Rel Carrier ℓ
+  _≈_ ()
+
+  _∙_     : Op₂ Carrier
+  _∙_ ()
+
+  refl : Reflexive _≈_
+  refl {x = ()}
+
+  sym : Symmetric _≈_
+  sym {x = ()}
+
+  trans : Transitive _≈_
+  trans {i = ()}
+
+  ∙-cong : Congruent₂ _≈_ _∙_
+  ∙-cong {x = ()}
+
+open ℤero
+
+------------------------------------------------------------------------
+-- Raw bundles
+
+rawMagma : RawMagma c ℓ
+rawMagma = record { Carrier = Carrier ; _≈_ = _≈_ ; _∙_ = _∙_ }
+
+------------------------------------------------------------------------
+-- Structures
+
+isEquivalence : IsEquivalence _≈_
+isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
+
+isMagma : IsMagma _≈_ _∙_
+isMagma = record { isEquivalence = isEquivalence ; ∙-cong = ∙-cong }
+
+isSemigroup : IsSemigroup _≈_ _∙_
+isSemigroup = record { isMagma = isMagma ; assoc = λ () }
+
+isBand : IsBand _≈_ _∙_
+isBand = record { isSemigroup = isSemigroup ; idem = λ () }
+
+------------------------------------------------------------------------
+-- Bundles
+
+magma : Magma c ℓ
+magma = record { isMagma = isMagma }
+
+semigroup : Semigroup c ℓ
+semigroup = record { isSemigroup = isSemigroup }
+
+band : Band c ℓ
+band = record { isBand = isBand }
+