Mercurial > hg > Members > kono > Proof > galois
changeset 12:d960f2ea902f
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 17 Aug 2020 15:12:17 +0900 |
| parents | 9dae7ef74342 |
| children | e0d16960d10d |
| files | Solvable.agda |
| diffstat | 1 files changed, 39 insertions(+), 14 deletions(-) [+] |
line wrap: on
line diff
--- a/Solvable.agda Mon Aug 17 14:40:54 2020 +0900 +++ b/Solvable.agda Mon Aug 17 15:12:17 2020 +0900 @@ -95,23 +95,48 @@ mpf p (mpf q (mpf r ε)) ∎ where open EqReasoning (Algebra.Group.setoid G) +mpg : {x : Carrier } → (m : MP x ) → Carrier → Carrier +mpg {x} (am x) y = y ∙ x +mpg (m o m₁) y = mpf m₁ ( mpf m y ) + +mp-flatten-g : {x : Carrier } → (m : MP x ) → Carrier +mp-flatten-g {x} m = mpg {x} m ε + +∙-flatten-g : {x : Carrier } → (m : MP x ) → x ≈ mp-flatten-g m +∙-flatten-g {x} (am x) = gsym (proj₁ identity _) +∙-flatten-g {_} (am x o q) = {!!} -- ∙-cong ( ∙-flatten-g q ) grefl +∙-flatten-g (_o_ {_} {z} (_o_ {x} {y} p q) r) = lemma9 _ _ _ {!!} ( ∙-flatten-g {z} r ) where + mp-cong : {p q r : Carrier} → (P : MP p) → q ≈ r → mpg P q ≈ mpg P r + mp-cong (am x) q=r = {!!} -- ∙-cong grefl q=r + mp-cong (P o P₁) q=r = {!!} -- mp-cong P ( mp-cong P₁ q=r ) + mp-assoc : {p q r : Carrier} → (P : MP p) → mpg P q ∙ r ≈ mpg P (q ∙ r ) + mp-assoc (am x) = {!!} -- assoc _ _ _ + mp-assoc {p} {q} {r} (P o P₁) = begin + {!!} ≈⟨ {!!} ⟩ + {!!} + ∎ where open EqReasoning (Algebra.Group.setoid G) + lemma9 : (x y z : Carrier) → x ∙ y ≈ mpg p (mpg q ε) → z ≈ mpg r ε → x ∙ y ∙ z ≈ mp-flatten-g ((p o q) o r) + lemma9 x y z t s = begin + {!!} ≈⟨ {!!} ⟩ + {!!} + ∎ where open EqReasoning (Algebra.Group.setoid G) + +tet1 : (f g : Carrier ) → {!!} +tet1 f g = mp-flatten-g ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ ))) + +tet2 : (f g : Carrier ) → {!!} +tet2 f g = mp-flatten ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ ))) lemma5 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹ lemma5 f g = begin - g ⁻¹ ∙ f ⁻¹ ≈⟨ gsym (proj₂ identity _) ⟩ - g ⁻¹ ∙ f ⁻¹ ∙ ε ≈⟨ gsym (∙-cong grefl (proj₂ inverse _ )) ⟩ - g ⁻¹ ∙ f ⁻¹ ∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ ) ≈⟨ assoc _ _ _ ⟩ - g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ g ∙ (f ∙ g) ⁻¹)) ≈⟨ ∙-cong grefl (gsym (assoc _ _ _)) ⟩ - g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ g) ∙ (f ∙ g) ⁻¹) ≈⟨ gsym ( assoc _ _ _) ⟩ - g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ g)) ∙ (f ∙ g) ⁻¹ ≈⟨ ∙-cong (gsym (assoc _ _ _ )) grefl ⟩ - (g ⁻¹ ∙ f ⁻¹) ∙ (f ∙ g) ∙ (f ∙ g) ⁻¹ ≈⟨ ∙-cong (assoc _ _ _ ) grefl ⟩ - (g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ g))) ∙ (f ∙ g) ⁻¹ ≈⟨ ∙-cong (∙-cong grefl (gsym (assoc _ _ _ )) ) grefl ⟩ - (g ⁻¹ ∙ ((f ⁻¹ ∙ f) ∙ g)) ∙ (f ∙ g) ⁻¹ ≈⟨ ∙-cong (gsym (assoc _ _ _ )) grefl ⟩ - (g ⁻¹ ∙ (f ⁻¹ ∙ f) ∙ g) ∙ (f ∙ g) ⁻¹ ≈⟨ ∙-cong (assoc _ _ _) grefl ⟩ - g ⁻¹ ∙ ((f ⁻¹ ∙ f) ∙ g) ∙ (f ∙ g) ⁻¹ ≈⟨ ∙-cong (∙-cong grefl (∙-cong (proj₁ inverse _ ) grefl )) grefl ⟩ - g ⁻¹ ∙ (ε ∙ g) ∙ (f ∙ g) ⁻¹ ≈⟨ ∙-cong (∙-cong grefl ( proj₁ identity _) ) grefl ⟩ - g ⁻¹ ∙ g ∙ (f ∙ g) ⁻¹ ≈⟨ ∙-cong (proj₁ inverse _) grefl ⟩ - ε ∙ (f ∙ g) ⁻¹ ≈⟨ proj₁ identity _ ⟩ + g ⁻¹ ∙ f ⁻¹ ≈⟨ gsym (proj₂ identity _) ⟩ + g ⁻¹ ∙ f ⁻¹ ∙ ε ≈⟨ gsym (∙-cong grefl (proj₂ inverse _ )) ⟩ + g ⁻¹ ∙ f ⁻¹ ∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ ) ≈⟨ ∙-flatten ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ ))) ⟩ + g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)))) ≈⟨ ∙-cong grefl (gsym (assoc _ _ _ )) ⟩ + g ⁻¹ ∙ ((f ⁻¹ ∙ f) ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))) ≈⟨ ∙-cong grefl (gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _)) ⟩ + g ⁻¹ ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)) ≈⟨ gsym (assoc _ _ _) ⟩ + (g ⁻¹ ∙ g ) ∙ ((f ∙ g) ⁻¹ ∙ ε) ≈⟨ gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _) ⟩ + (f ∙ g) ⁻¹ ∙ ε ≈⟨ proj₂ identity _ ⟩ (f ∙ g) ⁻¹ ∎ where open EqReasoning (Algebra.Group.setoid G)