Mercurial > hg > Members > kono > Proof > category

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

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
1109:71049ed05151 1110:45de2b31bf02
1 {-# OPTIONS --universe-polymorphism #-}
2 module Category.Group where
3 open import Category
4 open import Algebra
5 open import Algebra.Structures
6 open import Algebra.Morphism
7 import Algebra.Props.Group as GroupP
8 import Relation.Binary.EqReasoning as EqR
9 open import Relation.Binary.Core
10 open import Relation.Binary
11 open import Level
12 open import Data.Product
13
14 GrpObj : ∀{c ℓ} → Set (suc (c ⊔ ℓ))
15 GrpObj {c} {ℓ} = Group c ℓ
16
17 record _-Group⟶_ {c ℓ c′ ℓ′} (From : Group c ℓ) (To : Group c′ ℓ′) : Set (c ⊔ ℓ ⊔ c′ ⊔ ℓ′) where
18 private
19 module F = Group From
20 module T = Group To
21 open Definitions F.Carrier T.Carrier T._≈_
22 field
23 ⟦_⟧ : Morphism
24 ⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_
25 ∙-homo : Homomorphic₂ ⟦_⟧ F._∙_ T._∙_
26
27 ε-homo : Homomorphic₀ ⟦_⟧ F.ε T.ε
28 ε-homo = left-identity-unique ⟦ F.ε ⟧ ⟦ F.ε ⟧ (begin
29 T._∙_ ⟦ F.ε ⟧ ⟦ F.ε ⟧ ≈⟨ T.sym (∙-homo F.ε F.ε) ⟩
30 ⟦ F._∙_ F.ε F.ε ⟧ ≈⟨ ⟦⟧-cong (proj₁ (IsMonoid.identity (Monoid.isMonoid F.monoid)) F.ε) ⟩
31 ⟦ F.ε ⟧ ∎)
32 where
33 open GroupP To
34 open EqR T.setoid
35 ⁻¹-homo : Homomorphic₁ ⟦_⟧ F._⁻¹ T._⁻¹
36 ⁻¹-homo x = left-inverse-unique ⟦ F._⁻¹ x ⟧ ⟦ x ⟧ (begin
37 T._∙_ ⟦ F._⁻¹ x ⟧ ⟦ x ⟧ ≈⟨ T.sym (∙-homo (F._⁻¹ x) x) ⟩
38 ⟦ F._∙_ (F._⁻¹ x) x ⟧ ≈⟨ ⟦⟧-cong (proj₁ (IsGroup.inverse F.isGroup) x) ⟩
39 ⟦ F.ε ⟧ ≈⟨ ε-homo ⟩
40 T.ε ∎)
41 where
42 open GroupP To
43 open EqR T.setoid
44
45 _⟪_⟫ : ∀{c ℓ c′ ℓ′} {G : Group c ℓ} {F : Group c′ ℓ′} → (M : G -Group⟶ F) → Group.Carrier G → Group.Carrier F
46 f ⟪ x ⟫ = _-Group⟶_.⟦_⟧ f x
47
48 GrpId : ∀{c ℓ} {G : Group c ℓ} → G -Group⟶ G
49 GrpId {G = G} = record { ⟦_⟧ = ⟦_⟧ ; ⟦⟧-cong = ⟦⟧-cong ; ∙-homo = ∙-homo }
50 where
51 open Algebra.Group G
52 open Definitions Carrier Carrier _≈_
53 ⟦_⟧ : Carrier → Carrier
54 ⟦_⟧ = λ x → x
55 ⟦⟧-cong : ⟦_⟧ Preserves _≈_ ⟶ _≈_
56 ⟦⟧-cong = λ x → x
57 ∙-homo : Homomorphic₂ ⟦_⟧ _∙_ _∙_
58 ∙-homo x y = IsEquivalence.refl (Setoid.isEquivalence setoid)
59
60 _∘_ : ∀{c₁ ℓ₁ c₂ ℓ₂ c₃ ℓ₃} {G₁ : Group c₁ ℓ₁} {G₂ : Group c₂ ℓ₂} {G₃ : Group c₃ ℓ₃}
61 → (g : G₂ -Group⟶ G₃) → (f : G₁ -Group⟶ G₂) → G₁ -Group⟶ G₃
62 _∘_ {G₁ = G₁} {G₂} {G₃} g f = record { ⟦_⟧ = ⟦_⟧ ; ⟦⟧-cong = ⟦⟧-cong ; ∙-homo = ∙-homo }
63 where
64 module F = Group G₁
65 module M = Group G₂
66 module T = Group G₃
67 module hom = _-Group⟶_
68 open Definitions (F.Carrier) (T.Carrier) (T._≈_)
69 ⟦_⟧ : F.Carrier → T.Carrier
70 ⟦ x ⟧ = g ⟪ f ⟪ x ⟫ ⟫
71 ⟦⟧-cong : ⟦_⟧ Preserves F._≈_ ⟶ T._≈_
72 ⟦⟧-cong x = hom.⟦⟧-cong g (hom.⟦⟧-cong f x)
73 ∙-homo : Homomorphic₂ ⟦_⟧ (F._∙_) (T._∙_)
74 ∙-homo x y = begin
75 ⟦ F._∙_ x y ⟧ ≈⟨ hom.⟦⟧-cong g (hom.∙-homo f x y) ⟩
76 g ⟪ M._∙_ (f ⟪ x ⟫) (f ⟪ y ⟫) ⟫ ≈⟨ hom.∙-homo g (f ⟪ x ⟫) (f ⟪ y ⟫) ⟩
77 T._∙_ ⟦ x ⟧ ⟦ y ⟧ ∎
78 where
79 open IsEquivalence T.isEquivalence
80 open EqR T.setoid
81
82 _≈_ : ∀{c ℓ c′ ℓ′} {G₁ : Group c ℓ} {G₂ : Group c′ ℓ′} → Rel (G₁ -Group⟶ G₂) (ℓ′ ⊔ c)
83 _≈_ {G₁ = G₁} {G₂} φ ψ = ∀(x : F.Carrier) → T._≈_ (φ ⟪ x ⟫) (ψ ⟪ x ⟫)
84 where
85 module F = Group G₁
86 module T = Group G₂
87
88 ≈-refl : ∀{c ℓ c′ ℓ′} {G₁ : Group c ℓ} {G₂ : Group c′ ℓ′} {F : G₁ -Group⟶ G₂} → F ≈ F
89 ≈-refl {G₁ = G₁} {F = F} _ = _-Group⟶_.⟦⟧-cong F (IsEquivalence.refl (Group.isEquivalence G₁))
90
91 ≈-sym : ∀{c ℓ c′ ℓ′} {G₁ : Group c ℓ} {G₂ : Group c′ ℓ′} {F G : G₁ -Group⟶ G₂} → F ≈ G → G ≈ F
92 ≈-sym {G₁ = G₁} {G₂} {F} {G} F≈G x = IsEquivalence.sym (Group.isEquivalence G₂)(F≈G x)
93
94 ≈-trans : ∀{c ℓ c′ ℓ′} {G₁ : Group c ℓ} {G₂ : Group c′ ℓ′} {F G H : G₁ -Group⟶ G₂}
95 → F ≈ G → G ≈ H → F ≈ H
96 ≈-trans {G₁ = G₁} {G₂} {F} {G} F≈G G≈H x = IsEquivalence.trans (Group.isEquivalence G₂) (F≈G x) (G≈H x)
97
98 Grp : ∀{c ℓ} → Category _ _ _
99 Grp {c} {ℓ} = record { Obj = Group c ℓ
100 ; Hom = _-Group⟶_
101 ; Id = GrpId
102 ; _o_ = _∘_
103 ; _≈_ = _≈_
104 ; isCategory = isCategory
105 }
106 where
107 isCategory : IsCategory (Group c ℓ) _-Group⟶_ _≈_ _∘_ GrpId
108 isCategory =
109 record { isEquivalence = record { refl = λ {F} → ≈-refl {F = F}
110 ; sym = λ {F} {G} → ≈-sym {F = F} {G}
111 ; trans = λ {F} {G} {H} → ≈-trans {F = F} {G} {H}
112 }
113 ; identityL = λ {G₁} {G₂} {f} → identityL {G₁} {G₂} {f}
114 ; identityR = λ {G₁} {G₂} {f} → identityR {G₁} {G₂} {f}
115 ; o-resp-≈ = λ {A} {B} {C} {f} {g} {h} {i} → o-resp-≈ {A} {B} {C} {f} {g} {h} {i}
116 ; associative = λ {G₁} {G₂} {G₃} {G₄} {f} {g} {h} → associative {G₁} {G₂} {G₃} {G₄} {f} {g} {h}
117 }
118 where
119 identityL : {G₁ G₂ : Group c ℓ} {f : G₁ -Group⟶ G₂} → (GrpId ∘ f) ≈ f
120 identityL {G₁} {G₂} {f} = ≈-refl {G₁ = G₁} {F = f}
121 identityR : {G₁ G₂ : Group c ℓ} {f : G₁ -Group⟶ G₂} → (f ∘ GrpId) ≈ f
122 identityR {G₁} {G₂} {f} = ≈-refl {G₁ = G₁} {F = f}
123 o-resp-≈ : {G₁ G₂ G₃ : Group c ℓ} {f g : G₁ -Group⟶ G₂} {h i : G₂ -Group⟶ G₃}
124 → f ≈ g → h ≈ i → (h ∘ f) ≈ (i ∘ g)
125 o-resp-≈ {G₁} {G₂} {G₃} {f} {g} {h} {i} f≈g h≈i x = begin
126 (h ⟪ f ⟪ x ⟫ ⟫) ≈⟨ (h≈i ( f ⟪ x ⟫ )) ⟩
127 (i ⟪ f ⟪ x ⟫ ⟫) ≈⟨ _-Group⟶_.⟦⟧-cong i (f≈g x) ⟩
128 (i ⟪ g ⟪ x ⟫ ⟫) ∎
129 where
130 module T = Group G₃
131 open IsEquivalence T.isEquivalence
132 open EqR T.setoid
133 associative : {G₁ G₂ G₃ G₄ : Group c ℓ} {f : G₃ -Group⟶ G₄} {g : G₂ -Group⟶ G₃} {h : G₁ -Group⟶ G₂}
134 → (f ∘ (g ∘ h)) ≈ ((f ∘ g) ∘ h)
135 associative {G₁} {G₂} {G₃} {G₄} {f} {g} {h} = ≈-refl {G₁ = G₁} {F = f ∘ (g ∘ h)}