Mercurial > hg > Members > kono > Proof > galois
changeset 267:864afb582fc7
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 31 May 2022 12:27:07 +0900 |
| parents | e6f9eb2bfc78 |
| children | 86408a621c6e |
| files | src/Fundamental.agda |
| diffstat | 1 files changed, 22 insertions(+), 24 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Fundamental.agda Tue May 31 11:18:05 2022 +0900 +++ b/src/Fundamental.agda Tue May 31 12:27:07 2022 +0900 @@ -52,7 +52,7 @@ x ∎ where open EqReasoning (Algebra.Group.setoid G ) base1 : {G : Group c l} {K : NormalSubGroup G} → {x : Group.Carrier G } → Coset G K x → Group.Carrier G -base1 {G} (coset a b) = a ⁻¹ ∙ b where open Group G +base1 {G} {K} {x} (coset a b) = a ⁻¹ ∙ x where open Group G -- x ≡ a ∙ sub K b base1 (cscong x y) = base1 y base : {G : Group c l} {K : NormalSubGroup G} → ( (g : Group.Carrier G )→ Coset G K g) → Group.Carrier G @@ -100,32 +100,30 @@ open Group G hiding (refl ; sym ; trans ) open EqReasoning (Algebra.Group.setoid G) open IsGroupHomomorphism (s-homo K ) - idem-base : {x : COSET G K} → sub K (sub K (base x)) ≈ sub K (base x ) - idem-base {x} = ib01 (x ε) where - ib01 : {a : Carrier } → (t : Coset G K a ) → sub K (sub K (base1 t)) ≈ sub K (base1 t ) - ib01 {y} (coset a b) = begin - sub K (sub K (base1 {G} {K} (coset a b))) ≈⟨ {!!} ⟩ - sub K (sub K (a ⁻¹ ∙ b)) ≈⟨ {!!} ⟩ - sub K (a ⁻¹ ∙ b) ≈⟨ {!!} ⟩ - sub K (base1 {G} {K} (coset a b)) ∎ - ib01 (cscong x t) = ib01 t mbase : {x y : COSET G K} → sub K (base (mul x y)) ≈ sub K (base x ∙ base y) - mbase {x} {y} = mbase1 (x ε) (y ε) where - mbase1 : {a b : Carrier } → Coset G K a → Coset G K b → sub K (base (mul x y)) ≈ sub K (base x ∙ base y) - mbase1 (coset a b) (coset a₁ b₁) = begin - sub K ((ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙ (base1 (x ε) ∙ base1 (y ε))) ≈⟨ {!!} ⟩ - sub K ((sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙ (base1 (x ε) ∙ base1 (y ε))) ≈⟨ {!!} ⟩ - sub K ((sub K (base1 (x ε) ∙ base1 (y ε))) ∙ (base1 (x ε) ∙ base1 (y ε))) ≈⟨ {!!} ⟩ - sub K (sub K (base1 (x ε)) ∙ sub K (base1 (y ε)) ∙ (base1 (x ε) ∙ base1 (y ε))) ≈⟨ {!!} ⟩ - sub K (sub K (base1 (x ε)) ∙ base1 (x ε) ∙ sub K (base1 (y ε)) ∙ base1 (y ε)) ≈⟨ {!!} ⟩ - sub K (base1 (x ε)) ∙ sub K (base1 (y ε)) ≈⟨ {!!} ⟩ - sub K (base1 (x ε) ∙ base1 (y ε)) ∎ - mbase1 (coset a b) (cscong x t) = mbase1 (coset a b) t - mbase1 (cscong eq s) (coset a b) = mbase1 s (coset a b) - mbase1 (cscong eqs s) (cscong eqt t) = mbase1 s t + 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 ( ((ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙ + (ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹ )) ∙ + (base1 (x ε) ∙ base1 (y ε))) ≈⟨ ⟦⟧-cong ( ∙-cong ( + begin (ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙ (ε ∙ sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ≈⟨ {!!} ⟩ + sub K ((base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙ (sub K (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ≈⟨ {!!} ⟩ + sub K (((base1 (x ε) ∙ base1 (y ε)) ⁻¹) ⁻¹ ∙ (base1 (x ε) ∙ base1 (y ε)) ⁻¹) ≈⟨ {!!} ⟩ + sub K ε ≈⟨ {!!} ⟩ + ε ∎ ) (grefl G) ) ⟩ + sub K (ε ∙ (base1 {G} {K} (x ε) ∙ base1 {G} {K} (y ε))) ≈⟨ {!!} ⟩ + sub K (base1 {G} {K} (x ε) ∙ base1 {G} {K} (y ε)) ∎ cresp : {x y u v : COSET G K} → sub K (base x) ≈ sub K (base y) → sub K (base u )≈ sub K (base v) → sub K (base (mul x u)) ≈ sub K (base (mul y v)) - cresp {x} {y} {u} {v} x=y u=v = {!!} + cresp {x} {y} {u} {v} x=y u=v = begin + sub K (base (mul x u)) ≈⟨ {!!} ⟩ + sub K (base x ∙ base u) ≈⟨ {!!} ⟩ + sub K (base x ) ∙ sub K (base u) ≈⟨ {!!} ⟩ + sub K (base y ) ∙ sub K (base v) ≈⟨ {!!} ⟩ + 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 = {!!} where -- crefl1 (coset a b) = ⟦⟧-cong (grefl G)