-- Adjoining an element to an ideal in a commutative ring (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.IdealAdjoin
import IdealCore

-- I + (x): finite algebra, with no choice of generators or representatives.
def idealAdjoin (A add mul I x : Set) : Set :=
  {z ∈ A | ∃ i ∈ I, ∃ a ∈ A, z = call2(add, i, call2(mul, a, x))}

theorem idealAdjoin.contains (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 I ⊆ idealAdjoin(A, add, mul, I, x)
proof
  have ordinary := IsCommRing.ring with ring
  have zeroInA := IsRing.zero_in_carrier with ordinary
  have bounded := IsIdeal.subset_carrier with ideal
  intros i hi
  have iInA := bounded with i, hi
  have equation : i = call2(add, i, call2(mul, zero, x)) by ring
  exact idealAdjoin.membership.backward with ⟨iInA, i, hi, zero, zeroInA, equation⟩

theorem idealAdjoin.generator (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 ∈ idealAdjoin(A, add, mul, I, x)
proof
  have ordinary := IsCommRing.ring with ring
  have monoid := IsRing.multiplicative with ordinary
  have oneInA := IsMonoid.unit_in_carrier with monoid
  have zeroIn := IsIdeal.zero_closed with ideal
  have equation : x = call2(add, zero, call2(mul, one, x)) by ring
  exact idealAdjoin.membership.backward with ⟨hx, zero, zeroIn, one, oneInA, equation⟩

theorem idealAdjoin.ideal (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 IsIdeal(A, add, zero, neg, mul, idealAdjoin(A, add, mul, I, x))
proof
  have ordinary := IsCommRing.ring with ring
  have boundedI := IsIdeal.subset_carrier with ideal
  have contains := idealAdjoin.contains with *
  have zeroInI := IsIdeal.zero_closed with ideal
  have zeroIn := contains with zero, zeroInI
  unfold IsIdeal
  refine ⟨?_, ⟨zeroIn, ⟨?_, ⟨?_, ?_⟩⟩⟩⟩
    intros z hz
    have data := idealAdjoin.membership.forward with hz
    exact data.left
  . intros z hz w hw
    obtain ⟨zInA, i, hi, a, ha, zValue⟩ := idealAdjoin.membership.forward with hz
    obtain ⟨wInA, j, hj, b, hb, wValue⟩ := idealAdjoin.membership.forward with hw
    have iInA := boundedI with i, hi
    have jInA := boundedI with j, hj
    have sumInA := IsRing.add_closed at A, add, zero, neg, mul, one, z, w with *
    have sumInI := IsIdeal.add_closed with hi, hj
    have coefficientInA := IsRing.add_closed with ha, hb
    have equation : call2(add, z, w) = call2(add, call2(add, i, j), call2(mul, call2(add, a, b), x))
      rw [zValue, wValue]
      ring
    exact idealAdjoin.membership.backward with ⟨sumInA, call2(add, i, j), sumInI, call2(add, a, b), coefficientInA, equation⟩
  . intros z hz
    obtain ⟨zInA, n, hn, d, hd, value⟩ := idealAdjoin.membership.forward with hz
    have jInA := boundedI with n, hn
    have negInA := IsRing.neg_closed at A, add, zero, neg, mul, one, z with *
    have negInI := IsIdeal.neg_closed with hn
    have coefficientInA := IsRing.neg_closed with hd
    have equation : neg(z) = call2(add, neg(n), call2(mul, neg(d), x))
      rw value
      ring
    exact idealAdjoin.membership.backward with ⟨negInA, neg(n), negInI, neg(d), coefficientInA, equation⟩
  . intros t ht z hz
    obtain ⟨zInA, k, hk, c, hc, value⟩ := idealAdjoin.membership.forward with hz
    have kInA := boundedI with k, hk
    have leftInA := IsRing.mul_closed at A, add, zero, neg, mul, one, t,
      z with *
    have rightInA := IsRing.mul_closed at A, add, zero, neg, mul, one, z,
      t with *
    have productInI := IsIdeal.mul_left_closed with ht, hk
    have coefficientInA := IsRing.mul_closed with ht, hc
    have equation : call2(mul, t, z) = call2(add, call2(mul, t, k), call2(mul, call2(mul, t, c), x))
      rw value
      ring
    have reverse := IsCommRing.mul_comm at A, add, zero, neg, mul, one, z, t with *
    constructor
    . apply idealAdjoin.membership.backward at
      A, add, mul, I, x, call2(mul, t, z)
      refine ⟨leftInA, call2(mul, t, k), productInI, call2(mul, t, c), coefficientInA, equation⟩
    . rw reverse
      exact idealAdjoin.membership.backward with ⟨leftInA, call2(mul, t, k), productInI, call2(mul, t, c), coefficientInA, equation⟩

theorem idealAdjoin.least (A add zero neg mul I x J : Set)
  requires idealJ : IsIdeal(A, add, zero, neg, mul, J)
  requires contains : I ⊆ J
  requires generator : x ∈ J
  shows idealAdjoin(A, add, mul, I, x) ⊆ J
proof
  intros z hz
  obtain ⟨zInA, i, hi, a, ha, value⟩ := idealAdjoin.membership.forward with hz
  have iInJ := contains with i, hi
  have product := IsIdeal.mul_left_closed at A, add, zero, neg, mul, J, a, x with *
  have sum := IsIdeal.add_closed at A, add, zero, neg, mul, J, i, call2(mul, a, x) with *
  rwa value

theorem IsMaximalIdeal.bezout (A add zero neg mul one I x : Set)
  requires ring : IsCommRing(A, add, zero, neg, mul, one)
  requires maximal : IsMaximalIdeal(A, add, zero, neg, mul, one, I)
  requires hx : x ∈ A
  requires outside : ¬(x ∈ I)
  shows ∃ i ∈ I, ∃ a ∈ A, one = call2(add, i, call2(mul, a, x))
proof
  have ideal : IsIdeal(A, add, zero, neg, mul, I) by simp [IsMaximalIdeal, IsProperIdeal]
  have ordinary := IsCommRing.ring with ring
  have monoid := IsRing.multiplicative with ordinary
  have oneInA := IsMonoid.unit_in_carrier with monoid
  have adjoinIdeal := idealAdjoin.ideal at A, add, zero, neg, mul, one, I, x with *
  have contains := idealAdjoin.contains at A, add, zero, neg, mul, one, I, x with *
  have generator := idealAdjoin.generator at A, add, zero, neg, mul, one, I, x with *
  have alternatives := IsMaximalIdeal.eq_or_whole with *
  cases alternatives with same | whole
  . rw same at generator
    exfalso
    exact outside with generator
  . have oneIn : one ∈ idealAdjoin(A, add, mul, I, x)
      rwa whole
    have data := idealAdjoin.membership.forward with oneIn
    exact data.right