section‹Cofinality\label{sec:cofinality}› theory Cofinality imports ZF_Library begin subsection‹Basic results and definitions› text‹A set \<^term>‹X› is ∗‹cofinal› in \<^term>‹A› (with respect to the relation \<^term>‹r›) if every element of \<^term>‹A› is ``bounded above'' by some element of \<^term>‹X›. Note that \<^term>‹X› does not need to be a subset of \<^term>‹A›.› definition cofinal :: "[i,i,i] ⇒ o" where "cofinal(X,A,r) ≡ ∀a∈A. ∃x∈X. ⟨a,x⟩∈r ∨ a = x" (* (* Alternative definitions *) definition cofinal_predic :: "[i,i,[i,i]⇒o] ⇒ o" where "cofinal_predic(X,A,r) ≡ ∀a∈A. ∃x∈X. r(a,x) ∨ a = x" definition f_cofinal :: "[i⇒i,i,i,i] ⇒ o" where "f_cofinal(f,C,A,r) ≡ ∀a∈A. ∃x∈C. ⟨a,f(x)⟩∈r ∨ a = f(x)" (* The next definition doesn't work if 0 is the top element of A. But it works for limit ordinals. *) definition cofinal_fun' :: "[i,i,i] ⇒ o" where "cofinal_fun'(f,A,r) == f_cofinal(λx. f`x,domain(f),A, r)" *) text‹A function is cofinal if it range is.› definition cofinal_fun :: "[i,i,i] ⇒ o" where "cofinal_fun(f,A,r) ≡ ∀a∈A. ∃x∈domain(f). ⟨a,f`x⟩∈r ∨ a = f`x" lemma cofinal_funI: assumes "⋀a. a∈A ⟹ ∃x∈domain(f). ⟨a,f`x⟩∈r ∨ a = f`x" shows "cofinal_fun(f,A,r)" using assms unfolding cofinal_fun_def by simp lemma cofinal_funD: assumes "cofinal_fun(f,A,r)" "a∈A" shows "∃x∈domain(f). ⟨a,f`x⟩∈r ∨ a = f`x" using assms unfolding cofinal_fun_def by simp lemma cofinal_in_cofinal: assumes "trans(r)" "cofinal(Y,X,r)" "cofinal(X,A,r)" shows "cofinal(Y,A,r)" unfolding cofinal_def proof fix a assume "a∈A" moreover from ‹cofinal(X,A,r)› have "b∈A⟹∃x∈X. ⟨b,x⟩∈r ∨ b=x" for b unfolding cofinal_def by simp ultimately obtain y where "y∈X" "⟨a,y⟩∈r ∨ a=y" by auto moreover from ‹cofinal(Y,X,r)› have "c∈X⟹∃y∈Y. ⟨c,y⟩∈r ∨ c=y" for c unfolding cofinal_def by simp ultimately obtain x where "x∈Y" "⟨y,x⟩∈r ∨ y=x" by auto with ‹a∈A› ‹y∈X› ‹⟨a,y⟩∈r ∨ a=y› ‹trans(r)› show "∃x∈Y. ⟨a,x⟩∈r ∨ a=x" unfolding trans_def by auto qed lemma codomain_is_cofinal: assumes "cofinal_fun(f,A,r)" "f:C → D" shows "cofinal(D,A,r)" unfolding cofinal_def proof fix b assume "b ∈ A" moreover from assms have "a∈A ⟹ ∃x∈domain(f). ⟨a, f ` x⟩ ∈ r ∨ a = f`x" for a unfolding cofinal_fun_def by simp ultimately obtain x where "x∈domain(f)" "⟨b, f ` x⟩ ∈ r ∨ b = f`x" by blast moreover from ‹f:C → D› ‹x∈domain(f)› have "f`x∈D" using domain_of_fun apply_rangeI by simp ultimately show "∃y∈D. ⟨b, y⟩ ∈ r ∨ b = y" by auto qed lemma cofinal_range_iff_cofinal_fun: assumes "function(f)" shows "cofinal(range(f),A,r) ⟷ cofinal_fun(f,A,r)" unfolding cofinal_fun_def proof (intro iffI ballI) fix a assume "a∈A" ‹cofinal(range(f),A,r)› then obtain y where "y∈range(f)" "⟨a,y⟩ ∈ r ∨ a = y" unfolding cofinal_def by blast moreover from this obtain x where "⟨x,y⟩∈f" unfolding range_def domain_def converse_def by blast moreover note ‹function(f)› ultimately have "⟨a, f ` x⟩ ∈ r ∨ a = f ` x" using function_apply_equality by blast with ‹⟨x,y⟩∈f› show "∃x∈domain(f). ⟨a, f ` x⟩ ∈ r ∨ a = f ` x" by blast next assume "∀a∈A. ∃x∈domain(f). ⟨a, f ` x⟩ ∈ r ∨ a = f ` x" with assms show "cofinal(range(f), A, r)" using function_apply_Pair[of f] unfolding cofinal_def by fast qed lemma cofinal_comp: assumes "f∈ mono_map(C,s,D,r)" "cofinal_fun(f,D,r)" "h:B → C" "cofinal_fun(h,C,s)" "trans(r)" shows "cofinal_fun(f O h,D,r)" unfolding cofinal_fun_def proof fix a from ‹f∈ mono_map(C,s,D,r)› have "f:C → D" using mono_map_is_fun by simp with ‹h:B → C› have "domain(f) = C" "domain(h) = B" using domain_of_fun by simp_all moreover assume "a ∈ D" moreover note ‹cofinal_fun(f,D,r)› ultimately obtain c where "c∈C" "⟨a, f ` c⟩ ∈ r ∨ a = f ` c" unfolding cofinal_fun_def by blast with ‹cofinal_fun(h,C,s)› ‹domain(h) = B› obtain b where "b ∈ B" "⟨c, h ` b⟩ ∈ s ∨ c = h ` b" unfolding cofinal_fun_def by blast moreover from this and ‹h:B → C› have "h`b ∈ C" by simp moreover note ‹f ∈ mono_map(C,s,D,r)› ‹c∈C› ultimately have "⟨f`c, f` (h ` b)⟩ ∈ r ∨ f`c = f` (h ` b)" unfolding mono_map_def by blast with ‹⟨a, f ` c⟩ ∈ r ∨ a = f ` c› ‹trans(r)› ‹h:B → C› ‹b∈B› have "⟨a, (f O h) ` b⟩ ∈ r ∨ a = (f O h) ` b" using transD by auto moreover from ‹h:B → C› ‹domain(f) = C› ‹domain(h) = B› have "domain(f O h) = B" using range_fun_subset_codomain by blast moreover note ‹b∈B› ultimately show "∃x∈domain(f O h). ⟨a, (f O h) ` x⟩ ∈ r ∨ a = (f O h) ` x" by blast qed definition cf_fun :: "[i,i] ⇒ o" where "cf_fun(f,α) ≡ cofinal_fun(f,α,Memrel(α))" lemma cf_funI[intro!]: "cofinal_fun(f,α,Memrel(α)) ⟹ cf_fun(f,α)" unfolding cf_fun_def by simp lemma cf_funD[dest!]: "cf_fun(f,α) ⟹ cofinal_fun(f,α,Memrel(α))" unfolding cf_fun_def by simp lemma cf_fun_comp: assumes "Ord(α)" "f∈ mono_map(C,s,α,Memrel(α))" "cf_fun(f,α)" "h:B → C" "cofinal_fun(h,C,s)" shows "cf_fun(f O h,α)" using assms cofinal_comp[OF _ _ _ _ trans_Memrel] by auto definition cf :: "i⇒i" where "cf(γ) ≡ μ β. ∃A. A⊆γ ∧ cofinal(A,γ,Memrel(γ)) ∧ β = ordertype(A,Memrel(γ))" lemma Ord_cf [TC]: "Ord(cf(β))" unfolding cf_def using Ord_Least by simp lemma gamma_cofinal_gamma: assumes "Ord(γ)" shows "cofinal(γ,γ,Memrel(γ))" unfolding cofinal_def by auto lemma cf_is_ordertype: assumes "Ord(γ)" shows "∃A. A⊆γ ∧ cofinal(A,γ,Memrel(γ)) ∧ cf(γ) = ordertype(A,Memrel(γ))" (is "?P(cf(γ))") using gamma_cofinal_gamma LeastI[of ?P γ] ordertype_Memrel[symmetric] assms unfolding cf_def by blast lemma cf_fun_succ': assumes "Ord(β)" "Ord(α)" "f:α→succ(β)" shows "(∃x∈α. f`x=β) ⟷ cf_fun(f,succ(β))" proof (intro iffI) assume "(∃x∈α. f`x=β)" with assms show "cf_fun(f,succ(β))" using domain_of_fun[OF ‹f:α→succ(β)›] unfolding cf_fun_def cofinal_fun_def by auto next assume "cf_fun(f,succ(β))" with assms obtain x where "x∈α" "⟨β,f`x⟩ ∈ Memrel(succ(β)) ∨ β = f ` x" using domain_of_fun[OF ‹f:α→succ(β)›] unfolding cf_fun_def cofinal_fun_def by auto moreover from ‹Ord(β)› have "⟨β,y⟩ ∉ Memrel(succ(β))" for y using foundation unfolding Memrel_def by blast ultimately show "∃x∈α. f ` x = β" by blast qed lemma cf_fun_succ: "Ord(β) ⟹ f:1→succ(β) ⟹ f`0=β ⟹ cf_fun(f,succ(β))" using cf_fun_succ' by blast lemma ordertype_0_not_cofinal_succ: assumes "ordertype(A,Memrel(succ(i))) = 0" "A⊆succ(i)" "Ord(i)" shows "¬cofinal(A,succ(i),Memrel(succ(i)))" proof have 1:"ordertype(A,Memrel(succ(i))) = ordertype(0,Memrel(0))" using ‹ordertype(A,Memrel(succ(i))) = 0› ordertype_0 by simp from ‹A⊆succ(i)› ‹Ord(i)› have "∃f. f ∈ ⟨A, Memrel(succ(i))⟩ ≅ ⟨0, Memrel(0)⟩" using well_ord_Memrel well_ord_subset ordertype_eq_imp_ord_iso[OF 1] Ord_0 by blast then have "A=0" using ord_iso_is_bij bij_imp_eqpoll eqpoll_0_is_0 by blast moreover assume "cofinal(A, succ(i), Memrel(succ(i)))" moreover note ‹Ord(i)› ultimately show "False" using not_mem_empty unfolding cofinal_def by auto qed text‹I thank Edwin Pacheco Rodríguez for the following lemma.› lemma cf_succ: assumes "Ord(α)" shows "cf(succ(α)) = 1" proof - define f where "f ≡ {⟨0,α⟩}" then have "f : 1→succ(α)" "f`0 = α" using fun_extend3[of 0 0 "succ(α)" 0 α] singleton_0 by auto with assms have "cf_fun(f,succ(α))" using cf_fun_succ unfolding cofinal_fun_def by simp from ‹f:1→succ(α)› have "0∈domain(f)" using domain_of_fun by simp define A where "A={f`0}" with ‹cf_fun(f,succ(α))› ‹0∈domain(f)› ‹f`0=α› have "cofinal(A,succ(α),Memrel(succ(α)))" unfolding cofinal_def cofinal_fun_def by simp moreover from ‹f`0=α› ‹A={f`0}› have "A ⊆ succ(α)" unfolding succ_def by auto moreover from ‹Ord(α)› ‹A⊆ succ(α)› have "well_ord(A,Memrel(succ(α)))" using Ord_succ well_ord_Memrel well_ord_subset relation_Memrel by blast moreover from ‹Ord(α)› have "¬(∃A. A ⊆ succ(α) ∧ cofinal(A, succ(α), Memrel(succ(α))) ∧ 0 = ordertype(A, Memrel(succ(α))))" (is "¬?P(0)") using ordertype_0_not_cofinal_succ unfolding cf_def by auto moreover have "1 = ordertype(A,Memrel(succ(α)))" proof - from ‹A={f`0}› have "A≈1" using singleton_eqpoll_1 by simp with ‹well_ord(A,Memrel(succ(α)))› show ?thesis using nat_1I ordertype_eq_n by simp qed ultimately show "cf(succ(α)) = 1" using Ord_1 Least_equality[of ?P 1] unfolding cf_def by blast qed lemma cf_zero [simp]: "cf(0) = 0" unfolding cf_def cofinal_def using ordertype_0 subset_empty_iff Least_le[of _ 0] by auto lemma surj_is_cofinal: "f ∈ surj(δ,γ) ⟹ cf_fun(f,γ)" unfolding surj_def cofinal_fun_def cf_fun_def using domain_of_fun by force lemma cf_zero_iff: "Ord(α) ⟹ cf(α) = 0 ⟷ α = 0" proof (intro iffI) assume "α = 0" "Ord(α)" then show "cf(α) = 0" using cf_zero by simp next assume "cf(α) = 0" "Ord(α)" moreover from this obtain A where "A⊆α" "cf(α) = ordertype(A,Memrel(α))" "cofinal(A,α,Memrel(α))" using cf_is_ordertype by blast ultimately have "cofinal(0,α,Memrel(α))" using ordertype_zero_imp_zero[of A "Memrel(α)"] by simp then show "α=0" unfolding cofinal_def by blast qed ― ‹TODO: define Succ (predicate for successor ordinals)› lemma cf_eq_one_iff: assumes "Ord(γ)" shows "cf(γ) = 1 ⟷ (∃α. Ord(α) ∧ γ = succ(α))" proof (intro iffI) assume "∃α. Ord(α) ∧ γ = succ(α)" then show "cf(γ) = 1" using cf_succ by auto next assume "cf(γ) = 1" moreover from assms obtain A where "A ⊆ γ" "cf(γ) = ordertype(A,Memrel(γ))" "cofinal(A,γ,Memrel(γ))" using cf_is_ordertype by blast ultimately have "ordertype(A,Memrel(γ)) = 1" by simp moreover define f where "f≡converse(ordermap(A,Memrel(γ)))" moreover from this ‹ordertype(A,Memrel(γ)) = 1› ‹A ⊆ γ› assms have "f ∈ surj(1,A)" using well_ord_subset[OF well_ord_Memrel, THEN ordermap_bij, THEN bij_converse_bij, of γ A] bij_is_surj by simp with ‹cofinal(A,γ,Memrel(γ))› have "∀a∈γ. ⟨a, f`0⟩ ∈ Memrel(γ) ∨ a = f`0" unfolding cofinal_def surj_def by auto with assms ‹A ⊆ γ› ‹f ∈ surj(1,A)› show "∃α. Ord(α) ∧ γ = succ(α)" using Ord_has_max_imp_succ[of γ "f`0"] surj_is_fun[of f 1 A] apply_type[of f 1 "λ_.A" 0] unfolding lt_def by (auto intro:Ord_in_Ord) qed lemma ordertype_in_cf_imp_not_cofinal: assumes "ordertype(A,Memrel(γ)) ∈ cf(γ)" "A ⊆ γ" shows "¬ cofinal(A,γ,Memrel(γ))" proof note ‹A ⊆ γ› moreover assume "cofinal(A,γ,Memrel(γ))" ultimately have "∃B. B ⊆ γ ∧ cofinal(B, γ, Memrel(γ)) ∧ ordertype(A,Memrel(γ)) = ordertype(B, Memrel(γ))" (is "?P(ordertype(A,_))") by blast moreover from assms have "ordertype(A,Memrel(γ)) < cf(γ)" using Ord_cf ltI by blast ultimately show "False" unfolding cf_def using less_LeastE[of ?P "ordertype(A,Memrel(γ))"] by auto qed lemma cofinal_mono_map_cf: assumes "Ord(γ)" shows "∃j ∈ mono_map(cf(γ), Memrel(cf(γ)), γ, Memrel(γ)) . cf_fun(j,γ)" proof - note assms moreover from this obtain A where "A ⊆ γ" "cf(γ) = ordertype(A,Memrel(γ))" "cofinal(A,γ,Memrel(γ))" using cf_is_ordertype by blast moreover define j where "j ≡ converse(ordermap(A,Memrel(γ)))" moreover from calculation have "j :cf(γ) →⇩_{<}γ" using ordertype_ord_iso[THEN ord_iso_sym, THEN ord_iso_is_mono_map, THEN mono_map_mono, of A "Memrel(γ)" γ] well_ord_Memrel[THEN well_ord_subset] by simp moreover from calculation have "j ∈ surj(cf(γ),A)" using well_ord_Memrel[THEN well_ord_subset, THEN ordertype_ord_iso, THEN ord_iso_sym, of γ A, THEN ord_iso_is_bij, THEN bij_is_surj] by simp with ‹cofinal(A,γ,Memrel(γ))› have "cf_fun(j,γ)" using cofinal_range_iff_cofinal_fun[of j γ "Memrel(γ)"] surj_range[of j "cf(γ)" A] surj_is_fun fun_is_function by fastforce with ‹j ∈ mono_map(_,_,_,_)› show ?thesis by auto qed subsection‹The factorization lemma› text‹In this subsection we prove a factorization lemma for cofinal functions into ordinals, which shows that any cofinal function between ordinals can be ``decomposed'' in such a way that a commutative triangle of strictly increasing maps arises. The factorization lemma has a kind of fundamental character, in that the rest of the basic results on cofinality (for, instance, idempotence) follow easily from it, in a more algebraic way. This is a consequence that the proof encapsulates uses of transfinite recursion in the basic theory of cofinality; indeed, only one use is needed. In the setting of Isabelle/ZF, this is convenient since the machinery of recursion is pretty clumsy. On the downside, this way of presenting things results in a longer proof of the factorization lemma. This approach was taken by the author in the notes \<^cite>‹"apunte_st"› for an introductory course in Set Theory. To organize the use of the hypotheses of the factorization lemma, we set up a locale containing all the relevant ingredients. › locale cofinal_factor = fixes j δ ξ γ f assumes j_mono: "j :ξ →⇩_{<}γ" and ords: "Ord(δ)" "Ord(ξ)" "Limit(γ)" and f_type: "f: δ → γ" begin text‹Here, \<^term>‹f› is cofinal function from \<^term>‹δ› to \<^term>‹γ›, and the ordinal \<^term>‹ξ› is meant to be the cofinality of \<^term>‹γ›. Hence, there exists an increasing map \<^term>‹j› from \<^term>‹ξ› to \<^term>‹γ› by the last lemma. The main goal is to construct an increasing function \<^term>‹g:ξ→δ› such that the composition \<^term>‹f O g› is still cofinal but also increasing.› definition factor_body :: "[i,i,i] ⇒ o" where "factor_body(β,h,x) ≡ (x∈δ ∧ j`β ≤ f`x ∧ (∀α<β . f`(h`α) < f`x)) ∨ x=δ" definition factor_rec :: "[i,i] ⇒ i" where "factor_rec(β,h) ≡ μ x. factor_body(β,h,x)" text‹\<^term>‹factor_rec› is the inductive step for the definition by transfinite recursion of the ∗‹factor› function (called \<^term>‹g› above), which in turn is obtained by minimizing the predicate \<^term>‹factor_body›. Next we show that this predicate is monotonous.› lemma factor_body_mono: assumes "β∈ξ" "α<β" "factor_body(β,λx∈β. G(x),x)" shows "factor_body(α,λx∈α. G(x),x)" proof - from ‹α<β› have "α∈β" using ltD by simp moreover note ‹β∈ξ› moreover from calculation have "α∈ξ" using ords ltD Ord_cf Ord_trans by blast ultimately have "j`α ∈ j`β" using j_mono mono_map_increasing by blast moreover from ‹β∈ξ› have "j`β∈γ" using j_mono domain_of_fun apply_rangeI mono_map_is_fun by force moreover from this have "Ord(j`β)" using Ord_in_Ord ords Limit_is_Ord by auto ultimately have "j`α ≤ j`β" unfolding lt_def by blast then have "j`β ≤ f`θ ⟹ j`α ≤ f`θ" for θ using le_trans by blast moreover have "f`((λw∈α. G(w))`y) < f`z" if "z∈δ" "∀x<β. f`((λw∈β. G(w))`x) < f`z" "y<α" for y z proof - note ‹y<α› also note ‹α<β› finally have "y<β" by simp with ‹∀x<β. f`((λw∈β. G(w))`x) < f`z› have "f ` ((λw∈β. G(w)) ` y) < f ` z" by simp moreover from ‹y<α› ‹y<β› have "(λw∈β. G(w)) ` y = (λw∈α. G(w)) ` y" using beta_if by (auto dest:ltD) ultimately show ?thesis by simp qed moreover note ‹factor_body(β,λx∈β. G(x),x)› ultimately show ?thesis unfolding factor_body_def by blast qed lemma factor_body_simp[simp]: "factor_body(α,g,δ)" unfolding factor_body_def by simp lemma factor_rec_mono: assumes "β∈ξ" "α<β" shows "factor_rec(α,λx∈α. G(x)) ≤ factor_rec(β,λx∈β. G(x))" unfolding factor_rec_def using assms ords factor_body_mono Least_antitone by simp text‹We now define the factor as higher-order function. Later it will be restricted to a set to obtain a bona fide function of type @{typ i}.› definition factor :: "i ⇒ i" where "factor(β) ≡ transrec(β,factor_rec)" lemma factor_unfold: "factor(α) = factor_rec(α,λx∈α. factor(x))" using def_transrec[OF factor_def] . lemma factor_mono: assumes "β∈ξ" "α<β" "factor(α)≠δ" "factor(β)≠δ" shows "factor(α) ≤ factor(β)" proof - have "factor(α) = factor_rec(α, λx∈α. factor(x))" using factor_unfold . also from assms and factor_rec_mono have "... ≤ factor_rec(β, λx∈β. factor(x))" by simp also have "factor_rec(β, λx∈β. factor(x)) = factor(β)" using def_transrec[OF factor_def, symmetric] . finally show ?thesis . qed text‹The factor satisfies the predicate body of the minimization.› lemma factor_body_factor: "factor_body(α,λx∈α. factor(x),factor(α))" using ords factor_unfold[of α] LeastI[of "factor_body(_,_)" δ] unfolding factor_rec_def by simp lemma factor_type [TC]: "Ord(factor(α))" using ords factor_unfold[of α] unfolding factor_rec_def by simp text‹The value \<^term>‹δ› in \<^term>‹factor_body› (and therefore, in \<^term>‹factor›) is meant to be a ``default value''. Whenever it is not attained, the factor function behaves as expected: It is increasing and its composition with \<^term>‹f› also is.› lemma f_factor_increasing: assumes "β∈ξ" "α<β" "factor(β)≠δ" shows "f`factor(α) < f`factor(β)" proof - from assms have "f ` ((λx∈β. factor(x)) ` α) < f ` factor(β)" using factor_unfold[of β] ords LeastI[of "factor_body(β,λx∈β. factor(x))"] unfolding factor_rec_def factor_body_def by (auto simp del:beta_if) with ‹α<β› show ?thesis using ltD by auto qed lemma factor_increasing: assumes "β∈ξ" "α<β" "factor(α)≠δ" "factor(β)≠δ" shows "factor(α)<factor(β)" using assms f_factor_increasing factor_mono by (force intro:le_neq_imp_lt) lemma factor_in_delta: assumes "factor(β) ≠ δ" shows "factor(β) ∈ δ" using assms factor_body_factor ords unfolding factor_body_def by auto text‹Finally, we define the (set) factor function as the restriction of factor to the ordinal \<^term>‹ξ›.› definition fun_factor :: "i" where "fun_factor ≡ λβ∈ξ. factor(β)" lemma fun_factor_is_mono_map: assumes "⋀β. β ∈ ξ ⟹ factor(β) ≠ δ" shows "fun_factor ∈ mono_map(ξ, Memrel(ξ), δ, Memrel(δ))" unfolding mono_map_def proof (intro CollectI ballI impI) text‹Proof that \<^term>‹fun_factor› respects membership:› fix α β assume "α∈ξ" "β∈ξ" moreover note assms moreover from calculation have "factor(α)≠δ" "factor(β)≠δ" "Ord(β)" using factor_in_delta Ord_in_Ord ords by auto moreover assume "⟨α, β⟩ ∈ Memrel(ξ)" ultimately show "⟨fun_factor ` α, fun_factor ` β⟩ ∈ Memrel(δ)" unfolding fun_factor_def using ltI factor_increasing[THEN ltD] factor_in_delta by simp next text‹Proof that it has the appropriate type:› from assms show "fun_factor : ξ → δ" unfolding fun_factor_def using ltI lam_type factor_in_delta by simp qed lemma f_fun_factor_is_mono_map: assumes "⋀β. β ∈ ξ ⟹ factor(β) ≠ δ" shows "f O fun_factor ∈ mono_map(ξ, Memrel(ξ), γ, Memrel(γ))" unfolding mono_map_def using f_type proof (intro CollectI ballI impI comp_fun[of _ _ δ]) from assms show "fun_factor : ξ → δ" using fun_factor_is_mono_map mono_map_is_fun by simp text‹Proof that \<^term>‹f O fun_factor› respects membership› fix α β assume "⟨α, β⟩ ∈ Memrel(ξ)" then have "α<β" using Ord_in_Ord[of "ξ"] ltI ords by blast assume "α∈ξ" "β∈ξ" moreover from this and assms have "factor(α)≠δ" "factor(β)≠δ" by auto moreover have "Ord(γ)" "γ≠0" using ords Limit_is_Ord by auto moreover note ‹α<β› ‹fun_factor : ξ → δ› ultimately show "⟨(f O fun_factor) ` α, (f O fun_factor) ` β⟩ ∈ Memrel(γ)" using ltD[of "f ` factor(α)" "f ` factor(β)"] f_factor_increasing apply_in_codomain_Ord f_type unfolding fun_factor_def by auto qed end ― ‹\<^locale>‹cofinal_factor›› text‹We state next the factorization lemma.› lemma cofinal_fun_factorization: notes le_imp_subset [dest] lt_trans2 [trans] assumes "Ord(δ)" "Limit(γ)" "f: δ → γ" "cf_fun(f,γ)" shows "∃g ∈ cf(γ) →⇩_{<}δ. f O g : cf(γ) →⇩_{<}γ ∧ cofinal_fun(f O g,γ,Memrel(γ))" proof - from ‹Limit(γ)› have "Ord(γ)" using Limit_is_Ord by simp then obtain j where "j :cf(γ) →⇩_{<}γ" "cf_fun(j,γ)" using cofinal_mono_map_cf by blast then have "domain(j) = cf(γ)" using domain_of_fun mono_map_is_fun by force from ‹j ∈ _› assms interpret cofinal_factor j δ "cf(γ)" by (unfold_locales) (simp_all) text‹The core of the argument is to show that the factor function indeed maps into \<^term>‹δ›, therefore its values satisfy the first disjunct of \<^term>‹factor_body›. This holds in turn because no restriction of the factor composed with \<^term>‹f› to a proper initial segment of \<^term>‹cf(γ)› can be cofinal in \<^term>‹γ› by definition of cofinality. Hence there must be a witness that satisfies the first disjunct.› have factor_not_delta: "factor(β)≠δ" if "β ∈ cf(γ)" for β text‹For this, we induct on \<^term>‹β› ranging over \<^term>‹cf(γ)›.› proof (induct β rule:Ord_induct[OF _ Ord_cf[of γ]]) case 1 with that show ?case . next case (2 β) then have IH: "z∈β ⟹ factor(z)≠δ" for z by simp define h where "h ≡ λx∈β. f`factor(x)" from IH have "z∈β ⟹ factor(z) ∈ δ" for z using factor_in_delta by blast with ‹f:δ→γ› have "h : β → γ" unfolding h_def using apply_funtype lam_type by auto then have "h : β →⇩_{<}γ" unfolding mono_map_def proof (intro CollectI ballI impI) fix x y assume "x∈β" "y∈β" moreover from this and IH have "factor(y) ≠ δ" by simp moreover from calculation and ‹h ∈ β → γ› have "h`x ∈ γ" "h`y ∈ γ" by simp_all moreover from ‹β∈cf(γ)› and ‹y∈β› have "y ∈ cf(γ)" using Ord_trans Ord_cf by blast moreover from this have "Ord(y)" using Ord_cf Ord_in_Ord by blast moreover assume "⟨x,y⟩ ∈ Memrel(β)" moreover from calculation have "x<y" by (blast intro:ltI) ultimately show "⟨h ` x, h ` y⟩ ∈ Memrel(γ)" unfolding h_def using f_factor_increasing ltD by (auto) qed with ‹β∈cf(γ)› ‹Ord(γ)› have "ordertype(h``β,Memrel(γ)) = β" (* Maybe should use range(h) *) using mono_map_ordertype_image[of β] Ord_cf Ord_in_Ord by blast also note ‹β ∈cf(γ)› finally have "ordertype(h``β,Memrel(γ)) ∈ cf(γ)" by simp moreover from ‹h ∈ β → γ› have "h``β ⊆ γ" using mono_map_is_fun Image_sub_codomain by blast ultimately have "¬ cofinal(h``β,γ,Memrel(γ))" using ordertype_in_cf_imp_not_cofinal by simp then obtain α_0 where "α_0∈γ" "∀x∈h `` β. ¬ ⟨α_0, x⟩ ∈ Memrel(γ) ∧ α_0 ≠ x" unfolding cofinal_def by auto with ‹Ord(γ)› ‹h``β ⊆ γ› have "∀x∈h `` β. x ∈ α_0" using well_ord_Memrel[of γ] well_ord_is_linear[of γ "Memrel(γ)"] unfolding linear_def by blast from ‹α_0 ∈ γ› ‹j ∈ mono_map(_,_,γ,_)› ‹Ord(γ)› have "j`β ∈ γ" using mono_map_is_fun apply_in_codomain_Ord by force with ‹α_0 ∈ γ› ‹Ord(γ)› have "α_0 ∪ j`β ∈ γ" using Un_least_mem_iff Ord_in_Ord by auto with ‹cf_fun(f,γ)› obtain θ where "θ∈domain(f)" "⟨α_0 ∪ j`β, f ` θ⟩ ∈ Memrel(γ) ∨ α_0 ∪ j`β = f ` θ" by (auto simp add:cofinal_fun_def) blast moreover from this and ‹f:δ→γ› have "θ ∈ δ" using domain_of_fun by auto moreover note ‹Ord(γ)› moreover from this and ‹f:δ→γ› ‹α_0 ∈ γ› have "Ord(f`θ)" using apply_in_codomain_Ord Ord_in_Ord by blast moreover from calculation and ‹α_0 ∈ γ› and ‹Ord(δ)› and ‹j`β ∈ γ› have "Ord(α_0)" "Ord(j`β)" "Ord(θ)" using Ord_in_Ord by auto moreover from ‹∀x∈h `` β. x ∈ α_0› ‹Ord(α_0)› ‹h:β→γ› have "x∈β ⟹ h`x < α_0" for x using fun_is_function[of h β "λ_. γ"] Image_subset_Ord_imp_lt domain_of_fun[of h β "λ_. γ"] by blast moreover have "x∈β ⟹ h`x < f`θ" for x proof - fix x assume "x∈β" with ‹∀x∈h `` β. x ∈ α_0› ‹Ord(α_0)› ‹h:β→γ› have "h`x < α_0" using fun_is_function[of h β "λ_. γ"] Image_subset_Ord_imp_lt domain_of_fun[of h β "λ_. γ"] by blast also from ‹⟨α_0 ∪ _, f ` θ⟩ ∈ Memrel(γ) ∨ α_0 ∪ _= f ` θ› ‹Ord(f`θ)› ‹Ord(α_0)› ‹Ord(j`β)› have "α_0 ≤ f`θ" using Un_leD1[OF leI [OF ltI]] Un_leD1[OF le_eqI] by blast finally show "h`x < f`θ" . qed ultimately have "factor_body(β,λx∈β. factor(x),θ)" unfolding h_def factor_body_def using ltD by (auto dest:Un_memD2 Un_leD2[OF le_eqI]) with ‹Ord(θ)› have "factor(β) ≤ θ" using factor_unfold[of β] Least_le unfolding factor_rec_def by auto with ‹θ∈δ› ‹Ord(δ)› have "factor(β) ∈ δ" using leI[of θ] ltI[of θ] by (auto dest:ltD) then show ?case by (auto elim:mem_irrefl) qed moreover have "cofinal_fun(f O fun_factor, γ, Memrel(γ))" proof (intro cofinal_funI) fix a assume "a ∈ γ" with ‹cf_fun(j,γ)› ‹domain(j) = cf(γ)› obtain x where "x∈cf(γ)" "a ∈ j`x ∨ a = j`x" by (auto simp add:cofinal_fun_def) blast with factor_not_delta have "x ∈ domain(f O fun_factor)" using f_fun_factor_is_mono_map mono_map_is_fun domain_of_fun by force moreover have "a ∈ (f O fun_factor) `x ∨ a = (f O fun_factor) `x" proof - from ‹x∈cf(γ)› factor_not_delta have "j ` x ≤ f ` factor(x)" using mem_not_refl factor_body_factor factor_in_delta unfolding factor_body_def by auto with ‹a ∈ j`x ∨ a = j`x› have "a ∈ f ` factor(x) ∨ a = f ` factor(x)" using ltD by blast with ‹x∈cf(γ)› show ?thesis using lam_funtype[of "cf(γ)" factor] unfolding fun_factor_def by auto qed moreover note ‹a ∈ γ› moreover from calculation and ‹Ord(γ)› and factor_not_delta have "(f O fun_factor) `x ∈ γ" using Limit_nonzero apply_in_codomain_Ord mono_map_is_fun[of "f O fun_factor"] f_fun_factor_is_mono_map by blast ultimately show "∃x ∈ domain(f O fun_factor). ⟨a, (f O fun_factor) ` x⟩ ∈ Memrel(γ) ∨ a = (f O fun_factor) `x" by blast qed ultimately show ?thesis using fun_factor_is_mono_map f_fun_factor_is_mono_map by blast qed text‹As a final observation in this part, we note that if the original cofinal map was increasing, then the factor function is also cofinal.› lemma factor_is_cofinal: assumes "Ord(δ)" "Ord(γ)" "f :δ →⇩_{<}γ" "f O g ∈ mono_map(α,r,γ,Memrel(γ))" "cofinal_fun(f O g,γ,Memrel(γ))" "g: α → δ" shows "cf_fun(g,δ)" unfolding cf_fun_def cofinal_fun_def proof fix a assume "a ∈ δ" with ‹f ∈ mono_map(δ,_,γ,_)› have "f`a ∈ γ" using mono_map_is_fun by force with ‹cofinal_fun(f O g,γ,_)› obtain y where "y∈α" "⟨f`a, (f O g) ` y⟩ ∈ Memrel(γ) ∨ f`a = (f O g) ` y" unfolding cofinal_fun_def using domain_of_fun[OF ‹g:α → δ›] by blast with ‹g:α → δ› have "⟨f`a, f ` (g ` y)⟩ ∈ Memrel(γ) ∨ f`a = f ` (g ` y)" "g`y ∈ δ" using comp_fun_apply[of g α δ y f] by auto with assms(1-3) and ‹a∈δ› have "⟨a, g ` y⟩ ∈ Memrel(δ) ∨ a = g ` y" using Memrel_mono_map_reflects Memrel_mono_map_is_inj[of δ f γ γ] inj_apply_equality[of f δ γ] by blast with ‹y∈α› show "∃x∈domain(g). ⟨a, g ` x⟩ ∈ Memrel(δ) ∨ a = g ` x" using domain_of_fun[OF ‹g:α → δ›] by blast qed subsection‹Classical results on cofinalities› text‹Now the rest of the results follow in a more algebraic way. The next proof one invokes a case analysis on whether the argument is zero, a successor ordinal or a limit one; the last case being the most relevant one and is immediate from the factorization lemma.› lemma cf_le_domain_cofinal_fun: assumes "Ord(γ)" "Ord(δ)" "f:δ → γ" "cf_fun(f,γ)" shows "cf(γ)≤δ" using assms proof (cases rule:Ord_cases) case 0 with ‹Ord(δ)› show ?thesis using Ord_0_le by simp next case (succ γ) with assms obtain x where "x∈δ" "f`x=γ" using cf_fun_succ' by blast then have "δ≠0" by blast let ?f="{⟨0,f`x⟩}" from ‹f`x=γ› have "?f:1→succ(γ)" using singleton_0 singleton_fun[of 0 γ] singleton_subsetI fun_weaken_type by simp with ‹Ord(γ)› ‹f`x=γ› have "cf(succ(γ)) = 1" using cf_succ by simp with ‹δ≠0› succ show ?thesis using Ord_0_lt_iff succ_leI ‹Ord(δ)› by simp next case (limit) with assms obtain g where "g :cf(γ) →⇩_{<}δ" using cofinal_fun_factorization by blast with assms show ?thesis using mono_map_imp_le by simp qed lemma cf_ordertype_cofinal: assumes "Limit(γ)" "A⊆γ" "cofinal(A,γ,Memrel(γ))" shows "cf(γ) = cf(ordertype(A,Memrel(γ)))" proof (intro le_anti_sym) text‹We show the result by proving the two inequalities.› from ‹Limit(γ)› have "Ord(γ)" using Limit_is_Ord by simp with ‹A ⊆ γ› have "well_ord(A,Memrel(γ))" using well_ord_Memrel well_ord_subset by blast then obtain f α where "f:⟨α, Memrel(α)⟩ ≅ ⟨A,Memrel(γ)⟩" "Ord(α)" "α = ordertype(A,Memrel(γ))" using ordertype_ord_iso Ord_ordertype ord_iso_sym by blast moreover from this have "f: α → A" using ord_iso_is_mono_map mono_map_is_fun[of f _ "Memrel(α)"] by blast moreover from this have "function(f)" using fun_is_function by simp moreover from ‹f:⟨α, Memrel(α)⟩ ≅ ⟨A,Memrel(γ)⟩› have "range(f) = A" using ord_iso_is_bij bij_is_surj surj_range by blast moreover note ‹cofinal(A,γ,_)› ultimately have "cf_fun(f,γ)" using cofinal_range_iff_cofinal_fun by blast moreover from ‹Ord(α)› obtain h where "h :cf(α) →⇩_{<}α" "cf_fun(h,α)" using cofinal_mono_map_cf by blast moreover from ‹Ord(γ)› have "trans(Memrel(γ))" using trans_Memrel by simp moreover note ‹A⊆γ› ultimately have "cofinal_fun(f O h,γ,Memrel(γ))" using cofinal_comp ord_iso_is_mono_map[OF ‹f:⟨α,_⟩ ≅ ⟨A,_⟩›] mono_map_is_fun mono_map_mono by blast moreover from ‹f:α→A› ‹A⊆γ› ‹h∈mono_map(cf(α),_,α,_)› have "f O h : cf(α) → γ" using Pi_mono[of A γ] comp_fun mono_map_is_fun by blast moreover note ‹Ord(γ)› ‹Ord(α)› ‹α = ordertype(A,Memrel(γ))› ultimately show "cf(γ) ≤ cf(ordertype(A,Memrel(γ)))" using cf_le_domain_cofinal_fun[of _ _ "f O h"] by (auto simp add:cf_fun_def) text‹That finishes the first inequality. Now we go the other side.› from ‹f:⟨α, _⟩ ≅ ⟨A,_⟩› ‹A⊆γ› have "f :α →⇩_{<}γ" using mono_map_mono[OF ord_iso_is_mono_map] by simp then have "f: α → γ" using mono_map_is_fun by simp with ‹cf_fun(f,γ)› ‹Limit(γ)› ‹Ord(α)› obtain g where "g :cf(γ) →⇩_{<}α" "f O g :cf(γ) →⇩_{<}γ" "cofinal_fun(f O g,γ,Memrel(γ))" using cofinal_fun_factorization by blast moreover from this have "g:cf(γ)→α" using mono_map_is_fun by simp moreover note ‹Ord(α)› moreover from calculation and ‹f :α →⇩_{<}γ› ‹Ord(γ)› have "cf_fun(g,α)" using factor_is_cofinal by blast moreover note ‹α = ordertype(A,Memrel(γ))› ultimately show "cf(ordertype(A,Memrel(γ))) ≤ cf(γ)" using cf_le_domain_cofinal_fun[OF _ Ord_cf mono_map_is_fun] by simp qed lemma cf_idemp: assumes "Limit(γ)" shows "cf(γ) = cf(cf(γ))" proof - from assms obtain A where "A⊆γ" "cofinal(A,γ,Memrel(γ))" "cf(γ) = ordertype(A,Memrel(γ))" using Limit_is_Ord cf_is_ordertype by blast with assms have "cf(γ) = cf(ordertype(A,Memrel(γ)))" using cf_ordertype_cofinal by simp also have "... = cf(cf(γ))" using ‹cf(γ) = ordertype(A,Memrel(γ))› by simp finally show "cf(γ) = cf(cf(γ))" . qed lemma cf_le_cardinal: assumes "Limit(γ)" shows "cf(γ) ≤ |γ|" proof - from assms have ‹Ord(γ)› using Limit_is_Ord by simp then obtain f where "f ∈ surj(|γ|,γ)" using Ord_cardinal_eqpoll unfolding eqpoll_def bij_def by blast with ‹Ord(γ)› show ?thesis using Card_is_Ord[OF Card_cardinal] surj_is_cofinal cf_le_domain_cofinal_fun[of γ] surj_is_fun by blast qed lemma regular_is_Card: notes le_imp_subset [dest] assumes "Limit(γ)" "γ = cf(γ)" shows "Card(γ)" proof - from assms have "|γ| ⊆ γ" using Limit_is_Ord Ord_cardinal_le by blast also from ‹γ = cf(γ)› have "γ ⊆ cf(γ)" by simp finally have "|γ| ⊆ cf(γ)" . with assms show ?thesis unfolding Card_def using cf_le_cardinal by force qed lemma Limit_cf: assumes "Limit(κ)" shows "Limit(cf(κ))" using Ord_cf[of κ, THEN Ord_cases] ― ‹\<^term>‹cf(κ)› being $0$ or successor leads to contradiction› proof (cases) case 1 with ‹Limit(κ)› show ?thesis using cf_zero_iff Limit_is_Ord by simp next case (2 α) moreover note ‹Limit(κ)› moreover from calculation have "cf(κ) = 1" using cf_idemp cf_succ by fastforce ultimately show ?thesis using succ_LimitE cf_eq_one_iff Limit_is_Ord by auto qed lemma InfCard_cf: "Limit(κ) ⟹ InfCard(cf(κ))" using regular_is_Card cf_idemp Limit_cf nat_le_Limit Limit_cf unfolding InfCard_def by simp lemma cf_le_cf_fun: notes [dest] = Limit_is_Ord assumes "cf(κ) ≤ ν" "Limit(κ)" shows "∃f. f:ν → κ ∧ cf_fun(f, κ)" proof - note assms moreover from this obtain h where h_cofinal_mono: "cf_fun(h,κ)" "h :cf(κ) →⇩_{<}κ" "h : cf(κ) → κ" using cofinal_mono_map_cf mono_map_is_fun by force moreover from calculation obtain g where "g ∈ inj(cf(κ), ν)" using le_imp_lepoll by blast from this and calculation(2,3,5) obtain f where "f ∈ surj(ν, cf(κ))" "f: ν → cf(κ)" using inj_imp_surj[OF _ Limit_has_0[THEN ltD]] surj_is_fun Limit_cf by blast moreover from this have "cf_fun(f,cf(κ))" using surj_is_cofinal by simp moreover note h_cofinal_mono ‹Limit(κ)› moreover from calculation have "cf_fun(h O f,κ)" using cf_fun_comp by blast moreover from calculation have "h O f ∈ ν -> κ" using comp_fun by simp ultimately show ?thesis by blast qed lemma Limit_cofinal_fun_lt: notes [dest] = Limit_is_Ord assumes "Limit(κ)" "f: ν → κ" "cf_fun(f,κ)" "n∈κ" shows "∃α∈ν. n < f`α" proof - from ‹Limit(κ)› ‹n∈κ› have "succ(n) ∈ κ" using Limit_has_succ[OF _ ltI, THEN ltD] by auto moreover note ‹f: ν → _› moreover from this have "domain(f) = ν" using domain_of_fun by simp moreover note ‹cf_fun(f,κ)› ultimately obtain α where "α ∈ ν" "succ(n) ∈ f`α ∨ succ(n) = f `α" using cf_funD[THEN cofinal_funD] by blast moreover from this consider (1) "succ(n) ∈ f`α" | (2) "succ(n) = f `α" by blast then have "n < f`α" proof (cases) case 1 moreover have "n ∈ succ(n)" by simp moreover note ‹Limit(κ)› ‹f: ν → _› ‹α ∈ ν› moreover from this have "Ord(f ` α)" using apply_type[of f ν "λ_. κ", THEN [2] Ord_in_Ord] by blast ultimately show ?thesis using Ord_trans[of n "succ(n)" "f ` α"] ltI by blast next case 2 have "n ∈ f ` α" by (simp add:2[symmetric]) with ‹Limit(κ)› ‹f: ν → _› ‹α ∈ ν› show ?thesis using ltI apply_type[of f ν "λ_. κ", THEN [2] Ord_in_Ord] by blast qed ultimately show ?thesis by blast qed context includes Ord_dests Aleph_dests Aleph_intros Aleph_mem_dests mono_map_rules begin text‹We end this section by calculating the cofinality of Alephs, for the zero and limit case. The successor case depends on $\AC$.› lemma cf_nat: "cf(ω) = ω" using Limit_nat[THEN InfCard_cf] cf_le_cardinal[of ω] Card_nat[THEN Card_cardinal_eq] le_anti_sym unfolding InfCard_def by auto lemma cf_Aleph_zero: "cf(ℵ⇘0⇙) = ℵ⇘0⇙" using cf_nat unfolding Aleph_def by simp lemma cf_Aleph_Limit: assumes "Limit(γ)" shows "cf(ℵ⇘γ⇙) = cf(γ)" proof - note ‹Limit(γ)› moreover from this have "(λx∈γ. ℵ⇘x⇙) : γ → ℵ⇘γ⇙" (is "?f : _ → _") using lam_funtype[of _ Aleph] fun_weaken_type[of _ _ _ "ℵ⇘γ⇙"] by blast moreover from ‹Limit(γ)› have "x ∈ y ⟹ ℵ⇘x⇙ ∈ ℵ⇘y⇙" if "x ∈ γ" "y ∈ γ" for x y using that Ord_in_Ord[of γ] Ord_trans[of _ _ γ] by blast ultimately have "?f ∈ mono_map(γ,Memrel(γ),ℵ⇘γ⇙, Memrel(ℵ⇘γ⇙))" by auto with ‹Limit(γ)› have "?f ∈ ⟨γ, Memrel(γ)⟩ ≅ ⟨?f``γ, Memrel(ℵ⇘γ⇙)⟩" using mono_map_imp_ord_iso_Memrel[of γ "ℵ⇘γ⇙" ?f] Card_Aleph (* Already an intro rule, but need it explicitly *) by blast then have "converse(?f) ∈ ⟨?f``γ, Memrel(ℵ⇘γ⇙)⟩ ≅ ⟨γ, Memrel(γ)⟩" using ord_iso_sym by simp with ‹Limit(γ)› have "ordertype(?f``γ, Memrel(ℵ⇘γ⇙)) = γ" using ordertype_eq[OF _ well_ord_Memrel] ordertype_Memrel by auto moreover from ‹Limit(γ)› have "cofinal(?f``γ, ℵ⇘γ⇙, Memrel(ℵ⇘γ⇙))" unfolding cofinal_def proof (standard, intro ballI) fix a assume "a∈ℵ⇘γ⇙" "ℵ⇘γ⇙ = (⋃i<γ. ℵ⇘i⇙)" moreover from this obtain i where "i<γ" "a∈ℵ⇘i⇙" by auto moreover from this and ‹Limit(γ)› have "Ord(i)" using ltD Ord_in_Ord by blast moreover from ‹Limit(γ)› and calculation have "succ(i) ∈ γ" using ltD by auto moreover from this and ‹Ord(i)› have "ℵ⇘i⇙ < ℵ⇘succ(i)⇙" by (auto) ultimately have "⟨a,ℵ⇘i⇙⟩ ∈ Memrel(ℵ⇘γ⇙)" using ltD by (auto dest:Aleph_increasing) moreover from ‹i<γ› have "ℵ⇘i⇙ ∈ ?f``γ" using ltD apply_in_image[OF ‹?f : _ → _›] by auto ultimately show "∃x∈?f `` γ. ⟨a, x⟩ ∈ Memrel(ℵ⇘γ⇙) ∨ a = x" by blast qed moreover note ‹?f: γ → ℵ⇘γ⇙› ‹Limit(γ)› ultimately show "cf(ℵ⇘γ⇙) = cf(γ)" using cf_ordertype_cofinal[OF Limit_Aleph Image_sub_codomain, of γ ?f γ γ ] Limit_is_Ord by simp qed end ― ‹includes› end