# 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+). β < Gy"
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+). β < Gy 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α. Gmα  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 "|{Gmα . 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 "|{Gmα . 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κ" "Gn = (λαν. 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 Gn = (λαν. H(α))
have "Gnα = H(α)"
using ltD by simp
moreover from calculation and H_satisfies
have "m<fα. Gmα  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