Email Gateway (Aug 22 2022 at 13:06): Email Gateway (Aug 22 2022 at 13:06):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Is it possible, in HOL, to prove that for any I-indexed collection of sets
{F i: i ∈ I} there exists a set S that embeds (via injective maps) all of
the sets F i and furthermore is weakly universal for this property, so that
if S' is any other set that embeds all the F i then S' embeds S?
In more detail, I am thinking of something like the following:
definition embeds
where "embeds A B ≡ ∃f. f ∈ B → A ∧ inj_on f B"
lemma "∀F. ∃S. (∀x. embeds S (F x)) ∧ (∀S'. (∀x. embeds S' (F x)) ⟶ embeds S' S)"
In ZFC I suppose it would just be possible to take as S the least cardinal
greater than the cardinals of all the F i, but I don't have a very clear
idea of how/whether something similar could be done in HOL.
Before I spend a lot of time rummaging through the well ordering stuff in
the Isabelle library I thought I would risk asking to see if somebody on
this list knows the answer instantly. Thanks for any help you can give.
- Gene Stark
Email Gateway (Aug 22 2022 at 13:07):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Gene,
You can use the disjoint union (which is of course not only weakly, but also strongly universal).
Search for the text "Disjoint union of a family of sets" in https://isabelle.in.tum.de/dist/library/HOL/HOL/Product_Type.html
All the best,
Andrei
Email Gateway (Aug 22 2022 at 13:07):From: Dmitriy Traytel <traytel@inf.ethz.ch>
Hi Gene,
while Andrei is right on the high level, I should point out that your lemma does not hold in HOL as stated.
For instance the type of the existentially quantified "S :: ‘c set" might simply be not large enough to embed "(F :: ‘a => ‘b set) i” (counterexample: ‘c = unit, ‘a = ‘b = nat, F = %_. UNIV).
Here is a theorem, which I can prove easily using our cardinals library [1]. It fixes ‘c to be a large enough type to use Sigma as the witness (as Andrei suggested). It also requires the index type ‘a to be infinite and S’ to be larger than the index type as well.
theory Scratch
imports
"~~/src/HOL/Library/Cardinal_Notations"
"~~/src/HOL/Library/FuncSet"
begin
definition embeds
where "embeds A B ≡ ∃f. f ∈ B → A ∧ inj_on f B"
lemma embeds_ordLeq: "embeds A B ⟷ |B| ≤o |A|"
unfolding card_of_ordLeq[symmetric] embeds_def by auto
lemma
fixes F :: "'a ⇒ 'b set"
assumes "infinite (UNIV :: 'a set)"
shows "∃S :: ('a × 'b) set.
(∀x. embeds S (F x)) ∧
(∀S'. (∀x. embeds S' (F x)) ⟶ embeds S' (UNIV :: 'a set) ⟶ embeds S' S)"
unfolding embeds_ordLeq using assms
by (auto simp: image_iff card_of_ordLeq_finite
intro!: exI[of _ "Sigma UNIV F"] surj_imp_ordLeq[of _ snd] card_of_Sigma_ordLeq_infinite)
end
I did not think thoroughly if all my modifications are necessary. I.e., what happens if the index type ‘a is finite?
Best wishes,
Dmitriy
[1] Cardinals in Isabelle/HOL
Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel
ITP 2014, http://people.inf.ethz.ch/trayteld/papers/itp14-card/card.pdf
Email Gateway (Aug 22 2022 at 13:07):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Andrei, the disjoint union was not what I wanted, because although it
does in fact embed all the sets, it separates them and thus produces a set that
is not minimal with respect to embeddings. If we make identifications we
can get a more economical union. For example if A = {*}, then the disjoint
union A+A of A and A is a two-element set, but A itself already embeds A
and has only one element, so is itself embedded in A+A.
- Gene Stark
Email Gateway (Aug 22 2022 at 13:07):From: Andrei Popescu <a.popescu@mdx.ac.uk>
Hi Dmitriy and Gene,
Sorry, I lost sight of the word "embedding" in Gene's email...
Indeed, disjoint union does not fully work, as shown by Dmitriy's need for extra hypotheses. In particular, the size of the index causes trouble.
For a full solution, we really need cardinal suprema. In HOL, this is a bit more bureaucratic than in ZFC, but it works.
We can fix a well-order on 'b (where the family F has type 'a => 'b set).
For each i::'a, there exists a restriction of this fixed well-order, say, "k i", representing the cardinal of "F i".
The desired weakly universal set is the union of the fields of all these cardinals "k i".
All the best,
Andrei
Email Gateway (Aug 22 2022 at 13:07):From: Andrei Popescu <a.popescu@mdx.ac.uk>
Hi Gene,
Correct. In my other email I sketch such a (most) economical union, namely, on cardinal representatives.
This is useful result in our cardinal library, so I can add it myself.
Best,
Andrei
Email Gateway (Aug 22 2022 at 13:07):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
That sounds like the answer I was looking for. Thank you both for your replies.
- Gene Stark
Email Gateway (Aug 22 2022 at 13:08):From: Andrei Popescu <A.Popescu@mdx.ac.uk>
Hi Gene,
Thank you for your question -- this theorem was an important fact missing in our cardinal library,
and it triggered some further useful infrastructure lemmas.
A polished version of it will be part of the next distribution. In the meantime, attached is a theory file
that has the theorem at the end (also included in this message).
All the best,
Andrei
theory Embed imports Main
begin
(* Some order-filter infrastructure *)
lemma ofilter_embed2:
assumes r: "Well_order r" and e: "embed r r' f" and o: "ofilter r A"
shows "embed (Restr r A) r' f"
using assms Field_Restr_ofilter[OF r o] ofilter_Restr_under[OF r o]
unfolding embed_def ofilter_embed[OF r] by auto
lemma ofilter_incl_embed:
assumes r: "Well_order r" and oA: "ofilter r A" and oB: "ofilter r B"
and e: "embed (Restr r A) r' f" and i: "B ⊆ A"
shows "embed (Restr r B) r' f"
using Well_order_Restr[OF r] ofilter_Restr_subset[OF r oB i] ofilter_embed2[OF _ e] Restr_subset[OF i]
by fastforce
lemma ofilter_int:
assumes r: "Well_order r" and oA: "ofilter r A" and oB: "ofilter r B"
shows "ofilter r (A ∩ B)"
by (metis Int_absorb1 Int_absorb2 oA oB r wo_rel.intro wo_rel.ofilter_linord)
lemma ofilter_UNION:
assumes "∀ i ∈ I. ofilter r (A i)"
shows "ofilter r (⋃ i ∈ I. A i)"
using assms unfolding ofilter_def under_def by blast
lemma Restr_UNION_ofilter:
assumes "∀ i ∈ I. ofilter r (A i)"
shows "Restr r (⋃ i ∈ I. A i) = (⋃ i ∈ I. Restr r (A i))"
using assms unfolding ofilter_def under_def by blast
lemma ofilter_ordLeq_UNION:
assumes r: "Well_order r" and r': "Well_order r'"
and ofl: "∀ i ∈ I. ofilter r (A i) ∧ ordLeq3 (Restr r (A i)) r'"
shows "ordLeq3 (Restr r (⋃ i ∈ I. A i)) r'"
proof-
let ?U = "⋃ i ∈ I. A i"
{fix i assume i: "i ∈ I"
have "Well_order (Restr r (A i))" using Well_order_Restr r by fastforce
have "∃ gi. embed (Restr r (A i)) r' gi" using ofl i unfolding ordLeq_def by auto
}
then obtain g where g: "∀ i ∈ I. embed (Restr r (A i)) r' (g i)" by metis
def ii ≡ "λ a. SOME i. i ∈ I ∧ a ∈ A i"
def gg ≡ "λ a. g (ii a) a"
have "ofilter r ?U" using ofilter_UNION ofl by metis
hence F: "Field (Restr r ?U) = ?U" using Field_Restr_ofilter[OF r] by auto
have "embed (Restr r ?U) r' gg" unfolding embed_def proof
fix a let ?i = "ii a"
assume "a ∈ Field (Restr r ?U)"
hence "∃ i. i ∈ I ∧ a ∈ A i" unfolding F by auto
hence i: "?i ∈ I" and aa: "a ∈ A ?i" unfolding ii_def by (metis (no_types, lifting) someI_ex)+
hence a: "a∈Field (Restr r (A ?i))" using Field_Restr_ofilter[OF r] ofl by auto
hence 1: "bij_betw (g ?i) (under (Restr r (A ?i)) a) (under r' (g ?i a))" using g i unfolding embed_def by auto
have 2: "under (Restr r ?U) a = under (Restr r (A ?i)) a"
using aa ofl i aa unfolding under_def ofilter_def by auto
{fix b assume 0: "b ∈ under (Restr r (A ?i)) a"
let ?j = "ii b"
have "b ∈ Field (Restr r ?U)" using 2 subsetCE under_Field 0 by fastforce
hence "∃ i. i ∈ I ∧ b ∈ A i" unfolding F by auto
hence j: "?j ∈ I" and bb: "b ∈ A ?j" unfolding ii_def by (metis (no_types, lifting) someI_ex)+
hence b: "b ∈ Field (Restr r (A ?j))" using Field_Restr_ofilter[OF r] ofl by auto
hence 1: "embed (Restr r (A ?j)) r' (g ?j)" using g j by auto
let ?B = "A ?i ∩ A ?j"
have b: "b ∈ ?B" by (metis 0 Int_iff bb mem_Collect_eq mem_Sigma_iff under_def)
have 11: "embed (Restr r (A ?i)) r' (g ?i)" using g i by auto
have oB: "ofilter r ?B" using ofl i j ofilter_int r by fastforce
hence B1: "embed (Restr r ?B) r' (g ?i)" using 11 i inf_le1 ofilter_incl_embed ofl r by fastforce
have B2: "embed (Restr r ?B) r' (g ?j)" using 1 j by (metis oB inf_commute inf_le1 ofilter_incl_embed ofl r)
have B: "Well_order (Restr r ?B)" using Well_order_Restr r by blast
have "g ?i b = g ?j b" using b B1 B2 embed_unique[OF B r' B1 B2] Field_Restr_ofilter i j ofilter_int ofl r by blast
}
thus "bij_betw gg (under (Restr r ?U) a) (under r' (gg a))" using 1 2 unfolding gg_def
unfolding bij_betw_def inj_on_def image_def by auto
qed
thus ?thesis unfolding ordLeq_def using Restr_UNION_ofilter ofl r'
by (auto simp: Well_order_Restr r)
qed
(* Cardinal suprema (for a family of cardinals on the same host type) *)
context fixes I :: "'i set" and k :: "'i ⇒ 'a rel"
begin
definition K::"'a rel" where "K = card_of UNIV"
lemma card_order_K: "card_order K"
by (simp add: Embed.K_def card_of_card_order_on)
lemma ordLeq_K:
assumes "Card_order (k i)" shows "ordLeq3 (k i) K"
by (metis Card_order_iff_ordLeq_card_of Embed.K_def UNIV_I assms card_of_mono1
ordLeq_transitive subsetI)
definition f :: "'i ⇒ 'a ⇒ 'a" where
"f i ≡ SOME f. embed (k i) K f"
lemma embed_f:
assumes "Card_order (k i)"
shows "embed (k i) K (f i)"
unfolding f_def
apply(rule someI_ex[of "%f. embed (k i) K f"])
unfolding K_def
by (metis Cnotzero_UNIV K_def assms card_order_on_def not_ordLess_ordLeq ordLeq_K ordLess_iff)
definition A :: "'i ⇒ 'a set" where
"A i ≡ f i ` (Field (k i))"
lemma iso_A:
assumes "Card_order (k i)"
shows "iso (k i) (Restr K (A i)) (f i)"
by (metis A_def Embed.K_def Embed.card_order_K Embed.embed_f Field_card_of
assms card_order_on_def embed_implies_iso_Restr)
lemma ordIso2_A:
assumes "Card_order (k i)"
shows "ordIso2 (k i) (Restr K (A i))"
using iso_A[OF assms] assms card_order_on_def unfolding ordIso_def
by (auto simp: K_def Well_order_Restr card_of_Well_order)
lemma Card_order_A:
assumes "Card_order (k i)"
shows "Card_order (Restr K (A i))"
using Card_order_ordIso2 ordIso2_A[OF assms] assms by blast
definition csupr :: "'a rel" where
"csupr ≡ card_of (⋃ i ∈ I. A i)"
lemma Card_order_csupr:
"Card_order csupr"
by (simp add: csupr_def card_of_Card_order)
lemma ordLeq_csupr:
assumes c: "∀ i ∈ I. Card_order (k i)" and i: "i ∈ I"
shows "ordLeq3 (k i) csupr"
proof-
let ?k = "card_of (Field (k i))"
have "ordIso2 (k i) (Restr K (A i))" using ordIso2_A c i by auto
also have "ordIso2 (Restr K (A i)) (card_of (A i))"
by (metis Card_order_A Embed.A_def c card_of_unique i iso_A iso_Field)
also have "ordLeq3 (card_of (A i)) csupr" unfolding csupr_def
by (meson UN_I assms(2) card_of_mono1 subsetI)
finally show ?thesis .
qed
lemma ofilter_A:
assumes ci: "Card_order (k i)"
shows "ofilter K (A i)"
using ci iso_A[OF ci] unfolding A_def
by (metis Cnotzero_UNIV embed_f K_def card_order_on_well_order_on embed_Field_ofilter)
lemma csupr_ordLeq:
assumes ci: "∀ i ∈ I. Card_order (k i)"
and c: "Card_order r"
and ord: "⋀ i. i ∈ I ⟹ ordLeq3 (k i) r"
shows "ordLeq3 csupr r"
proof-
let ?U = "⋃ i ∈ I. A i"
let ?restr = "Restr K ?U"
have 0: "∀i ∈ I. ofilter K (A i)" using ofilter_A ci by auto
have restr: "Well_order ?restr" and K: "Well_order K" and r: "Well_order r"
using c card_order_on_def by (auto simp: Field_card_of K_def Well_order_Restr card_of_well_order_on)
have "Field ?restr = ?U"
using ofilter_A ofilter_UNION 0 by (intro Field_Restr_ofilter) (auto simp: K_def Field_card_of card_of_well_order_on)
hence 1: "well_order_on ?U ?restr" using restr by auto
have restr: "?restr = (⋃ i ∈ I. Restr K (A i))" using Restr_UNION_ofilter[OF 0] by auto
have 2: "⋀ i. i ∈ I ⟹ ordLeq3 (Restr K (A i)) r"
using ord by (metis ordIso2_A ci ordIso_iff_ordLeq ordLeq_transitive)
have "ordLeq3 (card_of ?U) ?restr" using 1 card_of_least by blast
also have "ordLeq3 ?restr r" using ofilter_ordLeq_UNION[OF K r] 0 2 by metis
finally show ?thesis unfolding csupr_def .
qed
end (* context *)
hide_const A K f
term csupr
thm Card_order_csupr
thm ordLeq_csupr
thm csupr_ordLeq
definition "embeds A B ≡ ∃ f. f ` B ⊆ A ∧ inj_on f B"
lemma embeds_ordLeq: "embeds A B ⟷ ordLeq3 (card_of B) (card_of A)"
unfolding card_of_ordLeq[symmetric] embeds_def by auto
lemma embeds_universal:
fixes I :: "'i set" and F :: "'i ⇒ 'a set"
defines "S ≡ Field (csupr I (card_of o F))"
shows "(∀ i. i ∈ I ⟶ embeds S (F i)) ∧
(∀ S'. (∀ i. i ∈ I ⟶ embeds S' (F i)) ⟶ embeds S' S)"
proof-
have 1: "∀ i ∈ I. Card_order ((card_of o F) i)"
by (simp add: Field_card_of card_of_card_order_on)
have "ordIso2 (card_of S) (csupr I (card_of o F))"
unfolding S_def using card_of_Field_ordIso[OF Card_order_csupr] .
with ordLeq_csupr[OF 1] csupr_ordLeq[OF 1]
show ?thesis unfolding S_def embeds_ordLeq o_def
by safe (simp add: Field_card_of csupr_def,
simp add: card_of_Card_order csupr_ordLeq ordIso_ordLeq_trans)
qed
end
Embed.thy
Last updated: Apr 20 2024 at 08:16 UTC