Mercurial > hg > Members > kono > Proof > category
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)}