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 "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 "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