Mercurial > hg > Members > kono > Proof > galois
changeset 278:ed06f82988c1
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 27 Jan 2023 11:12:14 +0900 |
| parents | 25c8b4d71085 |
| children | 386ece574509 |
| files | src/Fundamental.agda |
| diffstat | 1 files changed, 8 insertions(+), 4 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Fundamental.agda Fri Jan 27 10:45:25 2023 +0900 +++ b/src/Fundamental.agda Fri Jan 27 11:12:14 2023 +0900 @@ -193,14 +193,18 @@ aNeq {f} {g} f=g = an00 , ? where an00 : {x : Carrier} → f ∋ x → g ∋ x an00 {x} fnx = begin - a (g x) ∙ ⟦ n (g x) ⟧ ≈⟨ ∙-cong (gsym G (an01 (a (f x)))) (grefl G) ⟩ - (a (f x) ∙ ⟦ factor (a (g x)) (a (f x)) ⟧ ) ∙ ⟦ n (g x) ⟧ ≈⟨ ? ⟩ - a (f x) ∙ ( ⟦ factor (a (g x)) (a (f x)) ⟧ ∙ ⟦ n (g x) ⟧ ) ≈⟨ ? ⟩ - a (f x) ∙ ( ⟦ factor (a (g x)) (a (f x)) ∙ n (g x) ⟧ ) ≈⟨ ? ⟩ + a (g x) ∙ ⟦ n (g x) ⟧ ≈⟨ ∙-cong (gsym G (an01 (fgf ⁻¹ ∙ a (f x)))) (gsym G f=g) ⟩ + (fgf ⁻¹ ∙ a (f x)) ∙ ⟦ factor (a (g x)) (⟦ factor (a (g x)) (a (f x)) ⟧ ⁻¹ ∙ a (f x)) ⟧ ∙ ⟦ n (f x) ⟧ ≈⟨ ? ⟩ + (a (f x) ∙ fgf ⁻¹ ) ∙ ( ⟦ factor (a (g x)) (a (f x)) ⟧ ∙ ⟦ n (f x) ⟧ ) ≈⟨ ? ⟩ a (f x) ∙ ⟦ n (f x) ⟧ ≈⟨ fnx ⟩ x ∎ where + fgf = ⟦ factor (a (g x)) (a (f x)) ⟧ an01 : (y : Carrier) → y ∙ ⟦ factor (a (g x)) y ⟧ ≈ a (g x) an01 y = is-factor (a (g x)) y + an03 : ⟦ factor (a (g x)) (a (f x)) ⟧ ≈ ε + an03 = ? + an02 : ⟦ factor (a (g x)) (⟦ factor (a (g x)) (a (f x)) ⟧ ⁻¹ ∙ a (f x)) ⟧ ≈ ⟦ factor (a (g x)) (a (f x)) ⟧ + an02 = ? cong-i : {f g : Group.Carrier (G / K ) } → ({x : Carrier } → ⟦ n (f x) ⟧ ≈ ⟦ n (g x) ⟧ ) → inv-φ f ≈ inv-φ g cong-i = ?