-- Given two abelian groups A, B
--   the set of all group homomorphisms from A to B
-- is itself an abelian group.
-- In other words, Ab is cartesian closed.
-- This is needed to show Ab is an abelian category.


module Cubical.Algebra.AbGroup.Instances.Hom where

open import Cubical.Algebra.AbGroup.Base
open import Cubical.Algebra.Group.Morphisms
open import Cubical.Algebra.Group.MorphismProperties
open import Cubical.Algebra.Group.Properties
open import Cubical.Foundations.Prelude

private
  variable
     ℓ' : Level

module _ (A : AbGroup ) (B : AbGroup ℓ') where

  -- These names are useful for the proofs
  private
    open IsGroupHom
    open AbGroupStr (A .snd) using () renaming (0g to 0A; _+_ to _⋆_; -_ to inv)
    open AbGroupStr (B .snd) using (_+_; -_; +Comm; +Assoc; +IdR ; +InvR)
                             renaming (0g to 0B)
    open GroupTheory (AbGroup→Group B) using (invDistr) renaming (inv1g to inv0B)

    -- Some lemmas
    idrB : (b : B .fst)  b + 0B  b
    idrB b = +IdR b

    invrB : (b : B .fst)  b + (- b)  0B
    invrB b = +InvR b

    hom0AB : (f : AbGroupHom A B)  f .fst 0A  0B
    hom0AB f = hom1g (AbGroupStr→GroupStr (A .snd)) (f .fst)
                     (AbGroupStr→GroupStr (B .snd)) (f .snd .pres·)

    homInvAB : (f : AbGroupHom A B)  (a : A .fst)  f .fst (inv a)  (- f .fst a)
    homInvAB f a = homInv (AbGroupStr→GroupStr (A .snd)) (f .fst)
                          (AbGroupStr→GroupStr (B .snd)) (f .snd .pres·) a


  -- Zero morphism
  zero : AbGroupHom A B
  zero .fst a = 0B
  zero .snd .pres· a a' = sym (idrB _)
  zero .snd .pres1 = refl
  zero .snd .presinv a = sym (inv0B)


  -- Pointwise addition of morphisms
  module _ (f* g* : AbGroupHom A B) where
    private
      f = f* .fst
      g = g* .fst

    HomAdd : AbGroupHom A B
    HomAdd .fst = λ a  f a + g a

    HomAdd .snd .pres· a a' =
        f (a  a') + g (a  a')           ≡⟨ cong (_+ g(a  a')) (f* .snd .pres· _ _) 
        (f a + f a') + g (a  a')         ≡⟨ cong ((f a + f a') +_) (g* .snd .pres· _ _) 
        (f a + f a') + (g a + g a')       ≡⟨ sym (+Assoc _ _ _) 
        f a + (f a' + (g a + g a'))       ≡⟨ cong (f a +_) (+Assoc _ _ _) 
        f a + ((f a' + g a) + g a')       ≡⟨ cong  b  (f a + b + g a')) (+Comm _ _) 
        f a + ((g a + f a') + g a')       ≡⟨ cong (f a +_) (sym (+Assoc _ _ _)) 
        f a + (g a + (f a' + g a'))       ≡⟨ +Assoc _ _ _ 
        (f a + g a) + (f a' + g a')       

    HomAdd .snd .pres1 =
        f 0A + g 0A       ≡⟨ cong (_+ g 0A) (hom0AB f*) 
        0B + g 0A         ≡⟨ cong (0B +_) (hom0AB g*) 
        0B + 0B           ≡⟨ idrB _ 
        0B                

    HomAdd .snd .presinv a =
        f (inv a) + g (inv a)     ≡⟨ cong (_+ g (inv a)) (homInvAB f* _) 
        (- f a) + g (inv a)       ≡⟨ cong ((- f a) +_) (homInvAB g* _) 
        (- f a) + (- g a)         ≡⟨ +Comm _ _ 
        (- g a) + (- f a)         ≡⟨ sym (invDistr _ _) 
        - (f a + g a)             


  -- Pointwise inverse of morphism
  module _ (f* : AbGroupHom A B) where
    private
      f = f* .fst

    HomInv : AbGroupHom A B
    HomInv .fst = λ a  - f a

    HomInv .snd .pres· a a' =
        - f (a  a')            ≡⟨ cong -_ (f* .snd .pres· _ _) 
        - (f a + f a')          ≡⟨ invDistr _ _ 
        (- f a') + (- f a)      ≡⟨ +Comm _ _ 
        (- f a) + (- f a')      

    HomInv .snd .pres1 =
        - (f 0A)      ≡⟨ cong -_ (f* .snd .pres1) 
        - 0B          ≡⟨ inv0B 
        0B            

    HomInv .snd .presinv a =
        - f (inv a)     ≡⟨ cong -_ (homInvAB f* _) 
        - (- f a)       


  -- Group laws for morphisms
  private
    0ₕ = zero
    _+ₕ_ = HomAdd
    -ₕ_ = HomInv

  -- Morphism addition is associative
  HomAdd-assoc : (f g h : AbGroupHom A B)  (f +ₕ (g +ₕ h))  ((f +ₕ g) +ₕ h)
  HomAdd-assoc f g h = GroupHom≡ (funExt λ a  +Assoc _ _ _)

  -- Morphism addition is commutative
  HomAdd-comm : (f g : AbGroupHom A B)  (f +ₕ g)  (g +ₕ f)
  HomAdd-comm f g = GroupHom≡ (funExt λ a  +Comm _ _)

  -- zero is right identity
  HomAdd-zero : (f : AbGroupHom A B)  (f +ₕ zero)  f
  HomAdd-zero f = GroupHom≡ (funExt λ a  idrB _)

  -- -ₕ is right inverse
  HomInv-invr : (f : AbGroupHom A B)  (f +ₕ (-ₕ f))  zero
  HomInv-invr f = GroupHom≡ (funExt λ a  invrB _)


-- Abelian group structure on AbGroupHom A B
open AbGroupStr
HomAbGroupStr : (A : AbGroup )  (B : AbGroup ℓ')  AbGroupStr (AbGroupHom A B)
HomAbGroupStr A B .0g        = zero A B
HomAbGroupStr A B ._+_       = HomAdd A B
HomAbGroupStr A B .-_        = HomInv A B
HomAbGroupStr A B .isAbGroup = makeIsAbGroup isSetGroupHom
    (HomAdd-assoc A B) (HomAdd-zero A B) (HomInv-invr A B) (HomAdd-comm A B)

HomAbGroup : (A : AbGroup )  (B : AbGroup ℓ')  AbGroup (ℓ-max  ℓ')
HomAbGroup A B = AbGroupHom A B , HomAbGroupStr A B