{-# OPTIONS --safe #-}
module Cubical.Algebra.Ring.Kernel where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.Structure
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Powerset

open import Cubical.Algebra.Ring.Base
open import Cubical.Algebra.Ring.Properties
open import Cubical.Algebra.Ring.Ideal

private
  variable
     : Level

module _ {R S : Ring } (f′ : RingHom R S) where
  open IsRingHom (f′ .snd)
  open RingStr ⦃...⦄
  open isIdeal
  open RingTheory
  private
    instance
      _ = R
      _ = S
      _ = snd R
      _ = snd S
    f = fst f′

  kernel : fst R  hProp 
  kernel x = (f x  0r) , is-set _ _

  kernelIsIdeal : isIdeal R kernel
  +-closed kernelIsIdeal =
    λ fx≡0 fy≡0  f (_ + _)  ≡⟨ pres+ _ _ 
                  f _ + f _  ≡⟨ cong  u  u + f _) fx≡0 
                  0r + f _   ≡⟨ cong  u  0r + u) fy≡0 
                  0r + 0r    ≡⟨ 0Idempotent S 
                  0r 
  -closed kernelIsIdeal =
    λ fx≡0  f (- _)  ≡⟨ pres- _ 
             - f _    ≡⟨ cong -_ fx≡0 
             - 0r     ≡⟨ 0Selfinverse S 
             0r       
  0r-closed kernelIsIdeal = f 0r ≡⟨ pres0  0r 
  ·-closedLeft kernelIsIdeal = λ r fx≡0 
    f (r · _)    ≡⟨ pres· _ _ 
    f r · f (_)  ≡⟨ cong  u  f r · u) fx≡0 
    f r · 0r     ≡⟨ 0RightAnnihilates S _ 
    0r 
  ·-closedRight kernelIsIdeal = λ r fx≡0 
    f (_ · r)    ≡⟨ pres· _ _ 
    f _ · f r     ≡⟨ cong  u  u · f r) fx≡0 
    0r · f r      ≡⟨ 0LeftAnnihilates S _ 
    0r 

  kernelIdeal : IdealsIn R
  fst kernelIdeal = kernel
  snd kernelIdeal = kernelIsIdeal


  kernelFiber : (x y :  R )  f x  f y  x - y  kernel
  kernelFiber x y fx≡fy = f (x - y)     ≡⟨ pres+ x (- y) 
                          f x + f (- y) ≡[ i ]⟨ fx≡fy i + pres- y i 
                          f y - f y     ≡⟨ +InvR (f y) 
                          0r