-- Quotient rings of a bundled ring: the congruence modulo an ideal, the
-- quotient ring R ⧸ I (the value quotientRing(R, I)) on its classes, the ring laws of the
-- quotient, and the classes of sums, products, and negations; everything
-- here is ZF
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.Algebra.Ring.Quotient
import QuotientCore
import PrimeIdeal

-- x and y are related modulo I when x - y lies in I.
def quotientRelation (R I : Set) : Set :=
  idealRelation(R.carrier, R.add, R.neg, I)

-- The quotient ring of R by I: the classes modulo I with the induced
-- operations and the classes of zero and one.
def quotientRing (R I : Set) : Set :=
  Ring.mk((R.carrier ⧸ quotientRelation(R, I)),
    quotientBinary(R.carrier, quotientRelation(R, I), R.add),
    ⟦R.zero⟧[R.carrier, quotientRelation(R, I)],
    quotientUnary(R.carrier, quotientRelation(R, I), R.neg),
    quotientBinary(R.carrier, quotientRelation(R, I), R.mul),
    ⟦R.one⟧[R.carrier, quotientRelation(R, I)])

-- The quotient is written R ⧸ I wherever R is the ring of a hypothesis in
-- scope; the set quotient A ⧸ r keeps its meaning on every other left
-- operand.
notation infixl 70 "⧸" => quotientRing(R, _) via hypothesis Ring(R) for R
notation infixl 70 "⧸" => quotientRing(R, _) via hypothesis CommRing(R) for R
notation infixl 70 "⧸" => quotientRing(R, _) via hypothesis Ideal(R, I) for R

theorem quotientRelation.value (R I : Set)
  shows quotientRelation(R, I) = idealRelation(R.carrier, R.add, R.neg, I)
proof
  simp [quotientRelation]

theorem quotientRing.carrierOf (R I : Set)
  shows Ring.carrier(quotientRing(R, I)) =
    (R.carrier ⧸ quotientRelation(R, I))
proof
  simp [quotientRing, Ring.mk.carrier]

theorem quotientRing.addOf (R I : Set)
  shows Ring.add(quotientRing(R, I)) =
    quotientBinary(R.carrier, quotientRelation(R, I), R.add)
proof
  simp [quotientRing, Ring.mk.add]

theorem quotientRing.zeroOf (R I : Set)
  shows Ring.zero(quotientRing(R, I)) =
    ⟦R.zero⟧[R.carrier, quotientRelation(R, I)]
proof
  simp [quotientRing, Ring.mk.zero]

theorem quotientRing.negOf (R I : Set)
  shows Ring.neg(quotientRing(R, I)) =
    quotientUnary(R.carrier, quotientRelation(R, I), R.neg)
proof
  simp [quotientRing, Ring.mk.neg]

theorem quotientRing.mulOf (R I : Set)
  shows Ring.mul(quotientRing(R, I)) =
    quotientBinary(R.carrier, quotientRelation(R, I), R.mul)
proof
  simp [quotientRing, Ring.mk.mul]

theorem quotientRing.oneOf (R I : Set)
  shows Ring.one(quotientRing(R, I)) =
    ⟦R.one⟧[R.carrier, quotientRelation(R, I)]
proof
  simp [quotientRing, Ring.mk.one]

section QuotientRings
variable (R I : Set)
hypothesis comm : CommRing(R)
hypothesis ideal : Ideal(R, I)

theorem quotientRelation.relates (x y : R)
  shows relates(quotientRelation(R, I), x, y) ↔ x - y ∈ I
proof
  have xIn : x ∈ R by assumption
  have yIn : y ∈ R by assumption
  have criterion := idealRelation.relates at R.carrier, R.add, R.neg, I, x, y
    with xIn, yIn
  rw [quotientRelation.value, Ring.sub.value]
  constructor
  . intro related
    have same := criterion.forward with related
    unfold Congruent at same
    exact same
  . intro member
    have same : Congruent(R.add, R.neg, I, x, y)
      unfold Congruent
      exact member
    exact criterion.backward with same

theorem quotientRelation.equivalence
  shows Equivalence(R.carrier, quotientRelation(R, I))
proof
  have parts := CommRing.parts with comm
  have idealParts := Ideal.parts with ideal
  rw quotientRelation.value
  exact idealRelation.equivalence with parts, idealParts

-- The quotient is a commutative ring.
theorem quotientRing.comm_ring
  shows CommRing(R ⧸ I)
proof
  have parts := CommRing.parts with comm
  have idealParts := Ideal.parts with ideal
  have engine := idealQuotient.comm_ring with parts, idealParts
  unfold quotientRing
  apply CommRing.of_parts
  rw quotientRelation.value
  exact engine

instance quotientRing.class_mem (x : R)
  shows ⟦x⟧[R.carrier, quotientRelation(R, I)] ∈
    Ring.carrier(R ⧸ I)
proof
  have equivalence := quotientRelation.equivalence with comm, ideal
  rw quotientRing.carrierOf
  exact quotient.contains_class with equivalence, *

theorem quotientRing.representative (X : Set)
  requires hX : X ∈ Ring.carrier(R ⧸ I)
  shows ∃ x ∈ R, X = ⟦x⟧[R.carrier, quotientRelation(R, I)]
proof
  rw quotientRing.carrierOf at hX
  exact quotient.representative with hX

-- Two classes are equal exactly when the difference of representatives
-- lies in the ideal; a class is zero exactly when its representative does.
theorem quotientRing.class_eq_iff (x y : R)
  shows ⟦x⟧[R.carrier, quotientRelation(R, I)] =
    ⟦y⟧[R.carrier, quotientRelation(R, I)] ↔ x - y ∈ I
proof
  have parts := CommRing.parts with comm
  have idealParts := Ideal.parts with ideal
  have xIn : x ∈ R by assumption
  have yIn : y ∈ R by assumption
  have criterion := idealClass.eq_iff_congruent with parts, idealParts, xIn, yIn
  rw [quotientRelation.value, Ring.sub.value]
  constructor
  . intro equal
    have same := criterion.forward with equal
    unfold Congruent at same
    exact same
  . intro member
    have same : Congruent(R.add, R.neg, I, x, y)
      unfold Congruent
      exact member
    exact criterion.backward with same

theorem quotientRing.class_eq_zero_iff (x : R)
  shows ⟦x⟧[R.carrier, quotientRelation(R, I)] =
    ⟦R[0]⟧[R.carrier, quotientRelation(R, I)] ↔ x ∈ I
proof
  have parts := CommRing.parts with comm
  have idealParts := Ideal.parts with ideal
  have xIn : x ∈ R by assumption
  rw quotientRelation.value
  exact idealClass.eq_zero with parts, idealParts, xIn

-- The operations on classes are the classes of the operations.
theorem quotientRing.add_class (x y : R)
  shows Ring.add(R ⧸ I)(⟦x⟧[R.carrier, quotientRelation(R, I)],
      ⟦y⟧[R.carrier, quotientRelation(R, I)]) =
    ⟦x + y⟧[R.carrier, quotientRelation(R, I)]
proof
  have parts := CommRing.parts with comm
  have idealParts := Ideal.parts with ideal
  have equivalence := quotientRelation.equivalence with comm, ideal
  have compatible := idealRelation.add_compatible with parts, idealParts
  have magma : IsMagma(R.carrier, R.add) := IsGroup.magma with
    (IsAbelianGroup.group with (IsRing.additive with (IsCommRing.ring with parts)))
  rw [quotientRing.addOf, quotientRelation.value]
  rw quotientRelation.value at equivalence
  exact quotientBinary.classes with equivalence, magma, compatible, *

theorem quotientRing.mul_class (x y : R)
  shows Ring.mul(R ⧸ I)(⟦x⟧[R.carrier, quotientRelation(R, I)],
      ⟦y⟧[R.carrier, quotientRelation(R, I)]) =
    ⟦x * y⟧[R.carrier, quotientRelation(R, I)]
proof
  have parts := CommRing.parts with comm
  have idealParts := Ideal.parts with ideal
  have equivalence := quotientRelation.equivalence with comm, ideal
  have compatible := idealRelation.mul_compatible with parts, idealParts
  have monoid := IsRing.multiplicative with (IsCommRing.ring with parts)
  have magma : IsMagma(R.carrier, R.mul) := IsSemigroup.magma with
    (IsMonoid.semigroup with monoid)
  rw [quotientRing.mulOf, quotientRelation.value]
  rw quotientRelation.value at equivalence
  exact quotientBinary.classes with equivalence, magma, compatible, *

theorem quotientRing.neg_class (x : R)
  shows Ring.neg(R ⧸ I)(⟦x⟧[R.carrier, quotientRelation(R, I)])
    = ⟦-x⟧[R.carrier, quotientRelation(R, I)]
proof
  have parts := CommRing.parts with comm
  have idealParts := Ideal.parts with ideal
  have equivalence := quotientRelation.equivalence with comm, ideal
  have compatible := idealRelation.neg_compatible with parts, idealParts
  obtain ⟨negF, inverses⟩ := IsGroup.inverse with
    (IsAbelianGroup.group with (IsRing.additive with (IsCommRing.ring with parts)))
  rw [quotientRing.negOf, quotientRelation.value]
  rw quotientRelation.value at equivalence
  exact quotientUnary.classes with equivalence, negF, compatible, *

end QuotientRings