Mercurial > hg > Members > kono > Proof > galois
changeset 3:6e77fefcbe41
Permutation Group
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 16 Aug 2020 16:03:23 +0900 |
| parents | 1b73893387c0 |
| children | 121213cfc85a |
| files | PermAbel.agda PermGroup.agda |
| diffstat | 2 files changed, 89 insertions(+), 101 deletions(-) [+] |
line wrap: on
line diff
--- a/PermAbel.agda Sun Aug 16 13:50:07 2020 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,101 +0,0 @@ -module PermAbel where - -open import Level hiding ( suc ; zero ) -open import Algebra -open import Algebra.Structures -open import Data.Fin -open import Data.Fin.Permutation -open import Function hiding (id ; flip) -open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) -open import Function.LeftInverse using ( _LeftInverseOf_ ) -open import Function.Equality using (Π) -open import Data.Nat using (ℕ; suc; zero) -open import Relation.Binary.PropositionalEquality - -f1 : Fin 3 → Fin 3 -f1 zero = suc (suc zero) -f1 (suc zero) = zero -f1 (suc (suc zero)) = suc zero - -lemma1 : Permutation 3 3 -lemma1 = permutation f1 ( f1 ∘ f1 ) lemma2 where - lemma3 : (x : Fin 3 ) → f1 (f1 (f1 x)) ≡ x - lemma3 zero = refl - lemma3 (suc zero) = refl - lemma3 (suc (suc zero)) = refl - lemma2 : :→-to-Π (λ x → f1 (f1 x)) InverseOf :→-to-Π f1 - lemma2 = record { left-inverse-of = λ x → lemma3 x ; right-inverse-of = λ x → lemma3 x } - -fid : {p : ℕ } → Fin p → Fin p -fid x = x - --- Data.Fin.Permutation.id -pid : {p : ℕ } → Permutation p p -pid = permutation fid fid record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl } - --- Data.Fin.Permutation.flip -pinv : {p : ℕ } → Permutation p p → Permutation p p -pinv {p} P = permutation (_⟨$⟩ˡ_ P) (_⟨$⟩ʳ_ P ) record { left-inverse-of = λ x → inverseʳ P ; right-inverse-of = λ x → inverseˡ P } - -open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) - -PPP0 : {p : ℕ } (P : Permutation p p ) (x : Fin p) → (_⟨$⟩ˡ_ P) ((_⟨$⟩ʳ_ P) x) ≡ x -PPP0 P x = inverseˡ P - -PPP1 : {p : ℕ } (P : Permutation p p ) (x : Fin p) → (_⟨$⟩ʳ_ P) ((_⟨$⟩ˡ_ P) x) ≡ x -PPP1 P x = inverseʳ P - -p-≅ : {p : ℕ } → {f0 g0 f1 g1 : Fin p → Fin p } → f0 ≡ f1 → g0 ≡ g1 - → {fg0 : (x : Fin p ) → f0 (g0 x) ≡ x } → {fg1 : (x : Fin p ) → f1 (g1 x) ≡ x } - → {gf0 : (x : Fin p ) → g0 (f0 x) ≡ x } → {gf1 : (x : Fin p ) → g1 (f1 x) ≡ x } - → fg0 ≅ fg1 → gf0 ≅ gf1 → permutation f0 g0 record { left-inverse-of = gf0 ; right-inverse-of = fg0 } - ≡ permutation f1 g1 record { left-inverse-of = gf1 ; right-inverse-of = fg1 } -p-≅ refl refl HE.refl HE.refl = refl - -p-≅' : {p : ℕ } → {f0 g0 f1 g1 : Fin p → Fin p } → f0 ≡ f1 → g0 ≡ g1 - → {fg0 : (x : Fin p ) → f0 (g0 x) ≡ x } → {fg1 : (x : Fin p ) → f1 (g1 x) ≡ x } - → {gf0 : (x : Fin p ) → g0 (f0 x) ≡ x } → {gf1 : (x : Fin p ) → g1 (f1 x) ≡ x } - → fg0 ≅ fg1 → gf0 ≅ gf1 → record { to = →-to-⟶ f0 ; from = →-to-⟶ g0 ; inverse-of = record { left-inverse-of = gf0 ; right-inverse-of = fg0 } } - ≡ record { to = →-to-⟶ f1 ; from = →-to-⟶ g1 ; inverse-of = record { left-inverse-of = gf1 ; right-inverse-of = fg1 } } -p-≅' refl refl HE.refl HE.refl = refl - -Pp : {p : ℕ } → (P : Permutation p p ) → P ≡ record { to = →-to-⟶ (_⟨$⟩ʳ_ P ) ; from = →-to-⟶ (_⟨$⟩ˡ_ P ) - ; inverse-of = record { left-inverse-of = λ x → inverseˡ P ; right-inverse-of = λ x → inverseʳ P } } -Pp P = {!!} - -p-≡ : {p : ℕ } → (x y : Permutation p p ) → (_⟨$⟩ˡ_ x) ≡ (_⟨$⟩ˡ_ y) → (_⟨$⟩ʳ_ x ) ≡ (_⟨$⟩ʳ_ y ) → x ≡ y -p-≡ x y refl refl = lemma2 where - lemma3 : {p : ℕ } {i j : Fin p} {x y : Permutation p p } → i ≡ j - → (eq1 : Inverse.to x Π.⟨$⟩ i ≡ Inverse.to x Π.⟨$⟩ j ) - → (eq2 : Inverse.to y Π.⟨$⟩ i ≡ Inverse.to y Π.⟨$⟩ j ) → eq1 ≅ eq2 - lemma3 refl refl refl = ? - lemma4 : {p : ℕ } {i j : Fin p} {x y : Permutation p p } → i ≡ j → (p q : Inverse.from y Π.⟨$⟩ i ≡ Inverse.from y Π.⟨$⟩ j ) → p ≡ q - lemma4 refl refl refl = refl - lemma2 : record { to = record { _⟨$⟩_ = Π._⟨$⟩_ (Inverse.to y) ; cong = {!!} } ; - from = record { _⟨$⟩_ = Π._⟨$⟩_ (Inverse.from y) ; cong = {!!} } ; inverse-of = Inverse.Inverse.inverse-of x } ≡ y - lemma2 = {!!} - - -pgroup : ℕ → AbelianGroup Level.zero Level.zero -pgroup p = record { - Carrier = Permutation p p - ; _≈_ = _≡_ - ; _∙_ = _∘ₚ_ - ; ε = pid - ; _⁻¹ = pinv - ; isAbelianGroup = record { isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record { - isEquivalence = record {refl = refl ; trans = trans ; sym = sym} - ; ∙-cong = presp } - ; assoc = passoc } - ; identity = {!!} } - ; inverse = {!!} - ; ⁻¹-cong = {!!} - } ; comm = {!!} - } - } where - presp : {x y u v : Permutation p p } → x ≡ y → u ≡ v → (x ∘ₚ u) ≡ (y ∘ₚ v) - presp refl refl = refl - passoc : (x y z : Permutation p p) → ((x ∘ₚ y) ∘ₚ z) ≡ (x ∘ₚ (y ∘ₚ z)) - passoc x y z = p-≡ _ _ refl refl - -
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/PermGroup.agda Sun Aug 16 16:03:23 2020 +0900 @@ -0,0 +1,89 @@ +module PermAbel where + +open import Level hiding ( suc ; zero ) +open import Algebra +open import Algebra.Structures +open import Data.Fin +open import Data.Product +open import Data.Fin.Permutation +open import Function hiding (id ; flip) +open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) +open import Function.LeftInverse using ( _LeftInverseOf_ ) +open import Function.Equality using (Π) +open import Data.Nat using (ℕ; suc; zero) +open import Relation.Binary.PropositionalEquality + +f1 : Fin 3 → Fin 3 +f1 zero = suc (suc zero) +f1 (suc zero) = zero +f1 (suc (suc zero)) = suc zero + +lemma1 : Permutation 3 3 +lemma1 = permutation f1 ( f1 ∘ f1 ) lemma2 where + lemma3 : (x : Fin 3 ) → f1 (f1 (f1 x)) ≡ x + lemma3 zero = refl + lemma3 (suc zero) = refl + lemma3 (suc (suc zero)) = refl + lemma2 : :→-to-Π (λ x → f1 (f1 x)) InverseOf :→-to-Π f1 + lemma2 = record { left-inverse-of = λ x → lemma3 x ; right-inverse-of = λ x → lemma3 x } + +fid : {p : ℕ } → Fin p → Fin p +fid x = x + +-- Data.Fin.Permutation.id +pid : {p : ℕ } → Permutation p p +pid = permutation fid fid record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl } + +-- Data.Fin.Permutation.flip +pinv : {p : ℕ } → Permutation p p → Permutation p p +pinv {p} P = permutation (_⟨$⟩ˡ_ P) (_⟨$⟩ʳ_ P ) record { left-inverse-of = λ x → inverseʳ P ; right-inverse-of = λ x → inverseˡ P } + +record _=p=_ {p : ℕ } ( x y : Permutation p p ) : Set where + field + peq : ( q : Fin p ) → x ⟨$⟩ʳ q ≡ y ⟨$⟩ʳ q + +open _=p=_ + +prefl : {p : ℕ } { x : Permutation p p } → x =p= x +peq (prefl {p} {x}) q = refl + +psym : {p : ℕ } { x y : Permutation p p } → x =p= y → y =p= x +peq (psym {p} {x} {y} eq ) q = sym (peq eq q) + +ptrans : {p : ℕ } { x y z : Permutation p p } → x =p= y → y =p= z → x =p= z +peq (ptrans {p} {x} {y} x=y y=z ) q = trans (peq x=y q) (peq y=z q) + +pgroup : ℕ → Group Level.zero Level.zero +pgroup p = record { + Carrier = Permutation p p + ; _≈_ = _=p=_ + ; _∙_ = _∘ₚ_ + ; ε = pid + ; _⁻¹ = pinv + ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record { + isEquivalence = record {refl = prefl ; trans = ptrans ; sym = psym } + ; ∙-cong = presp } + ; assoc = passoc } + ; identity = ( (λ q → record { peq = λ q → refl } ) , (λ q → record { peq = λ q → refl } )) } + ; inverse = ( (λ x → record { peq = λ q → inverseʳ x} ) , (λ x → record { peq = λ q → inverseˡ x} )) + ; ⁻¹-cong = λ i=j → record { peq = λ q → p-inv i=j q } + } + } where + presp : {x y u v : Permutation p p } → x =p= y → u =p= v → (x ∘ₚ u) =p= (y ∘ₚ v) + presp {x} {y} {u} {v} x=y u=v = record { peq = λ q → lemma4 q } where + lemma4 : (q : Fin p) → ((x ∘ₚ u) ⟨$⟩ʳ q) ≡ ((y ∘ₚ v) ⟨$⟩ʳ q) + lemma4 q = trans (cong (λ k → Inverse.to u Π.⟨$⟩ k) (peq x=y q) ) (peq u=v _ ) + passoc : (x y z : Permutation p p) → ((x ∘ₚ y) ∘ₚ z) =p= (x ∘ₚ (y ∘ₚ z)) + passoc x y z = record { peq = λ q → refl } + p-inv : {i j : Permutation p p} → i =p= j → (q : Fin p) → pinv i ⟨$⟩ʳ q ≡ pinv j ⟨$⟩ʳ q + p-inv {i} {j} i=j q = begin + i ⟨$⟩ˡ q + ≡⟨ cong (λ k → i ⟨$⟩ˡ k) (sym (inverseʳ j) ) ⟩ + i ⟨$⟩ˡ ( j ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) + ≡⟨ cong (λ k → i ⟨$⟩ˡ k) (sym (peq i=j _ )) ⟩ + i ⟨$⟩ˡ ( i ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) + ≡⟨ inverseˡ i ⟩ + j ⟨$⟩ˡ q + ∎ where open ≡-Reasoning + +