{-# OPTIONS --lossy-unification #-}
module Cubical.Algebra.CommRing.Quotient.Base where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Structure
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Function
open import Cubical.Foundations.Powerset
open import Cubical.Functions.Surjection

open import Cubical.Data.Nat hiding (_+_)
open import Cubical.Data.FinData
open import Cubical.Data.Sigma using (Σ≡Prop)

open import Cubical.HITs.SetQuotients as SQ renaming (_/_ to _/ₛ_)
open import Cubical.HITs.PropositionalTruncation as PT

open import Cubical.Algebra.CommRing
open import Cubical.Algebra.CommRing.Ideal
open import Cubical.Algebra.CommRing.FGIdeal
open import Cubical.Algebra.CommRing.Kernel
open import Cubical.Algebra.Ring
import Cubical.Algebra.Ring.Quotient as Ring

private
  variable
    ℓ ℓ' ℓ'' : Level

module _ (R : CommRing ℓ) (I : IdealsIn R) where
  open CommRingStr (snd R)
  R/I = ⟨ R ⟩ /ₛ (λ x y → x - y ∈ (fst I))

  quotientCommRingStr : CommRingStr R/I
  quotientCommRingStr = snd
    (Ring→CommRing
        ((CommRing→Ring R) Ring./ (CommIdeal→Ideal I))
        (elimProp2 (λ _ _ → squash/ _ _)
                   λ x y i → [ CommRingStr.·Comm (snd R) x y i ]))

_/_ : (R : CommRing ℓ) (I : IdealsIn R) → CommRing ℓ
fst (R / I) = R/I R I
snd (R / I) = quotientCommRingStr R I

[_]/ : {R : CommRing ℓ} {I : IdealsIn R} → (a : fst R) → fst (R / I)
[ a ]/ = SQ.[ a ]

module Coherence (R : CommRing ℓ) (I : IdealsIn R) where
  opaque
    isRingHomCoh : IsRingHom (snd (CommRing→Ring (R / I)))
                             (λ x → x)
                             (snd ((CommRing→Ring R) Ring./ (CommIdeal→Ideal I)))
    IsRingHom.pres0 isRingHomCoh = refl
    IsRingHom.pres1 isRingHomCoh = refl
    IsRingHom.pres+ isRingHomCoh = λ _ _ → refl
    IsRingHom.pres· isRingHomCoh = λ _ _ → refl
    IsRingHom.pres- isRingHomCoh = λ _ → refl
    isRingHomCohInv : IsRingHom (snd ((CommRing→Ring R) Ring./ (CommIdeal→Ideal I)))
                             (λ x → x)
                             (snd (CommRing→Ring (R / I)))
    IsRingHom.pres0 isRingHomCohInv = refl
    IsRingHom.pres1 isRingHomCohInv = refl
    IsRingHom.pres+ isRingHomCohInv = λ _ _ → refl
    IsRingHom.pres· isRingHomCohInv = λ _ _ → refl
    IsRingHom.pres- isRingHomCohInv = λ _ → refl

    0r≡ : RingStr.0r (CommRing→Ring (R / I) .snd) ≡ RingStr.0r ((CommRing→Ring R Ring./ CommIdeal→Ideal I) .snd)
    0r≡ = refl

  ringStr : RingHom (CommRing→Ring (R / I))
                ((CommRing→Ring R) Ring./ (CommIdeal→Ideal I))

  fst ringStr x = x
  (snd ringStr) = isRingHomCoh

  ringStrInv : RingHom ((CommRing→Ring R) Ring./ (CommIdeal→Ideal I))
                   (CommRing→Ring (R / I))

  fst ringStrInv x = x
  (snd ringStrInv) = isRingHomCohInv


open RingHoms

module _ (R : CommRing ℓ) (I : IdealsIn R) where

  quotientHom : CommRingHom R (R / I)
  quotientHom =
    withOpaqueStr $
    RingHom→CommRingHom $
        Coherence.ringStrInv R I
     ∘r Ring.quotientHom (CommRing→Ring R) (CommIdeal→Ideal I)

  quotientHomSurjective : isSurjection (quotientHom .fst)
  quotientHomSurjective = Ring.quotientHomSurjective (CommRing→Ring R) (CommIdeal→Ideal I)

  quotientHomEpi : (S : hSet ℓ')
                   → (f g : ⟨ R / I ⟩ → ⟨ S ⟩)
                   → f ∘ quotientHom .fst ≡ g ∘ quotientHom .fst
                   → f ≡ g
  quotientHomEpi S f g p =
      (Ring.quotientHomEpi
         (CommRing→Ring R) (CommIdeal→Ideal I) S
         f g p)

module Quotient-FGideal-CommRing-Ring
  (R : CommRing ℓ)
  (S : Ring ℓ')
  (f : RingHom (CommRing→Ring R) S)
  {n : ℕ}
  (v : FinVec ⟨ R ⟩ n)
  (fnull : (k : Fin n) → f $r v k ≡ RingStr.0r (snd S))
  where

  open RingStr (snd S) using (0r; is-set)

  Iv = generatedIdeal R v

  zeroOnGeneratedIdeal : (x : ⟨ R ⟩) → x ∈ fst Iv → f $r x ≡ 0r
  zeroOnGeneratedIdeal x x∈FGIdeal =
    PT.elim
      (λ _ → is-set (f $r x) 0r)
      (λ {(α , isLC) → subst _ (sym isLC) (cancelLinearCombination R S f _ α v fnull)})
      x∈FGIdeal

  inducedHom : RingHom (CommRing→Ring (R / (generatedIdeal _ v))) S
  inducedHom = Ring.UniversalProperty.inducedHom
                 (CommRing→Ring R) (CommIdeal→Ideal Iv) f zeroOnGeneratedIdeal
               ∘r (Coherence.ringStr R Iv)

module Quotient-FGideal-CommRing-CommRing
  (R : CommRing ℓ)
  (S : CommRing ℓ')
  (f : CommRingHom R S)
  {n : ℕ}
  (v : FinVec ⟨ R ⟩ n)
  (fnull : (k : Fin n) → f $cr v k ≡ CommRingStr.0r (snd S))
  where

  inducedHom : CommRingHom (R / (generatedIdeal _ v)) S
  inducedHom = RingHom→CommRingHom $
               Quotient-FGideal-CommRing-Ring.inducedHom R (CommRing→Ring S) (CommRingHom→RingHom f) v fnull

module UniversalProperty
  (R S : CommRing ℓ)
  (I : IdealsIn R)
  (f : CommRingHom R S)
  (I⊆ker : (x : ⟨ R ⟩) → x ∈ fst I → fst f x ≡ CommRingStr.0r (snd S))
  where

  inducedHom : CommRingHom (R / I) S
  inducedHom =
    withOpaqueStr $
    RingHom→CommRingHom $
       Ring.UniversalProperty.inducedHom
         (CommRing→Ring R)
         (CommIdeal→Ideal I)
         (CommRingHom→RingHom f)
         I⊆ker
      ∘r Coherence.ringStr R I

  opaque
    isSolution : inducedHom ∘cr quotientHom R I ≡ f
    isSolution = Σ≡Prop (λ _ → isPropIsCommRingHom _ _ _)
                       (cong fst (Ring.UniversalProperty.solution
                                        (CommRing→Ring R)
                                        (CommIdeal→Ideal I)
                                        (CommRingHom→RingHom f)
                                        I⊆ker))

  opaque
    isUnique : (ψ : CommRingHom (R / I) S) → (ψIsSolution : ψ .fst ∘ quotientHom R I .fst ≡ f .fst)
             →  ψ ≡ inducedHom
    isUnique ψ ψIsSolution =
      Σ≡Prop (λ _ → isPropIsCommRingHom _ _ _)
             (cong fst
                   (Ring.UniversalProperty.unique'
                       (CommRing→Ring R)
                       (CommIdeal→Ideal I)
                       (CommRingHom→RingHom f)
                       I⊆ker
                       (CommRingHom→RingHom ψ)
                       ψIsSolution))


module _ {R : CommRing ℓ} (I : IdealsIn R) where
  open CommRingStr ⦃...⦄
  private
    π = quotientHom R I
    instance _ = snd R
             _ = snd (R / I)

  opaque
    kernel≡I : kernelIdeal R (R / I) π ≡ I
    kernel≡I =
      Σ≡Prop (CommIdeal.isPropIsCommIdeal _)
            (funExt
             λ x → Σ≡Prop (λ _ → isPropIsProp)
                     let reason = cong (λ y → π .fst x ≡ y) (Coherence.0r≡ R I)
                     in (π .fst x ≡ RingStr.0r (CommRing→Ring (R / I) .snd)                       ≡⟨ reason ⟩
                         π .fst x ≡ RingStr.0r ((CommRing→Ring R Ring./ CommIdeal→Ideal I) .snd) ∎))
     ∙ cong Ideal→CommIdeal (Ring.kernel≡I (CommIdeal→Ideal I))

    equatedToDiffInKernel : (x y : ⟨ R ⟩ ) → π $cr x ≡ π $cr y → (x - y) ∈ fst I
    equatedToDiffInKernel x y p = transport (cong (λ J → (x - y) ∈ (fst J) ) kernel≡I) $ equalIfDiffInKernelπ x y p  where
      equalIfDiffInKernelπ :  (x y : ⟨ R ⟩ ) → π $cr x ≡ π $cr y → x - y ∈ fst (kernelIdeal R (R / I ) π )
      equalIfDiffInKernelπ x y p = kernelFiber R (R / I)  π  x y p

  open IsCommRingHom (snd π)

  trivialQuotient→1∈I : Path ⟨ R / I ⟩ 1r 0r → 1r ∈ fst I
  trivialQuotient→1∈I p =
    transport (cong (λ a → a ∈ fst I ) q) (equatedToDiffInKernel 1r 0r p')  where
      p' : π $cr 1r ≡ π  $cr 0r
      p' = pres1 ∙ p ∙ sym pres0
      q : 1r - 0r ≡ 1r
      q = 1r - 0r
             ≡⟨⟩
          1r + (- 0r)
             ≡⟨ cong (1r +_) (RingTheory.0Selfinverse (CommRing→Ring R)) ⟩
          1r + 0r
             ≡⟨ +IdR 1r ⟩
          1r ∎

  zeroOnIdeal : (x : ⟨ R ⟩) → x ∈ fst I → fst π x ≡ 0r
  zeroOnIdeal x x∈I = subst (λ P → fst ((fst P) x)) (sym kernel≡I) x∈I