# 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)  dA . 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)  AP  (pA. qA.
pq  ¬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)  {(dJ) . 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({pA. 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 _ "d2" ] 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}. {pA. domain(p) = d})"
by auto
moreover
assume "countable({domain(p) . p  A})"
moreover
note d. countable({pA. domain(p) = d}) ¬countable(A)
ultimately
show "False"
using countable_imp_countable_UN[of "{domain(p). pA}"
"λ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:"d1D. d2D. 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) . pA})"
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({pA. 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 = (fPow(r×2) . {domain(p) . p{ xA. 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 "pA.  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{xA. 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 = (fPow(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 "j0  j1" "j0  ?Y(f)" "j1  ?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 "pA. qA. 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