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⇧+. ∃y∈cf(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⇧+. ∃y∈cf(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