Mercurial > hg > Members > kono > Proof > galois
changeset 269:0452e7021054
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 31 May 2022 13:34:40 +0900 |
| parents | 86408a621c6e |
| children | 0081e1ed5ead |
| files | src/Fundamental.agda |
| diffstat | 1 files changed, 11 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Fundamental.agda Tue May 31 12:42:57 2022 +0900 +++ b/src/Fundamental.agda Tue May 31 13:34:40 2022 +0900 @@ -13,6 +13,8 @@ open GroupMorphisms open import Gutil0 +open import Tactic.MonoidSolver using (solve; solve-macro) + -- -- Given two groups G and H and a group homomorphism f : G → H, -- let K be a normal subgroup in G and φ the natural surjective homomorphism G → G/K @@ -104,7 +106,8 @@ mbase {x} {y} = begin sub K ((ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙ (ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹ ∙ - sub K (base1 (x ε) ∙ base1 (y ε)))) ≈⟨ {!!} ⟩ + sub K (base1 (x ε) ∙ base1 (y ε)))) ≈⟨ {!!} ⟩ + {!!} ≈⟨ ⟦⟧-cong (solve (Algebra.Group.monoid G)) ⟩ sub K ( ((ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙ (ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹ )) ∙ (base1 (x ε) ∙ base1 (y ε))) ≈⟨ ⟦⟧-cong ( ∙-cong ( @@ -125,7 +128,13 @@ sub K (base y ∙ base v) ≈⟨ {!!} ⟩ sub K (base (mul y v)) ∎ assoc1 : (x y z : COSET G K) → sub K (base (mul (mul x y ) z)) ≈ sub K (base (mul x ( mul y z ) )) - assoc1 x y z = {!!} + assoc1 x y z = begin + sub K (base (mul (mul x y ) z)) ≈⟨ {!!} ⟩ + sub K (base (mul x y ) ∙ base z) ≈⟨ {!!} ⟩ + sub K ((base x ∙ base y ) ∙ base z) ≈⟨ {!!} ⟩ + sub K (base x ∙ ( base y ∙ base z)) ≈⟨ {!!} ⟩ + sub K (base x ∙ base (mul x y )) ≈⟨ {!!} ⟩ + sub K (base (mul x ( mul y z ))) ∎ -- crefl1 (coset a b) = ⟦⟧-cong (grefl G) -- K ⊂ ker(f)