lemmas about semiring structure induced by _× x (#2272)

* tidying up proofs of, and using, semiring structure induced by `_× x`

* reinstated lemma about `0#`

* fixed name clash

* added companion lemma for `1#`

* new lemma, plus refactoring

* removed anonymous `module`

* don't inline use  of the lemma

* revised deprecation warning

CHANGELOG.md

@@ -33,6 +33,11 @@ Deprecated modules
 Deprecated names
 ----------------
 
+* In `Algebra.Properties.Semiring.Mult`:
+  ```agda
+  1×-identityʳ  ↦  ×-homo-1
+  ```
+
 * In `Data.Nat.Divisibility.Core`:
   ```agda
   *-pres-∣  ↦  Data.Nat.Divisibility.*-pres-∣
@@ -90,6 +95,19 @@ Additions to existing modules
   rawModule          : RawModule R c ℓ
   ```
 
+* In `Algebra.Properties.Monoid.Mult`:
+  ```agda
+  ×-homo-0 : ∀ x → 0 × x ≈ 0#
+  ×-homo-1 : ∀ x → 1 × x ≈ x
+  ```
+
+* In `Algebra.Properties.Semiring.Mult`:
+  ```agda
+  ×-homo-0#     : ∀ x → 0 × x ≈ 0# * x
+  ×-homo-1#     : ∀ x → 1 × x ≈ 1# * x
+  idem-×-homo-* : (_*_ IdempotentOn x) → (m × x) * (n × x) ≈ (m ℕ.* n) × x
+  ```
+
 * In `Data.Fin.Properties`:
   ```agda
   nonZeroIndex : Fin n → ℕ.NonZero n

src/Algebra/Properties/Monoid/Mult.agda

@@ -51,6 +51,12 @@ open import Algebra.Definitions.RawMonoid rawMonoid public
 
 -- _×_ is homomorphic with respect to _ℕ+_/_+_.
 
+×-homo-0 : ∀ x → 0 × x ≈ 0#
+×-homo-0 x = refl
+
+×-homo-1 : ∀ x → 1 × x ≈ x
+×-homo-1 = +-identityʳ
+
 ×-homo-+ : ∀ x m n → (m ℕ.+ n) × x ≈ m × x + n × x
 ×-homo-+ x 0       n = sym (+-identityˡ (n × x))
 ×-homo-+ x (suc m) n = begin

src/Algebra/Properties/Semiring/Binomial.agda

@@ -216,7 +216,7 @@ term₁+term₂≈term x*y≈y*x n (suc i) with view i
 theorem : x * y ≈ y * x → ∀ n → (x + y) ^ n ≈ binomialExpansion n
 theorem x*y≈y*x zero    = begin
   (x + y) ^ 0                     ≡⟨⟩
-  1#                              ≈⟨ 1×-identityʳ 1# ⟨
+  1#                              ≈⟨ ×-homo-1 1# ⟨
   1 × 1#                          ≈⟨ *-identityʳ (1 × 1#) ⟨
   (1 × 1#) * 1#                   ≈⟨ ×-assoc-* 1 1# 1# ⟩
   1 × (1# * 1#)                   ≡⟨⟩

src/Algebra/Properties/Semiring/Mult.agda

@@ -6,14 +6,15 @@
 
 {-# OPTIONS --cubical-compatible --safe #-}
 
-open import Algebra
+open import Algebra.Bundles using (Semiring)
 open import Data.Nat.Base as ℕ using (zero; suc)
 
 module Algebra.Properties.Semiring.Mult
   {a ℓ} (S : Semiring a ℓ) where
 
 open Semiring S renaming (zero to *-zero)
 open import Relation.Binary.Reasoning.Setoid setoid
+open import Algebra.Definitions _≈_ using (_IdempotentOn_)
 
 ------------------------------------------------------------------------
 -- Re-export definition from the monoid
@@ -23,21 +24,15 @@ open import Algebra.Properties.Monoid.Mult +-monoid public
 ------------------------------------------------------------------------
 -- Properties of _×_
 
--- (_× 1#) is homomorphic with respect to _ℕ.*_/_*_.
+-- (0 ×_) is (0# *_)
 
-×1-homo-* : ∀ m n → (m ℕ.* n) × 1# ≈ (m × 1#) * (n × 1#)
-×1-homo-* 0       n = sym (zeroˡ (n × 1#))
-×1-homo-* (suc m) n = begin
-  (n ℕ.+ m ℕ.* n) × 1#                ≈⟨  ×-homo-+ 1# n (m ℕ.* n) ⟩
-  n × 1# + (m ℕ.* n) × 1#             ≈⟨  +-congˡ (×1-homo-* m n) ⟩
-  n × 1# + (m × 1#) * (n × 1#)        ≈⟨ +-congʳ (*-identityˡ _) ⟨
-  1# * (n × 1#) + (m × 1#) * (n × 1#) ≈⟨ distribʳ (n × 1#) 1# (m × 1#) ⟨
-  (1# + m × 1#) * (n × 1#)            ∎
+×-homo-0# : ∀ x → 0 × x ≈ 0# * x
+×-homo-0# x = sym (zeroˡ x)
 
--- (1 ×_) is the identity
+-- (1 ×_) is (1# *_)
 
-1×-identityʳ : ∀ x → 1 × x ≈ x
-1×-identityʳ = +-identityʳ
+×-homo-1# : ∀ x → 1 × x ≈ 1# * x
+×-homo-1# x = trans (×-homo-1 x) (sym (*-identityˡ x))
 
 -- (n ×_) commutes with _*_
 
@@ -60,3 +55,32 @@ open import Algebra.Properties.Monoid.Mult +-monoid public
   x * y + (n × x) * y   ≈⟨ +-congˡ (×-assoc-* n _ _) ⟩
   x * y + n × (x * y)   ≡⟨⟩
   suc n × (x * y)       ∎
+
+-- (_× x) is homomorphic with respect to _ℕ.*_/_*_ for idempotent x.
+
+idem-×-homo-* : ∀ m n {x} → (_*_ IdempotentOn x) → (m × x) * (n × x) ≈ (m ℕ.* n) × x
+idem-×-homo-* m n {x} idem = begin
+  (m × x) * (n × x)   ≈⟨ ×-assoc-* m x (n × x) ⟩
+  m × (x * (n × x))   ≈⟨ ×-congʳ m (×-comm-* n x x) ⟩
+  m × (n × (x * x))   ≈⟨ ×-assocˡ _ m n ⟩
+  (m ℕ.* n) × (x * x) ≈⟨ ×-congʳ (m ℕ.* n) idem ⟩
+  (m ℕ.* n) × x       ∎
+
+-- (_× 1#) is homomorphic with respect to _ℕ.*_/_*_.
+
+×1-homo-* : ∀ m n → (m ℕ.* n) × 1# ≈ (m × 1#) * (n × 1#)
+×1-homo-* m n = sym (idem-×-homo-* m n (*-identityʳ 1#))
+
+------------------------------------------------------------------------
+-- DEPRECATED NAMES
+------------------------------------------------------------------------
+-- Please use the new names as continuing support for the old names is
+-- not guaranteed.
+
+-- Version 2.1
+
+1×-identityʳ = ×-homo-1
+{-# WARNING_ON_USAGE 1×-identityʳ
+"Warning: 1×-identityʳ was deprecated in v2.1.
+Please use ×-homo-1 instead. "
+#-}