Mercurial > hg > Members > kono > Proof > galois
annotate src/Gutil0.agda @ 274:691b2ee844ef
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 26 Jan 2023 01:16:38 +0900 |
| parents | c209aebeab2a |
| children | 386ece574509 |
| rev | line source |
|---|---|
|
257
d500309866da
fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 open import Level hiding ( suc ; zero ) |
| 264 | 2 module Gutil0 where |
|
257
d500309866da
fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 |
|
d500309866da
fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 open import Algebra |
|
d500309866da
fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 open import Algebra.Structures |
|
d500309866da
fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 open import Algebra.Definitions |
|
d500309866da
fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 open import Data.Product |
|
d500309866da
fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 open import Relation.Binary.PropositionalEquality |
|
d500309866da
fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 open import Algebra.Morphism.Structures |
| 264 | 10 open import Data.Empty |
| 11 open import Relation.Nullary | |
| 12 | |
|
257
d500309866da
fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 open GroupMorphisms |
|
d500309866da
fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 |
| 264 | 15 GR : {c l : Level } → Group c l → RawGroup c l |
| 16 GR G = record { | |
|
257
d500309866da
fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 Carrier = Carrier G |
|
d500309866da
fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 ; _≈_ = _≈_ G |
|
d500309866da
fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 ; _∙_ = _∙_ G |
|
d500309866da
fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 ; ε = ε G |
|
d500309866da
fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 ; _⁻¹ = _⁻¹ G |
|
d500309866da
fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 } where open Group |
|
d500309866da
fundamental theorem on homomorphisms
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 |
| 264 | 24 record GAxiom {c l : Level } (G : Group c l) : Set ( c Level.⊔ l ) where |
| 25 open Group G | |
| 26 field | |
| 27 ∙-cong : {x y u v : Carrier } → x ≈ y → u ≈ v → x ∙ u ≈ y ∙ v | |
| 28 assoc : (x y z : Carrier ) → x ∙ y ∙ z ≈ x ∙ ( y ∙ z ) | |
| 29 identity : ((y : Carrier) → ε ∙ y ≈ y ) × ((y : Carrier) → y ∙ ε ≈ y ) | |
| 30 inverse : ((y : Carrier) → y ⁻¹ ∙ y ≈ ε ) × ((y : Carrier) → y ∙ y ⁻¹ ≈ ε ) | |
| 31 ⁻¹-cong : {x y : Carrier } → x ≈ y → x ⁻¹ ≈ y ⁻¹ | |
| 32 | |
| 33 GA : {c l : Level } → (G : Group c l) → GAxiom G | |
| 34 GA G = record { | |
| 35 ∙-cong = IsMagma.∙-cong ( IsSemigroup.isMagma ( IsMonoid.isSemigroup ( IsGroup.isMonoid isGroup))) | |
| 36 ; assoc = IsSemigroup.assoc ( IsMonoid.isSemigroup ( IsGroup.isMonoid isGroup)) | |
| 37 ; identity = IsMonoid.identity ( IsGroup.isMonoid isGroup) | |
| 38 ; inverse = IsGroup.inverse isGroup | |
| 39 ; ⁻¹-cong = IsGroup.⁻¹-cong isGroup | |
| 40 } where open Group G | |
| 41 | |
| 42 open import Relation.Binary.Structures | |
| 43 | |
| 44 Eq : {c l : Level } → (G : Group c l) → IsEquivalence _ | |
| 45 Eq G = IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup | |
| 46 (IsGroup.isMonoid (Group.isGroup G ))) ) | |
| 47 | |
| 48 grefl : {c l : Level } → (G : Group c l ) → {x : Group.Carrier G} → Group._≈_ G x x | |
| 49 grefl G = IsGroup.refl ( Group.isGroup G ) | |
| 50 | |
| 51 gsym : {c l : Level } → (G : Group c l ) → {x y : Group.Carrier G} → Group._≈_ G x y → Group._≈_ G y x | |
| 52 gsym G = IsGroup.sym ( Group.isGroup G ) | |
| 53 | |
| 54 gtrans : {c l : Level } → (G : Group c l ) → {x y z : Group.Carrier G} → Group._≈_ G x y → Group._≈_ G y z → Group._≈_ G x z | |
| 55 gtrans G = IsGroup.trans ( Group.isGroup G ) | |
| 56 | |
| 271 | 57 -- record NormalSubGroup {c l : Level } ( G : Group c l ) : Set ( c Level.⊔ l ) where |
| 58 -- open Group G | |
| 59 -- field | |
| 60 -- sub : Carrier → Carrier | |
| 61 -- s-homo : IsGroupHomomorphism (GR G) (GR G) sub | |
| 62 -- commute : ( g n : Carrier ) → g ∙ sub n ≈ sub n ∙ g | |
| 63 -- -- it has at least one element other than ε | |
| 64 -- -- anElement : Carrier | |
| 65 -- -- notE : ¬ ( Group._≈_ G anElement (Group.ε G) ) | |
| 259 | 66 |
| 264 | 67 -- open import Relation.Binary.Morphism.Structures |
| 259 | 68 |
| 69 import Relation.Binary.Reasoning.Setoid as EqReasoning | |
| 70 | |
| 271 | 71 -- record HomoMorphism {c l : Level } (G : Group c l) (f : Group.Carrier G → Group.Carrier G) : Set ( c Level.⊔ l ) where |
| 72 -- open Group G | |
| 73 -- field | |
| 74 -- f-cong : {x y : Carrier } → x ≈ y → f x ≈ f y | |
| 75 -- f-homo : (x y : Carrier ) → f ( x ∙ y ) ≈ f x ∙ f y | |
| 76 -- f-ε : f ( ε ) ≈ ε | |
| 77 -- f-inv : (x : Carrier) → f ( x ⁻¹ ) ≈ (f x ) ⁻¹ | |
| 259 | 78 |
| 264 | 79 -- HM : {c l : Level } → (G : Group c l ) → (f : Group.Carrier G → Group.Carrier G ) |
| 80 -- → IsGroupHomomorphism (GR G) (GR G) f → HomoMorphism G f | |
| 81 -- HM G f homo = record { | |
| 82 -- f-cong = λ eq → IsRelHomomorphism.cong ( IsMagmaHomomorphism.isRelHomomorphism | |
| 83 -- ( IsMonoidHomomorphism.isMagmaHomomorphism ( IsGroupHomomorphism.isMonoidHomomorphism homo))) eq | |
| 84 -- ; f-homo = IsMagmaHomomorphism.homo (IsMonoidHomomorphism.isMagmaHomomorphism ( IsGroupHomomorphism.isMonoidHomomorphism homo)) | |
| 85 -- ; f-ε = IsMonoidHomomorphism.ε-homo ( IsGroupHomomorphism.isMonoidHomomorphism homo) | |
| 86 -- ; f-inv = IsGroupHomomorphism.⁻¹-homo homo | |
| 87 -- } | |
| 88 -- | |
| 89 -- open HomoMorphism | |
| 90 -- | |
| 91 -- hm : {c l : Level } → (G : Group c l ) → (f : Group.Carrier G → Group.Carrier G ) | |
| 92 -- → HomoMorphism G f | |
| 93 -- → IsGroupHomomorphism (GR G) (GR G) f | |
| 94 -- hm G f hm = record { isMonoidHomomorphism = record { isMagmaHomomorphism = record { | |
| 95 -- isRelHomomorphism = record { cong = λ {x} {y} eq → f-cong hm {x} {y} eq } | |
| 96 -- ; homo = f-homo hm } ; ε-homo = f-ε hm } ; ⁻¹-homo = f-inv hm | |
| 97 -- } | |
| 98 -- |