-- 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 : Group.Carrier A ) →  (pn : NormalSubGroup.P N n) → IsaN N a (A < a ∙ n > )

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

_/_ : (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 = ? ; sym = λ a=b → ? 
          }
       ; ∙-cong = λ {x} {y} {u} {v} x=y u=v → ? }
       ; assoc = ? }
       ; identity =  ?   }
       ; inverse   =  (λ x → ? ) , (λ x → ? ) 
       ; ⁻¹-cong   = ? 
      }
   } where
       _=n=_ = aNeq N
       open Group A
       open NormalSubGroup N
       open EqReasoning (Algebra.Group.setoid A)
       open Gutil A
       open AN A N
       nrefl :  {x : Carrier} → x =n= x
       nrefl = ?


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

    gkε : ?
    gkε = ? -- record { a = ε ; n = ε ; pn = Pε }

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

    φ-homo : IsGroupHomomorphism (GR G) (GR (G / K)) φ
    φ-homo = record {⁻¹-homo = ? ; isMonoidHomomorphism = record { ε-homo = ?
           ; isMagmaHomomorphism = record { homo = ? ; isRelHomomorphism =
       record { cong = ? } }}} 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 = ?

    inv-φ : Group.Carrier (G / K ) → Carrier 
    inv-φ = ? -- record { a = a ; n = n ; pn = pn } = a ∙ n 

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