Try new definition for equivalences

Author: Taneb

src/Algebra/Construct/Quotient/Group.agda

@@ -29,31 +29,26 @@ open NormalSubgroup N
 infix 0 _by_
 
 data _≋_ (x y : Carrier) : Set (c ⊔ ℓ ⊔ c′) where
-  _by_ : ∀ g → x // y ≈ ι g → x ≋ y
+  _by_ : ∀ g → ι g ∙ x ≈ y → x ≋ y
 
 ≋-refl : Reflexive _≋_
-≋-refl {x} = N.ε by begin
-  x // x ≈⟨ inverseʳ x ⟩
-  ε      ≈⟨ ι.ε-homo ⟨
-  ι N.ε  ∎
+≋-refl {x} = N.ε by trans (∙-congʳ ι.ε-homo) (identityˡ x)
 
 ≋-sym : Symmetric _≋_
-≋-sym {x} {y} (g by x//y≈ιg) = g N.⁻¹ by begin
-  y // x      ≈⟨ ⁻¹-anti-homo-// x y ⟨
-  (x // y) ⁻¹ ≈⟨ ⁻¹-cong x//y≈ιg ⟩
-  ι g ⁻¹      ≈⟨ ι.⁻¹-homo g ⟨
-  ι (g N.⁻¹)  ∎
-
+≋-sym {x} {y} (g by ιg∙x≈y) = g N.⁻¹ by begin
+  ι (g N.⁻¹) ∙ y      ≈⟨ ∙-cong (ι.⁻¹-homo g) (sym ιg∙x≈y) ⟩
+  ι g ⁻¹ ∙ (ι g ∙ x)  ≈⟨ assoc (ι g ⁻¹) (ι g) x ⟨
+  (ι g ⁻¹  ∙ ι g) ∙ x ≈⟨ ∙-congʳ (inverseˡ (ι g)) ⟩
+  ε ∙ x               ≈⟨ identityˡ x ⟩
+  x                   ∎
 
 ≋-trans : Transitive _≋_
-≋-trans {x} {y} {z} (g by x//y≈ιg) (h by y//z≈ιh) = g N.∙ h by begin
-  x // z              ≈⟨ ∙-congʳ (identityʳ x) ⟨
-  x ∙ ε // z          ≈⟨ ∙-congʳ (∙-congˡ (inverseˡ y)) ⟨
-  x ∙ (y \\ y) // z   ≈⟨ ∙-congʳ (assoc x (y ⁻¹) y) ⟨
-  (x // y) ∙ y // z   ≈⟨ assoc (x // y) y (z ⁻¹) ⟩
-  (x // y) ∙ (y // z) ≈⟨ ∙-cong x//y≈ιg y//z≈ιh ⟩
-  ι g ∙ ι h           ≈⟨ ι.∙-homo g h ⟨
-  ι (g N.∙ h)         ∎
+≋-trans {x} {y} {z} (g by ιg∙x) (h by ιh∙y) = h N.∙ g by begin
+  ι (h N.∙ g) ∙ x ≈⟨ ∙-congʳ (ι.∙-homo h g) ⟩
+  (ι h ∙ ι g) ∙ x ≈⟨ assoc (ι h) (ι g) x ⟩
+  ι h ∙ (ι g ∙ x) ≈⟨ ∙-congˡ ιg∙x ⟩
+  ι h ∙ y         ≈⟨ ιh∙y ⟩
+  z               ∎
 
 ≋-isEquivalence : IsEquivalence _≋_
 ≋-isEquivalence = record
@@ -63,38 +58,39 @@ data _≋_ (x y : Carrier) : Set (c ⊔ ℓ ⊔ c′) where
   }
 
 ≈⇒≋ : _≈_ ⇒ _≋_
-≈⇒≋ {x} {y} x≈y = N.ε by begin
-  x // y ≈⟨ x≈y⇒x∙y⁻¹≈ε x≈y ⟩
-  ε      ≈⟨ ι.ε-homo ⟨
-  ι N.ε  ∎
+≈⇒≋ {x} {y} x≈y = N.ε by trans (∙-cong ι.ε-homo x≈y) (identityˡ y)
 
 open AlgDefs _≋_
 
 ≋-∙-cong : Congruent₂ _∙_
-≋-∙-cong {x} {y} {u} {v} (g by x//y≈ιg) (h by u//v≈ιh) = g N.∙ normal h y .proj₁ by begin
-  x ∙ u // y ∙ v              ≈⟨ ∙-congˡ (⁻¹-anti-homo-∙ y v) ⟩
-  x ∙ u ∙ (v ⁻¹ ∙ y ⁻¹)       ≈⟨ assoc (x ∙ u) (v ⁻¹) (y ⁻¹) ⟨
-  (x ∙ u // v) // y           ≈⟨ ∙-congʳ (assoc x u (v ⁻¹)) ⟩
-  x ∙ (u // v) // y           ≈⟨ ∙-congʳ (∙-congˡ u//v≈ιh) ⟩
-  x ∙ ι h // y                ≈⟨ ∙-congʳ (∙-congˡ (identityˡ (ι h))) ⟨
-  x ∙ (ε ∙ ι h) // y          ≈⟨ ∙-congʳ (∙-congˡ (∙-congʳ (inverseˡ y))) ⟨
-  x ∙ ((y \\ y) ∙ ι h) // y   ≈⟨ ∙-congʳ (∙-congˡ (assoc (y ⁻¹) y (ι h))) ⟩
-  x ∙ (y \\ y ∙ ι h) // y     ≈⟨ ∙-congʳ (assoc x (y ⁻¹) (y ∙ ι h)) ⟨
-  (x // y) ∙ (y ∙ ι h) // y   ≈⟨ assoc (x // y) (y ∙ ι h) (y ⁻¹) ⟩
-  (x // y) ∙ (y ∙ ι h // y)   ≈⟨ ∙-cong x//y≈ιg (proj₂ (normal h y)) ⟩
-  ι g ∙ ι (normal h y .proj₁) ≈⟨ ι.∙-homo g (normal h y .proj₁) ⟨
-  ι (g N.∙ normal h y .proj₁) ∎
+≋-∙-cong {x} {y} {u} {v} (g by ιg∙x≈y) (h by ιh∙u≈v) = g N.∙ h′ by begin
+  ι (g N.∙ h′) ∙ (x ∙ u) ≈⟨ ∙-congʳ (ι.∙-homo g h′) ⟩
+  (ι g ∙ ι h′) ∙ (x ∙ u) ≈⟨ assoc (ι g) (ι h′) (x ∙ u) ⟩
+  ι g ∙ (ι h′ ∙ (x ∙ u)) ≈⟨ ∙-congˡ (assoc (ι h′) x u) ⟨
+  ι g ∙ ((ι h′ ∙ x) ∙ u) ≈⟨ ∙-congˡ (∙-congʳ x∙ιh≈ιh′∙x) ⟨
+  ι g ∙ ((x ∙ ι h) ∙ u)  ≈⟨ ∙-congˡ (assoc x (ι h) u) ⟩
+  ι g ∙ (x ∙ (ι h ∙ u))  ≈⟨ assoc (ι g) x (ι h ∙ u) ⟨
+  (ι g ∙ x) ∙ (ι h ∙ u)  ≈⟨ ∙-cong ιg∙x≈y ιh∙u≈v ⟩
+  y ∙ v                  ∎
+  where
+    h′ : N.Carrier
+    h′ = normal h x .proj₁
+    x∙ιh≈ιh′∙x : x ∙ ι h ≈ ι h′ ∙ x
+    x∙ιh≈ιh′∙x = normal h x .proj₂
+
 
 ≋-⁻¹-cong : Congruent₁ _⁻¹
-≋-⁻¹-cong {x} {y} (g by x//y≈ιg) = normal (g N.⁻¹) (y ⁻¹) .proj₁ by begin
-  x ⁻¹ ∙ y ⁻¹ ⁻¹                      ≈⟨ ∙-congʳ (identityˡ (x ⁻¹)) ⟨
-  (ε ∙ x ⁻¹) ∙ y ⁻¹ ⁻¹                ≈⟨ ∙-congʳ (∙-congʳ (inverseʳ (y ⁻¹))) ⟨
-  ((y ⁻¹ ∙ y ⁻¹ ⁻¹) ∙ x ⁻¹) ∙ y ⁻¹ ⁻¹ ≈⟨ ∙-congʳ (assoc (y ⁻¹) ((y ⁻¹) ⁻¹) (x ⁻¹)) ⟩
-  y ⁻¹ ∙ (y ⁻¹ ⁻¹ ∙ x ⁻¹) ∙ y ⁻¹ ⁻¹   ≈⟨ ∙-congʳ (∙-congˡ (⁻¹-anti-homo-∙ x (y ⁻¹))) ⟨
-  y ⁻¹ ∙ (x ∙ y ⁻¹) ⁻¹ ∙ y ⁻¹ ⁻¹      ≈⟨ ∙-congʳ (∙-congˡ (⁻¹-cong x//y≈ιg)) ⟩
-  y ⁻¹ ∙ ι g ⁻¹ ∙ y ⁻¹ ⁻¹             ≈⟨ ∙-congʳ (∙-congˡ (ι.⁻¹-homo g)) ⟨
-  y ⁻¹ ∙ ι (g N.⁻¹) ∙ y ⁻¹ ⁻¹         ≈⟨ proj₂ (normal (g N.⁻¹) (y ⁻¹)) ⟩
-  ι (normal (g N.⁻¹) (y ⁻¹) .proj₁)   ∎
+≋-⁻¹-cong {x} {y} (g by ιg∙x≈y) = g′ by begin
+  ι g′ ∙ x ⁻¹       ≈⟨ x⁻¹∙ιg⁻¹≈ιg′∙x⁻¹ ⟨
+  x ⁻¹ ∙ ι (g N.⁻¹) ≈⟨ ∙-congˡ (ι.⁻¹-homo g) ⟩
+  x ⁻¹ ∙ ι g ⁻¹     ≈⟨ ⁻¹-anti-homo-∙ (ι g) x ⟨
+  (ι g ∙ x) ⁻¹      ≈⟨ ⁻¹-cong ιg∙x≈y ⟩
+  y ⁻¹              ∎
+  where
+    g′ : N.Carrier
+    g′ = normal (g N.⁻¹) (x ⁻¹) .proj₁
+    x⁻¹∙ιg⁻¹≈ιg′∙x⁻¹ : x ⁻¹ ∙ ι (g N.⁻¹) ≈ ι g′ ∙ x ⁻¹
+    x⁻¹∙ιg⁻¹≈ιg′∙x⁻¹ = normal (g N.⁻¹) (x ⁻¹) .proj₂
 
 quotientIsGroup : IsGroup _≋_ _∙_ ε _⁻¹
 quotientIsGroup = record

src/Algebra/Construct/Quotient/Ring.agda

@@ -19,22 +19,20 @@ open import Algebra.Construct.Quotient.Group +-group normalSubgroup public
   renaming (≋-∙-cong to ≋-+-cong; ≋-⁻¹-cong to ≋‿-‿cong)
 
 open import Algebra.Definitions _≋_
+open import Algebra.Properties.Semiring semiring
 open import Algebra.Properties.Ring R
 open import Algebra.Structures
 open import Level
 open import Relation.Binary.Reasoning.Setoid setoid
 
 ≋-*-cong : Congruent₂ _*_
-≋-*-cong {x} {y} {u} {v} (j by x-y≈ιj) (k by u-v≈ιk) = j I.*ᵣ u I.+ᴹ y I.*ₗ k by begin
-    x * u - y * v                       ≈⟨ +-congʳ (+-identityʳ (x * u)) ⟨
-    x * u + 0# - y * v                  ≈⟨ +-congʳ (+-congˡ (-‿inverseˡ (y * u))) ⟨
-    x * u + (- (y * u) + y * u) - y * v ≈⟨ +-congʳ (+-assoc (x * u) (- (y * u)) (y * u)) ⟨
-    ((x * u - y * u) + y * u) - y * v   ≈⟨ +-assoc (x * u - y * u) (y * u) (- (y * v)) ⟩
-    (x * u - y * u) + (y * u - y * v)   ≈⟨ +-cong ([y-z]x≈yx-zx u x y) (x[y-z]≈xy-xz y u v) ⟨
-    (x - y) * u + y * (u - v)           ≈⟨ +-cong (*-congʳ x-y≈ιj) (*-congˡ u-v≈ιk) ⟩
-    ι j * u + y * ι k                   ≈⟨ +-cong (ι.*ᵣ-homo u j) (ι.*ₗ-homo y k) ⟨
-    ι (j I.*ᵣ u) + ι (y I.*ₗ k)         ≈⟨ ι.+ᴹ-homo (j I.*ᵣ u) (y I.*ₗ k) ⟨
-    ι (j I.*ᵣ u I.+ᴹ y I.*ₗ k)          ∎
+≋-*-cong {x} {y} {u} {v} (j by ιj+x≈y) (k by ιk+u≈v) = ι j I.*ₗ k I.+ᴹ j I.*ᵣ u I.+ᴹ x I.*ₗ k by begin
+  ι (ι j I.*ₗ k I.+ᴹ j I.*ᵣ u I.+ᴹ x I.*ₗ k) + x * u   ≈⟨ +-congʳ (ι.+ᴹ-homo (ι j I.*ₗ k I.+ᴹ j I.*ᵣ u) (x I.*ₗ k)) ⟩
+  ι (ι j I.*ₗ k I.+ᴹ j I.*ᵣ u) + ι (x I.*ₗ k) + x * u  ≈⟨ +-congʳ (+-congʳ (ι.+ᴹ-homo (ι j I.*ₗ k) (j I.*ᵣ u))) ⟩
+  ι (ι j I.*ₗ k) + ι (j I.*ᵣ u) + ι (x I.*ₗ k) + x * u ≈⟨ +-congʳ (+-cong (+-cong (ι.*ₗ-homo (ι j) k) (ι.*ᵣ-homo u j)) (ι.*ₗ-homo x k)) ⟩
+  ι j * ι k + ι j * u + x * ι k + x * u                ≈⟨ binomial-expansion (ι j) x (ι k) u ⟨
+  (ι j + x) * (ι k + u)                                ≈⟨ *-cong ιj+x≈y ιk+u≈v ⟩
+  y * v                                                ∎
 
 quotientRawRing : RawRing c (c ⊔ ℓ ⊔ c′)
 quotientRawRing = record

src/Algebra/Ideal.agda

@@ -36,12 +36,7 @@ record Ideal c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
     ; ι-monomorphism = ι.+ᴹ-isGroupMonomorphism
     ; normal = λ n g → record
       { fst = n
-      ; snd = begin
-        g + ι n - g     ≈⟨ +-assoc g (ι n) (- g) ⟩
-        g + (ι n - g)   ≈⟨ +-congˡ (+-comm (ι n) (- g)) ⟩
-        g + (- g + ι n) ≈⟨ +-assoc g (- g) (ι n) ⟨
-        g - g + ι n     ≈⟨ +-congʳ (-‿inverseʳ g) ⟩
-        0# + ι n        ≈⟨ +-identityˡ (ι n) ⟩
-        ι n             ∎
+      -- this ends up a lot simpler now
+      ; snd = +-comm g (ι n)
       }
     }

src/Algebra/NormalSubgroup.agda

@@ -25,7 +25,7 @@ record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) wh
     ι : RawGroup.Carrier N → Carrier
     ι-monomorphism : IsGroupMonomorphism N rawGroup ι
     -- every element of N commutes in G
-    normal : ∀ n g → ∃[ n′ ] g ∙ ι n ∙ g ⁻¹ ≈ ι n′
+    normal : ∀ n g → ∃[ n′ ] g ∙ ι n ≈ ι n′ ∙ g
 
   module N = RawGroup N
   module ι = IsGroupMonomorphism ι-monomorphism

src/Data/Integer/ModularArithmetic.agda

@@ -38,17 +38,8 @@ module _ .{{_ : NonZero m}} where
 
   from-% : ∀ {x y} → x % m ≡ y % m → x ≋ y
   from-% {x} {y} x%m≡y%m = x / m - y / m by begin
-    x - y                                                   ≡⟨ ≡.cong₂ _-_ (a≡a%n+[a/n]*n x m) (a≡a%n+[a/n]*n y m) ⟩
-    (+ (x % m) + (x / m) * m) - (+ (y % m) + (y / m) * m)   ≡⟨ ≡.cong (λ z → (+ (x % m) + (x / m) * m) + z) (neg-distrib-+ (+ (y % m)) ((y / m) * m)) ⟩
-    (+ (x % m) + (x / m) * m) + (- + (y % m) - (y / m) * m) ≡⟨ +-assoc (+ (x % m) + (x / m) * m) (- + (y % m)) (- ((y / m) * m)) ⟨
-    ((+ (x % m) + (x / m) * m) - + (y % m)) - (y / m) * m   ≡⟨ ≡.cong (λ z → z - (y / m) * m) (+-assoc (+ (x % m)) ((x / m) * m) (- + (y % m))) ⟩
-    (+ (x % m) + ((x / m) * m - + (y % m))) - (y / m) * m   ≡⟨ ≡.cong (λ z → (+ (x % m) + z) - (y / m) * m) (+-comm ((x / m) * m) (- + (y % m))) ⟩
-    (+ (x % m) + (- + (y % m) + (x / m) * m)) - (y / m) * m ≡⟨ ≡.cong (λ z → z - (y / m) * m) (+-assoc (+ (x % m)) (- + (y % m)) ((x / m) * m)) ⟨
-    ((+ (x % m) - + (y % m)) + (x / m) * m) - (y / m) * m   ≡⟨ +-assoc (+ (x % m) - + (y % m)) ((x / m) * m) (- ((y / m) * m)) ⟩
-    (+ (x % m) - + (y % m)) + ((x / m) * m - (y / m) * m)   ≡⟨ ≡.cong₂ (λ a b → (+ a - + (y % m)) + ((x / m) * m + b)) x%m≡y%m (neg-distribˡ-* (y / m) m) ⟩
-    (+ (y % m) - + (y % m)) + ((x / m) * m + - (y / m) * m) ≡⟨ ≡.cong₂ _+_ (+-inverseʳ (+ (y % m))) (≡.sym (*-distribʳ-+ m (x / m) (- (y / m)))) ⟩
-    0ℤ + (x / m - y / m) * m                                ≡⟨ +-identityˡ ((x / m - y / m) * m) ⟩
-    (x / m - y / m) * m                                     ∎
+    (x / m - y / m) * m + x ≡⟨ {!!} ⟩
+    y                       ∎
     where open ≡-Reasoning
 
   to-% : ∀ {x y} → x ≋ y → x % m ≡ y % m
@@ -91,6 +82,3 @@ _≋?_ : Decidable _≋_
 _≋?_ with ℕ.nonZero? ∣ m ∣
 ... | yes p = _≋?′_ {{p}}
 ... | no ¬p = {!!}
-
-
-