Theory Twelvefold_Way_Entry9

(*  Author: Lukas Bulwahn <lukas.bulwahn-at-gmail.com> *)

section ‹Surjections from A to B up to a Permutation on B›

theory Twelvefold_Way_Entry9
imports Twelvefold_Way_Entry7
begin

subsection ‹Properties for Bijections›

lemma surjective_on_implies_card_eq:
  assumes "f ` A = B"
  shows "card ((λb. {x ∈ A. f x = b}) ` B - {{}}) = card B"
proof -
  from ‹f ` A = B› have "{} ∉ (λb. {x ∈ A. f x = b}) ` B" by auto
  from ‹f ` A = B› have "inj_on (λb. {x ∈ A. f x = b}) B" by (fastforce intro: inj_onI)
  have "card ((λb. {x ∈ A. f x = b}) ` B - {{}}) = card ((λb. {x ∈ A. f x = b}) ` B)"
    using ‹{} ∉ (λb. {x ∈ A. f x = b}) ` B› by simp
  also have "… = card B"
    using ‹inj_on (λb. {x ∈ A. f x = b}) B› by (rule card_image)
  finally show ?thesis .
qed

lemma card_eq_implies_surjective_on:
  assumes "finite B" "f ∈ A →⇩E B"
  assumes card_eq: "card ((λb. {x ∈ A. f x = b}) ` B - {{}}) = card B"
  shows "f ` A = B"
proof
  from ‹f ∈ A →⇩E B› show "f ` A ⊆ B" by auto
next
  show "B ⊆ f ` A"
  proof
    fix x
    assume "x ∈ B"
    have "{} ∉ (λb. {x ∈ A. f x = b}) ` B"
    proof (cases "card B ≥ 1")
      assume "¬ card B ≥ 1"
      from this have "card B = 0" by simp
      from this ‹finite B› have "B = {}" by simp
      from this show ?thesis by simp
    next
      assume "card B ≥ 1"
      show ?thesis
      proof (rule ccontr)
        assume "¬ {} ∉ (λb. {x ∈ A. f x = b}) ` B"
        from this have "{} ∈ (λb. {x ∈ A. f x = b}) ` B" by simp
        moreover have "card ((λb. {x ∈ A. f x = b}) ` B) ≤ card B"
          using ‹finite B› card_image_le by blast
        moreover have "finite ((λb. {x ∈ A. f x = b}) ` B)"
          using ‹finite B› by auto
        ultimately have "card ((λb. {x ∈ A. f x = b}) ` B - {{}}) ≤ card B - 1"
          by (auto simp add: card_Diff_singleton)
        from this card_eq ‹card B ≥ 1› show False by auto
      qed
    qed
    from this ‹x ∈ B› show "x ∈ f ` A" by force
  qed
qed

lemma card_partitions_of:
  assumes "F ∈ (A →⇩E B) // range_permutation A B"
  assumes "univ (λf. f ` A = B) F"
  shows "card (partitions_of A B F) = card B"
proof -
  from ‹F ∈ (A →⇩E B) // range_permutation A B› obtain f where "f ∈ A →⇩E B"
    and F_eq: "F = range_permutation A B `` {f}" using quotientE by blast
  from this ‹univ (λf. f ` A = B) F› have "f ` A = B"
    using univ_commute'[OF equiv_range_permutation surj_on_respects_range_permutation ‹f ∈ A →⇩E B›] by simp
  have "card (partitions_of A B F) = card (univ (λf. (λb. {x ∈ A. f x = b}) ` B - {{}}) F)"
    unfolding partitions_of_def ..
  also have "… = card (univ (λf. (λb. {x ∈ A. f x = b}) ` B - {{}}) (range_permutation A B `` {f}))"
    unfolding F_eq ..
  also have "… = card ((λb. {x ∈ A. f x = b}) ` B - {{}})"
    using equiv_range_permutation domain_partitions_respects_range_permutation ‹f ∈ A →⇩E B›
    by (subst univ_commute') auto
  also from ‹f ` A = B› have "… = card B"
    using surjective_on_implies_card_eq by auto
  finally show ?thesis .
qed

lemma functions_of_is_surj_on:
  assumes "finite A" "finite B"
  assumes "partition_on A P" "card P = card B"
  shows "univ (λf. f ` A = B) (functions_of P A B)"
proof -
  have "functions_of P A B ∈ (A →⇩E B) // range_permutation A B"
    using functions_of ‹finite A› ‹finite B› ‹partition_on A P› ‹card P = card B› by fastforce
  from this obtain f where eq_f: "functions_of P A B = range_permutation A B `` {f}" and "f ∈ A →⇩E B"
    using quotientE by blast
  from eq_f have "f ∈ functions_of P A B"
    using ‹f ∈ A →⇩E B› equiv_range_permutation equiv_class_self by fastforce
  from ‹f ∈ functions_of P A B› have eq: "(λb. {x ∈ A. f x = b}) ` B - {{}} = P"
    unfolding functions_of_def by auto
  from this have "card ((λb. {x ∈ A. f x = b}) ` B - {{}}) = card B"
    using ‹card P = card B› by simp
  from ‹finite B› ‹f ∈ A →⇩E B› this have "f ` A = B"
    using card_eq_implies_surjective_on by blast
  from this show ?thesis
    unfolding eq_f using equiv_range_permutation surj_on_respects_range_permutation ‹f ∈ A →⇩E B›
    by (subst univ_commute') assumption+
qed

subsection ‹Bijections›

lemma bij_betw_partitions_of:
  assumes "finite A" "finite B"
  shows "bij_betw (partitions_of A B) ({f ∈ A →⇩E B. f ` A = B} // range_permutation A B) {P. partition_on A P ∧ card P = card B}"
proof (rule bij_betw_byWitness[where f'="λP. functions_of P A B"])
  have quotient_eq: "{f ∈ A →⇩E B. f ` A = B} // range_permutation A B = {F ∈ ((A →⇩E B) // range_permutation A B). univ (λf. f ` A = B) F}"
  using equiv_range_permutation[of A B] surj_on_respects_range_permutation[of A B] by (simp only: univ_preserves_predicate)
  show "∀F∈{f ∈ A →⇩E B. f ` A = B} // range_permutation A B. functions_of (partitions_of A B F) A B = F"
    using ‹finite B› by (simp add: functions_of_partitions_of quotient_eq)
  show "∀P∈{P. partition_on A P ∧ card P = card B}. partitions_of A B (functions_of P A B) = P"
    using ‹finite A› ‹finite B› by (auto simp add: partitions_of_functions_of)
  show "partitions_of A B ` ({f ∈ A →⇩E B. f ` A = B} // range_permutation A B) ⊆ {P. partition_on A P ∧ card P = card B}"
    using ‹finite B› quotient_eq card_partitions_of partitions_of by fastforce
  show "(λP. functions_of P A B) ` {P. partition_on A P ∧ card P = card B} ⊆ {f ∈ A →⇩E B. f ` A = B} // range_permutation A B"
    using ‹finite A› ‹finite B› by (auto simp add: quotient_eq intro: functions_of functions_of_is_surj_on)
qed

subsection ‹Cardinality›

lemma card_surjective_functions_range_permutation:
  assumes "finite A" "finite B"
  shows "card ({f ∈ A →⇩E B. f ` A = B} // range_permutation A B) = Stirling (card A) (card B)"
proof -
  have "bij_betw (partitions_of A B) ({f ∈ A →⇩E B. f ` A = B} // range_permutation A B) {P. partition_on A P ∧ card P = card B}"
    using ‹finite A› ‹finite B› by (rule bij_betw_partitions_of)
  from this have "card ({f ∈ A →⇩E B. f ` A = B} // range_permutation A B) = card {P. partition_on A P ∧ card P = card B}"
    by (rule bij_betw_same_card)
  also have "card {P. partition_on A P ∧ card P = card B} = Stirling (card A) (card B)"
    using ‹finite A› by (rule card_partition_on)
  finally show ?thesis .
qed

end