---
title:       Ideals of distributive lattices
author:      Ayberk Tosun
start-date:  2024-02-14
---

This module contains the definition of the notion of ideal over a distributive
lattice.

\begin{code}

{-# OPTIONS --safe --without-K #-}

open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

module Locales.DistributiveLattice.Ideal
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
        (pe : Prop-Ext)
       where

open import Locales.DistributiveLattice.Definition fe pt
open import Locales.DistributiveLattice.Properties fe pt
open import Locales.Frame pt fe
open import MLTT.List
open import MLTT.Spartan
open import UF.Equiv hiding (_β– )
open import UF.Logic
open import UF.Powerset-MultiUniverse
open import UF.SubtypeClassifier

open AllCombinators pt fe hiding (_∨_)
open PropositionalTruncation pt hiding (_∨_)

\end{code}

The type of ideals of a distributive lattice.

\begin{code}

is-inhabited : (L : DistributiveLattice 𝓀) β†’ π“Ÿ {π“₯} ∣ L ∣ᡈ β†’ Ξ© (𝓀 βŠ” π“₯)
is-inhabited L S = Ǝ x κž‰ ∣ L ∣ᡈ , x ∈ S

is-downward-closed : (L : DistributiveLattice 𝓀) β†’ π“Ÿ {π“₯} ∣ L ∣ᡈ β†’ Ξ© (𝓀 βŠ” π“₯)
is-downward-closed L I =
 β±― x κž‰ ∣ L ∣ᡈ , β±― y κž‰ ∣ L ∣ᡈ , x β‰€α΅ˆ[ L ] y β‡’ y βˆˆβ‚š I β‡’ x βˆˆβ‚š I
  where
   open DistributiveLattice L

is-closed-under-binary-joins : (L : DistributiveLattice 𝓀)
                             β†’ π“Ÿ {π“₯} ∣ L ∣ᡈ β†’ Ξ© (𝓀 βŠ” π“₯)
is-closed-under-binary-joins L I =
 β±― x κž‰ ∣ L ∣ᡈ , β±― y κž‰ ∣ L ∣ᡈ , x βˆˆβ‚š I β‡’ y βˆˆβ‚š I β‡’ (x ∨ y) βˆˆβ‚š I
  where
   open DistributiveLattice L

record Ideal (L : DistributiveLattice 𝓀) : 𝓀 ⁺ Μ‡ where
 open DistributiveLattice L

 field
  I : π“Ÿ {𝓀} ∣ L ∣ᡈ
  I-is-inhabited       : is-inhabited L I holds
  I-is-downward-closed : is-downward-closed L I holds
  I-is-closed-under-∨  : is-closed-under-binary-joins L I holds

 I-contains-𝟎 : (𝟎 βˆˆβ‚š I) holds
 I-contains-𝟎 = βˆ₯βˆ₯-rec (holds-is-prop (𝟎 βˆˆβ‚š I)) † I-is-inhabited
  where
   † : Ξ£ x κž‰ X , (x βˆˆβ‚š I) holds β†’ 𝟎 ∈ I
   † (x , p) = I-is-downward-closed 𝟎 x (𝟎ᡈ-is-bottom L x) p

module IdealNotation (L : DistributiveLattice 𝓀)  where

 _∈ᡒ_ : ∣ L ∣ᡈ β†’ Ideal L β†’ Ξ© 𝓀
 x ∈ᡒ ℐ = Ideal.I ℐ x

 infix 30 _∈ᡒ_

 _∈ⁱ_ : ∣ L ∣ᡈ β†’ Ideal L β†’ 𝓀 Μ‡
 x ∈ⁱ ℐ = (x ∈ᡒ ℐ) holds

is-ideal : (L : DistributiveLattice 𝓀) β†’ π“Ÿ {𝓀} ∣ L ∣ᡈ β†’ Ξ© 𝓀
is-ideal L I =
 is-inhabited L I ∧ is-downward-closed L I ∧ is-closed-under-binary-joins L I

Idealβ‚€ : DistributiveLattice 𝓀 β†’ 𝓀 ⁺ Μ‡
Idealβ‚€ {𝓀} L = Ξ£ I κž‰ π“Ÿ {𝓀} ∣ L ∣ᡈ , is-ideal L I holds

to-idealβ‚€ : (L : DistributiveLattice 𝓀) β†’ Ideal L β†’ Idealβ‚€ L
to-idealβ‚€ L ℐ = I , I-is-inhabited , I-is-downward-closed , I-is-closed-under-∨
 where
  open Ideal ℐ

to-ideal : (L : DistributiveLattice 𝓀) β†’ Idealβ‚€ L β†’ Ideal L
to-ideal L ℐ@(I , ΞΉ , Ξ΄ , Ξ½) = record
                                { I                    = I
                                ; I-is-inhabited       = ΞΉ
                                ; I-is-downward-closed = Ξ΄
                                ; I-is-closed-under-∨  = ν
                               }

ideal-equiv-idealβ‚€ : (L : DistributiveLattice 𝓀) β†’ (Ideal L) ≃ (Idealβ‚€ L)
ideal-equiv-idealβ‚€ L =
 (to-idealβ‚€ L) , (to-ideal L , Ξ» _ β†’ refl) , (to-ideal L) , Ξ» _ β†’ refl

ideal-extensionality : (L : DistributiveLattice 𝓀)
                     β†’ (I₁ Iβ‚‚ : Ideal L)
                     β†’ Ideal.I I₁ βŠ† Ideal.I Iβ‚‚
                     β†’ Ideal.I Iβ‚‚ βŠ† Ideal.I I₁
                     β†’ I₁ ＝ Iβ‚‚
ideal-extensionality L I₁ Iβ‚‚ Ο† ψ = I₁                          ＝⟨ refl ⟩
                                   to-ideal L (to-idealβ‚€ L I₁) ＝⟨ † ⟩
                                   to-ideal L (to-idealβ‚€ L Iβ‚‚) ＝⟨ refl ⟩
                                   Iβ‚‚                          ∎
 where
  open Ideal I₁ renaming (I to I₁′)
  open Ideal Iβ‚‚ renaming (I to Iβ‚‚β€²)

  q : (x : ∣ L ∣ᡈ) β†’ I₁′ x ＝ Iβ‚‚β€² x
  q x = to-subtype-＝
         (Ξ» _ β†’ being-prop-is-prop fe)
         (pe (holds-is-prop (x βˆˆβ‚š I₁′)) (holds-is-prop (x βˆˆβ‚š Iβ‚‚β€²)) (Ο† x) (ψ x))

  ‑ : to-idealβ‚€ L I₁ ＝ to-idealβ‚€ L Iβ‚‚
  ‑ = to-subtype-＝ (Ξ» I β†’ holds-is-prop (is-ideal L I)) (dfunext fe q)

  † = ap (to-ideal L) ‑

\end{code}

Closed under finite joins.

\begin{code}

module _ (L : DistributiveLattice 𝓀) (I : Ideal L) where

 open IdealNotation L
 open Ideal I hiding (I)

 ideals-are-closed-under-finite-joins : (xs : List ∣ L ∣ᡈ)
                                      β†’ (((x , _) : type-from-list xs) β†’ (x ∈ᡒ I) holds)
                                      β†’ (join-listᡈ L xs ∈ᡒ I) holds
 ideals-are-closed-under-finite-joins []       Ο† = I-contains-𝟎
 ideals-are-closed-under-finite-joins (x ∷ xs) Ο† =
  I-is-closed-under-∨ x (join-listᡈ L xs) (Ο† (x , in-head)) IH
   where
    † : (k : type-from-list xs) β†’ (pr₁ k ∈ᡒ I) holds
    † (k , r) = Ο† (k , in-tail r)

    IH : (join-listᡈ L xs ∈ᡒ I) holds
    IH = ideals-are-closed-under-finite-joins xs †

\end{code}

The principal ideal.

\begin{code}

module PrincipalIdeals (L : DistributiveLattice 𝓀) where

 open DistributiveLattice L

 down-closure : ∣ L ∣ᡈ β†’ π“Ÿ {𝓀} ∣ L ∣ᡈ
 down-closure x = Ξ» y β†’ y β‰€α΅ˆ[ L ] x

 principal-ideal : ∣ L ∣ᡈ β†’ Ideal L
 principal-ideal x =
  let
   open PosetReasoning (poset-ofᡈ L)

   † : is-downward-closed L (down-closure x) holds
   † y z p q = y β‰€βŸ¨ p ⟩ z β‰€βŸ¨ q ⟩ x β– 

   ‑ : is-closed-under-binary-joins L (down-closure x) holds
   ‑ a b c p = ∨-is-least L a b x (c , p)
  in
   record
    { I                    = down-closure x
    ; I-is-inhabited       = ∣ x , ≀-is-reflexive (poset-ofᡈ L) x ∣
    ; I-is-downward-closed = †
    ; I-is-closed-under-∨  = ‑
   }

\end{code}

Some nice syntax. Tried turning this into a definition with the same precedence,
but it doesn't seem to work.


\begin{code}

 syntax principal-ideal x = ↓ x

 infix 32 principal-ideal

\end{code}