Mercurial > hg > Members > kono > Proof > galois
annotate src/Gutil0.agda @ 281:803f909fdd17
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 29 Jan 2023 08:19:19 +0900 |
| parents | 386ece574509 |
| children | ec6fc84284f7 |
| 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 | |
| 271 | 49 -- record NormalSubGroup {c l : Level } ( G : Group c l ) : Set ( c Level.⊔ l ) where |
| 50 -- open Group G | |
| 51 -- field | |
| 52 -- sub : Carrier → Carrier | |
| 53 -- s-homo : IsGroupHomomorphism (GR G) (GR G) sub | |
| 54 -- commute : ( g n : Carrier ) → g ∙ sub n ≈ sub n ∙ g | |
| 55 -- -- it has at least one element other than ε | |
| 56 -- -- anElement : Carrier | |
| 57 -- -- notE : ¬ ( Group._≈_ G anElement (Group.ε G) ) | |
| 259 | 58 |
| 264 | 59 -- open import Relation.Binary.Morphism.Structures |
| 259 | 60 |
| 61 import Relation.Binary.Reasoning.Setoid as EqReasoning | |
| 62 | |
| 271 | 63 -- record HomoMorphism {c l : Level } (G : Group c l) (f : Group.Carrier G → Group.Carrier G) : Set ( c Level.⊔ l ) where |
| 64 -- open Group G | |
| 65 -- field | |
| 66 -- f-cong : {x y : Carrier } → x ≈ y → f x ≈ f y | |
| 67 -- f-homo : (x y : Carrier ) → f ( x ∙ y ) ≈ f x ∙ f y | |
| 68 -- f-ε : f ( ε ) ≈ ε | |
| 69 -- f-inv : (x : Carrier) → f ( x ⁻¹ ) ≈ (f x ) ⁻¹ | |
| 259 | 70 |
| 264 | 71 -- HM : {c l : Level } → (G : Group c l ) → (f : Group.Carrier G → Group.Carrier G ) |
| 72 -- → IsGroupHomomorphism (GR G) (GR G) f → HomoMorphism G f | |
| 73 -- HM G f homo = record { | |
| 74 -- f-cong = λ eq → IsRelHomomorphism.cong ( IsMagmaHomomorphism.isRelHomomorphism | |
| 75 -- ( IsMonoidHomomorphism.isMagmaHomomorphism ( IsGroupHomomorphism.isMonoidHomomorphism homo))) eq | |
| 76 -- ; f-homo = IsMagmaHomomorphism.homo (IsMonoidHomomorphism.isMagmaHomomorphism ( IsGroupHomomorphism.isMonoidHomomorphism homo)) | |
| 77 -- ; f-ε = IsMonoidHomomorphism.ε-homo ( IsGroupHomomorphism.isMonoidHomomorphism homo) | |
| 78 -- ; f-inv = IsGroupHomomorphism.⁻¹-homo homo | |
| 79 -- } | |
| 80 -- | |
| 81 -- open HomoMorphism | |
| 82 -- | |
| 83 -- hm : {c l : Level } → (G : Group c l ) → (f : Group.Carrier G → Group.Carrier G ) | |
| 84 -- → HomoMorphism G f | |
| 85 -- → IsGroupHomomorphism (GR G) (GR G) f | |
| 86 -- hm G f hm = record { isMonoidHomomorphism = record { isMagmaHomomorphism = record { | |
| 87 -- isRelHomomorphism = record { cong = λ {x} {y} eq → f-cong hm {x} {y} eq } | |
| 88 -- ; homo = f-homo hm } ; ε-homo = f-ε hm } ; ⁻¹-homo = f-inv hm | |
| 89 -- } | |
| 90 -- |