-- Ideals, filters, and prime ideals of a 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.Ideal
import Bounded
import Set.WellOrder

-- An ideal is a nonempty lower set closed under joins; a filter is a
-- nonempty upper set closed under meets.
predicate IsLatticeIdeal (A r I : Set) :=
  IsLattice(A, r) ∧ (I ⊆ A) ∧ Nonempty(I) ∧
  (∀ x ∈ I, ∀ y ∈ I, join(A, r, x, y) ∈ I) ∧
  (∀ x ∈ I, ∀ y ∈ A, relates(r, y, x) → y ∈ I)

predicate IsLatticeFilter (A r F : Set) :=
  IsLattice(A, r) ∧ (F ⊆ A) ∧ Nonempty(F) ∧
  (∀ x ∈ F, ∀ y ∈ F, meet(A, r, x, y) ∈ F) ∧
  (∀ x ∈ F, ∀ y ∈ A, relates(r, x, y) → y ∈ F)

predicate IsLatticePrimeIdeal (A r I : Set) :=
  IsLatticeIdeal(A, r, I) ∧ I ≠ A ∧
  (∀ x ∈ A, ∀ y ∈ A, meet(A, r, x, y) ∈ I → x ∈ I ∨ y ∈ I)

-- The upper set of a point, dual to the initial segment below it.
def upperSegment (A r a : Set) : Set := { x ∈ A | relates(r, a, x) }

theorem upperSegment.subset (A r a : Set)
  shows upperSegment(A, r, a) ⊆ A
proof
  intros x hx
  have member := upperSegment.membership.forward with hx
  exact member.left

-- Projections

theorem IsLatticeIdeal.lattice (A r I : Set)
  requires h : IsLatticeIdeal(A, r, I)
  shows IsLattice(A, r)
proof
  simp [IsLatticeIdeal]

theorem IsLatticeIdeal.subset (A r I : Set)
  requires h : IsLatticeIdeal(A, r, I)
  shows I ⊆ A
proof
  simp [IsLatticeIdeal]

theorem IsLatticeIdeal.nonempty (A r I : Set)
  requires h : IsLatticeIdeal(A, r, I)
  shows Nonempty(I)
proof
  simp [IsLatticeIdeal]

theorem IsLatticeIdeal.join_closed (A r I x y : Set)
  requires h : IsLatticeIdeal(A, r, I)
  requires hx : x ∈ I
  requires hy : y ∈ I
  shows join(A, r, x, y) ∈ I
proof
  rcases h with ⟨lattice, bounded, nonempty, joins, downward⟩
  exact joins with x, hx, y, hy

theorem IsLatticeIdeal.downward (A r I x y : Set)
  requires h : IsLatticeIdeal(A, r, I)
  requires hx : x ∈ I
  requires hy : y ∈ A
  requires hyx : relates(r, y, x)
  shows y ∈ I
proof
  rcases h with ⟨lattice, bounded, nonempty, joins, downward⟩
  exact downward with x, hx, y, hy, hyx

theorem IsLatticeFilter.lattice (A r F : Set)
  requires h : IsLatticeFilter(A, r, F)
  shows IsLattice(A, r)
proof
  simp [IsLatticeFilter]

theorem IsLatticeFilter.subset (A r F : Set)
  requires h : IsLatticeFilter(A, r, F)
  shows F ⊆ A
proof
  simp [IsLatticeFilter]

theorem IsLatticeFilter.nonempty (A r F : Set)
  requires h : IsLatticeFilter(A, r, F)
  shows Nonempty(F)
proof
  simp [IsLatticeFilter]

theorem IsLatticeFilter.meet_closed (A r F x y : Set)
  requires h : IsLatticeFilter(A, r, F)
  requires hx : x ∈ F
  requires hy : y ∈ F
  shows meet(A, r, x, y) ∈ F
proof
  rcases h with ⟨lattice, bounded, nonempty, meets, upward⟩
  exact meets with x, hx, y, hy

theorem IsLatticeFilter.upward (A r F x y : Set)
  requires h : IsLatticeFilter(A, r, F)
  requires hx : x ∈ F
  requires hy : y ∈ A
  requires hxy : relates(r, x, y)
  shows y ∈ F
proof
  rcases h with ⟨lattice, bounded, nonempty, meets, upward⟩
  exact upward with x, hx, y, hy, hxy

theorem IsLatticePrimeIdeal.ideal (A r I : Set)
  requires h : IsLatticePrimeIdeal(A, r, I)
  shows IsLatticeIdeal(A, r, I)
proof
  simp [IsLatticePrimeIdeal]

theorem IsLatticePrimeIdeal.proper (A r I : Set)
  requires h : IsLatticePrimeIdeal(A, r, I)
  shows I ≠ A
proof
  simp [IsLatticePrimeIdeal]

theorem IsLatticePrimeIdeal.prime (A r I x y : Set)
  requires h : IsLatticePrimeIdeal(A, r, I)
  requires hx : x ∈ A
  requires hy : y ∈ A
  requires hxy : meet(A, r, x, y) ∈ I
  shows x ∈ I ∨ y ∈ I
proof
  rcases h with ⟨ideal, proper, prime⟩
  exact prime with x, hx, y, hy, hxy

-- Closure properties

theorem IsLatticeIdeal.meet_closed (A r I x y : Set)
  requires h : IsLatticeIdeal(A, r, I)
  requires hx : x ∈ I
  requires hy : y ∈ A
  shows meet(A, r, x, y) ∈ I
proof
  have lattice := IsLatticeIdeal.lattice with h
  have xA := IsLatticeIdeal.subset with h, x, hx
  have meetA := meet.member with lattice, xA, hy
  have below := meet.lower_left with lattice, xA, hy
  exact IsLatticeIdeal.downward with h, hx, meetA, below

theorem IsLatticeFilter.join_closed (A r F x y : Set)
  requires h : IsLatticeFilter(A, r, F)
  requires hx : x ∈ F
  requires hy : y ∈ A
  shows join(A, r, x, y) ∈ F
proof
  have lattice := IsLatticeFilter.lattice with h
  have xA := IsLatticeFilter.subset with h, x, hx
  have joinA := join.member with lattice, xA, hy
  have above := join.upper_left with lattice, xA, hy
  exact IsLatticeFilter.upward with h, hx, joinA, above

theorem IsLatticeIdeal.join_iff (A r I x y : Set)
  requires h : IsLatticeIdeal(A, r, I)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows join(A, r, x, y) ∈ I ↔ x ∈ I ∧ y ∈ I
proof
  have lattice := IsLatticeIdeal.lattice with h
  constructor
  . intro joined
    constructor
    . exact IsLatticeIdeal.downward with h, joined, hx,
        (join.upper_left with lattice, hx, hy)
    . exact IsLatticeIdeal.downward with h, joined, hy,
        (join.upper_right with lattice, hx, hy)
  . intro both
    exact IsLatticeIdeal.join_closed with h, both.left, both.right

theorem IsLatticeFilter.meet_iff (A r F x y : Set)
  requires h : IsLatticeFilter(A, r, F)
  requires hx : x ∈ A
  requires hy : y ∈ A
  shows meet(A, r, x, y) ∈ F ↔ x ∈ F ∧ y ∈ F
proof
  have lattice := IsLatticeFilter.lattice with h
  constructor
  . intro met
    constructor
    . exact IsLatticeFilter.upward with h, met, hx,
        (meet.lower_left with lattice, hx, hy)
    . exact IsLatticeFilter.upward with h, met, hy,
        (meet.lower_right with lattice, hx, hy)
  . intro both
    exact IsLatticeFilter.meet_closed with h, both.left, both.right

theorem IsLatticeIdeal.bottom (A r bot top I : Set)
  requires bounded : IsBoundedLattice(A, r, bot, top)
  requires h : IsLatticeIdeal(A, r, I)
  shows bot ∈ I
proof
  obtain ⟨x, hx⟩ := IsLatticeIdeal.nonempty with h
  have xA := IsLatticeIdeal.subset with h, x, hx
  have botA := IsBoundedLattice.bottom_member with bounded
  exact IsLatticeIdeal.downward with h, hx, botA,
      (IsBoundedLattice.bottom_le with bounded, xA)

theorem IsLatticeFilter.top (A r bot top F : Set)
  requires bounded : IsBoundedLattice(A, r, bot, top)
  requires h : IsLatticeFilter(A, r, F)
  shows top ∈ F
proof
  obtain ⟨x, hx⟩ := IsLatticeFilter.nonempty with h
  have xA := IsLatticeFilter.subset with h, x, hx
  have topA := IsBoundedLattice.top_member with bounded
  exact IsLatticeFilter.upward with h, hx, topA,
      (IsBoundedLattice.le_top with bounded, xA)

-- Examples: the whole lattice, principal ideals and filters, intersections

theorem IsLatticeIdeal.whole (A r : Set)
  requires lattice : IsLattice(A, r)
  requires nonempty : Nonempty(A)
  shows IsLatticeIdeal(A, r, A)
proof
  refine ⟨lattice, Subset.reflexive at A, nonempty, ?_, ?_⟩
  . intros x hx y hy
    exact join.member with lattice, hx, hy
  . intros x hx y hy hyx
    exact hy

theorem IsLatticeFilter.whole (A r : Set)
  requires lattice : IsLattice(A, r)
  requires nonempty : Nonempty(A)
  shows IsLatticeFilter(A, r, A)
proof
  refine ⟨lattice, Subset.reflexive at A, nonempty, ?_, ?_⟩
  . intros x hx y hy
    exact meet.member with lattice, hx, hy
  . intros x hx y hy hxy
    exact hy

theorem IsLatticeIdeal.principal (A r a : Set)
  requires lattice : IsLattice(A, r)
  requires ha : a ∈ A
  shows IsLatticeIdeal(A, r, segment(A, r, a))
proof
  have reflexive := IsLattice.reflexive with lattice
  have transitive := IsLattice.transitive with lattice
  have self : a ∈ segment(A, r, a) :=
    segment.membership.backward with ⟨ha, (reflexive with a, ha)⟩
  have nonempty : Nonempty(segment(A, r, a)) := ⟨a, self⟩
  refine ⟨lattice, (segment.subset at A, r, a), nonempty, ?_, ?_⟩
  . intros x hx y hy
    have xS := segment.membership.forward with hx
    have yS := segment.membership.forward with hy
    have joinA := join.member with lattice, xS.left, yS.left
    have below := join.least with lattice, xS.left, yS.left, ha, xS.right,
        yS.right
    exact segment.membership.backward with ⟨joinA, below⟩
  . intros x hx y hy hyx
    have xS := segment.membership.forward with hx
    have below := transitive with y, hy, x, xS.left, a, ha, hyx, xS.right
    exact segment.membership.backward with ⟨hy, below⟩

theorem IsLatticeFilter.principal (A r a : Set)
  requires lattice : IsLattice(A, r)
  requires ha : a ∈ A
  shows IsLatticeFilter(A, r, upperSegment(A, r, a))
proof
  have reflexive := IsLattice.reflexive with lattice
  have transitive := IsLattice.transitive with lattice
  have self : a ∈ upperSegment(A, r, a) :=
    upperSegment.membership.backward with ⟨ha, (reflexive with a, ha)⟩
  have nonempty : Nonempty(upperSegment(A, r, a)) := ⟨a, self⟩
  refine ⟨lattice, (upperSegment.subset at A, r, a), nonempty, ?_, ?_⟩
  . intros x hx y hy
    have xS := upperSegment.membership.forward with hx
    have yS := upperSegment.membership.forward with hy
    have meetA := meet.member with lattice, xS.left, yS.left
    have above := meet.greatest with lattice, xS.left, yS.left, ha, xS.right,
        yS.right
    exact upperSegment.membership.backward with ⟨meetA, above⟩
  . intros x hx y hy hxy
    have xS := upperSegment.membership.forward with hx
    have above := transitive with a, ha, x, xS.left, y, hy, xS.right, hxy
    exact upperSegment.membership.backward with ⟨hy, above⟩

theorem IsLatticeIdeal.intersection (A r I J : Set)
  requires hI : IsLatticeIdeal(A, r, I)
  requires hJ : IsLatticeIdeal(A, r, J)
  shows IsLatticeIdeal(A, r, I ∩ J)
proof
  have lattice := IsLatticeIdeal.lattice with hI
  have bounded := Subset.transitive with (intersection.subset_left at I, J),
      (IsLatticeIdeal.subset with hI)
  have nonempty : Nonempty(I ∩ J)
    obtain ⟨x, hx⟩ := IsLatticeIdeal.nonempty with hI
    obtain ⟨y, hy⟩ := IsLatticeIdeal.nonempty with hJ
    have xA := IsLatticeIdeal.subset with hI, x, hx
    have yA := IsLatticeIdeal.subset with hJ, y, hy
    have inI := IsLatticeIdeal.meet_closed with hI, hx, yA
    have swap := meet.commutative with lattice, xA, yA
    have inJ := IsLatticeIdeal.meet_closed with hJ, hy, xA
    rw ← swap at inJ
    refine ⟨meet(A, r, x, y), (intersection.membership.backward with ⟨inI,
        inJ⟩)⟩
  refine ⟨lattice, bounded, nonempty, ?_, ?_⟩
  . intros x hx y hy
    have xBoth := intersection.membership.forward with hx
    have yBoth := intersection.membership.forward with hy
    apply intersection.membership.backward
    constructor
    . exact IsLatticeIdeal.join_closed with hI, xBoth.left, yBoth.left
    . exact IsLatticeIdeal.join_closed with hJ, xBoth.right, yBoth.right
  . intros x hx y hy hyx
    have xBoth := intersection.membership.forward with hx
    apply intersection.membership.backward
    constructor
    . exact IsLatticeIdeal.downward with hI, xBoth.left, hy, hyx
    . exact IsLatticeIdeal.downward with hJ, xBoth.right, hy, hyx

-- Duality: ideals of the converse order are filters.

theorem IsLatticeIdeal.converse (A r I : Set)
  requires h : IsLatticeIdeal(A, r, I)
  shows IsLatticeFilter(A, converse(r, A, A), I)
proof
  have lattice := IsLatticeIdeal.lattice with h
  have bounded := IsLatticeIdeal.subset with h
  refine ⟨(IsLattice.converse with lattice), bounded,
      (IsLatticeIdeal.nonempty with h), ?_, ?_⟩
  . intros x hx y hy
    have swap := meet.converse with lattice, (bounded with x, hx),
        (bounded with y, hy)
    rw swap
    exact IsLatticeIdeal.join_closed with h, hx, hy
  . intros x hx y hy hxy
    have reversed := converse.reflects with hxy
    exact IsLatticeIdeal.downward with h, hx, hy, reversed

theorem IsLatticeFilter.converse (A r F : Set)
  requires h : IsLatticeFilter(A, r, F)
  shows IsLatticeIdeal(A, converse(r, A, A), F)
proof
  have lattice := IsLatticeFilter.lattice with h
  have bounded := IsLatticeFilter.subset with h
  refine ⟨(IsLattice.converse with lattice), bounded,
      (IsLatticeFilter.nonempty with h), ?_, ?_⟩
  . intros x hx y hy
    have swap := join.converse with lattice, (bounded with x, hx),
        (bounded with y, hy)
    rw swap
    exact IsLatticeFilter.meet_closed with h, hx, hy
  . intros x hx y hy hyx
    have reversed := converse.reflects with hyx
    exact IsLatticeFilter.upward with h, hx, hy, reversed