Theory Quantic_Nuclei_Conuclei

(* Title: Quantic Nuclei and Conuclei
   Author: Georg Struth
   Maintainer: Georg Struth <g.struth@sheffield.ac.uk> 
*)

section ‹Quantic Nuclei and Conuclei›

theory Quantic_Nuclei_Conuclei
  imports Quantale_Models 

begin

text ‹Quantic nuclei and conuclei are an important part of the structure theory of quantales. I formalise
the basics, following Rosenthal's book~\<^cite>‹"Rosenthal90"›. In the structure theorems, I collect all parts 
of the proof, but do not present the theorems in compact form due to difficulties to speak about subalgebras 
and homomorphic images without explicit carrier sets. Nuclei also arise in the context of complete Heyting algebras,
frames and locales~\<^cite>‹"Johnstone82"›. Their formalisation seems an interesting future task.›

subsection ‹Nuclei›

definition nucleus :: "('a::quantale ⇒ 'a::quantale) ⇒ bool" where 
  "nucleus f = (clop f ∧ (∀x y. f x ⋅ f y ≤ f (x ⋅ y)))"

lemma nuc_lax: "nucleus f ⟹ f x ⋅ f y ≤ f (x ⋅ y)"
  by (simp add: nucleus_def)   

definition unucleus :: "('a::unital_quantale ⇒ 'a::unital_quantale) ⇒ bool" where 
  "unucleus f = (nucleus f ∧ 1 ≤ f 1)"

lemma "nucleus f ⟹ f ⊥ = ⊥" (*nitpick*)
  oops

lemma "conucleus f ⟹ f ⊤ = ⊤" (*nitpick*)
  oops

lemma nuc_prop1: "nucleus f ⟹ f (x ⋅ y) = f (x ⋅ f y)"
  apply (rule antisym)
   apply (simp add: clop_extensive_var clop_iso_var nucleus_def psrpq.mult_isol)
  by (metis clop_alt clop_extensive_var dual_order.trans nucleus_def psrpq.mult_isol_var)

lemma nuc_prop2: "nucleus f ⟹ f (x ⋅ y) = f (f x ⋅ y)"
  apply (rule antisym)
  apply (simp add: clop_extensive_var clop_iso_var nsrnq.mult_isor nucleus_def)
  by (metis (mono_tags, opaque_lifting) clop_alt nuc_prop1 nucleus_def)

lemma nuc_comp_prop: "nucleus f ⟹  f (f x ⋅ f y) = f (x ⋅ y)"
  using nuc_prop1 nuc_prop2 by force

lemma nucleus_alt_def1: "nucleus f ⟹ f x → f y = x → f y"
proof (rule antisym)
  assume h: "nucleus f" 
  hence "x ≤ f x"
    by (simp add: clop_def nucleus_def clop_extensive_var)
  thus "f x → f y ≤ x → f y"
    by (simp add: bres_anti)
  have "f x ⋅ (x → f y) ≤ f x ⋅ f (x → f y)"
    using clop_extensive_var h nucleus_def proto_pre_quantale_class.mult_isol by blast
  also have "... ≤ f (x ⋅ (x → f y))"
    by (simp add: h nuc_lax)
  also have "... ≤ f (f y)"
    using h by (simp add: bres_canc1 nucleus_def clop_iso_var) 
  finally have "f x ⋅ (x → f y) ≤ f y"
    using h by (metis clop_alt dual_order.trans nucleus_def order_refl)
  thus "x → f y ≤ f x → f y"
    by (simp add: bres_galois_imp)
qed

lemma nucleus_alt_def2: "nucleus f ⟹ f y ← f x = f y ← x"
proof (rule antisym)
  assume h: "nucleus f" 
  hence "x ≤ f x"
    by (simp add: clop_extensive_var nucleus_def)
  thus "f y ← f x ≤ f y ← x"
    by (simp add: fres_anti)
  have "(f y ← x) ⋅ f x ≤ f (f y ← x) ⋅ f x"
    using clop_extensive_var h nsrnq.mult_isor nucleus_def by blast
  also have "... ≤ f ((f y ← x) ⋅ x)"
    by (simp add: h nuc_lax)
  also have "... ≤ f (f y)"
    using clop_iso_var fres_canc1 h nucleus_def by blast
  finally have "(f y ← x) ⋅ f x ≤ f y"
    using h by (metis clop_alt dual_order.trans nucleus_def order_refl)
  thus "f y ← x ≤ f y ← f x"
    by (simp add: fres_galois)
qed

lemma nucleus_alt_def3: 
  fixes f :: "'a::unital_quantale ⇒ 'a"
  shows "∀x y. f x → f y = x → f y ⟹ ∀x y. f y ← f x = f y ← x ⟹ nucleus f"
proof-
  assume h1: "∀x y. f x → f y = x → f y"
  and h2: "∀x y. f y ← f x = f y ← x"
  hence ext: "∀x. x ≤ f x"
    by (metis (full_types) fres_galois fres_one mult.left_neutral)
  have iso: "∀x y. x ≤ y ⟶ f x ≤ f y"
    by (metis (full_types) bres_galois dual_order.trans h1 ext nsrnqo.mult_oner)
  have trans: "∀x. f (f x) ≤ f x"
    by (metis fres_canc2 fres_galois h2 nsrnqo.mult_onel)
  have lax: "∀x y. f x ⋅ f y ≤ f (x ⋅ y)"
    by (metis h1 h2 bres_galois ext fres_galois)
  show ?thesis
    by (simp add: clop_def iso lax le_funI ext trans monoI nucleus_def)
qed

lemma nucleus_alt_def: 
  fixes f :: "'a::unital_quantale ⇒ 'a"
  shows "nucleus f = (∀ x y. f x → f y = x → f y ∧ f y ← f x = f y ← x)"
  using nucleus_alt_def1 nucleus_alt_def2 nucleus_alt_def3 by blast

lemma nucleus_alt_def_cor1: "nucleus f ⟹ f (x → y) ≤ x → f y"
  by (metis bres_galois bres_iso clop_extensive_var fres_galois nucleus_alt_def2 nucleus_def)

lemma nucleus_alt_def_cor2: "nucleus f ⟹ f (y ← x) ≤ f y ← x"
  by (metis bres_galois clop_extensive_var fres_galois fres_iso nucleus_alt_def1 nucleus_def)

lemma nucleus_ab_unital: 
  fixes f :: "'a::ab_unital_quantale ⇒ 'a"
  shows "nucleus f = (∀x y. f x → f y = x → f y)"
  by (simp add: bres_fres_eq nucleus_alt_def)

lemma nuc_comp_assoc: "nucleus f ⟹ f (x ⋅ f (y ⋅ z)) = f (f (x ⋅ y) ⋅ z)"
  by (metis mult.assoc nuc_prop1 nuc_prop2)

lemma nuc_Sup_closed: "nucleus f ⟹ f ∘ Sup ∘ (`) f = (f ∘ Sup)"
  apply (simp add: nucleus_def fun_eq_iff, safe, rule antisym)
  apply (meson SUP_least Sup_upper clop_alt clop_def monoD)
  by (simp add: SUP_upper2 Sup_le_iff clop_extensive_var clop_iso_var)

lemma nuc_Sup_closed_var: "nucleus f ⟹ f (⨆x ∈ X. f x) = f (⨆X)"
  by (metis nuc_Sup_closed o_apply)

lemma nuc_Inf_closed: "nucleus f ⟹ Sup_closed_set (Fix f)" (* nitpick *)
  oops

lemma nuc_Inf_closed: "nucleus f ⟹ Inf_closed_set (Fix f)"   
  by (simp add: clop_Inf_closed nucleus_def)

lemma nuc_comp_distl: "nucleus f ⟹ f (x ⋅ f (⨆Y)) = f (⨆y ∈ Y. f (x ⋅ y))"
  by (metis Sup_distl image_image nuc_Sup_closed_var nuc_prop1)

lemma nuc_comp_distr: "nucleus f ⟹ f (f (⨆X) ⋅ y) = f (⨆x ∈ X. f (x ⋅ y))"
  by (metis image_image Sup_distr nuc_Sup_closed_var nuc_prop2)

lemma "nucleus f ⟹ f (x ⋅ y) = f x ⋅ f y" (*nitpick*)
  oops

lemma nuc_bres_closed: "nucleus f ⟹ f (f x → f y) = f x → f y"
  unfolding nucleus_def apply clarsimp
  by (smt clop_closure clop_extensive_var nucleus_alt_def_cor1 nucleus_def order_class.order.antisym rangeI)

lemma "nucleus f ⟹ f (x → y) = f x → f y" (*nitpick*)
  oops

lemma nuc_fres_closed: "nucleus f ⟹ f (f x ← f y) = f x ← f y"
  unfolding nucleus_def apply clarsimp
  by (smt clop_closure clop_extensive_var eq_iff nucleus_alt_def_cor2 nucleus_def rangeI)

lemma nuc_fres_closed: "nucleus f ⟹ f (x ← y) = f x ← f y" (*nitpick*)
  oops

lemma nuc_inf_closed: "nucleus f ⟹ inf_closed_set (Fix f)"
  by (simp add: Inf_inf_closed nuc_Inf_closed)

lemma nuc_inf_closed_var: "nucleus f ⟹ f (f x ⊓ f y) = f x ⊓ f y"
  by (smt antisym_conv clop_alt clop_extensive_var inf_le2 inf_sup_ord(1) le_inf_iff nucleus_def)

text ‹Taken together these facts show that, for $f:Q\to Q$, $f[Q]$ forms a quantale with 
composition $f\, (-\cdot -)$ and sup $f\, (\bigsqcup -)$, and that $f:Q\to f[Q]$ is a quantale morphism. 
This is the first part of Theorem 3.1.1 in Rosenthal's book.›

class quantale_with_nuc = quantale + cl_op +
  assumes cl_op_nuc: "cl_op x ⋅ cl_op y ≤ cl_op (x ⋅ y)"

begin

subclass clattice_with_clop..

end

class unital_quantale_with_nuc = quantale_with_nuc + unital_quantale +
  assumes one_nuc: "1 ≤ cl_op 1"

lemma nucleus_cl_op: "nucleus (cl_op::'a::quantale_with_nuc ⇒ 'a)"
  by (simp add: cl_op_class.clop_iso cl_op_nuc  clop_def clop_ext le_funI monoI nucleus_def)

lemma unucleus_cl_op: "unucleus (cl_op::'a::unital_quantale_with_nuc ⇒ 'a)"
  by (simp add: nucleus_cl_op one_nuc unucleus_def)

instantiation cl_op_im :: (quantale_with_nuc) quantale
begin

lift_definition times_cl_op_im :: "'a::quantale_with_nuc cl_op_im ⇒ 'a cl_op_im ⇒ 'a cl_op_im" is "λx y. cl_op (x ⋅ y)"
  by simp

instance
  by (intro_classes; transfer, auto simp: nuc_comp_assoc nuc_comp_distr nucleus_cl_op nuc_comp_distl)

end

instantiation cl_op_im :: (unital_quantale_with_nuc) unital_quantale
begin

lift_definition one_cl_op_im :: "'a::unital_quantale_with_nuc cl_op_im" is "cl_op 1"
  by simp

instance
  by (intro_classes; transfer) (metis clop_closure nsrnqo.mult_onel nuc_prop2 nucleus_cl_op nucleus_def nsrnqo.mult_oner nuc_prop1)+

end


text ‹The usefulness of these theorems remains unclear; it seems difficult to make them collaborate with concrete nuclei.›

lemma nuc_hom: "Abs_cl_op_im ∘ cl_op ∈ quantale_homset"
  unfolding quantale_homset_iff comp_def fun_eq_iff
  apply safe
  apply (metis (no_types, lifting) Abs_cl_op_im_inverse Rep_cl_op_im_inverse nuc_comp_prop nucleus_cl_op rangeI times_cl_op_im.rep_eq)
  unfolding Sup_cl_op_im_def by (smt Abs_cl_op_im_inverse SUP_cong image_image map_fun_apply nuc_Sup_closed_var nucleus_cl_op rangeI)

text ‹This finishes the first statement of Theorem 3.1.1. The second part follows. It states that for every 
surjective quantale homomorphism there is a nucleus such that the range of the nucleus is isomorphic to the range of the surjection.› 
 
lemma quant_morph_nuc:
  fixes f :: "'a::quantale_with_dual ⇒ 'b::quantale_with_dual"
  assumes "f ∈ quantale_homset" 
  shows "nucleus ((radj f) ∘ f)"
proof-
  let ?φ = "(radj f) ∘ f"
  have adj: "f ⊣ (radj f)"
    by (simp add: assms quantale_hom_radj)
  hence a: "clop ?φ"
    by (simp add: clop_adj)
  {fix x y
    have "f (?φ x ⋅ ?φ y) = (f ∘ ?φ) x ⋅ (f ∘ ?φ) y"
      by (metis assms comp_eq_dest_lhs quantale_homset_iff)
  also have "... = f x ⋅ f y"
    by (simp add: adj adj_cancel_eq1 fun.map_comp)
  also have "... = f (x ⋅ y)"
    by (metis assms quantale_homset_iff)
  finally have "?φ x ⋅ ?φ y ≤ ?φ (x ⋅ y)"
    by (metis adj adj_def comp_apply order_refl)}
  thus ?thesis
    by (simp add: a nucleus_def)
qed 

lemma surj_quantale_hom_bij_on: 
  fixes f :: "'a::quantale_with_dual ⇒ 'b::quantale_with_dual"
  assumes "surj f"
  and "f ∈ quantale_homset"
  shows "bij_betw f (range (radj f ∘ f)) UNIV"
  using assms quantale_homset_iff surj_Sup_pres_bij_on by blast

text ‹This establishes the bijection, extending a similar fact about closure operators and complete lattices (surj-Sup-pres-bij). 
It remains to show that $f$ is a quantale morphism, that is, it preserves Sups and compositions of closed elements with operations 
defined as in the previous instantiation statement. Sup-preservation holds already for closure operators on complete lattices (surj-Sup-pres-iso).
Hence it remains to prove preservation of compositions.›

lemma surj_comp_pres_iso: 
  fixes f :: "'a::quantale_with_dual ⇒ 'b::quantale_with_dual"
  assumes "f ∈ quantale_homset"
  shows "f ((radj f ∘ f) (x ⋅ y)) = f x ⋅ f y"
proof-
  have "f ⊣ (radj f)"
    by (simp add: assms quantale_hom_radj)
  hence "f ((radj f ∘ f) (x ⋅ y)) = f (x ⋅ y)"
    by (metis adj_cancel_eq1 comp_eq_dest_lhs) 
  thus ?thesis
    using assms quantale_homset_iff by auto
qed

text ‹This establishes the quantale isomorphism and finishes the proof of Theorem 3.1.1.›

text ‹Next I prove Theorem 3.1.2 in Rosenthal's book. nuc-Inf-closed shows that $\mathit{Fix}\, f$ is Inf-closed. Hence the two following 
lemmas show one direction.›

lemma nuc_bres_pres: "nucleus f ⟹ y ∈ Fix f ⟹ x → y ∈ Fix f"
proof -
  assume a1: "nucleus f"
  assume a2: "y ∈ Fix f"
  have "clop f"
    using a1 by (simp add: nucleus_def)
  thus ?thesis
    using a2 a1
    by (metis clop_Fix_range clop_closure clop_extensive_var dual_order.antisym nucleus_alt_def_cor1) 
qed

lemma nuc_fres_pres: "nucleus f ⟹ y ∈ Fix f ⟹ y ← x ∈ Fix f"
proof -
  assume a1: "nucleus f"
  assume a2: "y ∈ Fix f"
  have "clop f"
    using a1 by (simp add: nucleus_def)
  thus ?thesis
    using a2 a1 by (metis antisym_conv clop_Fix_range clop_closure clop_extensive_var nucleus_alt_def_cor2) 
qed

lemma lax_aux: 
  fixes X :: "'a::quantale set"
  assumes "∀x.∀y ∈ X. x → y ∈ X"
  and "∀x. ∀y ∈ X. y ← x ∈ X"
shows "⨅{z ∈ X. x ≤ z} ⋅ ⨅{z ∈ X. y ≤ z} ≤ ⨅{z ∈ X. x ⋅ y ≤ z}"
proof-
  let ?φ = "λx. ⨅{w ∈ X. x ≤ w}"
  {fix z
  assume a: "x ⋅ y ≤ z"
  and b: "z ∈ X"
  hence c: "x ≤ z ← y"
    by (simp add: fres_galois)
  hence "z ← y ∈ X"
    by (simp add: assms(2) b)
  hence "?φ x ≤ z ← y"
    by (simp add: Inf_lower c)
  hence d: "y ≤ ?φ x → z"
    by (simp add: bres_galois_imp fres_galois)
  hence "?φ x  → z ∈ X"
    by (simp add: assms(1) b)
  hence "?φ x ⋅ ?φ y ≤ z"
    by (simp add: Inf_lower d bres_galois)}
  thus ?thesis
    by (simp add: le_Inf_iff)
qed

lemma Inf_closed_res_nuc: 
  fixes X :: "'a::quantale set"
  assumes "Inf_closed_set X"
  and  "∀x. ∀y ∈ X. x → y ∈ X"
  and "∀x. ∀y ∈ X. y ← x ∈ X"
  shows "nucleus (λy. ⨅{x ∈ X. y ≤ x})"
  unfolding nucleus_def by (simp add: Inf_closed_clop assms lax_aux)

lemma Inf_closed_res_Fix: 
  fixes X :: "'a::quantale set"
  assumes "Inf_closed_set X"
  and  "∀x. ∀y ∈ X. x → y ∈ X"
  and "∀x. ∀y ∈ X. y ← x ∈ X"
shows "X = Fix (λy. ⨅{x ∈ X. y ≤ x})"
  unfolding Fix_def
  apply safe
   apply (rule antisym, simp_all add: Inf_lower le_Inf_iff) 
  by (metis (no_types, lifting) Inf_closed_set_def assms(1) mem_Collect_eq subsetI)

text ‹This finishes the proof of Theorem 3.1.2›


subsection ‹A Representation Theorem›

text ‹The final proofs for nuclei lead to Rosenthal's representation theorem for quantales (Theorem 3.1.2).›

lemma down_set_lax_morph: "(↓ ∘ Sup) (X::'a::quantale set) ⋅ (↓ ∘ Sup) Y ⊆ (↓ ∘ Sup) (X ⋅ Y)"
proof-
  have "⨆((↓ ∘ Sup) X ⋅ (↓ ∘ Sup) Y) = ⨆(X ⋅ Y)"
    by (smt Sup_downset_adj adj_cancel_eq1 comp_apply comp_dist_mix)
  thus ?thesis
    by (simp add: Sup_downset_adj_var eq_iff)
qed

lemma downset_Sup_nuc: "nucleus (↓ ∘ (Sup::'a::quantale set ⇒ 'a))"
  using Sup_downset_adj clop_adj down_set_lax_morph nucleus_def by blast

lemma downset_surj: "surj_on ↓ (range (↓ ∘ Sup))"
  using surj_on_def by fastforce

text ‹In addition, $\downarrow$ is injective by Lemma downset-inj. Hence it is a bijection between the quantale and the powerset quantale. 
It remains to show that $\downarrow$ is a quantale morphism.›

lemma downset_Sup_pres_var: "↓ (⨆X) = (↓ ∘ Sup) (⇓ (X::'a::quantale set))"
  unfolding comp_def downset_prop downset_set_def 
  apply safe
  apply (smt Sup_subset_mono dual_order.refl mem_Collect_eq order_subst1 subset_iff)
  by (smt Sup_mono le_iff_inf le_infI2 mem_Collect_eq)

lemma downset_Sup_pres: "↓ (⨆X) = (↓ ∘ Sup) (⋃ (↓ ` (X::'a::quantale set)))"
  by (metis downset_Sup_pres_var downset_set_prop_var)  

lemma downset_comp_pres: "↓ ((x::'a::quantale) ⋅ y) = (↓ ∘ Sup) (↓x ⋅ ↓y)"
  by (metis (no_types, opaque_lifting) Sup_downset_adj_var comp_apply comp_dist_mix downset_iso_iff dual_order.antisym order_refl)

text ‹This finishes the proof of Theorem 3.1.2.›
 

subsection ‹Conuclei›

definition conucleus :: "('a::quantale ⇒ 'a::quantale) ⇒ bool" where
  "conucleus f = (coclop f ∧ (∀x y. f x ⋅ f y ≤ f (x ⋅ y)))"

lemma conuc_lax: "conucleus f ⟹ f x ⋅ f y ≤ f (x ⋅ y)"
  by (simp add: conucleus_def)

definition uconucleus :: "('a::unital_quantale ⇒ 'a::unital_quantale) ⇒ bool" where 
  "uconucleus f = (conucleus f ∧ f 1 ≤ 1)"

text ‹Next I prove Theorem 3.1.3.› 

lemma conuc_Sup_closed: "conucleus f ⟹ f ∘ Sup ∘ (`) f = Sup ∘ (`) f" 
  unfolding conucleus_def fun_eq_iff comp_def
  by (smt coclop_coextensive_var coclop_idem coclop_iso image_comp image_image le_iff_sup mono_SUP sup.orderE)

lemma conuc_comp_closed: "conucleus f ⟹ f (f x ⋅ f y) = f x ⋅ f y"
  unfolding conucleus_def by (metis antisym_conv coclop_coextensive_var coclop_idem_var)

text ‹The sets of fixpoints of conuclei are closed under Sups and composition; hence they form subquantales.›

lemma conuc_Sup_qclosed: "conucleus f ⟹ Sup_closed_set (Fix f) ∧ comp_closed_set (Fix f)"
  apply safe
   apply (simp add: coclop_Sup_closed conucleus_def)
  unfolding conucleus_def comp_closed_set_def by (metis coclop_coclosure coclop_coclosure_set coclop_coextensive_var dual_order.antisym)

text ‹This shows that the subset $\mathit{Fix} f$ of a quantale, for conucleus $f$, is closed under Sups and composition. 
It is therefore a subquantale. $f:f[Q]\to Q$ is an embedding. As before, this could be shown by formalising a type class of quantales with a conucleus operation,
converting the range of the conucleus into a type and providing a sublocale proof. First, this would require showing that the coclosed 
elements of a complete lattice form a complete sublattice. Relative to the proofs for closure operators and nuclei there is nothing to 
be learned. I provide this proof in the section on left-sided elements, where the conucleus can be expressed within the language of quantales.›

text ‹The second part of Theorem 3.1.3 states that every subquantale of a given quantale is equal to $\mathit{Fix} f$ for some conucleus $f$.›

lemma lax_aux2: 
  fixes X :: "'a::quantale set"
  assumes "Sup_closed_set X"
  and "comp_closed_set X"
  shows "⨆{z ∈ X. z ≤ x} ⋅ ⨆{z ∈ X. z ≤ y} ≤ ⨆{z ∈ X. z ≤ x ⋅ y}"
proof-
  let ?φ = "λx. ⨆{z ∈ X. z ≤ x}"
  have "?φ x ⋅ ?φ y = ⨆{⨆{v ⋅ w |v. v ∈ X ∧ v ≤ x} |w. w ∈ X ∧ w ≤ y}"
    by (simp add: Sup_distr Sup_distl setcompr_eq_image)
  also have "... = ⨆{v ⋅ w |v w. v ∈ X ∧ v ≤ x ∧ w ∈ X ∧ w ≤ y}"
    apply (rule antisym)
    apply (rule Sup_least, clarsimp, smt Collect_mono_iff Sup_subset_mono)
    by (rule Sup_least, clarsimp, smt Sup_upper2 eq_iff mem_Collect_eq)
  also have "... ≤ ?φ (x ⋅ y)"
    by (smt Collect_mono_iff Sup_subset_mono assms(2) comp_closed_set_def psrpq.mult_isol_var)
  finally show ?thesis
    by force
qed

lemma subquantale_conucleus: 
  fixes X :: "'a::quantale set"
  assumes "Sup_closed_set X"
  and "comp_closed_set X"
  shows "conucleus (λx. ⨆{y ∈ X. y ≤ x})" 
  unfolding conucleus_def by (safe, simp_all add: Sup_closed_coclop assms(1) assms(2) lax_aux2)

lemma subquantale_Fix: 
  fixes X :: "'a::quantale set"
  assumes "Sup_closed_set X"
  and "comp_closed_set X"
  shows "X = Fix (λx. ⨆{y ∈ X. y ≤ x})"
  unfolding Fix_def
  apply safe
  apply (metis (mono_tags, lifting) Sup_least Sup_upper antisym mem_Collect_eq order_refl)
  by (metis (no_types, lifting) Sup_closed_set_def assms(1) mem_Collect_eq subsetI)

text ‹This finishes the proof of Theorem 3.1.3›

end