Int.quot

-- ℤ/nℤ — the abstract machinery, run on a real group.
--
-- Everything above this file is stated at an abstract (G , g); this is
-- the check that it can be INSTANTIATED, and it is short because the
-- only things an instance has to supply are three bridges and three
-- closure proofs.
--
-- The bridges say what Int.group.intAddGroup's projections are. Naming
-- them once means no later item ever normalises through a spine of
-- .π₁s to find out that gop Int intAddGroup is intAdd.

import Core.id (Id, idToEq, eqToId)
import Int (Int, intZero, intOne, intNeg, intNegZero)
import Int.add (+, intAddComm, intAddAssoc)
import Int.mul (*, intMulZeroR, intMulOneR, intMulDistribL, intMulNegR, intMulAssoc, intMulComm)
import Rat.frac (intAddZeroL, intAddZeroR)
import Int.group (intAddGroup, intAddMonoid)
import Algebra.monoid (IsMonoid)
import Algebra.group (IsGroup)
import Algebra.groupTheory (gop, ge, ginv)
import Algebra.subgroup (IsSubgroup, IsNormal, sgIntro, sgUnit, sgOp, sgInv, abelianNormal, cosetRel)
import Algebra.quotGroup (QGroup, qcls, qclsEq, qclsEffective, qMul, qMulCls, qInv, qUnit, qIsGroup)
import Algebra.ring (IsCommRing)
import Algebra.ringTheory (raddGroup, rmul, rone)
import Algebra.ideal (IsIdeal, idIntro, idSub, idScale, idNormal)
import Int.ring (intCommRing)
import Algebra.quotRing (QRing, qrCls, qrMul, qrOne, qrAdd, qrAddGroup, qrIsCommRing)
import Core.equality (transportP, sym, trans, cong)

intGop : (x y : Int) → gop intAddGroup x y ≡ x + y
  using (Algebra.groupTheory.gop.eq, Int.group.intAddGroup.eq)
intGop = λx y. ⋆

intGe : ge intAddGroup ≡ intZero using (Algebra.groupTheory.ge.eq, Int.group.intAddGroup.eq)
intGe = ⋆

intGinv : (x : Int) → ginv intAddGroup x ≡ intNeg x
  using (Algebra.groupTheory.ginv.eq, Int.group.intAddGroup.eq)
intGinv = λx. ⋆

-- ℤ is abelian, in the group-theoretic vocabulary
intGopComm : (x y : Int) → gop intAddGroup x y ≡ gop intAddGroup y x
intGopComm = λx y. trans _ _ _ (intGop x y) (trans _ _ _ (intAddComm x y) (sym _ _ (intGop y x)))

-- ===== nℤ =====
--
-- "x is a multiple of n", with the witness under an Ω-squash: the
-- predicate a quotient's relation must be Ω-valued (ty-quot), and
-- nothing below ever needs the multiplier back as data — the three
-- closure proofs each unpack their hypotheses and repackage a new
-- witness, which is exactly what el-squash-e-prf allows.
nZfib : Int → Int → 𝕌
nZfib = λn x. (k : Int) × Id _ (n * k) x

nZ : Int → Int → Ω
nZ = λn x. ∥nZfib n x∥

nZIntro : (n x k : Int) → (n * k ≡ x) → nZ n x using (nZ.eq, nZfib.unfold)
nZIntro = λn x k e. ⋆ (k, eqToId _ _ e)

-- 0 = n · 0
nZUnit : (n : Int) → nZ n (ge intAddGroup)
nZUnit = λn. nZIntro _ _ _ (trans (n * intZero) _ _ intMulZeroR (sym _ _ intGe))

-- n·k₁ + n·k₂ = n·(k₁+k₂)
nZOp : (n x y : Int) → nZ n x → nZ n y → nZ n (gop intAddGroup x y) using (nZ.eq, nZfib.unfold)
nZOp =
  λn x y hx hy. squash-elim
    hx
    u. squash-elim
      hy
      v. nZIntro
        _
        _
        u .π₁ + v .π₁
        n * (u .π₁ + v .π₁)
          ≡⟨ intMulDistribL n (u .π₁) (v .π₁) ⟩ n * u .π₁ + n * v .π₁
          ≡⟨ cong (λw. Int) (λw. w + n * v .π₁) (idToEq _ _ _ (u .π₂)) ⟩ x + n * v .π₁
          ≡⟨ cong (λw. Int) (λw. x + w) (idToEq _ _ _ (v .π₂)) ⟩ x + y
          ≡⟨ sym _ _ (intGop x y) ⟩ gop intAddGroup x y

-- n·(−k) = −(n·k)
nZInv : (n x : Int) → nZ n x → nZ n (ginv intAddGroup x) using (nZ.eq, nZfib.unfold)
nZInv =
  λn x hx. squash-elim
    hx
    u. nZIntro
      _
      _
      intNeg (u .π₁)
      n * intNeg (u .π₁)
        ≡⟨ intMulNegR n (u .π₁) ⟩ intNeg (n * u .π₁)
        ≡⟨ cong (λw. Int) (λw. intNeg w) (idToEq _ _ _ (u .π₂)) ⟩ intNeg x
        ≡⟨ sym _ _ (intGinv x) ⟩ ginv intAddGroup x

nZIsSubgroup : (n : Int) → IsSubgroup intAddGroup (nZ n)
nZIsSubgroup = λn. sgIntro (nZUnit n) (nZOp n) (nZInv n)

-- ...and normal for free, ℤ being abelian
nZIsNormal : {n : Int} → IsNormal intAddGroup (nZ n)
nZIsNormal = λn. abelianNormal intGopComm

-- ===== ℤ/nℤ =====
IntMod : Int → 𝕌
IntMod = λn. QGroup _ intAddGroup (nZ n)

intModGroup : (n : Int) → IsGroup (IntMod n) using (IntMod.eq)
intModGroup = λn. qIsGroup _ _ _ (nZIsSubgroup n) nZIsNormal

intModCls : {n : Int} → Int → IntMod n using (IntMod.eq)
intModCls = λn. qcls intAddGroup (nZ n)

-- every multiple of n is zero in ℤ/nℤ — the defining property, at
-- abstract n and k, with no numeral in sight
intModMulZero : {n k : Int} → intModCls (n * k) ≡ intModCls intZero ∈ IntMod n
  using (intModCls.eq, Algebra.subgroup.cosetRel.eq)
intModMulZero =
  λn k. qclsEq
    nZIsSubgroup n
    n * k
    intZero
    nZIntro
      n
      gop intAddGroup (n * k) (ginv intAddGroup intZero)
      k
      n * k
        ≡⟨ sym _ _ (intAddZeroR (n * k)) ⟩ n * k + intZero
        ≡⟨ cong (λw. Int) (λw. n * k + w) (sym _ _ (trans _ _ _ (intGinv intZero) intNegZero)) ⟩
          n * k + ginv intAddGroup intZero
        ≡⟨ sym _ _ (intGop (n * k) (ginv intAddGroup intZero)) ⟩
          gop intAddGroup (n * k) (ginv intAddGroup intZero)

-- the instance in the smallest concrete case: n is zero in ℤ/nℤ
intModSelf : (n : Int) → intModCls n ≡ intModCls intZero ∈ IntMod n
intModSelf =
  λn. trans _ _ _ (cong (λw. IntMod n) (λw. intModCls w) (sym _ _ (intMulOneR n))) intModMulZero

-- ===== ...and ℤ/nℤ is a RING =====
--
-- nℤ is not just a subgroup: it is an IDEAL, because a·(n·k) = n·(a·k).
-- One bridge (raddGroup Int intCommRing is intAddGroup, by β) and one
-- closure proof, and Algebra/quotRing.nova supplies the rest.
intRaddGroup : raddGroup intCommRing ≡ intAddGroup
  using (Algebra.ringTheory.raddGroup.eq, Int.ring.intCommRing.eq)
intRaddGroup = ⋆

intRmul : (x y : Int) → rmul _ intCommRing x y ≡ x * y
  using (Algebra.ringTheory.rmul.eq, Int.ring.intCommRing.eq)
intRmul = λx y. ⋆

-- a·(n·k) = n·(a·k): one associativity and one commutation
nZScaleAlg : (n a k : Int) → a * (n * k) ≡ n * (a * k)
nZScaleAlg =
  λn a k. a * (n * k)
    ≡⟨ sym _ _ (intMulAssoc a n k) ⟩ a * n * k
    ≡⟨ cong (λw. Int) (λw. w * k) (intMulComm a n) ⟩ n * a * k
    ≡⟨ intMulAssoc n a k ⟩ n * (a * k)

nZScale : (n a x : Int) → nZ n x → nZ n (rmul _ intCommRing a x) using (nZ.eq, nZfib.unfold)
nZScale =
  λn a x hx. squash-elim
    hx
    u. nZIntro
      _
      _
      a * u .π₁
      n * (a * u .π₁)
        ≡⟨ sym _ _ (nZScaleAlg n a (u .π₁)) ⟩ a * (n * u .π₁)
        ≡⟨ cong (λw. Int) (λw. a * w) (idToEq _ _ _ (u .π₂)) ⟩ a * x
        ≡⟨ sym _ _ (intRmul a x) ⟩ rmul _ intCommRing a x

nZIsIdeal : (n : Int) → IsIdeal _ intCommRing (nZ n) using (intRaddGroup.rw)
nZIsIdeal = λn. idIntro (nZIsSubgroup n) (nZScale n)

-- ℤ/nℤ, as a commutative ring
intModRing : (n : Int) → IsCommRing (IntMod n)
  using (IntMod.eq,
    Algebra.quotRing.QRing.eq,
    Algebra.ringTheory.raddGroup.eq,
    Int.ring.intCommRing.eq)
intModRing = λn. qrIsCommRing (nZIsIdeal n)