-- fundamental homomorphism theorem
--

open import Level hiding ( suc ; zero )
module Fundamental (c l : Level) where

open import Algebra
open import Algebra.Structures
open import Algebra.Definitions
open import Data.Product
open import Relation.Binary.PropositionalEquality 
open import Algebra.Morphism.Structures 
open GroupMorphisms
open import Gutil0

--
-- 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
-- (where G/K is the quotient group of G by K).
-- If K is a subset of ker(f) then there exists a unique homomorphism h: G/K → H such that f = h∘φ.
--     https://en.wikipedia.org/wiki/Fundamental_theorem_on_homomorphisms
--
--       f
--    G --→ H
--    |   /
--  φ |  / h
--    ↓ /
--    G/K
--

import Relation.Binary.Reasoning.Setoid as EqReasoning

open HomoMorphism

--
--  Coset : N : NormalSubGroup →  { a ∙ n | G ∋ a , N ∋ n }
--

data Coset (G : Group c l)  (K : NormalSubGroup G) :  Group.Carrier G → Set ( c  Level.⊔  l ) where
    coset  : (a b : Group.Carrier G ) → Coset G K ( Group._∙_ G a (NormalSubGroup.sub K b) )
    cscong : {a b : Group.Carrier G } → Group._≈_ G a b  → Coset G K a → Coset G K b

open NormalSubGroup  -- G has at least an element other than ε

φ :   {G : Group c l} →  {K : NormalSubGroup G} → (g x : Group.Carrier G ) → Coset G K x
φ {G} {K} g x = cscong p01 ( coset (x ∙ (sub K g) ⁻¹ )  g)  where
   open Group G
   p01 : x ∙ sub K g ⁻¹ ∙ sub K g ≈ x
   p01 = begin x ∙ sub K g ⁻¹ ∙ sub K g ≈⟨ assoc x _ _  ⟩
         x ∙ (  sub K g ⁻¹ ∙ sub K g ) ≈⟨  ∙-cong (grefl G) (proj₁ inverse  _ ) ⟩
         x ∙ ε ≈⟨ proj₂ identity  _  ⟩
         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} {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
base {G} {K} x = base1 (x ε) where     -- with x ε won't work why?
    open Group G


--  Na ∙ Nb = Nab
mul : {G : Group c l}  {K : NormalSubGroup G} → (x y : (g : Group.Carrier G ) → Coset G K g ) → (g : Group.Carrier G ) → Coset G K g
mul {G} {K} x y g = φ (base x ∙ base y) g where open Group G

inv : {G : Group c l}  {K : NormalSubGroup G} → ( (g : Group.Carrier G )→ Coset G K g)  → ( (g : Group.Carrier G )→ Coset G K g)
inv {G} {K} x g = inv1 (x g) where
    open Group G
    inv1 : {a : Carrier} → (x : Coset G K a) → Coset G K g
    inv1 (coset a b) = φ  (a ⁻¹) g 
    inv1 (cscong eq x) = inv1 x

COSET : (G : Group c l)  (K : NormalSubGroup G) →  Set ( c  Level.⊔  l )
COSET G K = (g : Group.Carrier G ) → Coset G K g

-- import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
-- open HE

import Axiom.Extensionality.Propositional
postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m

-- G / K : Quotient
_/_ : (G : Group c l)  (K : NormalSubGroup G) → Group ( c  Level.⊔  l ) l
G / K = record {
     Carrier        = (g : Group.Carrier G ) → Coset G K g
     ; _≈_          = λ x y → Group._≈_ G (sub K (base x)) (sub K (base y))
     ; _∙_          = λ x y → mul x y
     ; ε            = φ (Group.ε G )
     ; _⁻¹          = λ x → inv x
     ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
       isEquivalence = record { refl = grefl G ; sym = gsym G ; trans = gtrans G } 
       ; ∙-cong = λ {x y u v} → cresp {x} {y} {u} {v} }
       ; assoc = assoc1 }
       ; identity = {!!} }
       ; inverse   = {!!}
       ; ⁻¹-cong   = λ {x} {y} → {!!}
      } 
   } where 
      open Group G hiding (refl ; sym ; trans )
      open EqReasoning (Algebra.Group.setoid G)
      open IsGroupHomomorphism (s-homo K )
      mbase :  {x y : COSET G K} → sub K (base (mul x y)) ≈ sub K (base x ∙ base y)
      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 =  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) 

-- K ⊂ ker(f)
K⊆ker : (G H : Group c l)  (K : NormalSubGroup G) (f : Group.Carrier G → Group.Carrier H ) → Set ( c  Level.⊔  l ) 
K⊆ker G H K f = (x : Group.Carrier G ) → f ( sub K x ) ≈ ε   where
  open Group H

record FundamentalHomomorphism (G H : Group c l)  
    (f : Group.Carrier G → Group.Carrier H ) 
    (homo : IsGroupHomomorphism (GR G) (GR H) f ) 
    (K : NormalSubGroup G ) (kf : K⊆ker G H K f) :  Set ( c  Level.⊔  l ) where
  open Group H
  field
    h : {!!} → Group.Carrier H
    h-homo :  IsGroupHomomorphism (GR (G / K) ) (GR H) {!!} 
    unique : (x : Group.Carrier G)  →  {!!} -- f x ≈ h ( φ x )

FundamentalHomomorphismTheorm : (G H : Group c l)
    (f : Group.Carrier G → Group.Carrier H )
    (homo : IsGroupHomomorphism (GR G) (GR H) f )
    (K : NormalSubGroup G ) → (kf : K⊆ker G H K f)   → FundamentalHomomorphism G H f homo K kf
FundamentalHomomorphismTheorm G H f homo K kf = record {
     h = h
   ; h-homo = h-homo
   ; unique = unique
  } where
    open Group H
    EqH =  IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup
             (IsGroup.isMonoid isGroup )))
    EqG =  IsMagma.isEquivalence (IsSemigroup.isMagma (IsMonoid.isSemigroup
             (IsGroup.isMonoid (Group.isGroup G) )))
    h1 : {x : Group.Carrier G } → Coset G K x → Carrier
    h1 (coset a b) = f a 
    h : {!!} -- CosetCarrier G K → Carrier   --  G / K → H
    h r = {!!}
    _o_ = Group._∙_ G
    h03 : (x y : Group.Carrier (G / K ) ) → {!!}
    h03 x y = {!!} 
    h-homo :  IsGroupHomomorphism (GR (G / K) ) (GR H) {!!} 
    h-homo = record {
     isMonoidHomomorphism = record {
          isMagmaHomomorphism = record {
             isRelHomomorphism = record { cong = λ {x} {y} eq → {!!} } 
           ; homo = h03 }
        ; ε-homo = {!!} }
       ; ⁻¹-homo = {!!} }
    unique : (x : Group.Carrier G)  →  f x ≈ h ( φ x )
    unique x = begin
         f x ≈⟨ {!!} ⟩
         f ( x o (Group._⁻¹ G (sub K x)))   ∎ where open EqReasoning (Algebra.Group.setoid H )