Mercurial > hg > Members > kono > Proof > galois
changeset 187:c22ef5bc695a
remove gen/uni from Commutator
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 28 Nov 2020 10:08:51 +0900 |
| parents | 3c7e8855996f |
| children | 9e0d946d35b6 |
| files | FLComm.agda Solvable.agda |
| diffstat | 2 files changed, 6 insertions(+), 20 deletions(-) [+] |
line wrap: on
line diff
--- a/FLComm.agda Fri Nov 27 20:54:55 2020 +0900 +++ b/FLComm.agda Sat Nov 28 10:08:51 2020 +0900 @@ -49,22 +49,16 @@ CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i ) CommStage→ zero x (Level.lift tt) = AnyFList (perm→FL x) -CommStage→ (suc i) ε uni = comm0 (CommFListN i) (CommStage→ i ε deriving-ε) where - comm0 : (L : FList n) → Any (_≡_ (perm→FL ε)) L → Any (_≡_ (perm→FL ε)) (tl2 L L []) - comm0 = {!!} -CommStage→ (suc i) .( [ g , h ] ) (comm {g} {h} p q) = comm2 (CommFListN i) (CommStage→ i g p) (CommStage→ i h q) where +CommStage→ (suc i) .( [ g , h ] ) (comm {g} {h} p q) = comm2 (CommFListN i) (CommFListN i) (CommStage→ i g p) (CommStage→ i h q) where G = perm→FL g H = perm→FL h - comm2 : (L : FList n) → Any (G ≡_) L → Any (H ≡_) L → Any (perm→FL [ g , h ] ≡_) (tl2 L L []) - comm2 L a b = {!!} -CommStage→ (suc i) .(f ∘ₚ g) (gen {f} {g} p q) = comm3 (CommFListN i) (CommStage→ i f {!!}) (CommStage→ i g {!!}) where - G = perm→FL f - H = perm→FL g - comm3 : (L : FList n) → Any (G ≡_) L → Any (H ≡_) L → Any (perm→FL (f ∘ₚ g) ≡_) (tl2 L L []) - comm3 L a b = {!!} + comm2 : (L L1 : FList n) → Any (G ≡_) L → Any (H ≡_) L1 → Any (perm→FL [ g , h ] ≡_) (tl2 L L1 []) + comm2 (cons G L xr) (cons H L1 yr) (here refl) (here refl) = {!!} + comm2 (cons x L xr) (cons y L1 yr) (here x₁) (there b) = {!!} + comm2 (cons x L xr) (cons y L1 yr) (there a) b = {!!} CommStage→ (suc i) x (ccong {f} {x} eq p) = subst (λ k → Any (k ≡_) (tl2 (CommFListN i) (CommFListN i) [])) (comm4 eq) (CommStage→ (suc i) f p ) where comm4 : f =p= x → perm→FL f ≡ perm→FL x - comm4 = {!!} + 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/Solvable.agda Fri Nov 27 20:54:55 2020 +0900 +++ b/Solvable.agda Sat Nov 28 10:08:51 2020 +0900 @@ -19,9 +19,7 @@ [ g , h ] = g ⁻¹ ∙ h ⁻¹ ∙ g ∙ h data Commutator (P : Carrier → Set (Level.suc n ⊔ m)) : (f : Carrier) → Set (Level.suc n ⊔ m) where - uni : Commutator P ε comm : {g h : Carrier} → P g → P h → Commutator P [ g , h ] - gen : {f g : Carrier} → Commutator P f → Commutator P g → Commutator P ( f ∙ g ) ccong : {f g : Carrier} → f ≈ g → Commutator P f → Commutator P g deriving : ( i : ℕ ) → Carrier → Set (Level.suc n ⊔ m) @@ -58,15 +56,9 @@ [ g , h ] ⁻¹ ∎ -deriving-mul : { i : ℕ } → { x y : Carrier } → deriving i x → deriving i y → deriving i ( x ∙ y ) -deriving-mul {zero} {x} {y} _ _ = lift tt -deriving-mul {suc i} {x} {y} ix iy = gen ix iy - deriving-inv : { i : ℕ } → { x : Carrier } → deriving i x → deriving i ( x ⁻¹ ) deriving-inv {zero} {x} (lift tt) = lift tt -deriving-inv {suc i} {ε} uni = ccong lemma3 uni deriving-inv {suc i} {_} (comm x x₁ ) = ccong (lemma4 _ _) (comm x₁ x) -deriving-inv {suc i} {_} (gen x x₁ ) = ccong (lemma5 _ _ ) ( gen (deriving-inv x₁) (deriving-inv x)) deriving-inv {suc i} {x} (ccong eq ix ) = ccong (⁻¹-cong eq) ( deriving-inv ix ) idcomtr : (g : Carrier ) → [ g , ε ] ≈ ε