refactor: simplify Quotients

Author: jamesmckinna

src/Algebra/Construct/Quotient/AbelianGroup.agda

@@ -8,6 +8,7 @@
 
 open import Algebra.Bundles using (Group; AbelianGroup)
 import Algebra.Construct.Sub.AbelianGroup as AbelianSubgroup
+import Algebra.Construct.Quotient.Group as Quotient
 
 module Algebra.Construct.Quotient.AbelianGroup
   {c ℓ} (G : AbelianGroup c ℓ)
@@ -20,16 +21,19 @@ private
 
 -- Re-export the quotient group
 
-open import Algebra.Construct.Quotient.Group G.group (normalSubgroup N) public
+open Quotient G.group (normalSubgroup N) public
+  hiding (_/_)
 
 -- With its additional bundle
 
-quotientAbelianGroup : AbelianGroup c _
-quotientAbelianGroup = record
+abelianGroup : AbelianGroup c _
+abelianGroup = record
   { isAbelianGroup = record
     { isGroup = isGroup
     ; comm = λ g h → ≈⇒≋ (G.comm g h)
     }
-  } where open Group quotientGroup
+  } where open Group group
 
--- Public re-exports, as needed?
+-- Public re-exports
+
+_/_ = abelianGroup

src/Algebra/Construct/Quotient/Group.agda

@@ -13,8 +13,7 @@ module Algebra.Construct.Quotient.Group
   {c ℓ} (G : Group c ℓ) {c′ ℓ′} (N : NormalSubgroup G c′ ℓ′) where
 
 open import Algebra.Definitions using (Congruent₁; Congruent₂)
-open import Algebra.Morphism.Structures
-  using (IsMagmaHomomorphism; IsMonoidHomomorphism; IsGroupHomomorphism)
+open import Algebra.Morphism.Structures using (IsGroupHomomorphism)
 open import Data.Product.Base using (_,_)
 open import Function.Base using (_∘_)
 open import Function.Definitions using (Surjective)
@@ -24,103 +23,106 @@ open import Relation.Binary.Definitions using (Reflexive; Symmetric; Transitive)
 
 private
   open module G = Group G
-
-open import Algebra.Properties.Group G using (⁻¹-anti-homo-∙)
-open import Algebra.Properties.Monoid monoid
-open import Relation.Binary.Reasoning.Setoid setoid
-
-private
+    using (_≈_; _∙_; ε; _⁻¹)
   open module N = NormalSubgroup N
     using (ι; module ι; conjugate; normal)
 
+open import Algebra.Properties.Group G using (⁻¹-anti-homo-∙)
+open import Algebra.Properties.Monoid G.monoid
+open import Relation.Binary.Reasoning.Setoid G.setoid
+
 infix 0 _by_
 
-data _≋_ (x y : Carrier) : Set (c ⊔ ℓ ⊔ c′) where
+data _≋_ (x y : G.Carrier) : Set (c ⊔ ℓ ⊔ c′) where
   _by_ : ∀ g → ι g ∙ x ≈ y → x ≋ y
 
 ≈⇒≋ : _≈_ ⇒ _≋_
-≈⇒≋ x≈y = N.ε by trans (∙-cong ι.ε-homo x≈y) (identityˡ _)
+≈⇒≋ x≈y = N.ε by G.trans (G.∙-cong ι.ε-homo x≈y) (G.identityˡ _)
 
-≋-refl : Reflexive _≋_
-≋-refl = ≈⇒≋ refl
+refl : Reflexive _≋_
+refl = ≈⇒≋ G.refl
 
-≋-sym : Symmetric _≋_
-≋-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)  ≈⟨ cancelˡ (inverseˡ (ι g)) x ⟩
+sym : Symmetric _≋_
+sym {x} {y} (g by ιg∙x≈y) = g N.⁻¹ by begin
+  ι (g N.⁻¹) ∙ y      ≈⟨ G.∙-cong (ι.⁻¹-homo g) (G.sym ιg∙x≈y) ⟩
+  ι g ⁻¹ ∙ (ι g ∙ x)  ≈⟨ cancelˡ (G.inverseˡ (ι g)) x ⟩
   x                   ∎
 
-≋-trans : Transitive _≋_
-≋-trans {x} {y} {z} (g by ιg∙x≈y) (h by ιh∙y≈z) = h N.∙ g by begin
-  ι (h N.∙ g) ∙ x ≈⟨ ∙-congʳ (ι.∙-homo h g) ⟩
+trans : Transitive _≋_
+trans {x} {y} {z} (g by ιg∙x≈y) (h by ιh∙y≈z) = h N.∙ g by begin
+  ι (h N.∙ g) ∙ x ≈⟨ G.∙-congʳ (ι.∙-homo h g) ⟩
   (ι h ∙ ι g) ∙ x ≈⟨ uv≈w⇒xu∙v≈xw ιg∙x≈y (ι h) ⟩
   ι h ∙ y         ≈⟨ ιh∙y≈z ⟩
   z               ∎
 
-≋-∙-cong : Congruent₂ _≋_ _∙_
-≋-∙-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′) ⟩
+∙-cong : Congruent₂ _≋_ _∙_
+∙-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) ≈⟨ G.∙-congʳ (ι.∙-homo g h′) ⟩
   (ι g ∙ ι h′) ∙ (x ∙ u) ≈⟨ uv≈wx⇒yu∙vz≈yw∙xz (normal h x) (ι g) u ⟩
-  (ι g ∙ x) ∙ (ι h ∙ u)  ≈⟨ ∙-cong ιg∙x≈y ιh∙u≈v ⟩
+  (ι g ∙ x) ∙ (ι h ∙ u)  ≈⟨ G.∙-cong ιg∙x≈y ιh∙u≈v ⟩
   y ∙ v                  ∎
   where h′ = conjugate h x
 
-≋-⁻¹-cong : Congruent₁ _≋_ _⁻¹
-≋-⁻¹-cong {x} {y} (g by ιg∙x≈y) = h by begin
+⁻¹-cong : Congruent₁ _≋_ _⁻¹
+⁻¹-cong {x} {y} (g by ιg∙x≈y) = h by begin
   ι h ∙ x ⁻¹        ≈⟨ normal (g N.⁻¹) (x ⁻¹) ⟩
-  x ⁻¹ ∙ ι (g N.⁻¹) ≈⟨ ∙-congˡ (ι.⁻¹-homo g) ⟩
+  x ⁻¹ ∙ ι (g N.⁻¹) ≈⟨ G.∙-congˡ (ι.⁻¹-homo g) ⟩
   x ⁻¹ ∙ ι g ⁻¹     ≈⟨ ⁻¹-anti-homo-∙ (ι g) x ⟨
-  (ι g ∙ x) ⁻¹      ≈⟨ ⁻¹-cong ιg∙x≈y ⟩
+  (ι g ∙ x) ⁻¹      ≈⟨ G.⁻¹-cong ιg∙x≈y ⟩
   y ⁻¹              ∎
   where h = conjugate (g N.⁻¹) (x ⁻¹)
 
-quotientGroup : Group c (c ⊔ ℓ ⊔ c′)
-quotientGroup = record
+group : Group c (c ⊔ ℓ ⊔ c′)
+group = record
   { isGroup = record
     { isMonoid = record
       { isSemigroup = record
         { isMagma = record
           { isEquivalence = record
-            { refl = ≋-refl
-            ; sym = ≋-sym
-            ; trans = ≋-trans
+            { refl = refl
+            ; sym = sym
+            ; trans = trans
             }
-          ; ∙-cong = ≋-∙-cong
+          ; ∙-cong = ∙-cong
           }
-        ; assoc = λ x y z → ≈⇒≋ (assoc x y z)
+        ; assoc = λ x y z → ≈⇒≋ (G.assoc x y z)
         }
-      ; identity = ≈⇒≋ ∘ identityˡ , ≈⇒≋ ∘ identityʳ
+      ; identity = ≈⇒≋ ∘ G.identityˡ , ≈⇒≋ ∘ G.identityʳ
       }
-    ; inverse = ≈⇒≋ ∘ inverseˡ , ≈⇒≋ ∘ inverseʳ
-    ; ⁻¹-cong = ≋-⁻¹-cong
+    ; inverse = ≈⇒≋ ∘ G.inverseˡ , ≈⇒≋ ∘ G.inverseʳ
+    ; ⁻¹-cong = ⁻¹-cong
     }
   }
 
-_/_ : Group c (c ⊔ ℓ ⊔ c′)
-_/_ = quotientGroup
+private module Q = Group group
 
-π : Group.Carrier G → Group.Carrier quotientGroup
-π x = x -- because we do all the work in the relation
+-- Public re-exports
 
-π-isMagmaHomomorphism : IsMagmaHomomorphism rawMagma (Group.rawMagma quotientGroup) π
-π-isMagmaHomomorphism = record
-  { isRelHomomorphism = record
-    { cong = ≈⇒≋
-    }
-  ; homo = λ _ _ → ≋-refl
-  }
+_/_ : Group c (c ⊔ ℓ ⊔ c′)
+_/_ = group
 
-π-isMonoidHomomorphism : IsMonoidHomomorphism rawMonoid (Group.rawMonoid quotientGroup) π
-π-isMonoidHomomorphism = record
-  { isMagmaHomomorphism = π-isMagmaHomomorphism
-  ; ε-homo = ≋-refl
-  }
+π : G.Carrier → Q.Carrier
+π x = x -- because we do all the work in the relation _≋_
 
-π-isGroupHomomorphism : IsGroupHomomorphism rawGroup (Group.rawGroup quotientGroup) π
+π-surjective : Surjective _≈_ _≋_ π
+π-surjective g = g , ≈⇒≋
+
+π-isGroupHomomorphism : IsGroupHomomorphism G.rawGroup Q.rawGroup π
 π-isGroupHomomorphism = record
-  { isMonoidHomomorphism = π-isMonoidHomomorphism
-  ; ⁻¹-homo = λ _ → ≋-refl
+  { isMonoidHomomorphism = record
+    { isMagmaHomomorphism = record
+      { isRelHomomorphism = record
+        { cong = ≈⇒≋
+        }
+      ; homo = λ _ _ → refl
+      }
+    ; ε-homo = refl
+    }
+  ; ⁻¹-homo = λ _ → refl
   }
 
-π-surjective : Surjective _≈_ _≋_ π
-π-surjective g = g , ≈⇒≋
+open IsGroupHomomorphism π-isGroupHomomorphism public
+  using ()
+  renaming (isMonoidHomomorphism to π-isMonoidHomomorphism
+           ; isMagmaHomomorphism to π-isMagmaHomomorphism
+           )

src/Algebra/Construct/Quotient/Ring.agda

@@ -6,71 +6,72 @@
 
 {-# OPTIONS --safe --cubical-compatible #-}
 
-open import Algebra.Bundles using (AbelianGroup; Ring; RawRing)
+open import Algebra.Bundles using (AbelianGroup; Ring)
 open import Algebra.Construct.Sub.Ring.Ideal using (Ideal)
+import Algebra.Construct.Quotient.AbelianGroup as Quotient
 
 module Algebra.Construct.Quotient.Ring
   {c ℓ} (R : Ring c ℓ) {c′ ℓ′} (I : Ideal R c′ ℓ′)
   where
 
+open import Algebra.Definitions using (Congruent₂)
 open import Algebra.Morphism.Structures using (IsRingHomomorphism)
 open import Data.Product.Base using (_,_)
 open import Function.Base using (_∘_)
 open import Level using (_⊔_)
 
-import Algebra.Construct.Quotient.AbelianGroup as Quotient
-
 private
   module R = Ring R
   module I = Ideal I
   module R/I = Quotient R.+-abelianGroup I.subgroup
 
 
 open R/I public
-  using (_≋_; _by_; ≋-refl; ≈⇒≋
-        ; quotientAbelianGroup
-        ; π; π-isMonoidHomomorphism; π-surjective
-        )
-
-open import Algebra.Definitions _≋_ using (Congruent₂)
+  using (_≋_; _by_; ≈⇒≋; π; π-isMonoidHomomorphism; π-surjective)
+  renaming (abelianGroup to +-abelianGroup)
 
-≋-*-cong : Congruent₂ R._*_
-≋-*-cong {x} {y} {u} {v} (j by ιj+x≈y) (k by ιk+u≈v) = ι j *ₗ k +ᴹ j *ᵣ u +ᴹ x *ₗ k by begin
+*-cong : Congruent₂ _≋_ R._*_
+*-cong {x} {y} {u} {v} (j by ιj+x≈y) (k by ιk+u≈v) =
+  ι j *ₗ k +ᴹ j *ᵣ u +ᴹ x *ₗ k by begin
   ι (ι j *ₗ k +ᴹ j *ᵣ u +ᴹ x *ₗ k) + x * u       ≈⟨ +-congʳ (ι.+ᴹ-homo (ι j *ₗ k +ᴹ j *ᵣ u) (x *ₗ k)) ⟩
   ι (ι j *ₗ k +ᴹ j *ᵣ u) + ι (x *ₗ k) + x * u    ≈⟨ +-congʳ (+-congʳ (ι.+ᴹ-homo (ι j *ₗ k) (j *ᵣ u))) ⟩
   ι (ι j *ₗ k) + ι (j *ᵣ u) + ι (x *ₗ 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 ⟩
+  (ι j + x) * (ι k + u)                          ≈⟨ R.*-cong ιj+x≈y ιk+u≈v ⟩
   y * v                                          ∎
   where
-  open R using (_+_; _*_; +-congʳ ;+-cong; *-cong)
+  open R using (_+_; _*_; +-congʳ ;+-cong)
   open import Algebra.Properties.Semiring R.semiring using (binomial-expansion)
   open import Relation.Binary.Reasoning.Setoid R.setoid
   open I using (ι; _*ₗ_; _*ᵣ_; _+ᴹ_)
 
-quotientRawRing : RawRing c (c ⊔ ℓ ⊔ c′)
-quotientRawRing = record { RawRing R.rawRing hiding (_≈_) ; _≈_ = _≋_ }
-
-quotientRing : Ring c (c ⊔ ℓ ⊔ c′)
-quotientRing = record
+ring : Ring c (c ⊔ ℓ ⊔ c′)
+ring = record
   { isRing = record
     { +-isAbelianGroup = isAbelianGroup
-    ; *-cong = ≋-*-cong
+    ; *-cong = *-cong
     ; *-assoc = λ x y z → ≈⇒≋ (R.*-assoc x y z)
     ; *-identity = ≈⇒≋ ∘ R.*-identityˡ , ≈⇒≋ ∘ R.*-identityʳ
     ; distrib = (λ x y z → ≈⇒≋ (R.distribˡ x y z)) , (λ x y z → ≈⇒≋ (R.distribʳ x y z))
     }
-  } where open AbelianGroup quotientAbelianGroup using (isAbelianGroup)
+  } where open AbelianGroup +-abelianGroup using (isAbelianGroup)
+
+private module Q = Ring ring
+
+-- Public re-exports
+
+_/_ : Ring c (c ⊔ ℓ ⊔ c′)
+_/_ = ring
 
-π-isRingHomomorphism : IsRingHomomorphism R.rawRing quotientRawRing π
+π-isRingHomomorphism : IsRingHomomorphism R.rawRing Q.rawRing π
 π-isRingHomomorphism = record
   { isSemiringHomomorphism = record
     { isNearSemiringHomomorphism = record
       { +-isMonoidHomomorphism = π-isMonoidHomomorphism
-      ; *-homo = λ _ _ → ≋-refl
+      ; *-homo = λ _ _ → Q.refl
       }
-    ; 1#-homo = ≋-refl
+    ; 1#-homo = Q.refl
     }
-  ; -‿homo = λ _ → ≋-refl
+  ; -‿homo = λ _ → Q.refl
   }