-- Ideals, filters, and prime ideals of a bundled lattice
-- 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.Lattice.Ideals
import Ideal
import Sublattices

-- An ideal is a nonempty lower set closed under joins, a filter a nonempty
-- upper set closed under meets, and a prime ideal a proper ideal that
-- contains a factor of every meet it contains.
predicate LatticeIdeal (P I : Set) := IsLatticeIdeal(points(P), le(P), I)
predicate LatticeFilter (P F : Set) := IsLatticeFilter(points(P), le(P), F)
predicate LatticePrimeIdeal (P I : Set) := IsLatticePrimeIdeal(points(P), le(P), I)

notation infixl 68 "⊔" => call2(sup(P), _, _) via hypothesis LatticeIdeal(P, I) for P.points
notation infixl 69 "⊓" => call2(inf(P), _, _) via hypothesis LatticeIdeal(P, I) for P.points
notation infix 50 "≤" => Le(P, _, _) via hypothesis LatticeIdeal(P, I) for P.points
notation infixl 68 "⊔" => call2(sup(P), _, _) via hypothesis LatticeFilter(P, F) for P.points
notation infixl 69 "⊓" => call2(inf(P), _, _) via hypothesis LatticeFilter(P, F) for P.points
notation infix 50 "≤" => Le(P, _, _) via hypothesis LatticeFilter(P, F) for P.points
notation infixl 68 "⊔" => call2(sup(P), _, _) via hypothesis LatticePrimeIdeal(P, I) for P.points
notation infixl 69 "⊓" => call2(inf(P), _, _) via hypothesis LatticePrimeIdeal(P, I) for P.points
notation infix 50 "≤" => Le(P, _, _) via hypothesis LatticePrimeIdeal(P, I) for P.points

instance LatticeIdeal.unbundled (P I : Set)
  requires ideal : LatticeIdeal(P, I)
  shows IsLatticeIdeal(points(P), le(P), I)
proof
  simp [LatticeIdeal]

instance LatticeFilter.unbundled (P F : Set)
  requires filter : LatticeFilter(P, F)
  shows IsLatticeFilter(points(P), le(P), F)
proof
  simp [LatticeFilter]

instance LatticePrimeIdeal.unbundled (P I : Set)
  requires prime : LatticePrimeIdeal(P, I)
  shows IsLatticePrimeIdeal(points(P), le(P), I)
proof
  simp [LatticePrimeIdeal]

theorem LatticeIdeal.mk (A r I : Set)
  requires ideal : IsLatticeIdeal(A, r, I)
  shows LatticeIdeal(Order.mk(A, r), I)
proof
  unfold LatticeIdeal
  rw [Order.mk.points, Order.mk.le]
  exact ideal

theorem LatticeFilter.mk (A r F : Set)
  requires filter : IsLatticeFilter(A, r, F)
  shows LatticeFilter(Order.mk(A, r), F)
proof
  unfold LatticeFilter
  rw [Order.mk.points, Order.mk.le]
  exact filter

theorem LatticePrimeIdeal.mk (A r I : Set)
  requires prime : IsLatticePrimeIdeal(A, r, I)
  shows LatticePrimeIdeal(Order.mk(A, r), I)
proof
  unfold LatticePrimeIdeal
  rw [Order.mk.points, Order.mk.le]
  exact prime

instance LatticeIdeal.lattice_of (P I : Set)
  requires ideal : LatticeIdeal(P, I)
  shows Lattice(P)
proof
  unfold Join.Lattice
  exact IsLatticeIdeal.lattice with (LatticeIdeal.unbundled with ideal)

instance LatticeFilter.lattice_of (P F : Set)
  requires filter : LatticeFilter(P, F)
  shows Lattice(P)
proof
  unfold Join.Lattice
  exact IsLatticeFilter.lattice with (LatticeFilter.unbundled with filter)

instance LatticePrimeIdeal.ideal_of (P I : Set)
  requires prime : LatticePrimeIdeal(P, I)
  shows LatticeIdeal(P, I)
proof
  unfold LatticeIdeal
  exact IsLatticePrimeIdeal.ideal with (LatticePrimeIdeal.unbundled with prime)

-- The principal lower and upper sets of a point.
def Iic (P a : Set) : Set := segment(points(P), le(P), a)
def Ici (P a : Set) : Set := upperSegment(points(P), le(P), a)

theorem Iic.membership (P a x : Set)
  shows x ∈ Iic(P, a) ↔ (x ∈ points(P) ∧ relates(le(P), x, a))
proof
  simp [Iic, segment]

theorem Ici.membership (P a x : Set)
  shows x ∈ Ici(P, a) ↔ (x ∈ points(P) ∧ relates(le(P), a, x))
proof
  simp [Ici, upperSegment]

section IdealLaws
variable (P I : Set)
hypothesis ideal : LatticeIdeal(P, I)

theorem LatticeIdeal.subset_points
  shows I ⊆ points(P)
proof
  exact IsLatticeIdeal.subset with (LatticeIdeal.unbundled with ideal)

theorem LatticeIdeal.mem_points (a : Set)
  requires aIn : a ∈ I
  shows a ∈ points(P)
proof
  have subset := LatticeIdeal.subset_points with ideal
  exact subset with a, aIn

theorem LatticeIdeal.nonempty_of
  shows Nonempty(I)
proof
  exact IsLatticeIdeal.nonempty with (LatticeIdeal.unbundled with ideal)

instance LatticeIdeal.sup_mem (a b : Set)
  requires aIn : a ∈ I
  requires bIn : b ∈ I
  shows a ⊔ b ∈ I
proof
  have aCarrier := LatticeIdeal.mem_points with ideal, aIn
  have bCarrier := LatticeIdeal.mem_points with ideal, bIn
  rw sup.join
  exact IsLatticeIdeal.join_closed with (LatticeIdeal.unbundled with ideal), aIn,
      bIn

theorem LatticeIdeal.mem_of_le (a : Set) (b ∈ points(P))
  requires aIn : a ∈ I
  requires hba : b ≤ a
  shows b ∈ I
proof
  exact IsLatticeIdeal.downward with (LatticeIdeal.unbundled with ideal), aIn,
      assumption, (Le.relates with hba)

instance LatticeIdeal.inf_mem_left (a : Set) (b ∈ points(P))
  requires aIn : a ∈ I
  shows a ⊓ b ∈ I
proof
  have aCarrier := LatticeIdeal.mem_points with ideal, aIn
  rw inf.meet
  exact IsLatticeIdeal.meet_closed with (LatticeIdeal.unbundled with ideal), aIn,
      assumption

theorem LatticeIdeal.sup_mem_iff (a b ∈ points(P))
  shows a ⊔ b ∈ I ↔ (a ∈ I ∧ b ∈ I)
proof
  rw sup.join
  exact IsLatticeIdeal.join_iff with (LatticeIdeal.unbundled with ideal),
      assumption, assumption

end IdealLaws

section IdealBounds
variable (P I : Set)
hypothesis bounded : BoundedLattice(P)
hypothesis ideal : LatticeIdeal(P, I)

theorem LatticeIdeal.bot_mem
  shows bot(P) ∈ I
proof
  exact IsLatticeIdeal.bottom with (BoundedLattice.unbundled with bounded),
      (LatticeIdeal.unbundled with ideal)

end IdealBounds

section FilterLaws
variable (P F : Set)
hypothesis filter : LatticeFilter(P, F)

theorem LatticeFilter.subset_points
  shows F ⊆ points(P)
proof
  exact IsLatticeFilter.subset with (LatticeFilter.unbundled with filter)

theorem LatticeFilter.mem_points (a : Set)
  requires aIn : a ∈ F
  shows a ∈ points(P)
proof
  have subset := LatticeFilter.subset_points with filter
  exact subset with a, aIn

theorem LatticeFilter.nonempty_of
  shows Nonempty(F)
proof
  exact IsLatticeFilter.nonempty with (LatticeFilter.unbundled with filter)

instance LatticeFilter.inf_mem (a b : Set)
  requires aIn : a ∈ F
  requires bIn : b ∈ F
  shows a ⊓ b ∈ F
proof
  have aCarrier := LatticeFilter.mem_points with filter, aIn
  have bCarrier := LatticeFilter.mem_points with filter, bIn
  rw inf.meet
  exact IsLatticeFilter.meet_closed with (LatticeFilter.unbundled with filter),
      aIn, bIn

theorem LatticeFilter.mem_of_le (a : Set) (b ∈ points(P))
  requires aIn : a ∈ F
  requires hab : a ≤ b
  shows b ∈ F
proof
  exact IsLatticeFilter.upward with (LatticeFilter.unbundled with filter), aIn,
      assumption, (Le.relates with hab)

instance LatticeFilter.sup_mem_left (a : Set) (b ∈ points(P))
  requires aIn : a ∈ F
  shows a ⊔ b ∈ F
proof
  have aCarrier := LatticeFilter.mem_points with filter, aIn
  rw sup.join
  exact IsLatticeFilter.join_closed with (LatticeFilter.unbundled with filter),
      aIn, assumption

theorem LatticeFilter.inf_mem_iff (a b ∈ points(P))
  shows a ⊓ b ∈ F ↔ (a ∈ F ∧ b ∈ F)
proof
  rw inf.meet
  exact IsLatticeFilter.meet_iff with (LatticeFilter.unbundled with filter),
      assumption, assumption

end FilterLaws

section FilterBounds
variable (P F : Set)
hypothesis bounded : BoundedLattice(P)
hypothesis filter : LatticeFilter(P, F)

theorem LatticeFilter.top_mem
  shows top(P) ∈ F
proof
  exact IsLatticeFilter.top with (BoundedLattice.unbundled with bounded),
      (LatticeFilter.unbundled with filter)

end FilterBounds

section PrimeLaws
variable (P I : Set)
hypothesis prime : LatticePrimeIdeal(P, I)

theorem LatticePrimeIdeal.ne_points
  shows I ≠ points(P)
proof
  exact IsLatticePrimeIdeal.proper with (LatticePrimeIdeal.unbundled with prime)

theorem LatticePrimeIdeal.mem_or_mem (a b ∈ points(P))
  requires meetIn : a ⊓ b ∈ I
  shows a ∈ I ∨ b ∈ I
proof
  rw inf.meet at meetIn
  exact IsLatticePrimeIdeal.prime with (LatticePrimeIdeal.unbundled with prime),
      assumption,
      assumption, meetIn

end PrimeLaws

-- The whole points, principal ideals and filters, intersections, and
-- duality.
theorem LatticeIdeal.univ (P : Set)
  requires lattice : Lattice(P)
  requires nonempty : Nonempty(points(P))
  shows LatticeIdeal(P, points(P))
proof
  unfold LatticeIdeal
  exact IsLatticeIdeal.whole with (Lattice.unbundled with lattice), nonempty

theorem LatticeFilter.univ (P : Set)
  requires lattice : Lattice(P)
  requires nonempty : Nonempty(points(P))
  shows LatticeFilter(P, points(P))
proof
  unfold LatticeFilter
  exact IsLatticeFilter.whole with (Lattice.unbundled with lattice), nonempty

theorem IsLatticeIdeal.principal (P a : Set)
  requires lattice : Lattice(P)
  requires aIn : a ∈ points(P)
  shows LatticeIdeal(P, Iic(P, a))
proof
  unfold LatticeIdeal
  unfold Iic
  exact IsLatticeIdeal.principal with (Lattice.unbundled with lattice), aIn

theorem IsLatticeFilter.principal (P a : Set)
  requires lattice : Lattice(P)
  requires aIn : a ∈ points(P)
  shows LatticeFilter(P, Ici(P, a))
proof
  unfold LatticeFilter
  unfold Ici
  exact IsLatticeFilter.principal with (Lattice.unbundled with lattice), aIn

theorem LatticeIdeal.inter (P I J : Set)
  requires hI : LatticeIdeal(P, I)
  requires hJ : LatticeIdeal(P, J)
  shows LatticeIdeal(P, I ∩ J)
proof
  unfold LatticeIdeal
  exact IsLatticeIdeal.intersection with (LatticeIdeal.unbundled with hI),
      (LatticeIdeal.unbundled with hJ)

theorem LatticeIdeal.dual (P I : Set)
  requires ideal : LatticeIdeal(P, I)
  shows LatticeFilter(dual(P), I)
proof
  unfold LatticeFilter
  rw [dual.points, dual.le]
  exact IsLatticeIdeal.converse with (LatticeIdeal.unbundled with ideal)

theorem LatticeFilter.dual (P F : Set)
  requires filter : LatticeFilter(P, F)
  shows LatticeIdeal(dual(P), F)
proof
  unfold LatticeIdeal
  rw [dual.points, dual.le]
  exact IsLatticeFilter.converse with (LatticeFilter.unbundled with filter)