Require Import base protype ordtype clat frame mono.

Definition is_adjunction {X Y : proType} (f : X -> Y) (g : Y -> X) :=
  forall (x : X) (y : Y), (f x ≤ y) <-> (x ≤ g y).
Existing Class is_adjunction.
Hint Mode is_adjunction - - ! - : typeclass_instances.
Hint Mode is_adjunction - - - ! : typeclass_instances.

Definition right_adjoint_proj {A B : proType} (f : A -> B) {g : B -> A}
  {h : is_adjunction f g} : B -> A := g.
Notation "f ^*" := (@right_adjoint_proj _ _ f _ _)
  (at level 2, format "f ^*") : ord_scope.

Lemma adjP {X Y : proType} (f : X -> Y) (g : Y -> X) {h : is_adjunction f g} x y :
  (f x ≤ y) <-> (x ≤ g y).
Proof. exact: h. Qed.

Section LeftAdjoints.
  Context {X Y : proType} (f : X -> Y) (g : Y -> X) {h : is_adjunction f g}.

  Lemma adj_unit x : x ≤ g (f x).
  Proof. by rewrite -adjP. Qed.

  Global Instance adj_monoL : monotone f.
  Proof.
    move=> x y lxy. rewrite adjP. apply: le_trans lxy _. exact: adj_unit.
  Qed.

  Lemma adj_lub I (F : I -> X) x :
    is_lub F x -> is_lub (f \o F) (f x).
  Proof.
    move=> lub y. rewrite adjP lub. split=> ub i /=. by rewrite adjP.
    rewrite -adjP. exact: ub.
  Qed.
End LeftAdjoints.

Instance rev_is_adjunction {X Y : proType} (f : X -> Y) (g : Y -> X) {h : is_adjunction f g} :
  is_adjunction (g : Y^r -> X^r) (f : X^r -> Y^r).
Proof. move=> x y. by rewrite !rev_leE h. Qed.

Section RightAdjoints.
  Context {X Y : proType} (f : X -> Y) (g : Y -> X) {h : is_adjunction f g}.
  Let Xr := [proType of X^r].
  Let Yr := [proType of Y^r].

  Lemma adj_counit x : f (g x) ≤ x.
  Proof. exact: (@adj_unit Yr Xr g f). Qed.

  Global Instance adj_monoR : monotone g.
  Proof. move=> x y. exact: (@adj_monoL Yr Xr). Qed.

  Lemma adj_glb I (F : I -> Y) x :
    is_glb F x -> is_glb (g \o F) (g x).
  Proof. exact: (@adj_lub Yr Xr). Qed.
End RightAdjoints.

Section AdjunctionsOrd.
  Variables X Y : ordType.

  Lemma adj_uniqR (f : X -> Y) (g1 g2 : Y -> X) :
    is_adjunction f g1 -> is_adjunction f g2 -> g1 = g2.
  Proof.
    move=> h1 h2. fext=> x. wlog suff: g1 g2 h1 h2 x / g1 x ≤ g2 x => [h|].
    apply: le_eq; exact: h. exact/h2/h1.
  Qed.

  Lemma adj_tripleL (f : X -> Y) (g : Y -> X) {h : is_adjunction f g} x :
    g (f (g x)) = g x.
  Proof.
    apply: le_eq. apply: mono. exact: adj_counit. by rewrite -adjP.
  Qed.
End AdjunctionsOrd.

Section AdjunctionsOrdDual.
  Variables X Y : ordType.
  Let Xr := [ordType of X^r].
  Let Yr := [ordType of Y^r].

  Lemma adj_uniqL (f1 f2 : X -> Y) (g : Y -> X) :
    is_adjunction f1 g -> is_adjunction f2 g -> f1 = f2.
  Proof.
    move=> h1 h2. apply: (@adj_uniqR Yr Xr g) => y x; by rewrite !rev_leE ?h1 ?h2.
  Qed.

  Lemma adj_tripleR (f : X -> Y) (g : Y -> X) {h : is_adjunction f g} x :
    f (g (f x)) = f x.
  Proof. exact: (@adj_tripleL Yr Xr g f). Qed.
End AdjunctionsOrdDual.

Section AdjunctionsCLat.
  Variables (X Y : clat) (f : X -> Y) (g : Y -> X).
  Context {H : is_adjunction f g}.

  Lemma adjB : f ⊥ = ⊥.
  Proof. apply: bot_eq. exact/adjP. Qed.

  Lemma adjJ x y : f (x ∨ y) = (f x ∨ f y).
  Proof.
    apply: le_eq; last by exact: monoJ.
    apply/adjP; focus; apply/adjP; by cauto.
  Qed.

  Lemma adjE I (F : I -> X) : f (sup F) = ∃ i, f (F i).
  Proof.
    apply: le_eq; last by exact: monoE.
    apply/adjP; focus=> i; apply/adjP. exact: exI.
  Qed.

  Lemma adjEc I (P : I -> Prop) (F : I -> X) :
    f (∃ i | P i, F i) = ∃ i | P i, f (F i).
  Proof.
    rewrite adjE. f_equal; fext=> i. exact: adjE.
  Qed.

  Lemma adjT : g ⊤ = ⊤.
  Proof. apply: top_eq. exact/adjP. Qed.

  Lemma adjM x y : g (x ∧ y) = (g x ∧ g y).
  Proof.
    apply: le_eq. exact: monoM.
    apply/adjP; focus; apply/adjP; by cauto.
  Qed.

  Lemma adjA I (F : I -> Y) : g (inf F) = ∀ i, g (F i).
  Proof.
    apply: le_eq. exact: monoA.
    apply/adjP; focus=> i; apply/adjP. exact: allE.
  Qed.

  Lemma adjAc I (P : I -> Prop) (F : I -> Y) :
    g (∀ i | P i, F i) = ∀ i | P i, g (F i).
  Proof.
    rewrite adjA. f_equal; fext=> i. exact: adjA.
  Qed.
End AdjunctionsCLat.

Section AdjunctionsFrame.
  Variable (X Y : frame) (f : X -> Y) (g : Y -> X).
  Context {H : is_adjunction f g}.

  Lemma adjH x y : g (x → y) ≤ g x → g y.
  Proof. apply: impI. by rewrite -adjM impEr. Qed.
End AdjunctionsFrame.

Definition is_closure {X : proType} (f : X -> X) := forall x y, (f x ≤ f y) <-> (x ≤ f y).
Existing Class is_closure.

Section ClosureOperatorsProType.
  Context {X : proType} (c : X -> X) {h : is_closure c}.

  Lemma closureP x y : (c x ≤ c y) <-> (x ≤ c y).
  Proof. exact: h. Qed.

  Lemma closure_inc x : x ≤ c x.
  Proof. by rewrite -closureP. Qed.

  Global Instance monotone_closure : monotone c.
  Proof. move=> x y le_x_y. rewrite closureP le_x_y. exact: closure_inc. Qed.
End ClosureOperatorsProType.

Section ClosureOperatorsOrdType.
  Context {X : ordType} (c : X -> X) {h : is_closure c}.

  Lemma closure_idem x : c (c x) = c x.
  Proof. apply: le_eq. by rewrite closureP. exact: closure_inc. Qed.

  Lemma closure_eq x y : x ≤ c y -> y ≤ c x -> c x = c y.
  Proof. move=> lxy lyx. apply: le_eq; by rewrite closureP. Qed.

  Lemma closure_stable x : c x ≤ x -> c x = x.
  Proof. move=> le_cx_x. apply: le_eq => //. exact: closure_inc. Qed.

  Lemma closure_lub T (f : T -> X) x y :
    is_lub (c \o f) x -> is_lub f y -> c x = c y.
  Proof.
    move=> lub1 lub2. apply: closure_eq.
    - rewrite lub1 => i /=. apply: mono. exact: ubP lub2.
    - rewrite lub2 => i. rewrite -closureP -[c x]closure_inc. exact: ubP lub1.
  Qed.

  Lemma closure_glb T (f : T -> X) x :
    is_glb (c \o f) x -> c x = x.
  Proof.
    move=> glb. apply: closure_stable. apply: glbP (glb) _ => i /=.
    rewrite closureP. exact: lbP glb.
  Qed.
End ClosureOperatorsOrdType.

Section ClosureCLat.
  Context {X : clat} (c : X -> X) {h : is_closure c}.

  Lemma closureT : c ⊤ = ⊤.
  Proof. apply: closure_stable. exact: topI. Qed.

  Lemma closureM x y : c (c x ∧ c y) = (c x ∧ c y).
  Proof.
    apply: closure_stable. focus; apply/closureP; cauto.
  Qed.

  Lemma closureJ x y : c (c x ∨ c y) = c (x ∨ y).
  Proof.
    apply: closure_lub (join_axiom x y). apply: mk_lub.
    case=> /=; by cauto. move=> z ub. focus.
    exact: (ub true). exact: (ub false).
  Qed.

  Lemma closureA I (F : I -> X) :
    c (∀ i, c (F i)) = ∀ i, c (F i).
  Proof.
    apply: closure_stable. focus=> i; apply/closureP; cauto.
  Qed.

  Lemma closureE I (F : I -> X) :
    c (∃ i, c (F i)) = c (∃ i, F i).
  Proof.
    apply: closure_lub (ex_axiom F) => x. split.
    - move=> le i /=. rewrite -le. exact: exI.
    - move=> le. focus=> i. exact: le.
  Qed.

  Lemma closureAc I (P : I -> Prop) (F : I -> X) :
    c (∀ i | P i, c (F i)) = ∀ i | P i, c (F i).
  Proof.
    apply: closure_stable. apply: allI => i. rewrite{2}/infguard -closureA.
    apply/closureP. rewrite closureA. focus=> pi. exact: allEc (i) pi _.
  Qed.

  Lemma closureEc I (P : I -> Prop) (F : I -> X) :
    c (∃ i | P i, c (F i)) = c (∃ i | P i, F i).
  Proof.
    rewrite -[c (∃ i | P i, F i)]closureE -closureE. repeat f_equal; fext=> i.
    exact: closureE.
  Qed.
End ClosureCLat.

Global Instance is_closure_unit {X Y : proType} (f : X -> Y) (g : Y -> X) {fP : is_adjunction f g} :
  is_closure (g \o f).
Proof.
  move=> x y /=. split=> [<-|e]. exact: adj_unit. apply: mono. by rewrite adjP.
Qed.

Definition is_kernel {X : proType} (f : X -> X) := forall x y, (f x ≤ f y) <-> (f x ≤ y).
Existing Class is_kernel.

(* Closure and kernel operators are dual concepts. *)
Lemma kernelP {X : proType} (c : X -> X) {h : is_kernel c} x y : (c x ≤ c y) <-> (c x ≤ y).
Proof. exact: h. Qed.

Instance is_kernel_closure_rev {X : proType} (c : X -> X) {h : is_closure c} :
  is_kernel (c : X^r -> X^r).
Proof. move=> x y. exact: (@closureP _ c). Qed.

Instance is_closure_kernel_rev {X : proType} (c : X -> X) {h : is_kernel c} :
  is_closure (c : X^r -> X^r).
Proof. move=> x y. exact: (@kernelP _ c). Qed.

Section KernelOperators.
  Context {X : proType} (c : X -> X) {h : is_kernel c}.
  Implicit Types (x y z : X).
  Let Xr := [proType of X^r].

  Lemma kernel_dec x : c x ≤ x.
  Proof. exact: (@closure_inc Xr). Qed.

  Global Instance monotone_kernel : monotone c.
  Proof. move=> x y. exact: (@monotone_closure Xr). Qed.
End KernelOperators.

Section KernelOperationsOrder.
  Context {X : ordType} (c : X -> X) {h : is_kernel c}.
  Implicit Types (x y z : X).
  Let Xr := [ordType of X^r].

  Lemma kernel_idem x : c (c x) = c x.
  Proof. exact: (@closure_idem Xr). Qed.

  Lemma kernel_eq x y : c x ≤ y -> c y ≤ x -> c x = c y.
  Proof. move=> h1 h2. exact: (@closure_eq Xr). Qed.

  Lemma kernel_stable x : x ≤ c x -> c x = x.
  Proof. exact: (@closure_stable Xr). Qed.

  Lemma kernel_glb I (f : I -> X) x y :
    is_glb (c \o f) x -> is_glb f y -> c x = c y.
  Proof. exact: (@closure_lub Xr). Qed.

  Lemma kernel_lub I (f : I -> X) x :
    is_lub (c \o f) x -> c x = x.
  Proof. exact: (@closure_glb Xr). Qed.
End KernelOperationsOrder.

Instance is_kernel_counit {X Y : proType} (f : X -> Y) (g : Y -> X) {fP : is_adjunction f g} :
  is_kernel (f \o g).
Proof. move=> x y. exact: (@is_closure_unit [proType of Y^r] [proType of X^r]). Qed.