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