Theory Quantale_Modules
section ‹Quantale Modules and Semidirect Products›
theory Quantale_Modules
imports Quantale_Star
begin
subsection ‹Quantale Modules›
text ‹Quantale modules are extensions of semigroup actions in that a quantale acts on a complete lattice.
These have been investigated by Abramsky and Vickers~\<^cite>‹"AbramskyV93"› and others, predominantly in the context
of pointfree topology.›
locale unital_quantale_module =
fixes act :: "'a::unital_quantale ⇒ 'b::complete_lattice_with_dual ⇒ 'b" (‹α›)
assumes act1: "α (x ⋅ y) p = α x (α y p)"
and act2 [simp]: "α 1 p = p"
and act3: "α (⨆X) p = (⨆x ∈ X. α x p)"
and act4: "α x (⨆P) = (⨆p ∈ P. α x p)"
context unital_quantale_module
begin
text ‹Actions are morphisms. The curried notation is particularly convenient for this.›
lemma act_morph1: "α (x ⋅ y) = (α x) ∘ (α y)"
by (simp add: fun_eq_iff act1)
lemma act_morph2 [simp]: "α 1 = id"
by (simp add: fun_eq_iff)
lemma emp_act [simp]: "α (⨆{}) p = ⊥"
by (simp only: act3, force)
lemma emp_act_var [simp]: "α ⊥ p = ⊥"
using emp_act by auto
lemma act_emp [simp]: "α x (⨆{}) = ⊥"
by (simp only: act4, force)
lemma act_emp_var [simp]: "α x ⊥ = ⊥"
using act_emp by auto
lemma act_sup_distl: "α x (p ⊔ q) = (α x p) ⊔ (α x q)"
by (metis (mono_tags, lifting) act4 image_insert image_is_empty sup_Sup)
lemma act_sup_distr: "α (x ⊔ y) p = (α x p) ⊔ (α y p)"
by (metis (no_types, lifting) SUP_insert Sup_empty Sup_insert act3 sup_bot_right)
lemma act_sup_distr_var: "α (x ⊔ y) = (α x) ⊔ (α y)"
by (simp add: fun_eq_iff act_sup_distr)
subsection ‹Semidirect Products and Weak Quantales›
text ‹Next, the semidirect product of a unital quantale and a complete lattice is defined. ›
definition "sd_prod x y = (fst x ⋅ fst y, snd x ⊔ α (fst x) (snd y))"
lemma sd_distr: "sd_prod (Sup_prod X) y = Sup_prod {sd_prod x y |x. x ∈ X}"
proof -
have "sd_prod (Sup_prod X) y = sd_prod ((⨆x ∈ X. fst x), (⨆x ∈ X. snd x)) y"
by (simp add: Sup_prod_def)
also have "... = ((⨆x ∈ X. fst x) ⋅ fst y, (⨆x ∈ X. snd x) ⊔ (α (⨆x ∈ X. fst x) (snd y)))"
by (simp add: sd_prod_def)
also have "... = ((⨆x ∈ X. (fst x ⋅ fst y)), (⨆x ∈ X. snd x) ⊔ (α (⨆x ∈ X. fst x) (snd y)))"
by (simp add: Sup_distr image_comp)
also have "... = ((⨆x ∈ X. (fst x ⋅ fst y)), (⨆x ∈ X. snd x) ⊔ (⨆x ∈ X. (α (fst x) (snd y))))"
by (simp add: act3 image_comp)
also have "... = ((⨆x ∈ X. (fst x ⋅ fst y)), (⨆x ∈ X. (snd x ⊔ (α (fst x) (snd y)))))"
using complete_lattice_class.SUP_sup_distrib by fastforce
also have "... = Sup_prod {(fst x ⋅ fst y, snd x ⊔ (α (fst x) (snd y))) |x. x ∈ X}"
apply (unfold Sup_prod_def, safe)
by ( simp add: SUP_Sup_eq, rule_tac f=Sup in arg_cong, force)+
finally show ?thesis
by (simp add: sd_prod_def)
qed
lemma sd_distl_aux: "Y ≠ {} ⟹ p ⊔ (⨆y ∈ Y. α x (snd y)) = (⨆y ∈ Y. p ⊔ α x (snd y))"
apply (rule antisym)
apply (rule sup_least, metis SUP_bot_conv(2) SUP_const SUP_upper2 sup_ge1)
apply (rule Sup_least, force simp: SUP_upper2 image_iff)
by (rule Sup_least, safe, metis Sup_upper image_iff sup.idem sup.mono sup_ge2)
lemma sd_distl: "Y ≠ {} ⟹ sd_prod x (Sup_prod Y) = Sup_prod {sd_prod x y |y. y ∈ Y}"
proof -
assume a: "Y ≠ {}"
have "sd_prod x (Sup_prod Y) = sd_prod x ((⨆y ∈ Y. fst y), (⨆y ∈ Y. snd y))"
by (simp add: Sup_prod_def)
also have "... = ((fst x) ⋅ (⨆y ∈ Y. fst y), (snd x ⊔ (α (fst x) (⨆y ∈ Y. snd y))))"
by (simp add: sd_prod_def)
also have "... = ((⨆y ∈ Y. fst x ⋅ fst y), (snd x ⊔ (α (fst x) (⨆y ∈ Y. snd y))))"
by (simp add: Sup_distl image_comp)
also have "... = ((⨆y ∈ Y. fst x ⋅ fst y), (snd x ⊔ (⨆y ∈ Y. α (fst x) (snd y))))"
by (simp add: act4 image_comp)
also have "... = ((⨆y ∈ Y. fst x ⋅ fst y), (⨆y ∈ Y. snd x ⊔ (α (fst x) (snd y))))"
using a sd_distl_aux by blast
also have "... = Sup_prod {(fst x ⋅ fst y, snd x ⊔ (α (fst x) (snd y))) |y. y ∈ Y}"
apply (unfold Sup_prod_def, safe)
by ( simp add: SUP_Sup_eq, rule_tac f=Sup in arg_cong, force)+
finally show ?thesis
by (simp add: sd_prod_def)
qed
definition "sd_unit = (1,⊥)"
lemma sd_unitl [simp]: "sd_prod sd_unit x = x"
by (simp add: sd_prod_def sd_unit_def)
lemma sd_unitr [simp]: "sd_prod x sd_unit = x"
by (simp add: sd_prod_def sd_unit_def)
text ‹The following counterexamples rule out that semidirect products of quantales and complete lattices form quantales.
The reason is that the right annihilation law fails.›
lemma "sd_prod x (Sup_prod Y) = Sup_prod {sd_prod x y |y. y ∈ Y}"
oops
lemma "sd_prod x bot_prod = bot_prod"
oops
text ‹However one can show that semidirect products of (unital) quantales with complete lattices form weak (unital) quantales.
This provides an example of how weak quantales arise quite naturally.›
sublocale dp_quantale: weak_quantale sd_prod Inf_prod Sup_prod inf_prod less_eq_prod less_prod sup_prod bot_prod top_prod
apply unfold_locales
apply (simp add: act1 act_sup_distl mult.assoc sd_prod_def sup_assoc)
apply (metis Setcompr_eq_image sd_distr)
by (metis Setcompr_eq_image sd_distl)
sublocale dpu_quantale: unital_weak_quantale sd_unit sd_prod Inf_prod Sup_prod inf_prod less_eq_prod less_prod sup_prod bot_prod top_prod
by unfold_locales simp_all
subsection ‹The Star in Semidirect Products›
text ‹I define the star operation for a semidirect product of a quantale and a complete lattice,
and prove a characteristic property.›
abbreviation "sd_power ≡ dpu_quantale.power"
abbreviation "sd_star ≡ dpu_quantale.qstar"
lemma sd_power_zero [simp]: "sd_power x 0 = (1,⊥)"
using sd_unit_def by simp
lemma sd_power_prop_aux: "α (x ^ 0) y ⊔ (⨆{α (x ^ k) y |k. 0 < k ∧ k ≤ Suc i}) = ⨆{α (x ^ k) y |k. k ≤ Suc i}"
apply (rule antisym)
apply (rule sup_least, intro Sup_upper, blast, intro Sup_mono, blast)
apply (rule Sup_least, safe)
by (metis (mono_tags, lifting) Sup_insert Sup_upper insert_iff le_0_eq linorder_not_le mem_Collect_eq)
lemma sd_power_prop1 [simp]: "sd_power (x,y) (Suc i) = (x ^ (Suc i), ⨆{α (x ^ k) y|k. k ≤ i})"
proof (induct i)
case 0 thus ?case
by auto
next
case (Suc i) thus ?case
proof-
assume "sd_power (x,y) (Suc i) = (x ^ Suc i, ⨆{α (x ^ k) y |k. k ≤ i})"
hence "sd_power (x,y) (Suc (Suc i)) = (x ^ Suc (Suc i), α (x ^ 0) y ⊔ (⨆{α (x ^ (Suc k)) y |k. k ≤ i}))"
apply (simp add: sd_prod_def act1 act4)
apply safe
by (metis act4 image_Collect image_image)
also have "... = (x ^ Suc (Suc i), α (x ^ 0) y ⊔ (⨆{α (x ^ k) y |k. 0 < k ∧ k ≤ Suc i}))"
by (metis (no_types, opaque_lifting) Suc_le_eq Suc_le_mono le_0_eq not0_implies_Suc zero_less_Suc)
finally show ?thesis
using sd_power_prop_aux by simp
qed
qed
lemma sd_power_prop2 [simp]: "sd_power (x,y) i = (x ^ i, ⨆{α (x ^ k) y|k. k < i})"
apply (case_tac i)
using sd_unit_def apply force
using le_simps(2) unital_quantale_module.sd_power_prop1 unital_quantale_module_axioms by fastforce
lemma sdstar_prop: "sd_star (x,y) = (qstar x, α (qstar x) y)"
proof -
have "sd_star (x,y) = sup_prod (1,⊥) (Sup_prod {sd_power (x,y) (Suc i) |i. True})"
by (metis dpu_quantale.Sup_iter_unfold dpu_quantale.qstar_def full_SetCompr_eq sd_power_zero)
also have "... = sup_prod (1,⊥) (Sup_prod {(x^(Suc i), ⨆{α (x ^ k) y|k. k ≤ i}) |i. True})"
using sd_power_prop1 by auto
also have "... = (1 ⊔( ⨆i. x ^ (Suc i)), (⨆i. ⨆{α (x ^ k) y|k. k ≤ i}))"
apply (unfold sup_prod_def Sup_prod_def, safe)
apply (simp, rule_tac f="λx. 1 ⊔ x" in arg_cong)
by (simp add: SUP_Sup_eq, rule_tac f=Sup in arg_cong, force)+
also have "... = (qstar x, (⨆i. ⨆{α (x ^ k) y|k. k ≤ i}))"
by (safe, metis (no_types) fSup_unfold power_0 qstar_def)
also have "... = (qstar x, (⨆i. α (x ^ i) y))"
apply safe
apply (rule antisym)
apply (safe intro!: Sup_least, simp add: Sup_upper)
by (metis (mono_tags, lifting) SUP_upper2 Sup_upper mem_Collect_eq order_refl)
finally show ?thesis
by (simp add: qstar_def act3 image_comp)
qed
end
end