Mercurial > hg > Members > kono > Proof > galois
changeset 330:1ff0b95e437f default tip
try to add --cubical-compatible on Solvable
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 12 Oct 2023 10:12:16 +0900 |
| parents | 5d7a811ee428 |
| children | |
| files | src/FLComm.agda src/Homomorphism.agda src/Solvable.agda src/sym2.agda src/sym5h.agda |
| diffstat | 5 files changed, 87 insertions(+), 79 deletions(-) [+] |
line wrap: on
line diff
--- a/src/FLComm.agda Sun Sep 24 18:10:44 2023 +0900 +++ b/src/FLComm.agda Thu Oct 12 10:12:16 2023 +0900 @@ -1,4 +1,4 @@ -{-# OPTIONS --safe #-} -- cannot use --cubical-compatible because of Solvable +{-# OPTIONS --cubical-compatible --safe #-} open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n ) module FLComm (n : ℕ) where @@ -152,23 +152,20 @@ CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) (CommFListN i) CommStage→ zero x (Level.lift tt) = anyP (anyFL n) (perm→FL x) -CommStage→ (suc i) .( [ g , h ] ) (comm {g} {h} p q) = comm2 where +CommStage→ (suc i) ix (comm {g} {h} p q eq ) = comm2 where G = perm→FL g H = perm→FL h - comm3 : perm→FL [ FL→perm G , FL→perm H ] ≡ perm→FL [ g , h ] + comm3 : perm→FL [ FL→perm G , FL→perm H ] ≡ perm→FL ix comm3 = begin perm→FL [ FL→perm G , FL→perm H ] ≡⟨ pcong-pF (comm-resp (FL←iso _) (FL←iso _)) ⟩ perm→FL [ g , h ] + ≡⟨ pcong-pF (psym eq) ⟩ + perm→FL ix ∎ where open ≡-Reasoning - comm2 : Any (_≡_ (perm→FL [ g , h ])) (CommFListN (suc i)) + comm2 : Any (_≡_ (perm→FL ix)) (CommFListN (suc i)) comm2 = subst (λ k → Any (_≡_ k) (CommFListN (suc i)) ) comm3 ( commAny ( anyComm (CommFListN i) (CommFListN i) (λ p q → perm→FL [ FL→perm p , FL→perm q ] )) G H (CommStage→ i g p) (CommStage→ i h q) ) -CommStage→ (suc i) x (ccong {f} {x} eq p) = - subst (λ k → Any (k ≡_) (commList (anyComm ( CommFListN i ) ( CommFListN i ) (λ p q → perm→FL [ FL→perm p , FL→perm q ] )))) - (comm4 eq) (CommStage→ (suc i) f p ) where - comm4 : f =p= x → perm→FL f ≡ perm→FL x - comm4 = pcong-pF CommSolved : (x : Permutation n n) → (y : FList n) → y ≡ FL0 ∷# [] → (FL→perm (FL0 {n}) =p= pid ) → Any (perm→FL x ≡_) y → x =p= pid CommSolved x .(cons FL0 [] (Level.lift tt)) refl eq0 (here eq) = FLpid _ eq eq0
--- a/src/Homomorphism.agda Sun Sep 24 18:10:44 2023 +0900 +++ b/src/Homomorphism.agda Thu Oct 12 10:12:16 2023 +0900 @@ -293,7 +293,7 @@ f x ≈⟨ h1-is-solution _ ⟩ h1 x ∎ -- --- Another from of Fundamental Homomorphism Theorm +-- Another form of Fundamental Homomorphism Theorm -- i.e. G / Ker f ≈ Im f record IsImage {c d : Level} (G : Group c d) (H : Group c d)
--- a/src/Solvable.agda Sun Sep 24 18:10:44 2023 +0900 +++ b/src/Solvable.agda Thu Oct 12 10:12:16 2023 +0900 @@ -1,4 +1,4 @@ -{-# OPTIONS --safe #-} -- we cannot use --cubical-compatible because of Termination +{-# OPTIONS --cubical-compatible --safe #-} open import Level hiding ( suc ; zero ) open import Algebra @@ -21,18 +21,17 @@ [ g , h ] = g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h data Commutator (P : Carrier → Set (Level.suc n ⊔ m)) : (f : Carrier) → Set (Level.suc n ⊔ m) where - comm : {g h : Carrier} → P g → P h → Commutator P [ g , h ] - ccong : {f g : Carrier} → f ≈ g → Commutator P f → Commutator P g + comm : {g h i : Carrier} → P g → P h → i ≈ [ g , h ] → Commutator P i deriving : ( i : ℕ ) → Carrier → Set (Level.suc n ⊔ m) deriving 0 x = Lift (Level.suc n ⊔ m) ⊤ deriving (suc i) x = Commutator (deriving i) x -open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) +-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) deriving-subst : { i : ℕ } → {x y : Carrier } → x ≈ y → (dx : deriving i x ) → deriving i y deriving-subst {zero} {x} {y} x=y dx = lift tt -deriving-subst {suc i} {x} {y} x=y dx = ccong x=y dx +deriving-subst {suc i} {x} {y} x=y (comm ig ih x=gh) = comm ig ih (gtrans (gsym x=y) x=gh) record solvable : Set (Level.suc n ⊔ m) where field @@ -62,8 +61,7 @@ deriving-inv : { i : ℕ } → { x : Carrier } → deriving i x → deriving i ( x ⁻¹ ) deriving-inv {zero} {x} (lift tt) = lift tt -deriving-inv {suc i} {_} (comm x x₁ ) = ccong (lemma4 _ _) (comm x₁ x) -deriving-inv {suc i} {x} (ccong eq ix ) = ccong (⁻¹-cong eq) ( deriving-inv ix ) +deriving-inv {suc i} {x} (comm ig ih x=gh ) = comm ih ig (gtrans (⁻¹-cong x=gh) (gsym (lemma4 _ _))) idcomtr : (g : Carrier ) → [ g , ε ] ≈ ε idcomtr g = begin @@ -85,7 +83,7 @@ deriving-ε : { i : ℕ } → deriving i ε deriving-ε {zero} = lift tt -deriving-ε {suc i} = ccong (idcomtr ε) (comm deriving-ε deriving-ε) +deriving-ε {suc i} = comm (deriving-ε {i}) (deriving-ε {i}) (gsym (idcomtr ε)) comm-refl : {f g : Carrier } → f ≈ g → [ f , g ] ≈ ε comm-refl {f} {g} f=g = begin @@ -111,7 +109,9 @@ Pcomm : {a b : Carrier} → (i : ℕ) → deriving i a → deriving i (b ∙ (a ∙ b ⁻¹ )) Pcomm {a} {b} zero (lift tt) = lift tt -Pcomm {.([ _ , _ ])} {b} (suc i) (comm {g} {h} pg ph ) = ccong cc2 (comm (Pcomm {_} {b} i pg) (Pcomm {_} {b} i ph)) where +Pcomm {a} {b} (suc i) (comm {g} {h} pg ph eq ) = comm (Pcomm {_} {b} i pg) (Pcomm {_} {b} i ph) (gtrans cc3 (gsym cc2)) where + cc3 : b ∙ (a ∙ b ⁻¹) ≈ b ∙ ([ g , h ] ∙ b ⁻¹) + cc3 = cdr (car eq ) cc2 : [ b ∙ (g ∙ b ⁻¹) , b ∙ (h ∙ b ⁻¹) ] ≈ b ∙ ([ g , h ] ∙ b ⁻¹) cc2 = begin [ b ∙ (g ∙ b ⁻¹) , b ∙ (h ∙ b ⁻¹) ] ≈⟨ grefl ⟩ @@ -133,7 +133,6 @@ ((b ∙ g ⁻¹ ) ∙ h ⁻¹ ) ∙ (g ∙ (h ∙ b ⁻¹)) ≈⟨ solve monoid ⟩ b ∙ (( g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h ) ∙ b ⁻¹) ≈⟨ grefl ⟩ b ∙ ([ g , h ] ∙ b ⁻¹) ∎ -Pcomm {a} {b} (suc i) (ccong f=a pa) = ccong (∙-cong grefl (∙-cong f=a grefl)) (Pcomm {_} {b} (suc i) pa) -- Finitely Generated Commutator is normal subgroup of G
--- a/src/sym2.agda Sun Sep 24 18:10:44 2023 +0900 +++ b/src/sym2.agda Thu Oct 12 10:12:16 2023 +0900 @@ -1,4 +1,4 @@ -{-# OPTIONS --safe #-} +{-# OPTIONS --cubical-compatible --safe #-} open import Level hiding ( suc ; zero ) open import Algebra @@ -51,67 +51,79 @@ open _=p=_ open ≡-Reasoning + -- we cannot use sym2lem0 g h q with perm→FL g in g=00 | perm→FL h in h=00 + -- because of Panic: uncaught pattern violation + sym2lem0 : ( g h : Permutation 2 2 ) → (q : Fin 2) → ([ g , h ] ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q) sym2lem0 g h q with perm→FL g in g=00 | perm→FL h in h=00 - sym2lem0 g h q | zero :: (zero :: f0) | _ = begin - [ g , h ] ⟨$⟩ʳ q - ≡⟨⟩ - h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) - ≡⟨ cong (λ k → h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ k))) ((peqˡ sym2lem1 _ )) ⟩ - h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q ))) - ≡⟨ cong (λ k → h ⟨$⟩ʳ k ) (peq sym2lem1 _ ) ⟩ - h ⟨$⟩ʳ (pid ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q ))) - ≡⟨⟩ - [ pid , h ] ⟨$⟩ʳ q - ≡⟨ peq (idcomtl h) q ⟩ - q - ∎ where - sym2lem1 : g =p= pid - sym2lem1 = FL-inject g=00 - sym2lem0 g h q | t | zero :: (zero :: f0) = begin - [ g , h ] ⟨$⟩ʳ q - ≡⟨⟩ - h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) - ≡⟨ peq sym2lem2 _ ⟩ - pid ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) - ≡⟨ cong (λ k → pid ⟨$⟩ʳ (g ⟨$⟩ʳ k)) (peqˡ sym2lem2 _ ) ⟩ - pid ⟨$⟩ʳ (g ⟨$⟩ʳ ( pid ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) - ≡⟨⟩ - [ g , pid ] ⟨$⟩ʳ q - ≡⟨ peq (idcomtr g) q ⟩ - q - ∎ where - sym2lem2 : h =p= pid - sym2lem2 = FL-inject h=00 - sym2lem0 g h q | suc zero :: (zero :: f0) | suc zero :: (zero :: f0) = begin - [ g , h ] ⟨$⟩ʳ q - ≡⟨⟩ - h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) - ≡⟨ peq (psym g=h ) _ ⟩ - g ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) - ≡⟨ cong (λ k → g ⟨$⟩ʳ (g ⟨$⟩ʳ k) ) (peqˡ (psym g=h) _) ⟩ - g ⟨$⟩ʳ (g ⟨$⟩ʳ ( g ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) - ≡⟨ cong (λ k → g ⟨$⟩ʳ k) ( inverseʳ g ) ⟩ - g ⟨$⟩ʳ ( g ⟨$⟩ˡ q ) - ≡⟨ inverseʳ g ⟩ - q - ∎ where - g=h : g =p= h - g=h = FL-inject (trans g=00 (sym h=00)) - sym2lem0 g h q | s | t = ? + ... | s | t = ? + +-- sym2lem0 g h q | zero :: (zero :: f0) | _ = begin +-- [ g , h ] ⟨$⟩ʳ q +-- ≡⟨⟩ +-- h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) +-- ≡⟨ cong (λ k → h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ k))) ((peqˡ sym2lem1 _ )) ⟩ +-- h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q ))) +-- ≡⟨ cong (λ k → h ⟨$⟩ʳ k ) (peq sym2lem1 _ ) ⟩ +-- h ⟨$⟩ʳ (pid ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q ))) +-- ≡⟨⟩ +-- [ pid , h ] ⟨$⟩ʳ q +-- ≡⟨ peq (idcomtl h) q ⟩ +-- q +-- ∎ where +-- sym2lem1 : g =p= pid +-- sym2lem1 = FL-inject g=00 +-- sym2lem0 g h q | t | zero :: (zero :: f0) = begin +-- [ g , h ] ⟨$⟩ʳ q +-- ≡⟨⟩ +-- h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) +-- ≡⟨ peq sym2lem2 _ ⟩ +-- pid ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) +-- ≡⟨ cong (λ k → pid ⟨$⟩ʳ (g ⟨$⟩ʳ k)) (peqˡ sym2lem2 _ ) ⟩ +-- pid ⟨$⟩ʳ (g ⟨$⟩ʳ ( pid ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) +-- ≡⟨⟩ +-- [ g , pid ] ⟨$⟩ʳ q +-- ≡⟨ peq (idcomtr g) q ⟩ +-- q +-- ∎ where +-- sym2lem2 : h =p= pid +-- sym2lem2 = FL-inject h=00 +-- sym2lem0 g h q | suc zero :: (zero :: f0) | suc zero :: (zero :: f0) = begin +-- [ g , h ] ⟨$⟩ʳ q +-- ≡⟨⟩ +-- h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) +-- ≡⟨ peq (psym g=h ) _ ⟩ +-- g ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) +-- ≡⟨ cong (λ k → g ⟨$⟩ʳ (g ⟨$⟩ʳ k) ) (peqˡ (psym g=h) _) ⟩ +-- g ⟨$⟩ʳ (g ⟨$⟩ʳ ( g ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) +-- ≡⟨ cong (λ k → g ⟨$⟩ʳ k) ( inverseʳ g ) ⟩ +-- g ⟨$⟩ʳ ( g ⟨$⟩ˡ q ) +-- ≡⟨ inverseʳ g ⟩ +-- q +-- ∎ where +-- g=h : g =p= h +-- g=h = FL-inject (trans g=00 (sym h=00)) +-- sym2lem0 g h q | s | t = ? + solved : (x : Permutation 2 2) → Commutator (λ x₁ → Lift (Level.suc Level.zero) ⊤) x → x =p= pid - solved x (comm {g} {h} _ _) = record { peq = sym2lem0 g h } - solved x (ccong {f} {g} (record {peq = f=g}) d) with solved f d - ... | record { peq = f=e } = record { peq = λ q → cc q } where - cc : ( q : Fin 2 ) → x ⟨$⟩ʳ q ≡ q + solved x (comm {f} {g} _ _ eq ) = record { peq = cc } where + cc : (q : Fin 2) → x ⟨$⟩ʳ q ≡ pid ⟨$⟩ʳ q cc q = begin - x ⟨$⟩ʳ q - ≡⟨ sym (f=g q) ⟩ - f ⟨$⟩ʳ q - ≡⟨ f=e q ⟩ - q - ∎ where open ≡-Reasoning + x ⟨$⟩ʳ q ≡⟨ peq eq q ⟩ + [ f , g ] ⟨$⟩ʳ q ≡⟨ sym2lem0 f g q ⟩ + q ∎ where open ≡-Reasoning + + -- solved x (ccong {f} {g} (record {peq = f=g}) d) with solved f d +-- ... | record { peq = f=e } = record { peq = λ q → cc q } where +-- cc : ( q : Fin 2 ) → x ⟨$⟩ʳ q ≡ q +-- cc q = begin +-- x ⟨$⟩ʳ q +-- ≡⟨ sym (f=g q) ⟩ +-- f ⟨$⟩ʳ q +-- ≡⟨ f=e q ⟩ +-- q +-- ∎ where open ≡-Reasoning +-- -
--- a/src/sym5h.agda Sun Sep 24 18:10:44 2023 +0900 +++ b/src/sym5h.agda Thu Oct 12 10:12:16 2023 +0900 @@ -101,7 +101,7 @@ s12 : abc ≡ perm→FL [ dba , aec ] s12 = refl s11 : FL→perm abc =p= [ dba , aec ] - s11 = ptrans (pcong-Fp s12 ) (FL←iso _) + s11 = ptrans (pcong-Fp s12 ) ? -- (FL←iso _) s17 : deriving (suc i) ( FL→perm abc ) s17 = ccong (psym s11) (comm (Pcomm {_} {FL→perm dc} i (deriving-inv s10)) (Pcomm {_} {FL→perm be} i s10) )