Split product up into two fields in IsNormal

Author: Taneb

src/Algebra/Construct/Quotient/Group.agda

@@ -18,7 +18,7 @@ open import Algebra.Morphism.Structures using (IsGroupHomomorphism)
 open import Algebra.Properties.Monoid monoid
 open import Algebra.Properties.Group G using (⁻¹-anti-homo-∙)
 open import Algebra.Structures using (IsGroup)
-open import Data.Product.Base using (_,_; proj₁; proj₂)
+open import Data.Product.Base using (_,_)
 open import Function.Definitions using (Surjective)
 open import Level using (_⊔_)
 open import Relation.Binary.Core using (_⇒_)
@@ -28,7 +28,7 @@ open import Relation.Binary.Reasoning.Setoid setoid
 
 private
   module N = NormalSubgroup N
-open NormalSubgroup N using (ι; module ι; normal)
+open NormalSubgroup N using (ι; module ι; conjugate; normal)
 
 infix 0 _by_
 
@@ -66,19 +66,19 @@ open AlgDefs _≋_
 ≋-∙-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′) ⟩
-  (ι g ∙ ι h′) ∙ (x ∙ u) ≈⟨ uv≈wx⇒yu∙vz≈yw∙xz (normal h x .proj₂) (ι g) u ⟩
+  (ι 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 ⟩
   y ∙ v                  ∎
-  where h′ = normal h x .proj₁
+  where h′ = conjugate h x
 
 ≋-⁻¹-cong : Congruent₁ _⁻¹
 ≋-⁻¹-cong {x} {y} (g by ιg∙x≈y) = h by begin
-  ι h ∙ x ⁻¹        ≈⟨ normal (g N.⁻¹) (x ⁻¹) .proj₂ ⟩
+  ι h ∙ x ⁻¹        ≈⟨ normal (g N.⁻¹) (x ⁻¹) ⟩
   x ⁻¹ ∙ ι (g N.⁻¹) ≈⟨ ∙-congˡ (ι.⁻¹-homo g) ⟩
   x ⁻¹ ∙ ι g ⁻¹     ≈⟨ ⁻¹-anti-homo-∙ (ι g) x ⟨
   (ι g ∙ x) ⁻¹      ≈⟨ ⁻¹-cong ιg∙x≈y ⟩
   y ⁻¹              ∎
-  where h = normal (g N.⁻¹) (x ⁻¹) .proj₁
+  where h = conjugate (g N.⁻¹) (x ⁻¹)
 
 quotientIsGroup : IsGroup _≋_ _∙_ ε _⁻¹
 quotientIsGroup = record

src/Algebra/NormalSubgroup.agda

@@ -12,7 +12,6 @@ module Algebra.NormalSubgroup {c ℓ} (G : Group c ℓ)  where
 
 open import Algebra.Definitions
 open import Algebra.Construct.Sub.Group G using (Subgroup)
-open import Data.Product.Base using (∃-syntax; _,_)
 open import Level using (suc; _⊔_)
 
 private
@@ -22,7 +21,8 @@ private
 record IsNormal {c′ ℓ′} (subgroup : Subgroup c′ ℓ′) : Set (c ⊔ ℓ ⊔ c′) where
   open Subgroup subgroup
   field
-    normal : ∀ n g → ∃[ n′ ] ι n′ G.∙ g G.≈ g G.∙ ι n
+    conjugate : ∀ n g → Carrier
+    normal : ∀ n g → ι (conjugate n g) G.∙ g G.≈ g G.∙ ι n
 
 record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) where
   field
@@ -33,5 +33,5 @@ record NormalSubgroup c′ ℓ′ : Set (c ⊔ ℓ ⊔ suc (c′ ⊔ ℓ′)) wh
   open IsNormal isNormal public
 
 abelian⇒subgroup-normal : ∀ {c′ ℓ′} → Commutative G._≈_ G._∙_ → (subgroup : Subgroup c′ ℓ′) → IsNormal subgroup
-abelian⇒subgroup-normal ∙-comm subgroup = record { normal = λ n g → n , ∙-comm (ι n) g }
+abelian⇒subgroup-normal ∙-comm subgroup = record { normal = λ n g → ∙-comm (ι n) g }
   where open Subgroup subgroup