Theory Konig

theory Konig
  imports
    Cofinality
    Cardinal_Library

begin

text‹Now, using the Axiom of choice, we can show that all successor
cardinals are regular.›

lemma cf_csucc:
  assumes "InfCard(z)"
  shows "cf(z+) = z+"
proof (rule ccontr)
  assume "cf(z+)  z+"
  moreover from InfCard(z)
  have "Ord(z+)" "Ord(z)" "Limit(z)" "Limit(z+)" "Card(z+)" "Card(z)"
    using InfCard_csucc Card_is_Ord InfCard_is_Card InfCard_is_Limit
    by fastforce+
  moreover from calculation
  have "cf(z+) < z+"
    using cf_le_cardinal[of "z+", THEN le_iff[THEN iffD1]]
      Card_cardinal_eq
    by simp
  ultimately
  obtain G where "G:cf(z+) z+" "βz+. ycf(z+). β < G`y"
    using Limit_cofinal_fun_lt[of "z+" _ "cf(z+)"] Ord_cf
      cf_le_cf_fun[of "z+" "cf(z+)"] le_refl[of "cf(z+)"]
    by auto
  with Card(z) Card(z+) Ord(z+)
  have "βcf(z+). |G`β|  z"
    using apply_type[of G "cf(z+)" "λ_. z+", THEN ltI] Card_lt_iff[THEN iffD2]
      Ord_in_Ord[OF Card_is_Ord, of "z+"] cardinal_lt_csucc_iff[THEN iffD1]
    by auto
  from cf(z+) < z+ InfCard(z) Ord(z)
  have "cf(z+)  z"
    using cardinal_lt_csucc_iff[of "z" "cf(z+)"] Card_csucc[of "z"]
      le_Card_iff[of "z" "cf(z+)"] InfCard_is_Card
      Card_lt_iff[of "cf(z+)" "z+"] lt_Ord[of "cf(z+)" "z+"]
    by simp
  with cf(z+) < z+ βcf(z+). |G`β|  _ InfCard(z)
  have "|βcf(z+). G`β|  z"
    using InfCard_csucc[of z]
      subset_imp_lepoll[THEN lepoll_imp_cardinal_le, of "βcf(z+). G`β" "z"]
    by (rule_tac lepoll_imp_cardinal_UN_le) auto
  moreover
  note Ord(z)
  moreover from βz+. ycf(z+). β < G`y and this
  have "z+  (βcf(z+). G`β)"
    by (blast dest:ltD)
  ultimately
  have "z+  z"
    using subset_imp_le_cardinal[of "z+" "βcf(z+). G`β"] le_trans
      InfCard_is_Card Card_csucc[of z] Card_cardinal_eq
    by auto
  with Ord(z)
  show "False"
    using lt_csucc[of z] not_lt_iff_le[THEN iffD2, of z "z+"]
      Card_csucc[THEN Card_is_Ord]
    by auto
qed

text‹And this finishes the calculation of cofinality of Alephs.›

lemma cf_Aleph_succ: "Ord(z)  cf(ℵ⇘succ(z)) = ℵ⇘succ(z)⇙"
  using Aleph_succ cf_csucc InfCard_Aleph by simp

subsection‹König's Theorem\label{sec:konig}›

text‹We end this section by proving König's Theorem on the cofinality
of cardinal exponentiation. This is a strengthening of Cantor's theorem
and it is essentially the only basic way to prove strict cardinal
inequalities.

It is proved rather straightforwardly with the tools already developed.›

lemma konigs_theorem:
  notes [dest] = InfCard_is_Card Card_is_Ord
    and [trans] = lt_trans1 lt_trans2
  assumes
    "InfCard(κ)" "InfCard(ν)" "cf(κ)  ν"
  shows
    "κ < κ⇗↑ν⇖"
  using assms(1,2) Card_cexp
proof (intro not_le_iff_lt[THEN iffD1] notI)
  assume "κ⇗↑ν κ"
  moreover
  note InfCard(κ)
  moreover from calculation
  have "ν  κ  κ"
    using Card_cardinal_eq[OF InfCard_is_Card, symmetric]
      Card_le_imp_lepoll
    unfolding cexp_def by simp
  ultimately
  obtain G where "G  surj(κ, ν  κ)"
    using inj_imp_surj[OF _ function_space_nonempty,
        OF _ nat_into_InfCard] by blast
  from assms
  obtain f where "f:ν  κ" "cf_fun(f,κ)"
    using cf_le_cf_fun[OF _ InfCard_is_Limit] by blast
  define H where "H(α)  μ x. xκ  (m<f`α. G`m`α  x)"
    (is "_  μ x. ?P(α,x)") for α
  have H_satisfies: "?P(α,H(α))" if "α  ν" for α
  proof -
    obtain h where "?P(α,h)"
    proof -
      from αν f:ν  κ InfCard(κ)
      have "f`α < κ"
        using apply_type[of _ _ "λ_ . κ"] by (auto intro:ltI)
      have "|{G`m`α . m  {xκ . x < f`α}}|  |{xκ . x < f`α}|"
        using cardinal_RepFun_le by simp
      also from f`α < κ InfCard(κ)
      have "|{xκ . x < f`α}| < |κ|"
        using Card_lt_iff[OF lt_Ord, THEN iffD2, of "f`α" κ κ]
          Ord_eq_Collect_lt[of "f`α" κ] Card_cardinal_eq
        by force
      finally
      have "|{G`m`α . m  {xκ . x < f`α}}| < |κ|" .
      moreover from f`α < κ InfCard(κ)
      have "m<f`α  mκ" for m
        using Ord_trans[of m "f`α" κ]
        by (auto dest:ltD)
      ultimately
      have "h. ?P(α,h)"
        using lt_cardinal_imp_not_subset by blast
      with that
      show ?thesis by blast
    qed
    with assms
    show "?P(α,H(α))"
      using LeastI[of "?P(α)" h] lt_Ord Ord_in_Ord
      unfolding H_def by fastforce
  qed
  then
  have "(λαν. H(α)): ν  κ"
    using lam_type by auto
  with G  surj(κ, ν  κ)
  obtain n where "nκ" "G`n = (λαν. H(α))"
    unfolding surj_def by blast
  moreover
  note InfCard(κ) f: ν  κ cf_fun(f,_)
  ultimately
  obtain α where "n < f`α" "αν"
    using Limit_cofinal_fun_lt[OF InfCard_is_Limit] by blast
  moreover from calculation and G`n = (λαν. H(α))
  have "G`n`α = H(α)"
    using ltD by simp
  moreover from calculation and H_satisfies
  have "m<f`α. G`m`α  H(α)" by simp
  ultimately
  show "False" by blast
qed blast+

lemma cf_cexp:
  assumes
    "Card(κ)" "InfCard(ν)" "2  κ"
  shows
    "ν < cf(κ⇗↑ν)"
proof (rule ccontr)
  assume "¬ ν < cf(κ⇗↑ν)"
  with InfCard(ν)
  have "cf(κ⇗↑ν)  ν" 
    using not_lt_iff_le Ord_cf InfCard_is_Card Card_is_Ord by simp
  moreover
  note assms
  moreover from calculation
  have "InfCard(κ⇗↑ν)" using InfCard_cexp by simp
  moreover from calculation
  have "κ⇗↑ν< (κ⇗↑ν)⇗↑ν⇖" 
    using konigs_theorem by simp
  ultimately
  show "False" using cexp_cexp_cmult InfCard_csquare_eq by auto
qed

text‹Finally, the next two corollaries illustrate the only possible
exceptions to the value of the cardinality of the continuum: The limit
cardinals of countable cofinality. That these are the only exceptions
is a consequence of Easton's Theorem~cite‹Thm 15.18› in "Jech_Millennium".›

corollary cf_continuum: "ℵ⇘0< cf(2⇗↑ℵ⇘0⇙⇖)"
  using cf_cexp InfCard_Aleph nat_into_Card by simp

corollary continuum_not_eq_Aleph_nat: "2⇗↑ℵ⇘0⇙⇖  ℵ⇘ω⇙"
  using cf_continuum cf_Aleph_Limit[OF Limit_nat] cf_nat
    Aleph_zero_eq_nat by auto

end