-- fundamental homomorphism theorem
--

open import Level hiding ( suc ; zero )
module homomorphism (c d : Level) where

open import Algebra
open import Algebra.Structures
open import Algebra.Definitions
open import Algebra.Core
open import Algebra.Bundles

open import Data.Product
open import Relation.Binary.PropositionalEquality
open import NormalSubgroup
import Gutil
import Function.Definitions as FunctionDefinitions

import Algebra.Morphism.Definitions as MorphismDefinitions
open import Algebra.Morphism.Structures

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
-- (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 GroupMorphisms

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

open import Data.Empty
open import Relation.Nullary

-- Set of a ∙ ∃ n ∈ N
--

data IsaN  {A : Group c d }  (N : NormalSubGroup A) (a : Group.Carrier A ) : (x : Group.Carrier A ) → Set (Level.suc c ⊔ d) where
    an : (n x : Group.Carrier A ) →  A < A < a ∙ n > ≈ x > → (pn : NormalSubGroup.P N n) → IsaN N a x

record aNeq {A : Group c d }  (N : NormalSubGroup A )  (a b : Group.Carrier A)  : Set (Level.suc c ⊔ d) where
    field
        eq→  : {x : Group.Carrier A}  → IsaN N a x → IsaN N b x
        eq←  : {x : Group.Carrier A}  → IsaN N b x → IsaN N a x

module AN (A : Group c d) (N : NormalSubGroup A  ) where
    open Group A
    open NormalSubGroup N
    open EqReasoning (Algebra.Group.setoid A)
    open Gutil A
    open aNeq
    --
    -- (aN)(bN) = a(Nb)N = a(bN)N = (ab)NN = (ab)N.
    --
    naN : {a x : Carrier} → IsaN N a x → Carrier
    naN (an n x eq pn) = n
    PaN : {a x : Carrier} → (iax : IsaN N a x) → P (naN iax)
    PaN (an n x eq pn) = pn
    anaN=x : {a x : Carrier} → (ax : IsaN N a x) → a ∙ naN ax ≈ x
    anaN=x (an n x eq pn) = eq
    an-factor : {x y a : Carrier } → (xua : IsaN N (x ∙ y) a ) → IsaN N x (a ∙ y ⁻¹) × IsaN N y y
    an-factor {x} {y} {a} (an n a1 eqa pn) = an n1 _ an02 (Pcomm pn) 
                  , an n2 _ an03 Pε where
        an04 : x ∙ y ∙ n  ≈ a 
        an04 = eqa
        -- n ≈ (((y ⁻¹) ∙ (n1 ∙ ((y ⁻¹) ⁻¹ ))) ∙ n2)
        -- n ∙ n2 ⁻¹ ≈ (((y ⁻¹) ∙ (n1 ∙ ((y ⁻¹) ⁻¹ ))) 
        -- y ∙ (n ∙ n2 ⁻¹) ∙ y ⁻¹  ≈ n1 
        n1 : Carrier
        n1 = y ∙ (n ∙ y ⁻¹)
        n2 : Carrier
        n2 = ε
        an02 : x ∙ n1  ≈ a ∙ y ⁻¹
        an02 = begin
           x ∙ n1 ≈⟨ grefl ⟩
           x ∙ (y ∙ (n ∙ y ⁻¹))  ≈⟨ solve monoid  ⟩
           (x ∙ y ∙ n ) ∙ y ⁻¹  ≈⟨ car eqa  ⟩
           a ∙ y ⁻¹ ∎
        an03 : y ∙ n2  ≈ y
        an03 = proj₂ identity _
    an-comp : {x y a b : Carrier } → IsaN N x a →  IsaN N y b → IsaN N (x ∙ y) (a ∙ b)
    an-comp {x} {y} {a} {b} (an n1 a1 eqa p1) (an n2 a2 eqb p2) = an  (((y ⁻¹) ∙ (n1 ∙ ((y ⁻¹) ⁻¹ ))) ∙ n2) _ an01  (P∙ (Pcomm p1) p2) where
        an01 : x ∙ y ∙ (((y ⁻¹) ∙ (n1 ∙ ((y ⁻¹) ⁻¹ ))) ∙ n2)  ≈ a ∙ b
        an01 = begin
           x ∙ y ∙ (((y ⁻¹) ∙ (n1 ∙ ((y ⁻¹) ⁻¹ ))) ∙ n2)  ≈⟨ solve monoid ⟩
           (x ∙ (y ∙ y ⁻¹) ∙ n1) ∙ (y ⁻¹) ⁻¹  ∙ n2  ≈⟨ car (∙-cong (car (cdr (proj₂ inverse _))) f⁻¹⁻¹≈f ) ⟩
           (x ∙ ε ∙ n1) ∙ y  ∙ n2  ≈⟨ solve monoid ⟩
           (x ∙ n1) ∙ (y ∙ n2)  ≈⟨ ∙-cong eqa eqb ⟩
           a ∙ b  ∎
    an-cong : {a b x : Carrier } → a ≈ b → IsaN N a x → IsaN N b x
    an-cong {a} {b} {x} eq (an n _ eq1 pn) = an n _ an04 pn where
        an04 : b ∙ n  ≈ x
        an04 = begin
           b ∙ n ≈⟨ car (gsym eq) ⟩
           a ∙ n ≈⟨ eq1 ⟩
           x ∎
    conj : (n x : Carrier) → Carrier
    conj n x = x ∙ (n ∙ x ⁻¹)
    Pconj  : (n x : Carrier) → P n → P (conj n x)
    Pconj n x pn = Pcomm pn
    aN=Na : {x n : Carrier} → x ∙ n ≈ conj n x ∙ x 
    aN=Na {x} {n}  = gsym ( begin
        (x ∙ (n ∙ x ⁻¹)) ∙ x ≈⟨ solve monoid ⟩
        (x ∙ n ) ∙ (x ⁻¹ ∙ x) ≈⟨ cdr (proj₁ inverse _) ⟩
        (x ∙ n ) ∙ ε  ≈⟨ proj₂ identity _ ⟩
        x ∙ n ∎ )
    Na=aN : {x n  : Carrier} → n ∙ x ≈ x ∙ conj n (x ⁻¹) 
    Na=aN {x} {n}  = gsym ( begin
        x ∙ ( x ⁻¹ ∙ (n ∙ (x ⁻¹ ) ⁻¹ ) )  ≈⟨ solve monoid ⟩
        (x ∙ x ⁻¹ ) ∙ (n ∙ (x ⁻¹) ⁻¹) ≈⟨ ∙-cong (proj₂ inverse _) (cdr f⁻¹⁻¹≈f) ⟩
        ε ∙ (n ∙ x) ≈⟨ proj₁ identity _ ⟩
        n ∙ x ∎ )

    aneq : {a b : Carrier } → a ≈ b → aNeq N a b
    aneq {a} {b} eq = record { eq→ = λ {x} lt → an-cong eq lt ; eq← = λ lt → an-cong (gsym eq) lt }   
    -- this may wrong 
    -- aNeq→n-eq : {a b x : Carrier } → aNeq N a b → (ia : IsaN N a x) → (ib : IsaN N b x)  →  naN ia ≈ naN ib
    ayxi : {x y : Carrier} → aNeq N x y → {n : Carrier} → P n → IsaN N y (x ∙ n)
    ayxi {x} {y} x=y {n} pn = eq→ x=y (an n _ grefl pn)
    ayxn : {x y : Carrier} → aNeq N x y → {n : Carrier} → P n → Carrier
    ayxn {x} {y} x=y {n} pn = naN (ayxi x=y pn)
    Payxn : {x y : Carrier} → (x=y : aNeq N x y) → {n : Carrier} → (pn : P n) → P (ayxn x=y pn)
    Payxn {x} {y} x=y {n} pn with ayxi x=y pn
    ... | an n₁ .((A Group.∙ x) n) x₁ pn₁ = pn₁
    anxn=yn : {x y n : Carrier } → (x=y : aNeq N x y) → (pn : P n) → x ∙ n ≈ y ∙ (ayxn x=y pn)
    anxn=yn {x} {y} {n} x=y pn with ayxi x=y pn
    ... | an n₁ .((A Group.∙ x) n) eq1 pn₁ = gsym eq1

_/_ : (A : Group c d ) (N  : NormalSubGroup A ) → Group c (Level.suc c ⊔ d) 
_/_ A N  = record {
    Carrier  = Group.Carrier A
    ; _≈_      = aNeq N
    ; _∙_      = _∙_
    ; ε        = ε
    ; _⁻¹      = λ x → x ⁻¹
    ; isGroup = record { isMonoid  = record { isSemigroup = record { isMagma = record {
       isEquivalence = record {refl = nrefl
           ; trans = ntrans ; sym = λ a=b → nsym a=b 
          }
       ; ∙-cong = λ {x} {y} {u} {v} x=y u=v → gk00 x=y u=v }
       ; assoc = gkassoc }
       ; identity =  (λ a → aneq (proj₁ identity _)) , (λ a → aneq (proj₂ identity _) )  }
       ; inverse   =  (λ a → aneq (proj₁ inverse _)) , (λ x → aneq (proj₂ inverse _) ) 
       ; ⁻¹-cong   = gkcong⁻¹
      }
   } where
       _=n=_ = aNeq N
       open Group A
       open NormalSubGroup N
       open EqReasoning (Algebra.Group.setoid A)
       open Gutil A
       open AN A N
       open aNeq 
       nrefl :  {x : Carrier} → x =n= x
       nrefl {x} = record { eq→ = λ {lt} ix → ix ; eq← =  λ {lt} ix → ix }
       nsym : {x y  : Carrier} → x =n= y → y =n= x
       nsym {x} {y} eq = record { eq→ = λ {lt} ix → eq← eq ix ; eq← =  λ {lt} ix → eq→ eq ix }
       ntrans : {x y  z : Carrier} → x =n= y → y =n= z → x =n= z
       ntrans {x} {y} {z} x=y y=z = record { eq→ = λ {lt} ix → eq→ y=z (eq→ x=y ix) 
            ; eq← =  λ {lt} ix → eq← x=y (eq← y=z ix) }
       gk00 : {x y u v : Carrier } → aNeq N x y → aNeq N u v → aNeq N (x ∙ u) (y ∙ v)
       gk00 {x} {y} {u} {v} x=y u=v = record { eq→ = gk01 x=y u=v ; eq← =  gk01 (nsym x=y) (nsym u=v) } where
           -- xN ≈ yN → uN ≈ vN → xuN ≈ xN⁻¹NuN  ≈ yN⁻¹NvN  ≈ yvN
           gk01 : {a x y u v : Carrier} → aNeq N x y → aNeq N u v  → IsaN N (x ∙ u) a → IsaN N (y ∙ v) a
           gk01 {a} {x} {y} {u} {v} x=y u=v (an n z eq pn) = an gk1n z gk13 (PaN gk14) where
              gk10 : IsaN N x (a ∙ u ⁻¹)
              gk10 = proj₁ (an-factor (an n z eq pn))
              gk12 : IsaN N u u
              gk12 = proj₂ (an-factor (an n z eq pn))
              gk14 : IsaN  N _ _
              gk14 = an-comp (eq→ x=y gk10) (eq→ u=v gk12 )
              gk1n : Carrier
              gk1n = naN gk14
              gk13 : (y ∙ v) ∙ gk1n  ≈ a
              gk13 = begin
                 y ∙ v ∙ gk1n  ≈⟨ grefl ⟩ 
                 y ∙ v ∙ naN gk14  ≈⟨ anaN=x gk14 ⟩ 
                 a ∙ u ⁻¹ ∙ u  ≈⟨ solve monoid ⟩ 
                 a ∙ (u ⁻¹ ∙ u)  ≈⟨ cdr ( proj₁ inverse _)  ⟩ 
                 a ∙ ε  ≈⟨ solve monoid  ⟩ 
                 a ∎
       gkassoc : (x y z : Carrier ) → aNeq N ((x ∙ y ) ∙ z) (x ∙ (y ∙ z))
       gkassoc x y z = record { eq→ = gk04 ; eq← =  gk06 }  where
          gk04 : {a : Carrier } →  IsaN N (x ∙ y ∙ z) a → IsaN N (x ∙ (y ∙ z)) a
          gk04 {a} (an n _ eq pn) = an n _ gk05 pn where
              gk05 :  x ∙ (y ∙ z) ∙ n  ≈ a
              gk05 = begin
                 x ∙ (y ∙ z) ∙ n  ≈⟨ solve monoid ⟩
                 x ∙ y ∙ z ∙ n  ≈⟨ eq ⟩
                 a ∎
          gk06 : {a : Carrier } →  IsaN N (x ∙ (y ∙ z)) a → IsaN N (x ∙ y ∙ z) a
          gk06 {a} (an n _ eq pn) = an n _ gk05 pn where
              gk05 :  x ∙ y ∙ z ∙ n  ≈ a
              gk05 = begin
                 x ∙ y ∙ z ∙ n  ≈⟨ solve monoid ⟩
                 x ∙ (y ∙ z) ∙ n  ≈⟨ eq ⟩
                 a ∎
       gkcong⁻¹ : {x y : Carrier } → aNeq N x y → aNeq N (x ⁻¹) (y ⁻¹) 
       gkcong⁻¹ {x} {y} x=y  = record { eq→ = gk07 x=y ; eq← =  gk07 (nsym x=y) }  where
          --  a⁻¹N     ≈ (Na)⁻¹          ≈ (aN)⁻¹        ≈ (bN)⁻¹        ≈ (Nb)⁻¹         ≈ b⁻¹N
          --  a ⁻¹ ∙ n ≈ ( n ⁻¹ ∙ a ) ⁻¹ ≈ ( a ∙ n₁ ) ⁻¹ ≈ ( b ∙ n₂ ) ⁻¹ ≈ ( n₃  ∙ b ) ⁻¹ ≈ b ⁻¹ ∙ n₃
          gk07 : {a x y : Carrier } → (x=y : aNeq N x y) →  IsaN N (x ⁻¹) a → IsaN N (y ⁻¹) a
          gk07 {a} {x} {y} x=y (an n _ eq pn) = an ((conj (ayxn x=y pj) y )⁻¹)  _ gk01 (P⁻¹ _ (Pconj _ _ (Payxn x=y pj ) ) ) where
              pj : P (conj (n ⁻¹) (x ⁻¹)) 
              pj = Pcomm (P⁻¹ _ pn) 
              gk01 : y ⁻¹ ∙  (conj (ayxn x=y pj) y ) ⁻¹  ≈ a
              gk01 = begin
                 y ⁻¹ ∙ (conj (ayxn x=y pj) _ ) ⁻¹   ≈⟨ lemma5 _ _  ⟩
                 ( conj (ayxn x=y pj) _ ∙ y ) ⁻¹  ≈⟨  ⁻¹-cong (gsym aN=Na)  ⟩
                 (y ∙ ayxn x=y pj ) ⁻¹  ≈⟨ gsym ( ⁻¹-cong ( anxn=yn x=y pj ))  ⟩
                 (x ∙ conj (n ⁻¹) (x ⁻¹) ) ⁻¹  ≈⟨  ⁻¹-cong (gsym Na=aN )  ⟩
                 (n ⁻¹ ∙ x ) ⁻¹  ≈⟨ gsym (lemma5 _ _  ) ⟩
                 x ⁻¹ ∙ (n ⁻¹) ⁻¹   ≈⟨ cdr f⁻¹⁻¹≈f ⟩
                 x ⁻¹ ∙ n  ≈⟨ eq ⟩
                 a ∎

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

open import Function.Surjection
open import Function.Equality

module GK (G : Group c d) (K : NormalSubGroup G  ) where
    open Group G
    open NormalSubGroup K
    open EqReasoning (Algebra.Group.setoid G)
    open Gutil G
    open AN G K

    gkε : Group.Carrier (G / K)
    gkε = Group.ε (G / K) 

    φ : Group.Carrier G → Group.Carrier (G / K )
    φ g = g

    φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ
    φ-homo = record {⁻¹-homo = λ x → aneq grefl ; isMonoidHomomorphism = record { ε-homo = aneq grefl
           ; isMagmaHomomorphism = record { homo = λ x y → aneq grefl ; isRelHomomorphism =
       record { cong = λ eq → aneq eq } }}} where


    φe : (Algebra.Group.setoid G)  Function.Equality.⟶ (Algebra.Group.setoid (G / K))
    φe = record { _⟨$⟩_ = φ ; cong = gk40 }  where
          gk40 : {i j : Carrier} → i ≈ j → (G / K ) < φ i ≈ φ j >
          gk40 {i} {j} i=j = aneq i=j

    inv-φ : Group.Carrier (G / K ) → Carrier 
    inv-φ x = ?

    φ-surjective : Surjective φe
    φ-surjective = record { from = record { _⟨$⟩_ = inv-φ ; cong = λ {f} {g} → gk50 f g }
          ; right-inverse-of = gk60 } where
       gk50 :  (f g : Group.Carrier (G / K)) → (G / K) < f ≈ g > → inv-φ f ≈ inv-φ g
       gk50 f g f=g = ?
       gk60 : (x : Group.Carrier (G / K )) → aNeq K (φ (inv-φ x)) x
       gk60 = ?

    gk01 : (x : Group.Carrier (G / K ) ) → (G / K) < φ ( inv-φ x ) ≈ x >
    gk01 = ?


record FundamentalHomomorphism (G H : Group c d )
    (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 (Level.suc c ⊔ d) where
  open Group H
  -- open GK G K
  field
    h : Group.Carrier (G / K ) → Group.Carrier H
    h-homo :  IsGroupHomomorphism (GR (G / K) ) (GR H) h
    is-solution : (x : Group.Carrier G)  →  f x ≈ h ( GK.φ G K x )
    unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H)  → (homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 )
       → ( (x : Group.Carrier G)  →  f x ≈ h1 ( GK.φ G K x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )

FundamentalHomomorphismTheorm : (G H : Group c d)
    (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
   ; is-solution = is-solution
   ; unique = unique
  } where
    -- open GK G K
    open Group H
    open Gutil H
    -- open NormalSubGroup K ?
    open IsGroupHomomorphism homo
    open EqReasoning (Algebra.Group.setoid H)
    h : Group.Carrier (G / K ) → Group.Carrier H
    h r = f ( GK.inv-φ G K r )
    h03 : (x y : Group.Carrier (G / K ) ) →  h ( (G / K) < x ∙ y > ) ≈ h x ∙ h y
    h03 = ?
    h-homo :  IsGroupHomomorphism (GR (G / K ) ) (GR H) h
    h-homo = record {
     isMonoidHomomorphism = record {
          isMagmaHomomorphism = record {
             isRelHomomorphism = record { cong = λ {x} {y} eq → {!!} }
           ; homo = h03 }
        ; ε-homo = {!!} }
       ; ⁻¹-homo = {!!} }
    is-solution : (x : Group.Carrier G)  →  f x ≈ h ( GK.φ ? ? x )
    is-solution x = begin
         f x ≈⟨ ? ⟩
         h ( GK.φ ? ? x ) ∎ 
    unique : (h1 : Group.Carrier (G / K ) → Group.Carrier H)  → (h1-homo : IsGroupHomomorphism (GR (G / K)) (GR H) h1 )
       → ( (x : Group.Carrier G)  →  f x ≈ h1 ( GK.φ ? ? x ) ) → ( ( x : Group.Carrier (G / K)) → h x ≈ h1 x )
    unique h1 h1-homo h1-is-solution x = begin
         h x ≈⟨ grefl ⟩
         f ( GK.inv-φ ? ? x ) ≈⟨ h1-is-solution _ ⟩
         h1 ( GK.φ ? ? ( GK.inv-φ  ? ? x ) ) ≈⟨ IsGroupHomomorphism.⟦⟧-cong h1-homo (GK.gk01 ? ? x)  ⟩
         h1 x ∎