{-# OPTIONS --cubical --no-import-sorts --safe #-}
module Cubical.Algebra.Ring.QuotientRing where

open import Cubical.Foundations.Prelude
open import Cubical.Foundations.Equiv
open import Cubical.Foundations.HLevels
open import Cubical.Foundations.Structure
open import Cubical.Foundations.Powerset using (_∈_; _⊆_) -- \in, \sub=

open import Cubical.HITs.SetQuotients.Base renaming (_/_ to _/ₛ_)
open import Cubical.HITs.SetQuotients.Properties

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

private
  variable
    ℓ : Level

module _ (R' : Ring {ℓ}) (I : ⟨ R' ⟩  → hProp ℓ) (I-isIdeal : isIdeal R' I) where
  open RingStr (snd R')
  private R = ⟨ R' ⟩
  open isIdeal I-isIdeal
  open Theory R'

  R/I : Type ℓ
  R/I = R /ₛ (λ x y → x - y ∈ I)

  private
    homogeneity : ∀ (x a b : R)
                 → (a - b ∈ I)
                 → (x + a) - (x + b) ∈ I
    homogeneity x a b p = subst (λ u → u ∈ I) (translatedDifference x a b) p

    isSetR/I : isSet R/I
    isSetR/I = squash/
    [_]/I : (a : R) → R/I
    [ a ]/I = [ a ]

    lemma : (x y a : R)
            → x - y ∈ I
            → [ x + a ]/I ≡ [ y + a ]/I
    lemma x y a x-y∈I = eq/ (x + a) (y + a) (subst (λ u → u ∈ I) calculate x-y∈I)
      where calculate : x - y ≡ (x + a) - (y + a)
            calculate =
                      x - y                 ≡⟨ translatedDifference a x y ⟩
                      ((a + x) - (a + y))   ≡⟨ cong (λ u → u - (a + y)) (+Comm _ _) ⟩
                      ((x + a) - (a + y))   ≡⟨ cong (λ u → (x + a) - u) (+Comm _ _) ⟩
                      ((x + a) - (y + a))   ∎

    pre-+/I : R → R/I → R/I
    pre-+/I x = elim
                    (λ _ → squash/)
                    (λ y → [ x + y ])
                    λ y y' diffrenceInIdeal
                      → eq/ (x + y) (x + y') (homogeneity x y y' diffrenceInIdeal)

    pre-+/I-DescendsToQuotient : (x y : R) → (x - y ∈ I)
                  → pre-+/I x ≡ pre-+/I y
    pre-+/I-DescendsToQuotient x y x-y∈I i r = pointwise-equal r i
      where
        pointwise-equal : ∀ (u : R/I)
                          → pre-+/I x u ≡ pre-+/I y u
        pointwise-equal = elimProp (λ u → isSetR/I (pre-+/I x u) (pre-+/I y u))
                                   (λ a → lemma x y a x-y∈I)

    _+/I_ : R/I → R/I → R/I
    x +/I y = (elim R/I→R/I-isSet pre-+/I pre-+/I-DescendsToQuotient x) y
      where
        R/I→R/I-isSet : R/I → isSet (R/I → R/I)
        R/I→R/I-isSet _ = isSetΠ (λ _ → squash/)

    +/I-comm : (x y : R/I) → x +/I y ≡ y +/I x
    +/I-comm = elimProp2 (λ _ _ → squash/ _ _) eq
       where eq : (x y : R) → [ x ] +/I [ y ] ≡ [ y ] +/I [ x ]
             eq x y i =  [ +Comm x y i ]

    +/I-assoc : (x y z : R/I) → x +/I (y +/I z) ≡ (x +/I y) +/I z
    +/I-assoc = elimProp3 (λ _ _ _ → squash/ _ _) eq
      where eq : (x y z : R) → [ x ] +/I ([ y ] +/I [ z ]) ≡ ([ x ] +/I [ y ]) +/I [ z ]
            eq x y z i =  [ +Assoc x y z i ]


    0/I : R/I
    0/I = [ 0r ]

    1/I : R/I
    1/I = [ 1r ]

    -/I : R/I → R/I
    -/I = elim (λ _ → squash/) (λ x' → [ - x' ]) eq
      where
        eq : (x y : R) → (x - y ∈ I) → [ - x ] ≡ [ - y ]
        eq x y x-y∈I = eq/ (- x) (- y) (subst (λ u → u ∈ I) eq' (isIdeal.-closed I-isIdeal x-y∈I))
          where
            eq' = - (x + (- y))       ≡⟨ sym (-Dist _ _) ⟩
                  (- x) - (- y)       ∎

    +/I-rinv : (x : R/I) → x +/I (-/I x) ≡ 0/I
    +/I-rinv = elimProp (λ x → squash/ _ _) eq
      where
        eq : (x : R) → [ x ] +/I (-/I [ x ]) ≡ 0/I
        eq x i = [ +Rinv x i ]


    +/I-rid : (x : R/I) → x +/I 0/I ≡ x
    +/I-rid = elimProp (λ x → squash/ _ _) eq
      where
        eq : (x : R) → [ x ] +/I 0/I ≡ [ x ]
        eq x i = [ +Rid x i ]

    _·/I_ : R/I → R/I → R/I
    _·/I_ =
      elim (λ _ → isSetΠ (λ _ → squash/))
               (λ x → left· x)
               eq'
      where
        eq : (x y y' : R) → (y - y' ∈ I) → [ x · y ] ≡ [ x · y' ]
        eq x y y' y-y'∈I = eq/ _ _
                             (subst (λ u → u ∈ I)
                                  (x · (y - y')            ≡⟨ ·Rdist+ _ _ _ ⟩
                                  ((x · y) + x · (- y'))   ≡⟨ cong (λ u → (x · y) + u)
                                                                   (-DistR· x y')  ⟩
                                  (x · y) - (x · y')       ∎)
                                  (isIdeal.·-closedLeft I-isIdeal x y-y'∈I))
        left· : (x : R) → R/I → R/I
        left· x = elim (λ y → squash/)
                     (λ y → [ x · y ])
                     (eq x)
        eq' : (x x' : R) → (x - x' ∈ I) → left· x ≡ left· x'
        eq' x x' x-x'∈I i y = elimProp (λ y → squash/ (left· x y) (left· x' y))
                                       (λ y → eq′ y)
                                       y i
                              where
                                eq′ : (y : R) → left· x [ y ] ≡ left· x' [ y ]
                                eq′ y = eq/ (x · y) (x' · y)
                                            (subst (λ u → u ∈ I)
                                              ((x - x') · y         ≡⟨ ·Ldist+ x (- x') y ⟩
                                               x · y + (- x') · y   ≡⟨ cong
                                                                         (λ u → x · y + u)
                                                                         (-DistL· x' y) ⟩
                                               x · y - x' · y       ∎)
                                              (isIdeal.·-closedRight I-isIdeal y x-x'∈I))


    -- more or less copy paste from '+/I' - this is preliminary anyway
    ·/I-assoc : (x y z : R/I) → x ·/I (y ·/I z) ≡ (x ·/I y) ·/I z
    ·/I-assoc = elimProp3 (λ _ _ _ → squash/ _ _) eq
      where eq : (x y z : R) → [ x ] ·/I ([ y ] ·/I [ z ]) ≡ ([ x ] ·/I [ y ]) ·/I [ z ]
            eq x y z i =  [ ·Assoc x y z i ]

    ·/I-lid : (x : R/I) → 1/I ·/I x ≡ x
    ·/I-lid = elimProp (λ x → squash/ _ _) eq
      where
        eq : (x : R) → 1/I ·/I [ x ] ≡ [ x ]
        eq x i = [ ·Lid x i ]

    ·/I-rid : (x : R/I) → x ·/I 1/I ≡ x
    ·/I-rid = elimProp (λ x → squash/ _ _) eq
      where
        eq : (x : R) → [ x ] ·/I 1/I ≡ [ x ]
        eq x i = [ ·Rid x i ]


    /I-ldist : (x y z : R/I) → (x +/I y) ·/I z ≡ (x ·/I z) +/I (y ·/I z)
    /I-ldist = elimProp3 (λ _ _ _ → squash/ _ _) eq
      where
        eq : (x y z : R) → ([ x ] +/I [ y ]) ·/I [ z ] ≡ ([ x ] ·/I [ z ]) +/I ([ y ] ·/I [ z ])
        eq x y z i = [ ·Ldist+ x y z i ]

    /I-rdist : (x y z : R/I) → x ·/I (y +/I z) ≡ (x ·/I y) +/I (x ·/I z)
    /I-rdist = elimProp3 (λ _ _ _ → squash/ _ _) eq
      where
        eq : (x y z : R) → [ x ] ·/I ([ y ] +/I [ z ]) ≡ ([ x ] ·/I [ y ]) +/I ([ x ] ·/I [ z ])
        eq x y z i = [ ·Rdist+ x y z i ]

  asRing : Ring {ℓ}
  asRing = makeRing 0/I 1/I _+/I_ _·/I_ -/I isSetR/I
                    +/I-assoc +/I-rid +/I-rinv +/I-comm
                    ·/I-assoc ·/I-rid ·/I-lid /I-rdist /I-ldist

_/_ : (R : Ring {ℓ}) → (I : IdealsIn R) → Ring {ℓ}
R / (I , IisIdeal) = asRing R I IisIdeal

[_]/I : {R : Ring {ℓ}} {I : IdealsIn R} → (a : ⟨ R ⟩) → ⟨ R / I ⟩
[ a ]/I = [ a ]


module UniversalProperty (R : Ring {ℓ}) (I : IdealsIn R) where
  open RingStr ⦃...⦄
  open Theory ⦃...⦄
  Iₛ = fst I
  private
    instance
      _ = R
      _ = snd R

  module _ {S : Ring {ℓ}} (φ : RingHom R S) where
    open RingHom φ renaming (map to f)
    open HomTheory φ
    private
      instance
        _ = S
        _ = snd S

    inducedHom : Iₛ ⊆ kernelSubtype φ → RingHom (R / I) S
    f (inducedHom Iₛ⊆kernel) = elim
                                 (λ _ → isSetRing S)
                                 f
                                 λ r₁ r₂ r₁-r₂∈I → equalByDifference (f r₁) (f r₂)
                                   (f r₁ - f r₂     ≡⟨ cong (λ u → f r₁ + u) (sym (-commutesWithHom _)) ⟩
                                    f r₁ + f (- r₂) ≡⟨ sym (isHom+ _ _) ⟩
                                    f (r₁ - r₂)     ≡⟨ Iₛ⊆kernel (r₁ - r₂) r₁-r₂∈I ⟩
                                    0r ∎)
    pres1 (inducedHom Iₛ⊆kernel) = pres1
    isHom+ (inducedHom Iₛ⊆kernel) =
      elimProp2 (λ _ _ → isSetRing S _ _) isHom+
    isHom· (inducedHom Iₛ⊆kernel) =
      elimProp2 (λ _ _ → isSetRing S _ _) isHom·
    {-
      ringhom (elim
                                 (λ _ → isSetRing S)
                                 f
                                 λ r₁ r₂ r₁-r₂∈I → equalByDifference (f r₁) (f r₂)
                                   (f r₁ - f r₂     ≡⟨ cong (λ u → f r₁ + u) (sym (-commutesWithHom _)) ⟩
                                    f r₁ + f (- r₂) ≡⟨ sym (isHom+ _ _) ⟩
                                    f (r₁ - r₂)     ≡⟨ Iₛ⊆kernel (r₁ - r₂) r₁-r₂∈I ⟩
                                    0r ∎))
              pres1
              (elimProp2 (λ _ _ → isSetRing S _ _) isHom+)
              (elimProp2 (λ _ _ → isSetRing S _ _) isHom·)
              -}

    solution : (p : Iₛ ⊆ kernelSubtype φ)
               → (x : ⟨ R ⟩) → inducedHom p $ [ x ] ≡ φ $ x
    solution p x = refl

    unique : (p : Iₛ ⊆ kernelSubtype φ)
             → (ψ : RingHom (R / I) S) → (ψIsSolution : (x : ⟨ R ⟩) → ψ $ [ x ] ≡ φ $ x)
             → (x : ⟨ R ⟩) → ψ $ [ x ] ≡ inducedHom p $ [ x ]
    unique p ψ ψIsSolution x = ψIsSolution x