dcpo.lean

import order.ideal

/- Say a partial order `P` is directed complete, or a dcpo, if every directed subset in `P` has a 
supremum (we actually work with ideals instead of general directed subsets, but every directed
subset is cofinal with an ideal so it doesn't matter). A morphism `P → Q` of dcpo's is a monotone
function which preserves suprema of directed subsets. 

The main result of this file is that for any preorder `P`, `ideal P` is the free dcpo on `P`, in
the sense that any monotone funtcion `P → Q` where `Q` is a dcpo extends uniquely to a morphism 
`ideal P → Q` of dcpo's. -/

namespace order

variables {P Q R : Type*} [preorder P] [partial_order Q] [partial_order R]

def ideal.map : (P →ₘ Q) →ₘ ideal P →ₘ ideal Q :=
{ to_fun := λ f, 
    { to_fun := λ I, 
      { carrier := { q | ∃ p ∈ I, q ≤ f p },
        nonempty := by { cases I.nonempty with p hp, exact ⟨_, p, hp, le_refl _⟩ },
        directed := begin
            rintro x ⟨a, ai, xa⟩ y ⟨b, bi, yb⟩,
            rcases I.directed a ai b bi with ⟨c, hc, ac, bc⟩,
            exact ⟨_, ⟨c, hc, le_refl _⟩, le_trans xa (f.monotone ac), le_trans yb (f.monotone bc)⟩,
          end,
        mem_of_le := λ x y yx ⟨p, hp, xp⟩, ⟨p, hp, le_trans yx xp⟩ },
      monotone' := λ I J ij q ⟨p, pi, qp⟩, ⟨p, ij pi, qp⟩ },
  monotone' := λ f g fg I q ⟨p, pi, qp⟩, ⟨p, pi, le_trans qp (fg p)⟩ }

def ideal.mul (I : ideal (ideal P)) : ideal P :=
{ carrier := { p | ∃ i ∈ I, p ∈ i },
  nonempty := begin
      cases I.nonempty with i hi,
      cases i.nonempty with p hp,
      exact ⟨p, i, hi, hp⟩
    end,
  directed := begin
      rintro p ⟨i, hi, pi⟩ q ⟨j, hj, qj⟩, 
      rcases I.directed i hi j hj with ⟨k, hk, ik, jk⟩,
      rcases k.directed p (ik pi) q (jk qj) with ⟨r, rk, pr, qr⟩,
      exact ⟨r, ⟨k, hk, rk⟩, pr, qr⟩
    end,
  mem_of_le := λ x y xy ⟨i, hi, yi⟩, ⟨i, hi, i.mem_of_le xy yi⟩ }

lemma mul_is_lub (I : ideal (ideal P)) : is_lub I.carrier I.mul :=
⟨λ i hi p pi, ⟨i, hi, pi⟩, λ i hi p ⟨j, hj, pj⟩, hi hj pj⟩

def principal_mono : P →ₘ ideal P :=
{ to_fun := ideal.principal,
  monotone' := λ p q pq, ideal.principal_le_iff.mpr pq }

lemma mul_eq_self (I : ideal P) : ideal.mul (ideal.map principal_mono I) = I :=
begin
  ext p,
  split,
  { rintro ⟨j, ⟨q, qi, jq⟩, pj⟩, exact I.mem_of_le (jq pj) qi },
  { intro pi, exact ⟨_, ⟨p, pi, le_refl _⟩, le_refl _⟩ }
end

lemma mul_comp (f : P →ₘ Q) (g : Q →ₘ R) (I : ideal P) :
  ideal.map (g.comp f) I = ideal.map g (ideal.map f I) :=
begin
  ext r,
  split,
  { rintro ⟨p, hp, rp⟩, exact ⟨_, ⟨_, hp, le_refl _⟩, rp⟩ },
  { rintro ⟨q, ⟨p, hp, qp⟩, qr⟩, exact ⟨p, hp, le_trans qr (g.monotone qp)⟩ }
end

variables (P Q)

class dcpo :=
(dsup (I : ideal P) : P)
(is_lub (I : ideal P) : is_lub I.carrier (dsup I))

@[ext] structure dcpo_hom [dcpo P] [dcpo Q] extends preorder_hom P Q :=
(map_dsup : ∀ I : ideal P, to_fun (dcpo.dsup I) = dcpo.dsup (ideal.map to_preorder_hom I))

instance : dcpo (ideal P) := { dsup := ideal.mul, is_lub := mul_is_lub }

/-- The free-forgetful adjunction. -/
def lift [dcpo Q] : (P →ₘ Q) ≃ (dcpo_hom (ideal P) Q) :=
{ to_fun := λ f, ⟨⟨λ I, dcpo.dsup (ideal.map f I), 
    λ I J ij, is_lub.mono (dcpo.is_lub _) (dcpo.is_lub _) ((ideal.map f).monotone ij)⟩, 
    begin
      intro I,
      apply le_antisymm;
      apply (dcpo.is_lub _).2,
      { rintro q ⟨p, ⟨i, hi, pi⟩, qp⟩,
        exact le_trans qp ((dcpo.is_lub _).1 ⟨i, hi, (dcpo.is_lub _).1 ⟨p, pi, le_refl _⟩⟩) },
      { rintro q ⟨i, hi, qi⟩,
        exact le_trans qi (preorder_hom.monotone _ $ (dcpo.is_lub I).1 hi) }
    end⟩,
  inv_fun := λ f, f.to_preorder_hom.comp principal_mono,
  left_inv := λ f, begin
      ext p,
      apply (dcpo.is_lub _).unique,
      split,
      { rintros q ⟨p', hp', qp'⟩, exact le_trans qp' (f.monotone hp') },
      { intros q hq, exact hq ⟨p, le_refl _, le_refl _⟩ }
    end,
  right_inv := λ f, begin
      ext i,
      dsimp,
      convert (f.map_dsup (ideal.map principal_mono i)).symm,
      { apply mul_comp },
      { exact (mul_eq_self i).symm }
    end }

end order