Algebra.ideal

-- IDEALS.
--
-- An ideal is an additive SUBGROUP closed under multiplication by
-- arbitrary ring elements. Both halves are ฮฉ-valued propositions, for
-- the same reason Algebra/subgroup.nova's are: the quotient's relation
-- must be.
--
-- The additive half is Algebra/subgroup.nova's IsSubgroup at the ring's
-- additive group โ€” nothing is restated. And because that group is
-- abelian (rAddComm), idNormal is Algebra.subgroup.abelianNormal
-- applied and nothing more: an ideal is automatically a normal
-- subgroup, so the whole of Algebra/quotGroup.nova is available to R/I
-- before a single new well-definedness proof is written. Only the
-- MULTIPLICATION has to descend, and that is Algebra/quotRing.nova.

import Core.prop (โˆง, andIntro, andFst, andSnd)
import Algebra.monoid (IsMonoid)
import Algebra.group (IsGroup)
import Algebra.ring (IsCommRing)
import Algebra.groupTheory (gop, ge, ginv)
import Algebra.ringTheory (raddGroup, rmul, rone, rMulComm, rAddComm, rMulSub)
import Algebra.subgroup (IsSubgroup, IsNormal, sgIntro, sgUnit, sgOp, sgInv, abelianNormal, cosetRel)
import Core.equality (transportP, sym, trans, cong)

closedScale : (R : ๐•Œ) (r : IsCommRing R) (I : R โ†’ ฮฉ) โ†’ ฮฉ
closedScale = ฮปR r I. โˆฅ(a x : R) โ†’ I x โ†’ I (rmul _ r a x)โˆฅ

IsIdeal : (R : ๐•Œ) (r : IsCommRing R) (I : R โ†’ ฮฉ) โ†’ ฮฉ
IsIdeal = ฮปR r I. IsSubgroup (raddGroup r) I โˆง closedScale _ r I

idIntro : {R : ๐•Œ}
  {r : IsCommRing R}
  {I : R โ†’ ฮฉ}
  โ†’ IsSubgroup (raddGroup r) I โ†’ ((a x : R) โ†’ I x โ†’ I (rmul _ r a x)) โ†’ IsIdeal _ r I
  using (IsIdeal.eq, closedScale.eq)
idIntro = ฮปR r I sub sc. andIntro sub (โ‹† sc)

idSub : {R : ๐•Œ} {r : IsCommRing R} {I : R โ†’ ฮฉ} โ†’ IsIdeal _ r I โ†’ IsSubgroup (raddGroup r) I
  using (IsIdeal.eq)
idSub = ฮปR r I h. andFst h

idScale : (R : ๐•Œ)
  (r : IsCommRing R)
  (I : R โ†’ ฮฉ)
  โ†’ IsIdeal _ r I โ†’ (a x : R) โ†’ I x โ†’ I (rmul _ r a x)
  using (IsIdeal.eq, closedScale.unfold)
idScale = ฮปR r I h a x hx. squash-elim (andSnd h) (u. u a x hx)

-- an ideal is a normal subgroup of (R , +), because (R , +) is abelian
idNormal : (R : ๐•Œ) (r : IsCommRing R) (I : R โ†’ ฮฉ) โ†’ IsNormal (raddGroup r) I
idNormal = ฮปR r I. abelianNormal (rAddComm _ r)

-- ===== the two closure facts the descent will want =====
--
-- The ideal is a LEFT ideal โ€” closed under aยทx โ€” and multiplication is
-- commutative, so the same closure serves both sides of the descent.
-- In a non-commutative ring these would be two independent hypotheses
-- (a two-sided ideal), and the outer half of the descent below would
-- use the RIGHT one. The asymmetry Algebra/quotGroup.nova had to face
-- for the group operation is here paid for by commutativity โ€” which is
-- exactly what "commutative ring" buys and what a group does not have.
idScaleR : (R : ๐•Œ)
  (r : IsCommRing R)
  (I : R โ†’ ฮฉ)
  โ†’ IsIdeal _ r I โ†’ (a x : R) โ†’ I x โ†’ I (rmul _ r x a)
idScaleR = ฮปR r I h a x hx. transportP I (rMulComm _ r a x) (idScale _ _ _ h a x hx)