-- Prime ideals of a bundled ring: PrimeIdeal(R, I) under a ring hypothesis,
-- the bridges to the form over separate pieces, the factor laws, and the
-- primality of maximal ideals in a commutative ring; 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.PrimeIdeal
import Ideal
import PrimeIdealCore

-- Under a hypothesis Ring(R), a prime ideal is a proper ideal that contains
-- a factor of every product it contains. IsPrimeIdeal(A, add, zero, neg, mul,
-- one, I) remains the form over separate pieces, bridged below.
section Definitions
variable (R : Set)
hypothesis ring : Ring(R)

predicate PrimeIdeal (I : Set) :=
  ProperIdeal(R, I) ∧ (∀ x y ∈ R, x * y ∈ I → x ∈ I ∨ y ∈ I)

end Definitions

notation infixl 60 "+" => call2(R.add, _, _) via hypothesis PrimeIdeal(R, I) for I
notation infixl 70 "*" => call2(R.mul, _, _) via hypothesis PrimeIdeal(R, I) for I
notation prefix 75 "-" => apply(R.neg, _) via hypothesis PrimeIdeal(R, I) for I
notation infixl 60 "-" => Ring.sub(R, _, _) via hypothesis PrimeIdeal(R, I) for I

instance PrimeIdeal.parts (R I : Set)
  requires prime : PrimeIdeal(R, I)
  shows IsPrimeIdeal(R.carrier, R.add, R.zero, R.neg, R.mul, R.one, I)
proof
  obtain ⟨proper, factors⟩ := prime
  have parts := ProperIdeal.parts with proper
  unfold IsPrimeIdeal
  exact ⟨parts, factors⟩

theorem PrimeIdeal.of_projections (R I : Set)
  requires prime : IsPrimeIdeal(R.carrier, R.add, R.zero, R.neg, R.mul, R.one,
    I)
  shows PrimeIdeal(R, I)
proof
  obtain ⟨proper, factors⟩ := prime
  have bundled := ProperIdeal.of_projections with proper
  unfold PrimeIdeal.PrimeIdeal
  exact ⟨bundled, factors⟩

theorem PrimeIdeal.of_parts (A add zero neg mul one I : Set)
  requires prime : IsPrimeIdeal(A, add, zero, neg, mul, one, I)
  shows PrimeIdeal(Ring.mk(A, add, zero, neg, mul, one), I)
proof
  have shifted : IsPrimeIdeal(Ring.carrier(Ring.mk(A, add, zero, neg, mul, one)),
      Ring.add(Ring.mk(A, add, zero, neg, mul, one)),
      Ring.zero(Ring.mk(A, add, zero, neg, mul, one)),
      Ring.neg(Ring.mk(A, add, zero, neg, mul, one)),
      Ring.mul(Ring.mk(A, add, zero, neg, mul, one)),
      Ring.one(Ring.mk(A, add, zero, neg, mul, one)), I)
    ring_projections
  exact PrimeIdeal.of_projections with shifted

instance PrimeIdeal.to_proper (R I : Set)
  requires prime : PrimeIdeal(R, I)
  shows ProperIdeal(R, I)
proof
  obtain ⟨proper, factors⟩ := prime
  exact proper

theorem PrimeIdeal.to_ideal (R I : Set)
  requires prime : PrimeIdeal(R, I)
  shows Ideal(R, I)
proof
  have proper := PrimeIdeal.to_proper with prime
  exact ProperIdeal.to_ideal with proper

section PrimeLaws
variable (R I : Set)
hypothesis ring : Ring(R)
hypothesis prime : PrimeIdeal(R, I)

-- A product lies in a prime ideal exactly when a factor does.
theorem PrimeIdeal.mem_or_mem (x y : R)
  requires productIn : x * y ∈ I
  shows x ∈ I ∨ y ∈ I
proof
  obtain ⟨proper, factors⟩ := prime
  have xIn : x ∈ R by assumption
  have yIn : y ∈ R by assumption
  exact factors with x, xIn, y, yIn, productIn

theorem PrimeIdeal.mem_of_mul (x y : R)
  requires productIn : x * y ∈ I
  requires absent : y ∉ I
  shows x ∈ I
proof
  have alternatives := PrimeIdeal.mem_or_mem with *
  cases alternatives with xIn | yIn
  . exact xIn
  . exfalso
    exact absent with yIn

theorem PrimeIdeal.mul_mem_iff (x y : R)
  shows x * y ∈ I ↔ x ∈ I ∨ y ∈ I
proof
  have ideal := PrimeIdeal.to_ideal with prime
  constructor
  . intro productIn
    exact PrimeIdeal.mem_or_mem with *
  . intro alternatives
    cases alternatives with xIn | yIn
    . exact Ideal.mul_right_mem with *
    . exact Ideal.mul_left_mem with *

end PrimeLaws

section CommutativeRings
variable (R : Set)
hypothesis comm : CommRing(R)

-- In a commutative ring every maximal ideal is prime.
theorem MaximalIdeal.prime (M : Set)
  requires maximal : MaximalIdeal(R, M)
  shows PrimeIdeal(R, M)
proof
  have parts := CommRing.parts with comm
  have engine := MaximalIdeal.parts with maximal
  have prime := IsMaximalIdeal.is_prime with parts, engine
  exact PrimeIdeal.of_projections with prime

end CommutativeRings