-- Ideal congruences and quotient rings over separate pieces, constructed
-- in ZF: the engine under Quotient
-- 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.QuotientCore
import PrimeIdealCore
import Relation.QuotientOperations

predicate Congruent (add neg I x y : Set) := call2(add, x, neg(y)) ∈ I

theorem Congruent.refl (A add zero neg mul one I x : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  requires hx : x ∈ A
  shows Congruent(add, neg, I, x, x)
proof
  have zeroIn : zero ∈ I by simp [IsIdeal]
  have cancel : call2(add, x, neg(x)) = zero by ring
  unfold Congruent
  rwa cancel

theorem Congruent.symm (A add zero neg mul one I x y : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires same : Congruent(add, neg, I, x, y)
  shows Congruent(add, neg, I, y, x)
proof
  have negative := IsIdeal.neg_closed at A, add, zero, neg, mul, I, call2(add, x, neg(y)) with *
  unfold Congruent
  ring_nf at negative
  ring_nf
  exact negative

theorem Congruent.trans (A add zero neg mul one I x y z : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hz : z ∈ A
  requires xy : Congruent(add, neg, I, x, y)
  requires yz : Congruent(add, neg, I, y, z)
  shows Congruent(add, neg, I, x, z)
proof
  have sum := IsIdeal.add_closed at A, add, zero, neg, mul, I, call2(add, x, neg(y)), call2(add, y, neg(z)) with *
  unfold Congruent
  ring_nf at sum
  ring_nf
  exact sum

theorem Congruent.add (A add zero neg mul one I x y u v : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hu : u ∈ A
  requires hv : v ∈ A
  requires xy : Congruent(add, neg, I, x, y)
  requires uv : Congruent(add, neg, I, u, v)
  shows Congruent(add, neg, I, call2(add, x, u), call2(add, y, v))
proof
  have sum := IsIdeal.add_closed at A, add, zero, neg, mul, I, call2(add, x, neg(y)), call2(add, u, neg(v)) with *
  unfold Congruent
  ring_nf at sum
  ring_nf
  exact sum

theorem Congruent.neg (A add zero neg mul one I x y : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires xy : Congruent(add, neg, I, x, y)
  shows Congruent(add, neg, I, neg(x), neg(y))
proof
  have negative := IsIdeal.neg_closed at A, add, zero, neg, mul, I, call2(add, x, neg(y)) with *
  unfold Congruent
  ring_nf at negative
  ring_nf
  exact negative

theorem Congruent.mul (A add zero neg mul one I x y u v : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hu : u ∈ A
  requires hv : v ∈ A
  requires xy : Congruent(add, neg, I, x, y)
  requires uv : Congruent(add, neg, I, u, v)
  shows Congruent(add, neg, I, call2(mul, x, u), call2(mul, y, v))
proof
  have first := IsIdeal.mul_left_closed at A, add, zero, neg, mul, I, u, call2(add, x, neg(y)) with *
  have second := IsIdeal.mul_left_closed at A, add, zero, neg, mul, I, y, call2(add, u, neg(v)) with *
  have sum := IsIdeal.add_closed at A, add, zero, neg, mul, I, call2(mul, u, call2(add, x, neg(y))), call2(mul, y, call2(add, u, neg(v))) with *
  unfold Congruent
  ring_nf at sum
  ring_nf
  exact sum

def idealRelation (A add neg I : Set) : Set :=
  {p ∈ A × A | ∃ x ∈ A, ∃ y ∈ A, p = (x, y) ∧ Congruent(add, neg, I, x, y)}

notation scoped idealRelation(R, I) => idealRelation(R.carrier, R.add, R.neg, I)

theorem idealRelation.relates (A add neg I x y : Set)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows relates(idealRelation(A, add, neg, I), x, y) ↔ Congruent(add, neg, I, x, y)
proof
  constructor
  . intro related
    obtain ⟨bounded, u, hu, v, hv, shape, same⟩ := idealRelation.membership.forward at
      A, add, neg, I, (x, y) with related
    have coordinates := orderedPair.injective with shape
    rwa [coordinates.left, coordinates.right]
  . intro same
    unfold relates
    apply idealRelation.membership.backward
    have bounded := product.pair at x, y, A, A with *
    refine ⟨bounded, x, hx, y, hy, rfl, same⟩

theorem idealRelation.equivalence (A add zero neg mul one I : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  shows Equivalence(A, idealRelation(A, add, neg, I))
proof
  unfold Equivalence
  refine ⟨?_, ⟨?_, ⟨?_, ?_⟩⟩⟩
  . settle with RelationOn, RelationBetween, Subset, idealRelation.membership
    intros x hx
    apply idealRelation.relates.backward with hx, hx
    exact Congruent.refl with *
    intros x hx y hy related
    have same := idealRelation.relates.forward with hx, hy, related
    have reverse := Congruent.symm with *
    exact idealRelation.relates.backward with hy, hx, reverse
    intros x hx y hy z hz xy yz
    have first := idealRelation.relates.forward with hx, hy, xy
    have second := idealRelation.relates.forward with hy, hz, yz
    have composed := Congruent.trans at A, add, zero, neg, mul, one, I, x, y, z with *
    exact idealRelation.relates.backward with hx, hz, composed

theorem idealRelation.add_compatible (A add zero neg mul one I : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  shows CompatibleBinary(A, idealRelation(A, add, neg, I), add)
proof
  intros x hx y hy u hu v hv xy uv
  have first := idealRelation.relates.forward with hx, hy, xy
  have second := idealRelation.relates.forward with hu, hv, uv
  have congruence := Congruent.add at A, add, zero, neg, mul, one, I, x, y, u, v with *
  have ordinary := IsCommRing.ring with ring
  have leftClosed := IsRing.add_closed at A, add, zero, neg, mul, one, x,
    u with *
  have rightClosed := IsRing.add_closed at A, add, zero, neg, mul, one, y, v with *
  exact idealRelation.relates.backward with leftClosed, rightClosed, congruence

theorem idealRelation.neg_compatible (A add zero neg mul one I : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  shows CompatibleUnary(A, idealRelation(A, add, neg, I), neg)
proof
  intros x hx y hy xy
  have first := idealRelation.relates.forward with hx, hy, xy
  have congruence := Congruent.neg with *
  have ordinary := IsCommRing.ring with ring
  have leftClosed := IsRing.neg_closed with hx
  have rightClosed := IsRing.neg_closed with hy
  exact idealRelation.relates.backward with leftClosed, rightClosed, congruence

theorem idealRelation.mul_compatible (A add zero neg mul one I : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  shows CompatibleBinary(A, idealRelation(A, add, neg, I), mul)
proof
  intros x hx y hy u hu v hv xy uv
  have first := idealRelation.relates.forward with hx, hy, xy
  have second := idealRelation.relates.forward with hu, hv, uv
  have congruence := Congruent.mul at A, add, zero, neg, mul, one, I, x, y, u, v with *
  have ordinary := IsCommRing.ring with ring
  have leftClosed := IsRing.mul_closed at A, add, zero, neg, mul, one, x,
    u with *
  have rightClosed := IsRing.mul_closed at A, add, zero, neg, mul, one, y, v with *
  exact idealRelation.relates.backward with leftClosed, rightClosed, congruence

-- A ring on the quotient set, with graph-valued operations.
theorem idealQuotient.comm_ring (A add zero neg mul one I : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  shows IsCommRing((A ⧸ idealRelation(A, add, neg, I)),
    quotientBinary(A, idealRelation(A, add, neg, I), add),
    ⟦zero⟧[A, idealRelation(A, add, neg, I)],
    quotientUnary(A, idealRelation(A, add, neg, I), neg),
    quotientBinary(A, idealRelation(A, add, neg, I), mul),
    ⟦one⟧[A, idealRelation(A, add, neg, I)])
proof
  have equivalence := idealRelation.equivalence with *
  have addCompatible := idealRelation.add_compatible with *
  have mulCompatible := idealRelation.mul_compatible with *
  have negCompatible := idealRelation.neg_compatible with *
  exact quotient.comm_ring with *

theorem idealClass.eq_iff_congruent (A add zero neg mul one I x y : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows ⟦x⟧[A, idealRelation(A, add, neg, I)] = ⟦y⟧[A, idealRelation(A, add, neg, I)] ↔
    Congruent(add, neg, I, x, y)
proof
  have equivalence := idealRelation.equivalence with *
  constructor
  . intro equal
    have related := equivalenceClass.related_of_eq with *
    exact idealRelation.relates.forward with hx, hy, related
  . intro same
    have related := idealRelation.relates.backward with hx, hy, same
    exact equivalenceClass.eq with *

theorem idealClass.eq_zero (A add zero neg mul one I x : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  requires hx : x ∈ A
  shows ⟦x⟧[A, idealRelation(A, add, neg, I)] = ⟦zero⟧[A, idealRelation(A, add, neg, I)] ↔ x ∈ I
proof
  have ordinary := IsCommRing.ring with ring
  have zeroInA := IsRing.zero_in_carrier with ordinary
  have equivalence := idealRelation.equivalence with *
  have subtractZero : call2(add, x, neg(zero)) = x by ring
  constructor
  . intro equal
    have related := equivalenceClass.related_of_eq with *
    have same := idealRelation.relates.forward with hx, zeroInA, related
    unfold Congruent at same
    rwa subtractZero at same
  . intro member
    have same : Congruent(add, neg, I, x, zero)
      unfold Congruent
      rwa subtractZero
    have related := idealRelation.relates.backward with hx, zeroInA, same
    exact equivalenceClass.eq with *

theorem idealQuotient.nontrivial_iff (A add zero neg mul one I : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  shows Nontrivial((A ⧸ idealRelation(A, add, neg, I)), ⟦zero⟧[A, idealRelation(A, add, neg, I)], ⟦one⟧[A, idealRelation(A, add, neg, I)]) ↔
    IsProperIdeal(A, add, zero, neg, mul, one, I)
proof
  have ordinary := IsCommRing.ring with ring
  have zeroInA := IsRing.zero_in_carrier with ordinary
  have monoid := IsRing.multiplicative with ordinary
  have oneInA := IsMonoid.unit_in_carrier with monoid
  have equivalence := idealRelation.equivalence with *
  have zeroIn := quotient.contains_class at A, idealRelation(A, add, neg, I), zero with *
  have oneIn := quotient.contains_class at A, idealRelation(A, add, neg, I), one with *
  have criterion := idealClass.eq_zero at A, add, zero, neg, mul, one, I, one with *
  constructor
  . intro nontrivial
    unfold IsProperIdeal
    refine ⟨ideal, ?_⟩
    intro member
    have equal := criterion.backward with member
    apply nontrivial.right.right
    symm
    exact equal
  . intro proper
    unfold Nontrivial
    refine ⟨zeroIn, oneIn, ?_⟩
    intro equal
    have reversed : ⟦one⟧[A, idealRelation(A, add, neg, I)] = ⟦zero⟧[A, idealRelation(A, add, neg, I)]
      symm
      exact equal
    have member := criterion.forward with reversed
    exact proper.right with member

theorem idealQuotient.domain_of_prime (A add zero neg mul one I : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires prime : IsPrimeIdeal(A, add, zero, neg, mul, one, I)
  shows IsIntegralDomain((A ⧸ idealRelation(A, add, neg, I)),
    quotientBinary(A, idealRelation(A, add, neg, I), add), ⟦zero⟧[A, idealRelation(A, add, neg, I)],
    quotientUnary(A, idealRelation(A, add, neg, I), neg), quotientBinary(A, idealRelation(A, add, neg, I), mul), ⟦one⟧[A, idealRelation(A, add, neg, I)])
proof
  have proper := IsPrimeIdeal.proper with prime
  have ideal : IsIdeal(A, add, zero, neg, mul, I) by simp [IsProperIdeal]
  have ordinary := IsCommRing.ring with ring
  have equivalence := idealRelation.equivalence with *
  have compatible := idealRelation.mul_compatible with *
  have closed : IsMagma(A, mul) by simp [IsRing, IsMonoid, IsSemigroup]
  have quotientRing := idealQuotient.comm_ring with *
  have nontrivial := idealQuotient.nontrivial_iff.backward with ring, ideal, proper
  unfold IsIntegralDomain
  refine ⟨quotientRing, nontrivial, ?_⟩
  intros X hX Y hY productZero
  obtain ⟨x, hx, xShape⟩ := quotient.representative with hX
  obtain ⟨y, hy, yShape⟩ := quotient.representative with hY
  have multiply := quotientBinary.classes with equivalence, closed, compatible, hx, hy
  have productInA := IsRing.mul_closed with hx, hy
  have zeroProduct : ⟦call2(mul, x, y)⟧[A, idealRelation(A, add, neg, I)] = ⟦zero⟧[A, idealRelation(A, add, neg, I)]
    cc
  have productIn := idealClass.eq_zero.forward with ring, ideal, productInA, zeroProduct
  have factors := prime.right with x, hx, y, hy, productIn
  cases factors with xIn | yIn
  . left
    have equal := idealClass.eq_zero.backward with ring, ideal, hx, xIn
    cc
  . right
    have equal := idealClass.eq_zero.backward with ring, ideal, hy, yIn
    cc

theorem idealQuotient.domain_iff_prime (A add zero neg mul one I : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  shows IsIntegralDomain((A ⧸ idealRelation(A, add, neg, I)),
    quotientBinary(A, idealRelation(A, add, neg, I), add), ⟦zero⟧[A, idealRelation(A, add, neg, I)],
    quotientUnary(A, idealRelation(A, add, neg, I), neg), quotientBinary(A, idealRelation(A, add, neg, I), mul), ⟦one⟧[A, idealRelation(A, add, neg, I)]) ↔ IsPrimeIdeal(A, add, zero, neg, mul, one, I)
proof
  constructor
  . intro domain
    have proper := idealQuotient.nontrivial_iff.forward with ring, ideal, domain.right.left
    have factors := domain.right.right
    have ordinary := IsCommRing.ring with ring
    have equivalence := idealRelation.equivalence with *
    have compatible := idealRelation.mul_compatible with *
    have closed : IsMagma(A, mul) by simp [IsRing, IsMonoid, IsSemigroup]
    unfold IsPrimeIdeal
    refine ⟨proper, ?_⟩
    intros x hx y hy productIn
    have xIn := quotient.contains_class with hx
    have yIn := quotient.contains_class with hy
    have productInA := IsRing.mul_closed with hx, hy
    have zeroProduct := idealClass.eq_zero.backward with ring, ideal, productInA, productIn
    have multiply := quotientBinary.classes with hx, hy
    have equation : (quotientBinary(A, idealRelation(A, add, neg, I), mul))(⟦x⟧[A, idealRelation(A, add, neg, I)], ⟦y⟧[A, idealRelation(A, add, neg, I)]) = ⟦zero⟧[A, idealRelation(A, add, neg, I)]
      cc
    have alternatives := factors with ⟦x⟧[A, idealRelation(A, add, neg, I)], xIn, ⟦y⟧[A, idealRelation(A, add, neg, I)], yIn, equation
    cases alternatives with xZero | yZero
    . left
      exact idealClass.eq_zero.forward with ring, ideal, hx, xZero
    . right
      exact idealClass.eq_zero.forward with ring, ideal, hy, yZero
  . intro prime
    exact idealQuotient.domain_of_prime with *

theorem idealQuotient.projection_kernel (A add zero neg mul one I x : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  requires hx : x ∈ A
  shows quotientProjection(A, idealRelation(A, add, neg, I))[x] =
    ⟦zero⟧[A, idealRelation(A, add, neg, I)] ↔ x ∈ I
proof
  have equivalence := idealRelation.equivalence with *
  have value := quotientProjection.value at A, idealRelation(A, add, neg, I), x with *
  rw value
  exact idealClass.eq_zero with *