-- Two-sided ideals over separate pieces: the engine under Ideal, with the
-- proper and maximal ideals and the closure results, all in 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.IdealCore
import Core
import Set.Order

-- IsIdeal(A, add, zero, neg, mul, I) is the two-sided ideal over separate
-- pieces; the bundled Ideal(R, I) under a ring hypothesis is defined in
-- Ideal and bridged to this form. Ring laws appear as hypotheses of the
-- ring-specific results.
predicate IsIdeal (A add zero neg mul I : Set) :=
  I ⊆ A ∧ zero ∈ I ∧
  (∀ x ∈ I, ∀ y ∈ I, call2(add, x, y) ∈ I) ∧
  (∀ x ∈ I, neg(x) ∈ I) ∧
  (∀ a ∈ A, ∀ x ∈ I, call2(mul, a, x) ∈ I ∧ call2(mul, x, a) ∈ I)
predicate IsProperIdeal (A add zero neg mul one I : Set) :=
  IsIdeal(A, add, zero, neg, mul, I) ∧ ¬(one ∈ I)
predicate IsMaximalIdeal (A add zero neg mul one M : Set) :=
  IsProperIdeal(A, add, zero, neg, mul, one, M) ∧
  (∀ J, IsProperIdeal(A, add, zero, neg, mul, one, J) → M ⊆ J → J = M)

notation scoped IsIdeal(R, I) => IsIdeal(R.carrier, R.add, R.zero, R.neg, R.mul, I)

notation scoped IsProperIdeal(R, I) => IsProperIdeal(R.carrier, R.add, R.zero, R.neg, R.mul, R.one, I)

notation scoped IsMaximalIdeal(R, M) => IsMaximalIdeal(R.carrier, R.add, R.zero, R.neg, R.mul, R.one, M)


theorem IsMaximalIdeal.proper (A add zero neg mul one I : Set)
  requires h : IsMaximalIdeal(A, add, zero, neg, mul, one, I)
  shows IsProperIdeal(A, add, zero, neg, mul, one, I)
proof
  exact h.left

theorem IsMaximalIdeal.ideal (A add zero neg mul one I : Set)
  requires h : IsMaximalIdeal(A, add, zero, neg, mul, one, I)
  shows IsIdeal(A, add, zero, neg, mul, I)
proof
  have proper := IsMaximalIdeal.proper with h
  exact proper.left

theorem IsIdeal.subset_carrier (A add zero neg mul I : Set)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  shows I ⊆ A
proof
  simp [IsIdeal]

theorem IsIdeal.zero_closed (A add zero neg mul I : Set)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  shows zero ∈ I
proof
  simp [IsIdeal]

theorem IsIdeal.add_closed (A add zero neg mul I x y : Set)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  requires hx : x ∈ I
  requires hy : y ∈ I
  shows call2(add, x, y) ∈ I
proof
  exact ideal.right.right.left with x, hx, y, hy

theorem IsIdeal.neg_closed (A add zero neg mul I x : Set)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  requires hx : x ∈ I
  shows neg(x) ∈ I
proof
  exact ideal.right.right.right.left with x, hx

theorem IsIdeal.mul_left_closed (A add zero neg mul I a x : Set)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  requires ha : a ∈ A
  requires hx : x ∈ I
  shows call2(mul, a, x) ∈ I
proof
  have products := ideal.right.right.right.right with a, ha, x, hx
  exact products.left

theorem IsIdeal.mul_right_closed (A add zero neg mul I a x : Set)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  requires ha : a ∈ A
  requires hx : x ∈ I
  shows call2(mul, x, a) ∈ I
proof
  have products := ideal.right.right.right.right with a, ha, x, hx
  exact products.right

theorem IsIdeal.union_chain (A add zero neg mul S : Set)
  requires inhabited : Nonempty(S)
  requires ideals : ∀ I ∈ S, IsIdeal(A, add, zero, neg, mul, I)
  requires nested : ∀ I ∈ S, ∀ J ∈ S, I ⊆ J ∨ J ⊆ I
  shows IsIdeal(A, add, zero, neg, mul, ⋃(S))
proof
  obtain ⟨I0, hI0⟩ := inhabited
  obtain ⟨subset0, zero0, add0, neg0, mul0⟩ := ideals with I0, hI0
  have bounded : ⋃(S) ⊆ A
    apply union.subset
    intros B hB
    obtain ⟨subsetI, restI⟩ := ideals with B, hB
    exact subsetI
  have zeroIn : zero ∈ ⋃(S) := set.union.backward with ⟨I0, hI0, zero0⟩
  constructor
  . exact bounded
  . constructor
    . exact zeroIn
    . constructor
      . intros x hx y hy
        obtain ⟨I, hI, xI⟩ := set.union.forward with hx
        obtain ⟨J, hJ, yJ⟩ := set.union.forward with hy
        have alternatives := nested with I, hI, J, hJ
        cases alternatives with ij | ji
          have xJ := ij with x, xI
          obtain ⟨boundedJ, zeroJ, addJ, negJ, mulJ⟩ := ideals with J, hJ
          have sum := addJ with x, xJ, y, yJ
          exact set.union.backward with ⟨J, hJ, sum⟩
          have yI := ji with y, yJ
          obtain ⟨boundedI, zeroI, addI, negI, mulI⟩ := ideals with I, hI
          have sum := addI with x, xI, y, yI
          exact set.union.backward with ⟨I, hI, sum⟩
      . constructor
        . intros x hx
          obtain ⟨N, hI, xI⟩ := set.union.forward with hx
          obtain ⟨boundedI, zeroI, addI, negI, mulI⟩ := ideals with N, hI
          have negative := negI with x, xI
          exact set.union.backward with ⟨N, hI, negative⟩
        . intros a ha x hx
          obtain ⟨P, hI, xI⟩ := set.union.forward with hx
          obtain ⟨boundedI, zeroI, addI, negI, mulI⟩ := ideals with P, hI
          obtain ⟨leftProduct, rightProduct⟩ := mulI with a, ha, x, xI
          constructor
          . apply set.union.backward at S, call2(mul, a, x)
            refine ⟨P, hI, leftProduct⟩
          . apply set.union.backward at S, call2(mul, x, a)
            refine ⟨P, hI, rightProduct⟩

theorem IsProperIdeal.union_chain (A add zero neg mul one S : Set)
  requires inhabited : Nonempty(S)
  requires ideals : ∀ I ∈ S, IsProperIdeal(A, add, zero, neg, mul, one, I)
  requires nested : ∀ I ∈ S, ∀ J ∈ S, I ⊆ J ∨ J ⊆ I
  shows IsProperIdeal(A, add, zero, neg, mul, one, ⋃(S))
proof
  have underlying : ∀ I ∈ S, IsIdeal(A, add, zero, neg, mul, I)
    intros B hB
    obtain ⟨idealI, absent⟩ := ideals with B, hB
    exact idealI
  have unionIdeal := IsIdeal.union_chain with inhabited, underlying, nested
  constructor
  . exact unionIdeal
  . intro oneIn
    obtain ⟨I, hI, oneI⟩ := set.union.forward with oneIn
    obtain ⟨idealI, absent⟩ := ideals with I, hI
    exact absent with oneI

theorem IsIdeal.whole_of_one (A add zero neg mul one I : Set)
  requires ring : IsRing(A, add, zero, neg, mul, one)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  requires contains : one ∈ I
  shows I = A
proof
  rcases ideal with ⟨bounded, zeroIn, addClosed, negClosed, absorbs⟩
  have monoid := IsRing.multiplicative with ring
  apply Subset.antisymmetric with bounded
  intros x hx
  obtain ⟨product, unused⟩ := absorbs with x, hx, one, contains
  have identity := IsMonoid.right_identity with monoid, hx
  rwa identity at product

theorem IsIdeal.zero_ideal (A add zero neg mul one : Set)
  requires ring : IsRing(A, add, zero, neg, mul, one)
  shows IsIdeal(A, add, zero, neg, mul, {zero})
proof
  have zeroIn := IsRing.zero_in_carrier with ring
  have additive := IsRing.additive with ring
  have group := IsAbelianGroup.group with additive
  have negZero := IsGroup.inverse_unit with group
  have addZero := IsRing.add_left_identity with ring, zeroIn
  constructor
    intros x hx
    have equal := singleton.membership.forward with hx
    rwa equal
  . constructor
    . exact singleton.self at zero
    . constructor
      . intros x hx y hy
        have ex := singleton.membership.forward with hx
        have ey := singleton.membership.forward with hy
        rw [ex, ey, addZero]
        exact singleton.self
      . constructor
        . intros x hx
          have ex := singleton.membership.forward with hx
          rw [ex, negZero]
          exact singleton.self
        . intros a ha x hx
          have ex := singleton.membership.forward with hx
          rw ex
          have leftZero := IsRing.mul_zero with ring, ha
          have rightZero := IsRing.zero_mul with ring, ha
          constructor
          . rw leftZero
            exact singleton.self
          . rw rightZero
            exact singleton.self

theorem IsProperIdeal.zero_ideal (A add zero neg mul one : Set)
  requires ring : IsRing(A, add, zero, neg, mul, one)
  requires nontrivial : Nontrivial(A, zero, one)
  shows IsProperIdeal(A, add, zero, neg, mul, one, {zero})
proof
  have ideal := IsIdeal.zero_ideal with ring
  rcases nontrivial with ⟨zeroIn, oneIn, distinct⟩
  constructor
  . exact ideal
  . intro member
    have equal := singleton.membership.forward with member
    apply distinct
    symm
    exact equal

theorem IsProperIdeal.iff_ne_whole (A add zero neg mul one I : Set)
  requires ring : IsRing(A, add, zero, neg, mul, one)
  requires ideal : IsIdeal(A, add, zero, neg, mul, I)
  shows IsProperIdeal(A, add, zero, neg, mul, one, I) ↔ I ≠ A
proof
  constructor
  . intros proper equal
    rcases proper with ⟨underlying, absent⟩
    have monoid := IsRing.multiplicative with ring
    have oneIn := IsMonoid.unit_in_carrier with monoid
    rw ← equal at oneIn
    exact absent with oneIn
  . intro distinct
    constructor
    . exact ideal
    . intro oneIn
      have equal := IsIdeal.whole_of_one with ring, ideal, oneIn
      exact distinct with equal

theorem IsMaximalIdeal.eq_or_whole (A add zero neg mul one M J : Set)
  requires ring : IsRing(A, add, zero, neg, mul, one)
  requires maximal : IsMaximalIdeal(A, add, zero, neg, mul, one, M)
  requires ideal : IsIdeal(A, add, zero, neg, mul, J)
  requires contains : M ⊆ J
  shows J = M ∨ J = A
proof
  have alternatives : one ∈ J ∨ ¬(one ∈ J) by tauto
  cases alternatives with oneIn | absent
  . right
    exact IsIdeal.whole_of_one with ring, ideal, oneIn
  . left
    rcases maximal with ⟨properM, largest⟩
    have properJ : IsProperIdeal(A, add, zero, neg, mul, one, J)
      unfold IsProperIdeal
      refine ⟨ideal, absent⟩
    exact largest with J, properJ, contains