Algebra.quotRing

-- THE QUOTIENT RING R/I.
--
-- The additive group is already done: an ideal is a normal subgroup of
-- (R , +) (Algebra.ideal.idNormal), so Algebra/quotGroup.nova supplies
-- the carrier, the addition, the negation and IsGroup outright. What is
-- new is the MULTIPLICATION, and it descends by the same nested
-- quot-elim, owing the same two well-definedness proofs.
--
-- The contrast with Algebra/quotGroup.nova is the point of this module.
-- There, the outer half could not be got by commuting and the two
-- halves were genuinely different statements — the inner one needed
-- normality, the outer one nothing. Here BOTH halves are the ideal's
-- single closure law, applied on different sides:
--
--   INNER   a·b − a·b' = a·(b − b')   —  idScale  (a on the left)
--   OUTER   a·b − a'·b = (a − a')·b   —  idScaleR (b on the right)
--
-- and idScaleR is idScale composed with rMulComm. So commutativity does
-- pay for the outer half after all — but as a fact about the IDEAL,
-- not as Real.seq.wdOuterOfComm's trick on the operation. In a
-- non-commutative ring the two would be the two halves of "two-sided
-- ideal", and neither would follow from the other.

import Core.id (Id, idToEq, eqToId)
import Algebra.monoid (IsMonoid)
import Algebra.group (IsGroup)
import Algebra.ring (IsCommRing)
import Algebra.groupTheory (gop, ge, ginv, gAssoc, gUnitL, gUnitR, gInvL, gInvR)
import Algebra.ringTheory (raddGroup, rmul, rone, rMulAssoc, rMulComm, rMulOne, rAddComm, rDistribL, rDistribR, rMulZero, rMulNeg, rMulSub)
import Algebra.subgroup (IsSubgroup, IsNormal, cosetRel, cosetRefl, cosetSymm, cosetTrans)
import Algebra.ideal (IsIdeal, idSub, idScale, idScaleR, idNormal)
import Algebra.quotGroup (QGroup, qcls, qclsEq, qclsEffective, qMul, qMulCls, qInv, qUnit, qIsGroup, qAssoc, qUnitL, qUnitR)
import Core.quotEffective (classEqOfRel)
import Core.equality (transportP, sym, trans, cong)

QRing : (R : 𝕌) (r : IsCommRing R) (I : R → Ω) → 𝕌
QRing = λR r I. QGroup _ (raddGroup r) I

qrCls : {R : 𝕌} {r : IsCommRing R} {I : R → Ω} → R → QRing _ r I using (QRing.eq)
qrCls = λR r I. qcls (raddGroup r) I

-- ===== the two well-definedness proofs =====
qrMulWDInner : {R : 𝕌}
  {r : IsCommRing R}
  {I : R → Ω}
  → IsIdeal _ r I
    → {a b b' : R}
      → cosetRel (raddGroup r) I b b' → cosetRel (raddGroup r) I (rmul _ r a b) (rmul _ r a b')
  using (Algebra.subgroup.cosetRel.eq)
qrMulWDInner =
  λR r I id a b b' h. transportP
    I
    sym _ _ (rMulSub _ r a b b')
    idScale _ _ _ id a (gop (raddGroup r) b (ginv (raddGroup r) b')) h

qrMulWDOuter : {R : 𝕌}
  {r : IsCommRing R}
  {I : R → Ω}
  → IsIdeal _ r I
    → {a a' b : R}
      → cosetRel (raddGroup r) I a a' → cosetRel (raddGroup r) I (rmul _ r a b) (rmul _ r a' b)
  using (Algebra.subgroup.cosetRel.eq)
qrMulWDOuter =
  λR r I id a a' b h. transportP
    I
    {rmul _ r (gop (raddGroup r) a (ginv (raddGroup r) a')) b}
    {gop (raddGroup r) (rmul _ r a b) (ginv (raddGroup r) (rmul _ r a' b))}
    rmul _ r (gop (raddGroup r) a (ginv (raddGroup r) a')) b
      ≡⟨ rMulComm _ r (gop (raddGroup r) a (ginv (raddGroup r) a')) b ⟩
        rmul _ r b (gop (raddGroup r) a (ginv (raddGroup r) a'))
      ≡⟨ sym _ _ (rMulSub _ r b a a') ⟩
        gop (raddGroup r) (rmul _ r b a) (ginv (raddGroup r) (rmul _ r b a'))
      ≡⟨ cong
        λw. R
        λw. gop (raddGroup r) w (ginv (raddGroup r) (rmul _ r b a'))
        rMulComm _ r b a ⟩
        gop (raddGroup r) (rmul _ r a b) (ginv (raddGroup r) (rmul _ r b a'))
      ≡⟨ cong
        λw. R
        λw. gop (raddGroup r) (rmul _ r a b) (ginv (raddGroup r) w)
        rMulComm _ r b a' ⟩
        gop (raddGroup r) (rmul _ r a b) (ginv (raddGroup r) (rmul _ r a' b))
    idScaleR _ _ _ id b (gop (raddGroup r) a (ginv (raddGroup r) a')) h

-- ===== the descent, in qrCls vocabulary (B-21) =====
qrMulWDInnerCls : (R : 𝕌)
  (r : IsCommRing R)
  (I : R → Ω)
  → IsIdeal _ r I
    → (a b b' : R)
      → cosetRel (raddGroup r) I b b' → qrCls (rmul _ r a b) ≡ qrCls (rmul _ r a b') ∈ QRing _ r I
  using (qrCls.eq, Algebra.quotGroup.qcls.eq)
qrMulWDInnerCls =
  λR r I id a b b' h. classEqOfRel
    cosetRel (raddGroup r) I
    rmul _ r a b
    rmul _ r a b'
    qrMulWDInner id h

qrMulWDOuterCls : {R : 𝕌}
  {r : IsCommRing R}
  {I : R → Ω}
  → IsIdeal _ r I
    → {a a' b : R}
      → cosetRel (raddGroup r) I a a' → qrCls (rmul _ r a b) ≡ qrCls (rmul _ r a' b) ∈ QRing _ r I
  using (qrCls.eq, Algebra.quotGroup.qcls.eq)
qrMulWDOuterCls =
  λR r I id a a' b h. classEqOfRel
    cosetRel (raddGroup r) I
    rmul _ r a b
    rmul _ r a' b
    qrMulWDOuter id h

qrMulWDOuterElim : (R : 𝕌)
  (r : IsCommRing R)
  (I : R → Ω)
  → IsIdeal _ r I
    → (x x' : R)
      → cosetRel (raddGroup r) I x x'
        → (v : QRing _ r I)
          → quot-elim (w. QRing _ r I) (q. qrCls (rmul _ r x q)) v
            ≡ quot-elim (q. qrCls (rmul _ r x' q)) v
  using (QRing.eq, Algebra.quotGroup.QGroup.unfold, qrMulWDInnerCls)
qrMulWDOuterElim =
  λR r I id x x' h v. quot-elim
    w. quot-elim (z. QRing _ r I) (q. qrCls (rmul _ r x q)) w
      ≡ quot-elim (q. qrCls (rmul _ r x' q)) w
    c. qrMulWDOuterCls id h
    v

qrMul : (R : 𝕌)
  (r : IsCommRing R)
  (I : R → Ω)
  → IsIdeal _ r I → QRing _ r I → QRing _ r I → QRing _ r I
  using (QRing.eq, Algebra.quotGroup.QGroup.unfold, qrMulWDInnerCls, qrMulWDOuterElim)
qrMul = λR r I id u v. quot-elim (p. quot-elim (q. qrCls (rmul _ r p q)) v) u

qrMulCls : (R : 𝕌)
  (r : IsCommRing R)
  (I : R → Ω)
  (id : IsIdeal _ r I)
  (a b : R)
  → qrMul _ _ _ id (class a) (class b) ≡ class (rmul _ r a b)
  using (QRing.eq, qrCls.eq, Algebra.quotGroup.QGroup.unfold, Algebra.quotGroup.qcls.eq, qrMul.eq)
qrMulCls = λR r I id a b. ⋆

qrOne : {R : 𝕌} {r : IsCommRing R} {I : R → Ω} → QRing _ r I
  using (QRing.eq, Algebra.quotGroup.QGroup.unfold)
qrOne = λR r I. class (rone r)

-- ===== the additive side, renamed =====
--
-- Algebra/quotGroup.nova already built it; these three names only put
-- it in ring vocabulary and bridge qIsGroup's projections once.
qrAddGroup : {R : 𝕌} {r : IsCommRing R} {I : R → Ω} → IsIdeal _ r I → IsGroup (QRing _ r I)
  using (QRing.eq)
qrAddGroup = λR r I id. qIsGroup _ _ _ (idSub id) (idNormal _ r I)

qrAdd : {R : 𝕌}
  {r : IsCommRing R}
  {I : R → Ω}
  → IsIdeal _ r I → QRing _ r I → QRing _ r I → QRing _ r I
  using (QRing.eq)
qrAdd = λR r I id. qMul _ _ _ (idNormal _ r I)

qrGop : (R : 𝕌)
  (r : IsCommRing R)
  (I : R → Ω)
  (id : IsIdeal _ r I)
  (u v : QRing _ r I)
  → gop (qrAddGroup id) u v ≡ qrAdd id u v
  using (qrAddGroup.eq, qrAdd.eq, Algebra.groupTheory.gop.eq, Algebra.quotGroup.qIsGroup.eq)
qrGop = λR r I id u v. ⋆

qrAddCls : (R : 𝕌)
  (r : IsCommRing R)
  (I : R → Ω)
  (id : IsIdeal _ r I)
  (a b : R)
  → qrAdd id (class a) (class b) ≡ class (gop (raddGroup r) a b)
  using (QRing.eq, qrAdd.eq, Algebra.quotGroup.QGroup.unfold)
qrAddCls = λR r I id a b. qMulCls _ _ _ (idNormal _ r I) a b

-- ===== the multiplicative laws, each a descent into Ω =====
qrMulAssoc : (R : 𝕌)
  (r : IsCommRing R)
  (I : R → Ω)
  (id : IsIdeal _ r I)
  (u v w : QRing _ r I)
  → qrMul _ _ _ id (qrMul _ _ _ id u v) w ≡ qrMul _ _ _ id u (qrMul _ _ _ id v w)
  using (QRing.eq, Algebra.quotGroup.QGroup.unfold, qrMulCls.rw)
qrMulAssoc =
  λR r I id u v w. quot-elim
    a. quot-elim
      b. quot-elim
        c. trans
          _
          _
          _
          ⋆
          trans
            _
            _
            qrMul _ _ _ id (class a) (qrMul _ _ _ id (class b) (class c))
            cong
              λz. QRing _ r I
              λz. class z
              {rmul _ r (rmul _ r a b) c}
              {rmul _ r a (rmul _ r b c)}
              rMulAssoc
            ⋆
        w
      v
    u

qrMulComm : (R : 𝕌)
  (r : IsCommRing R)
  (I : R → Ω)
  (id : IsIdeal _ r I)
  (u v : QRing _ r I)
  → qrMul _ _ _ id u v ≡ qrMul _ _ _ id v u
  using (QRing.eq, Algebra.quotGroup.QGroup.unfold, qrMulCls.rw)
qrMulComm =
  λR r I id u v. quot-elim
    a. quot-elim
      b. trans
        _
        _
        _
        ⋆
        trans
          _
          _
          qrMul _ _ _ id (class b) (class a)
          cong (λz. QRing _ r I) (λz. class z) (rMulComm _ r a b)
          ⋆
      v
    u

qrMulOne : (R : 𝕌)
  (r : IsCommRing R)
  (I : R → Ω)
  (id : IsIdeal _ r I)
  (u : QRing _ r I)
  → qrMul _ _ _ id u qrOne ≡ u
  using (QRing.eq, Algebra.quotGroup.QGroup.unfold, qrOne.eq, qrMulCls.rw)
qrMulOne =
  λR r I id u. quot-elim
    a. trans _ _ _ ⋆ (cong (λz. QRing _ r I) (λz. class z) {rmul _ r a (rone r)} {a} rMulOne)
    u

qrAddComm : {R : 𝕌}
  {r : IsCommRing R}
  {I : R → Ω}
  {id : IsIdeal _ r I}
  {u v : QRing _ r I}
  → qrAdd id u v ≡ qrAdd id v u
  using (QRing.eq, Algebra.quotGroup.QGroup.unfold, qrAddCls.rw)
qrAddComm =
  λR r I id u v. quot-elim
    a. quot-elim
      b. trans
        _
        _
        _
        ⋆
        trans
          _
          _
          qrAdd id (class b) (class a)
          cong (λz. QRing _ r I) (λz. class z) (rAddComm _ r a b)
          ⋆
      v
    u

qrDistribL : {R : 𝕌}
  {r : IsCommRing R}
  {I : R → Ω}
  {id : IsIdeal _ r I}
  {u v w : QRing _ r I}
  → qrMul _ _ _ id u (qrAdd id v w) ≡ qrAdd id (qrMul _ _ _ id u v) (qrMul _ _ _ id u w)
  using (QRing.eq, Algebra.quotGroup.QGroup.unfold, qrMulCls.rw, qrAddCls.rw)
qrDistribL =
  λR r I id u v w. quot-elim
    a. quot-elim
      b. quot-elim
        c. trans
          _
          _
          _
          ⋆
          trans
            _
            _
            qrAdd id (qrMul _ _ _ id (class a) (class b)) (qrMul _ _ _ id (class a) (class c))
            cong (λz. QRing _ r I) (λz. class z) (rDistribL _ r a b c)
            ⋆
        w
      v
    u

-- ===== R/I is a commutative ring =====
qrIsCommRing : {R : 𝕌} {r : IsCommRing R} {I : R → Ω} → IsIdeal _ r I → IsCommRing (QRing _ r I)
  using (Algebra.ring.IsCommRing.unfold, Algebra.groupTheory.gop.eq)
qrIsCommRing =
  λR r I id. (,)
    qrAddGroup id
    qrMul _ _ _ id
    qrOne
    λx y z. eqToId _ _ (qrMulAssoc _ _ _ id x y z)
    λx y. eqToId _ _ (qrMulComm _ _ _ id x y)
    λx. eqToId _ _ (qrMulOne _ _ _ id x)
    λx y. eqToId
      gop (qrAddGroup id) x y
      gop (qrAddGroup id) y x
      trans
        _
        _
        _
        qrGop _ _ _ id x y
        trans (qrAdd id x y) _ _ qrAddComm (sym _ _ (qrGop _ _ _ id y x))
    λx y z. eqToId
      qrMul _ _ _ id x (gop (qrAddGroup id) y z)
      gop (qrAddGroup id) (qrMul _ _ _ id x y) (qrMul _ _ _ id x z)
      trans
        _
        _
        _
        cong (λz2. QRing _ r I) (λz2. qrMul _ _ _ id x z2) (qrGop _ _ _ id y z)
        trans
          qrMul _ _ _ id x (qrAdd id y z)
          _
          _
          qrDistribL
          sym _ _ (qrGop _ _ _ id (qrMul _ _ _ id x y) (qrMul _ _ _ id x z))