diff src/Category/Group.agda @ 1110:45de2b31bf02

add original library and fix for safe mode
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 07 Oct 2023 19:43:31 +0900
parents
children 5620d4a85069
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Category/Group.agda	Sat Oct 07 19:43:31 2023 +0900
@@ -0,0 +1,135 @@
+{-# OPTIONS --universe-polymorphism #-}
+module Category.Group where
+open import Category
+open import Algebra
+open import Algebra.Structures
+open import Algebra.Morphism
+import Algebra.Props.Group as GroupP
+import Relation.Binary.EqReasoning as EqR
+open import Relation.Binary.Core
+open import Relation.Binary
+open import Level
+open import Data.Product
+
+GrpObj : ∀{c ℓ} → Set (suc (c ⊔ ℓ))
+GrpObj {c} {ℓ} = Group c ℓ
+
+record _-Group⟶_ {c ℓ c′ ℓ′} (From : Group c ℓ) (To : Group c′ ℓ′) : Set (c ⊔ ℓ ⊔ c′ ⊔ ℓ′) where
+  private 
+    module F = Group From
+    module T = Group To
+  open Definitions F.Carrier T.Carrier T._≈_
+  field
+    ⟦_⟧ : Morphism
+    ⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_
+    ∙-homo : Homomorphic₂ ⟦_⟧ F._∙_ T._∙_
+  
+  ε-homo : Homomorphic₀ ⟦_⟧ F.ε T.ε
+  ε-homo = left-identity-unique ⟦ F.ε ⟧ ⟦ F.ε ⟧ (begin
+    T._∙_ ⟦ F.ε ⟧ ⟦ F.ε ⟧ ≈⟨ T.sym (∙-homo F.ε F.ε) ⟩
+    ⟦ F._∙_ F.ε F.ε ⟧ ≈⟨ ⟦⟧-cong (proj₁ (IsMonoid.identity (Monoid.isMonoid F.monoid)) F.ε) ⟩
+    ⟦ F.ε ⟧ ∎)
+    where
+      open GroupP To
+      open EqR T.setoid
+  ⁻¹-homo : Homomorphic₁ ⟦_⟧ F._⁻¹ T._⁻¹
+  ⁻¹-homo x = left-inverse-unique ⟦ F._⁻¹ x ⟧ ⟦ x ⟧ (begin
+    T._∙_  ⟦ F._⁻¹ x ⟧ ⟦ x ⟧ ≈⟨ T.sym (∙-homo (F._⁻¹ x) x) ⟩
+    ⟦ F._∙_ (F._⁻¹ x) x ⟧   ≈⟨ ⟦⟧-cong (proj₁ (IsGroup.inverse F.isGroup) x) ⟩ 
+    ⟦ F.ε ⟧               ≈⟨ ε-homo ⟩
+    T.ε                  ∎)
+    where
+      open GroupP To
+      open EqR T.setoid
+
+_⟪_⟫ : ∀{c ℓ c′ ℓ′} {G : Group c ℓ} {F : Group c′ ℓ′} → (M : G -Group⟶ F) → Group.Carrier G → Group.Carrier F
+f ⟪ x ⟫ = _-Group⟶_.⟦_⟧ f x
+
+GrpId : ∀{c ℓ} {G : Group c ℓ} → G -Group⟶ G
+GrpId {G = G} = record { ⟦_⟧ = ⟦_⟧ ; ⟦⟧-cong = ⟦⟧-cong ; ∙-homo = ∙-homo }
+  where
+    open Algebra.Group G
+    open Definitions Carrier Carrier _≈_
+    ⟦_⟧ : Carrier → Carrier
+    ⟦_⟧ = λ x → x
+    ⟦⟧-cong : ⟦_⟧ Preserves _≈_ ⟶ _≈_
+    ⟦⟧-cong = λ x → x
+    ∙-homo : Homomorphic₂ ⟦_⟧ _∙_ _∙_
+    ∙-homo x y = IsEquivalence.refl (Setoid.isEquivalence setoid)
+
+_∘_ : ∀{c₁ ℓ₁ c₂ ℓ₂ c₃ ℓ₃} {G₁ : Group c₁ ℓ₁} {G₂ : Group c₂ ℓ₂} {G₃ : Group c₃ ℓ₃}
+  → (g : G₂ -Group⟶ G₃) → (f : G₁ -Group⟶ G₂) → G₁ -Group⟶ G₃
+_∘_ {G₁ = G₁} {G₂} {G₃} g f = record { ⟦_⟧ = ⟦_⟧ ; ⟦⟧-cong = ⟦⟧-cong ; ∙-homo = ∙-homo }
+  where
+    module F = Group G₁
+    module M = Group G₂
+    module T = Group G₃
+    module hom = _-Group⟶_
+    open Definitions (F.Carrier) (T.Carrier) (T._≈_)
+    ⟦_⟧ : F.Carrier → T.Carrier
+    ⟦ x ⟧ = g ⟪ f ⟪ x ⟫ ⟫
+    ⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_
+    ⟦⟧-cong x = hom.⟦⟧-cong g (hom.⟦⟧-cong f x)
+    ∙-homo : Homomorphic₂ ⟦_⟧ (F._∙_) (T._∙_)
+    ∙-homo x y = begin
+      ⟦ F._∙_ x y ⟧                     ≈⟨ hom.⟦⟧-cong g (hom.∙-homo f x y) ⟩
+      g ⟪ M._∙_ (f ⟪ x ⟫) (f ⟪ y ⟫) ⟫   ≈⟨ hom.∙-homo g (f ⟪ x ⟫) (f ⟪ y ⟫) ⟩
+      T._∙_ ⟦ x ⟧ ⟦ y ⟧ ∎
+      where
+        open IsEquivalence T.isEquivalence
+        open EqR T.setoid
+
+_≈_ : ∀{c ℓ c′ ℓ′} {G₁ : Group c ℓ} {G₂ : Group c′ ℓ′} → Rel (G₁ -Group⟶ G₂) (ℓ′ ⊔ c)
+_≈_ {G₁ = G₁} {G₂} φ ψ = ∀(x : F.Carrier) → T._≈_ (φ ⟪ x ⟫) (ψ ⟪ x ⟫)
+  where
+    module F = Group G₁
+    module T = Group G₂
+
+≈-refl : ∀{c ℓ c′ ℓ′} {G₁ : Group c ℓ} {G₂ : Group c′ ℓ′} {F : G₁ -Group⟶ G₂} → F ≈ F
+≈-refl {G₁ = G₁} {F = F} _ = _-Group⟶_.⟦⟧-cong F (IsEquivalence.refl (Group.isEquivalence G₁))
+
+≈-sym : ∀{c ℓ c′ ℓ′} {G₁ : Group c ℓ} {G₂ : Group c′ ℓ′} {F G : G₁ -Group⟶ G₂} → F ≈ G → G ≈ F
+≈-sym {G₁ = G₁} {G₂} {F} {G} F≈G x = IsEquivalence.sym (Group.isEquivalence G₂)(F≈G x)
+
+≈-trans : ∀{c ℓ c′ ℓ′} {G₁ : Group c ℓ} {G₂ : Group c′ ℓ′} {F G H : G₁ -Group⟶ G₂}
+        → F ≈ G → G ≈ H → F ≈ H
+≈-trans {G₁ = G₁} {G₂} {F} {G} F≈G G≈H x = IsEquivalence.trans (Group.isEquivalence G₂) (F≈G x) (G≈H x)
+
+Grp : ∀{c ℓ} → Category _ _ _
+Grp {c} {ℓ} = record { Obj = Group c ℓ
+                     ; Hom = _-Group⟶_
+                     ; Id = GrpId
+                     ; _o_ = _∘_
+                     ; _≈_ = _≈_
+                     ; isCategory = isCategory
+                     }
+  where
+    isCategory : IsCategory (Group c ℓ) _-Group⟶_ _≈_ _∘_ GrpId
+    isCategory =
+      record { isEquivalence = record { refl  = λ {F} → ≈-refl {F = F}
+                                      ; sym   = λ {F} {G} → ≈-sym {F = F} {G}
+                                      ; trans = λ {F} {G} {H} → ≈-trans {F = F} {G} {H}
+                                      }
+             ; identityL   = λ {G₁} {G₂} {f} → identityL {G₁} {G₂} {f}
+             ; identityR   = λ {G₁} {G₂} {f} → identityR {G₁} {G₂} {f}
+             ; o-resp-≈    = λ {A} {B} {C} {f} {g} {h} {i} → o-resp-≈ {A} {B} {C} {f} {g} {h} {i}
+             ; associative = λ {G₁} {G₂} {G₃} {G₄} {f} {g} {h} → associative {G₁} {G₂} {G₃} {G₄} {f} {g} {h}
+             }
+      where
+        identityL : {G₁ G₂ : Group c ℓ} {f : G₁ -Group⟶ G₂} → (GrpId ∘ f) ≈ f
+        identityL {G₁} {G₂} {f} = ≈-refl {G₁ = G₁} {F = f}
+        identityR : {G₁ G₂ : Group c ℓ} {f : G₁ -Group⟶ G₂} → (f ∘ GrpId) ≈ f
+        identityR {G₁} {G₂} {f} = ≈-refl {G₁ = G₁} {F = f}
+        o-resp-≈ : {G₁ G₂ G₃ : Group c ℓ} {f g : G₁ -Group⟶ G₂} {h i : G₂ -Group⟶ G₃}
+                 → f ≈ g → h ≈ i → (h ∘ f) ≈ (i ∘ g)
+        o-resp-≈ {G₁} {G₂} {G₃} {f} {g} {h} {i} f≈g h≈i x = begin
+            (h ⟪ f ⟪ x ⟫ ⟫)           ≈⟨ (h≈i ( f ⟪ x ⟫ )) ⟩
+            (i ⟪ f ⟪ x ⟫ ⟫)           ≈⟨ _-Group⟶_.⟦⟧-cong i (f≈g x) ⟩
+            (i ⟪ g ⟪ x ⟫ ⟫)           ∎
+          where
+            module T = Group G₃
+            open IsEquivalence T.isEquivalence
+            open EqR T.setoid
+        associative : {G₁ G₂ G₃ G₄ : Group c ℓ} {f : G₃ -Group⟶ G₄} {g : G₂ -Group⟶ G₃} {h : G₁ -Group⟶ G₂}
+                    → (f ∘ (g ∘ h)) ≈ ((f ∘ g) ∘ h)
+        associative {G₁} {G₂} {G₃} {G₄} {f} {g} {h} = ≈-refl {G₁ = G₁} {F = f ∘ (g ∘ h)}