Mercurial > hg > Members > kono > Proof > galois
changeset 261:ea6c61079789
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 30 May 2022 10:57:30 +0900 (2022-05-30) |
parents | 26c0d50e455f |
children | f36d2ed8ed9e |
files | src/FundamentalHomomorphism.agda |
diffstat | 1 files changed, 79 insertions(+), 75 deletions(-) [+] |
line wrap: on
line diff
--- a/src/FundamentalHomomorphism.agda Sun May 29 20:23:40 2022 +0900 +++ b/src/FundamentalHomomorphism.agda Mon May 30 10:57:30 2022 +0900 @@ -25,59 +25,47 @@ open Group G field sub : Carrier → Carrier - subgroup : IsGroupHomomorphism (Group→Raw G) (Group→Raw G) sub + s-homo : IsGroupHomomorphism (Group→Raw G) (Group→Raw G) sub commute : ( g n : Carrier ) → g ∙ sub n ≈ sub n ∙ g open import Relation.Binary.Morphism.Structures import Relation.Binary.Reasoning.Setoid as EqReasoning - -f-cong : (G : Group c l ) → (f : Group.Carrier G → Group.Carrier G ) - → IsGroupHomomorphism (Group→Raw G) (Group→Raw G) f → {x y : Group.Carrier G } → (Group._≈_ G) x y → (Group._≈_ G) (f x) (f y) -f-cong G f homo eq = IsRelHomomorphism.cong ( IsMagmaHomomorphism.isRelHomomorphism - ( IsMonoidHomomorphism.isMagmaHomomorphism ( IsGroupHomomorphism.isMonoidHomomorphism homo))) eq +record HomoMorphism (G : Group c l) (f : Group.Carrier G → Group.Carrier G) : Set ( c Level.⊔ l ) where + open Group G + field + f-cong : {x y : Carrier } → x ≈ y → f x ≈ f y + f-homo : (x y : Carrier ) → f ( x ∙ y ) ≈ f x ∙ f y + f-ε : f ( ε ) ≈ ε + f-inv : (x : Carrier) → f ( x ⁻¹ ) ≈ (f x ) ⁻¹ -f-homo : (G : Group c l ) → (f : Group.Carrier G → Group.Carrier G ) - → IsGroupHomomorphism (Group→Raw G) (Group→Raw G) f → (x y : Group.Carrier G ) - → Group._≈_ G (f ( Group._∙_ G x y )) ( Group._∙_ G (f x) (f y)) -f-homo G f homo = IsMagmaHomomorphism.homo (IsMonoidHomomorphism.isMagmaHomomorphism ( IsGroupHomomorphism.isMonoidHomomorphism homo)) +HM : (G : Group c l ) → (f : Group.Carrier G → Group.Carrier G ) + → IsGroupHomomorphism (Group→Raw G) (Group→Raw G) f → HomoMorphism G f +HM G f homo = record { + f-cong = λ eq → IsRelHomomorphism.cong ( IsMagmaHomomorphism.isRelHomomorphism + ( IsMonoidHomomorphism.isMagmaHomomorphism ( IsGroupHomomorphism.isMonoidHomomorphism homo))) eq + ; f-homo = IsMagmaHomomorphism.homo (IsMonoidHomomorphism.isMagmaHomomorphism ( IsGroupHomomorphism.isMonoidHomomorphism homo)) + ; f-ε = IsMonoidHomomorphism.ε-homo ( IsGroupHomomorphism.isMonoidHomomorphism homo) + ; f-inv = IsGroupHomomorphism.⁻¹-homo homo + } -f-ε : (G : Group c l ) → (f : Group.Carrier G → Group.Carrier G ) - → IsGroupHomomorphism (Group→Raw G) (Group→Raw G) f → Group._≈_ G (f ( Group.ε G )) (Group.ε G) -f-ε G f homo = IsMonoidHomomorphism.ε-homo ( IsGroupHomomorphism.isMonoidHomomorphism homo) +open HomoMorphism -f-inv : (G : Group c l ) → (f : Group.Carrier G → Group.Carrier G ) - → IsGroupHomomorphism (Group→Raw G) (Group→Raw G) f → (x : Group.Carrier G) → Group._≈_ G (f ( Group._⁻¹ G x )) (Group._⁻¹ G (f x )) -f-inv G f homo = IsGroupHomomorphism.⁻¹-homo homo - -p01 : (G : Group c l ) → (f : Group.Carrier G → Group.Carrier G ) +hm : (G : Group c l ) → (f : Group.Carrier G → Group.Carrier G ) + → HomoMorphism G f → IsGroupHomomorphism (Group→Raw G) (Group→Raw G) f - → IsGroupHomomorphism (Group→Raw G) (Group→Raw G) f -p01 G f homo = record { - isMonoidHomomorphism = record { - isMagmaHomomorphism = record { - isRelHomomorphism = record { cong = λ {x} {y} eq → p02 x y eq } - ; homo = p03 - } - ; ε-homo = p04 - } - ; ⁻¹-homo = p05 - } where - open Group G - p02 : (x y : Carrier ) → x ≈ y → f x ≈ f y - p02 x y = f-cong G f homo - p03 : (x y : Carrier ) → f ( x ∙ y ) ≈ f x ∙ f y - p03 = f-homo G f homo - p04 : f ( ε ) ≈ ε - p04 = f-ε G f homo - p05 : (x : Carrier) → f ( x ⁻¹ ) ≈ (f x ) ⁻¹ - p05 = f-inv G f homo +hm G f hm = record { isMonoidHomomorphism = record { isMagmaHomomorphism = record { + isRelHomomorphism = record { cong = λ {x} {y} eq → f-cong hm {x} {y} eq } + ; homo = f-homo hm } ; ε-homo = f-ε hm } ; ⁻¹-homo = f-inv hm + } +-- +-- Coset : N : NormalSubGroup → { a ∙ n | G ∋ a , N ∋ n } +-- data Coset (G : Group c l) (K : NormalSubGroup G) : Group.Carrier G → Set ( c Level.⊔ l ) where coset : (a b : Group.Carrier G ) → Coset G K ( Group._∙_ G a (NormalSubGroup.sub K b) ) - cscong : {a b : Group.Carrier G } → Group._≈_ G (NormalSubGroup.sub K a) (NormalSubGroup.sub K b) → Coset G K a → Coset G K b record CosetCarrier (G : Group c l) (K : NormalSubGroup G) : Set ( c Level.⊔ l ) where field @@ -86,47 +74,60 @@ open CosetCarrier open NormalSubGroup +open import Relation.Binary.Structures φ : {G : Group c l} → {K : NormalSubGroup G} → Group.Carrier G → CosetCarrier G K -φ {G} {K} x = record { r = sub K x ; isCoset = p1 } where +φ {G} {K} x = record { r = ((x ∙ (sub K x) ⁻¹) ∙ sub K x) ; isCoset = coset (x ∙ (sub K x) ⁻¹) x } where open Group G - p1 : Coset G K (sub K x) - p1 = cscong - (f-cong G (sub K) (subgroup K) (proj₁ (Group.identity G) (NormalSubGroup.sub K x ) ) ) - (coset (Group.ε G) x ) -- G / K : Quotient -_/_ : (G : Group c l) (K : NormalSubGroup G) → Group ( c Level.⊔ l ) l +_/_ : (G : Group c l) (K : NormalSubGroup G) → Group ( c Level.⊔ l ) l G / K = record { Carrier = CosetCarrier G K ; _≈_ = λ x y → sub K (r x) ≈ sub K (r y) - ; _∙_ = λ x y → record { r = r x ∙ r y ; isCoset = q01 x y } - ; ε = record { r = ε ; isCoset = cscong {!!} (coset ε ε) } - ; _⁻¹ = λ x → record { r = (r x) ⁻¹ ; isCoset = cscong {!!} ( coset ε ((r x) ⁻¹ )) } + ; _∙_ = λ x y → φ ( r x ∙ r y ) + ; ε = φ ε + ; _⁻¹ = λ x → φ ( (r x) ⁻¹ ) ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record { - isEquivalence = {!!} - ; ∙-cong = {!!} } - ; assoc = {!!} } - ; identity = {!!} } + isEquivalence = ise + ; ∙-cong = λ {x y u v} → ∙-cong1 {x} {y} {u} {v} } + ; assoc = assoc1 } + ; identity = identity1 } ; inverse = {!!} ; ⁻¹-cong = {!!} } } where open Group G open EqReasoning (Algebra.Group.setoid G) - q01 : (x y : CosetCarrier G K ) → Coset G K (r x ∙ r y) - q01 x y with isCoset x | isCoset y - ... | coset a b | coset c d = cscong q02 ( coset (a ∙ c) (b ∙ d) ) where - q02 : sub K (a ∙ c ∙ sub K (b ∙ d)) ≈ sub K (a ∙ sub K b ∙ (c ∙ sub K d)) - q02 = f-cong G (sub K) (subgroup K) ( begin - a ∙ c ∙ sub K (b ∙ d) ≈⟨ {!!} ⟩ - a ∙ c ∙ (sub K b ∙ sub K d) ≈⟨ {!!} ⟩ - a ∙ (c ∙ sub K b ) ∙ sub K d ≈⟨ {!!} ⟩ - a ∙ (sub K b ∙ c ) ∙ sub K d ≈⟨ {!!} ⟩ - a ∙ sub K b ∙ (c ∙ sub K d) ∎ ) - ... | coset a b | cscong eq x = {!!} - ... | cscong eq x | coset a b = {!!} - ... | cscong eqx x | cscong eqy y = {!!} + open HomoMorphism (HM G (sub K) (s-homo K )) + Eq = IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup + (IsGroup.isMonoid isGroup ))) + ise : Relation.Binary.Structures.IsEquivalence _ + ise = record { refl = IsEquivalence.refl Eq ; sym = IsEquivalence.sym Eq ; trans = IsEquivalence.trans Eq } where + postulate -- cheat + ∙-cong1 : {x y u v : CosetCarrier G K } + → sub K (r x) ≈ sub K (r y) + → sub K (r u) ≈ sub K (r v) + → sub K (r ( φ {G} {K} (r x ∙ r u ) )) ≈ sub K (r ( φ {G} {K} (r y ∙ r v ) )) + -- ∙-cong1 {x} {y} {u} {v} x=y y=z = begin + -- sub K ((r x ∙ r u) ∙ sub K (r x ∙ r u) ⁻¹ ∙ sub K (r x ∙ r u)) ≈⟨ {!!} ⟩ + -- sub K ((r y ∙ r v) ∙ sub K (r y ∙ r v) ⁻¹ ∙ sub K (r y ∙ r v)) ≈⟨ {!!} ⟩ + -- sub K (r ( φ {G} {K} (r y ∙ r v ) )) ∎ + assoc1 : (x y z : CosetCarrier G K ) + → sub K (r (φ {G} {K} (r (φ {G} {K} (r x ∙ r y)) ∙ r z))) ≈ sub K (r (φ {G} {K} (r x ∙ r (φ {G} {K} (r y ∙ r z))))) + -- assoc1 x y z = begin + -- sub K (r x ∙ r y ∙ sub K (r x ∙ r y) ⁻¹ ∙ sub K (r x ∙ r y) ∙ r z ∙ + -- sub K (r x ∙ r y ∙ sub K (r x ∙ r y) ⁻¹ ∙ sub K (r x ∙ r y) ∙ r z) ⁻¹ ∙ + -- sub K (r x ∙ r y ∙ sub K (r x ∙ r y) ⁻¹ ∙ sub K (r x ∙ r y) ∙ r z)) ≈⟨ {!!} ⟩ + -- sub K (r x ∙ r y ∙ r z ∙ sub K (r x ∙ r y ∙ r z) ⁻¹ ∙ sub K (r x ∙ r y ∙ r z)) ≈⟨ {!!} ⟩ + -- sub K (r x ∙ r y ∙ r z ) ≈⟨ {!!} ⟩ + -- sub K (r x ∙ (r y ∙ r z ∙ sub K (r y ∙ r z) ⁻¹ ∙ sub K (r y ∙ r z)) ∙ + -- sub K (r x ∙ (r y ∙ r z ∙ sub K (r y ∙ r z) ⁻¹ ∙ sub K (r y ∙ r z))) ⁻¹ ∙ + -- sub K (r x ∙ (r y ∙ r z ∙ sub K (r y ∙ r z) ⁻¹ ∙ sub K (r y ∙ r z)))) ∎ + identity1 : ( (x : CosetCarrier G K ) → sub K (r (φ {G} {K} (r (φ {G} {K} ε) ∙ r x))) ≈ sub K (r x) ) + × ( ( x : CosetCarrier G K ) → sub K (r (φ {G} {K} (r x ∙ r (φ {G} {K} ε)))) ≈ sub K (r x) ) + inverse1 : Inverse (λ x y → sub K (r x) ≈ sub K (r y)) (φ {G} {K}ε) (λ x → φ {G} {K}(r x ⁻¹)) (λ x y → φ {G} {K}(r x ∙ r y)) + ⁻¹-cong1 : Congruent₁ (λ x y → sub K (r x) ≈ sub K (r y)) (λ x → φ {G} {K}(r x ⁻¹)) -- K ⊂ ker(f) K⊆ker : (G H : Group c l) (K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set ( c Level.⊔ l ) @@ -153,24 +154,25 @@ ; unique = unique } where open Group H + EqH = IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup + (IsGroup.isMonoid isGroup ))) + EqG = IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup + (IsGroup.isMonoid (Group.isGroup G) ))) h1 : {x : Group.Carrier G } → Coset G K x → Carrier - h1 (coset a b) = f b - h1 (cscong eq t) = h1 t + h1 (coset a b) = f (sub K b) h : CosetCarrier G K → Carrier -- G / K → H h r = h1 (isCoset r) _o_ = Group._∙_ G + open EqReasoning (Algebra.Group.setoid H ) h03 : (x y : Group.Carrier (G / K ) ) → h ( Group._∙_ (G / K ) x y ) ≈ h x ∙ h y h03 x y = h13 (isCoset x) (isCoset y) where h13 : {gx gy : Group.Carrier G } → ( x : Coset G K gx ) ( y : Coset G K gy ) → h (Group._∙_ (G / K) record { r = gx ; isCoset = x } record {r = gy ; isCoset = y } ) ≈ h1 x ∙ h1 y h13 (coset a b) (coset c d) = begin - h1 (coset (a o c) (b o d) ) ≈⟨ {!!} ⟩ - f (b o d) ≈⟨ {!!} ⟩ - f b ∙ f d ≈⟨ {!!} ⟩ - h1 (coset a b) ∙ h1 (coset c d) ∎ where open EqReasoning (Algebra.Group.setoid H ) - h13 (coset a b) (cscong x y) = {!!} - h13 (cscong x x₁) (coset a b) = {!!} - h13 (cscong x x₁) (cscong x₂ y) = {!!} + h (φ {G} {K} ((a o sub K b) o (c o sub K d) )) ≈⟨ IsEquivalence.refl EqH ⟩ + f (sub K (( a o sub K b ) o (c o sub K d ))) ≈⟨ {!!} ⟩ + f (sub K b) ∙ f (sub K d) ≈⟨ IsEquivalence.refl EqH ⟩ + h1 (coset a b) ∙ h1 (coset c d) ∎ h-homo : IsGroupHomomorphism (Group→Raw (G / K) ) (Group→Raw H) h h-homo = record { isMonoidHomomorphism = record { @@ -180,7 +182,9 @@ ; ε-homo = {!!} } ; ⁻¹-homo = {!!} } unique : (x : Group.Carrier G) → f x ≈ h ( φ x ) - unique x = Algebra.Group.refl H + unique x = begin + f x ≈⟨ {!!} ⟩ + f (sub K x ) ∎