Theory Cohen_Posets
subsection‹Application to Cohen posets\label{sec:cohen}›
theory Cohen_Posets
imports
Delta_System
begin
text‹We end this session by applying DSL to the combinatorics of
finite function posets. We first define some basic concepts; we take
a different approach from \<^cite>‹"2020arXiv200109715G"›, in that the
order relation is presented as a predicate (of type @{typ ‹[i,i] ⇒ o›}).
Two elements of a poset are ∗‹compatible› if they have a common lower
bound.›
definition compat_in :: "[i,[i,i]⇒o,i,i]⇒o" where
"compat_in(A,r,p,q) ≡ ∃d∈A . r(d,p) ∧ r(d,q)"
text‹An ∗‹antichain› is a subset of pairwise incompatible members.›
definition
antichain :: "[i,[i,i]⇒o,i]⇒o" where
"antichain(P,leq,A) ≡ A⊆P ∧ (∀p∈A. ∀q∈A.
p≠q ⟶ ¬compat_in(P,leq,p,q))"
text‹A poset has the ∗‹countable chain condition› (ccc) if all of its
antichains are countable.›
definition
ccc :: "[i,[i,i]⇒o]⇒o" where
"ccc(P,leq) ≡ ∀A. antichain(P,leq,A) ⟶ countable(A)"
text‹Finally, the ∗‹Cohen poset› is the set of finite partial functions
between two sets with the order of reverse inclusion.›
definition
Fn :: "[i,i] ⇒ i" where
"Fn(I,J) ≡ ⋃{(d→J) . d ∈ {x ∈ Pow(I). Finite(x)}}"
abbreviation
Supset :: "i ⇒ i ⇒ o" (infixl ‹⊇› 50) where
"f ⊇ g ≡ g ⊆ f"
lemma FnI[intro]:
assumes "p : d → J" "d ⊆ I" "Finite(d)"
shows "p ∈ Fn(I,J)"
using assms unfolding Fn_def by auto
lemma FnD[dest]:
assumes "p ∈ Fn(I,J)"
shows "∃d. p : d → J ∧ d ⊆ I ∧ Finite(d)"
using assms unfolding Fn_def by auto
lemma Fn_is_function: "p ∈ Fn(I,J) ⟹ function(p)"
unfolding Fn_def using fun_is_function by auto
lemma restrict_eq_imp_compat:
assumes "f ∈ Fn(I, J)" "g ∈ Fn(I, J)"
"restrict(f, domain(f) ∩ domain(g)) = restrict(g, domain(f) ∩ domain(g))"
shows "f ∪ g ∈ Fn(I, J)"
proof -
from assms
obtain d1 d2 where "f : d1 → J" "d1 ∈ Pow(I)" "Finite(d1)"
"g : d2 → J" "d2 ∈ Pow(I)" "Finite(d2)"
by blast
with assms
show ?thesis
using domain_of_fun
restrict_eq_imp_Un_into_Pi[of f d1 "λ_. J" g d2 "λ_. J"]
by auto
qed
text‹We finally arrive to our application of DSL.›
lemma ccc_Fn_2: "ccc(Fn(I,2), (⊇))"
proof -
{
fix A
assume "¬ countable(A)"
assume "A ⊆ Fn(I, 2)"
moreover from this
have "countable({p∈A. domain(p) = d})" for d
proof (cases "Finite(d) ∧ d ⊆ I")
case True
with ‹A ⊆ Fn(I, 2)›
have "{p ∈ A . domain(p) = d} ⊆ d → 2"
using domain_of_fun by fastforce
moreover from True
have "Finite(d → 2)"
using Finite_Pi lesspoll_nat_is_Finite by auto
ultimately
show ?thesis using subset_Finite[of _ "d→2" ] Finite_imp_countable
by auto
next
case False
with ‹A ⊆ Fn(I, 2)›
have "{p ∈ A . domain(p) = d} = 0"
by (intro equalityI) (auto dest!: domain_of_fun)
then
show ?thesis using empty_lepollI by auto
qed
moreover
have "uncountable({domain(p) . p ∈ A})"
proof
from ‹A ⊆ Fn(I, 2)›
have "A = (⋃d∈{domain(p) . p ∈ A}. {p∈A. domain(p) = d})"
by auto
moreover
assume "countable({domain(p) . p ∈ A})"
moreover
note ‹⋀d. countable({p∈A. domain(p) = d})› ‹¬countable(A)›
ultimately
show "False"
using countable_imp_countable_UN[of "{domain(p). p∈A}"
"λd. {p ∈ A. domain(p) = d }"]
by auto
qed
moreover from ‹A ⊆ Fn(I, 2)›
have "p ∈ A ⟹ Finite(domain(p))" for p
using lesspoll_nat_is_Finite[of "domain(p)"]
domain_of_fun[of p _ "λ_. 2"] by auto
ultimately
obtain D where "delta_system(D)" "D ⊆ {domain(p) . p ∈ A}" "D ≈ ℵ⇘1⇙"
using delta_system_uncountable[of "{domain(p) . p ∈ A}"] by auto
then
have delta:"∀d1∈D. ∀d2∈D. d1 ≠ d2 ⟶ d1 ∩ d2 = ⋂D"
using delta_system_root_eq_Inter
by simp
moreover from ‹D ≈ ℵ⇘1⇙›
have "uncountable(D)"
using uncountable_iff_subset_eqpoll_Aleph1 by auto
moreover from this and ‹D ⊆ {domain(p) . p ∈ A}›
obtain p1 where "p1 ∈ A" "domain(p1) ∈ D"
using uncountable_not_empty[of D] by blast
moreover from this and ‹p1 ∈ A ⟹ Finite(domain(p1))›
have "Finite(domain(p1))" using Finite_domain by simp
moreover
define r where "r ≡ ⋂D"
ultimately
have "Finite(r)" using subset_Finite[of "r" "domain(p1)"] by auto
have "countable({restrict(p,r) . p∈A})"
proof -
have "f ∈ Fn(I, 2) ⟹ restrict(f,r) ∈ Pow(r × 2)" for f
using restrict_subset_Sigma[of f _ "λ_. 2" r]
by (force simp: Pi_def)
with ‹A ⊆ Fn(I, 2)›
have "{restrict(f,r) . f ∈ A } ⊆ Pow(r × 2)"
by fast
with ‹Finite(r)›
show ?thesis
using Finite_Sigma[THEN Finite_Pow, of r "λ_. 2"]
by (intro Finite_imp_countable) (auto intro:subset_Finite)
qed
moreover
have "uncountable({p∈A. domain(p) ∈ D})" (is "uncountable(?X)")
proof
from ‹D ⊆ {domain(p) . p ∈ A}›
have "(λp∈?X. domain(p)) ∈ surj(?X, D)"
using lam_type unfolding surj_def by auto
moreover
assume "countable(?X)"
moreover
note ‹uncountable(D)›
ultimately
show False
using surj_countable by auto
qed
moreover
have "D = (⋃f∈Pow(r×2) . {domain(p) . p∈{ x∈A. restrict(x,r) = f ∧ domain(x) ∈ D}})"
proof -
{
fix z
assume "z ∈ D"
with ‹D ⊆ _›
obtain p where "domain(p) = z" "p ∈ A"
by auto
moreover from ‹A ⊆ Fn(I, 2)› and this
have "p : z → 2"
using domain_of_fun by force
moreover from this
have "restrict(p,r) ⊆ r × 2"
using function_restrictI[of p r] fun_is_function[of p z "λ_. 2"]
restrict_subset_Sigma[of p z "λ_. 2" r]
by (auto simp:Pi_def)
ultimately
have "∃p∈A. restrict(p,r) ∈ Pow(r×2) ∧ domain(p) = z" by auto
}
then
show ?thesis
by (intro equalityI) (force)+
qed
obtain f where "uncountable({domain(p) . p∈{x∈A. restrict(x,r) = f ∧ domain(x) ∈ D}})"
(is "uncountable(?Y(f))")
proof -
{
from ‹Finite(r)›
have "countable(Pow(r×2))"
using Finite_Sigma[THEN Finite_Pow, THEN Finite_imp_countable]
by simp
moreover
assume "countable(?Y(f))" for f
moreover
note ‹D = (⋃f∈Pow(r×2) .?Y(f))›
moreover
note ‹uncountable(D)›
ultimately
have "False"
using countable_imp_countable_UN[of "Pow(r×2)" ?Y] by auto
}
with that
show ?thesis by auto
qed
then
obtain j where "j ∈ inj(nat, ?Y(f))"
using uncountable_iff_nat_lt_cardinal[THEN iffD1, THEN leI,
THEN cardinal_le_imp_lepoll, THEN lepollD]
by auto
then
have "j`0 ≠ j`1" "j`0 ∈ ?Y(f)" "j`1 ∈ ?Y(f)"
using inj_is_fun[THEN apply_type, of j nat "?Y(f)"]
unfolding inj_def by auto
then
obtain p q where "domain(p) ≠ domain(q)" "p ∈ A" "q ∈ A"
"domain(p) ∈ D" "domain(q) ∈ D"
"restrict(p,r) = restrict(q,r)" by auto
moreover from this and delta
have "domain(p) ∩ domain(q) = r" unfolding r_def by simp
moreover
note ‹A ⊆ Fn(I, 2)›
moreover from calculation
have "p ∪ q ∈ Fn(I, 2)"
by (rule_tac restrict_eq_imp_compat) auto
ultimately
have "∃p∈A. ∃q∈A. p ≠ q ∧ compat_in(Fn(I, 2), (⊇), p, q)"
unfolding compat_in_def
by (rule_tac bexI[of _ p], rule_tac bexI[of _ q]) blast
}
then
show ?thesis unfolding ccc_def antichain_def by auto
qed
text‹The fact that a poset $P$ has the ccc has useful consequences for the
theory of forcing, since it implies that cardinals from the original
model are exactly the cardinals in any generic extension by $P$
\<^cite>‹‹Chap.~IV› in "kunen2011set"›.›
end