Theory Twelvefold_Way_Entry12

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

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

theory Twelvefold_Way_Entry12
imports Twelvefold_Way_Entry9 Twelvefold_Way_Entry10
begin

subsection ‹Properties for Bijections›

lemma size_eq_card_implies_surj_on:
  assumes "finite A" "finite B"
  assumes "size N = card B"
  assumes "f ∈ functions_of A B N"
  shows   "f ` A = B"
proof -
  from ‹f ∈ functions_of A B N› have "f ∈ A →⇩E B" and
    "N = image_mset card (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}}))"
    unfolding functions_of_def by auto
  from this ‹size N = card B› have "card ((λb. {x ∈ A. f x = b}) ` B - {{}}) = card B" by simp
  from this ‹finite B› ‹f ∈ A →⇩E B› show "f ` A = B"
    using card_eq_implies_surjective_on by blast
qed

lemma surj_on_implies_size_eq_card:
  assumes "finite A" "finite B"
  assumes "F ∈ (A →⇩E B) // domain_and_range_permutation A B"
  assumes "univ (λf. f ` A = B) F"
  shows "size (number_partition_of A B F) = card B"
proof -
  from ‹F ∈ (A →⇩E B) // domain_and_range_permutation A B› obtain f where "f ∈ A →⇩E B"
    and F_eq: "F = domain_and_range_permutation A B `` {f}" using quotientE by blast
  have "number_partition_of A B F = univ (λf. image_mset card (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}}))) F"
    unfolding number_partition_of_def ..
  also have "… =  univ (λf. image_mset card (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}}))) (domain_and_range_permutation A B `` {f})"
    unfolding F_eq ..
  also have "… = image_mset card (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}}))"
    using ‹finite B› equiv_domain_and_range_permutation multiset_of_partition_cards_respects_domain_and_range_permutation ‹f ∈ A →⇩E B›
    by (subst univ_commute') auto
  finally have eq: "number_partition_of A B F = image_mset card (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}}))" .
  from iffD1[OF univ_commute', OF equiv_domain_and_range_permutation, OF surjective_respects_domain_and_range_permutation, OF ‹f ∈ A →⇩E B›]
    assms(4) have "f ` A = B" by (simp add: F_eq)
  have "size (number_partition_of A B F) = size (image_mset card (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}})))"
    unfolding eq ..
  also have "… = card ((λb. {x ∈ A. f x = b}) ` B - {{}})" by simp
  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 "number_partition (card A) N" "size N = card B"
  shows "univ (λf. f ` A = B) (functions_of A B N)"
proof -
  have "functions_of A B N ∈ (A →⇩E B) // domain_and_range_permutation A B"
    using functions_of ‹finite A› ‹finite B› ‹number_partition (card A) N › ‹size N = card B›
    by fastforce
  from this obtain f where eq_f: "functions_of A B N = domain_and_range_permutation A B `` {f}" and "f ∈ A →⇩E B"
    using quotientE by blast
  from eq_f have "f ∈ functions_of A B N"
    using ‹f ∈ A →⇩E B› equiv_domain_and_range_permutation equiv_class_self by fastforce
  have "f ` A = B"
    using ‹f ∈ functions_of A B N› assms size_eq_card_implies_surj_on by blast
  from this show ?thesis
    unfolding eq_f using equiv_domain_and_range_permutation surjective_respects_domain_and_range_permutation ‹f ∈ A →⇩E B›
    by (subst univ_commute') assumption+
qed

subsection ‹Bijections›

lemma bij_betw_number_partition_of:
   assumes "finite A" "finite B"
  shows "bij_betw (number_partition_of A B) ({f ∈ A →⇩E B. f ` A = B} // domain_and_range_permutation A B) {N. number_partition (card A) N ∧ size N = card B}"
proof (rule bij_betw_byWitness[where f'="functions_of A B"])
  have quotient_eq: "{f ∈ A →⇩E B. f ` A = B} // domain_and_range_permutation A B = {F ∈ ((A →⇩E B) // domain_and_range_permutation A B). univ (λf. f ` A = B) F}"
    using equiv_domain_and_range_permutation[of A B] surjective_respects_domain_and_range_permutation[of A B] by (simp only: univ_preserves_predicate)
  show "∀F∈{f ∈ A →⇩E B. f ` A = B} // domain_and_range_permutation A B.
       functions_of A B (number_partition_of A B F) = F"
    using ‹finite A› ‹finite B› by (auto simp only: quotient_eq functions_of_number_partition_of)
  show "∀N∈{N. number_partition (card A) N  ∧ size N = card B}. number_partition_of A B (functions_of A B N) = N"
    using ‹finite A› ‹finite B› by (simp add: number_partition_of_functions_of)
  show "number_partition_of A B ` ({f ∈ A →⇩E B. f ` A = B} // domain_and_range_permutation A B)
    ⊆ {N. number_partition (card A) N  ∧ size N = card B}"
    using ‹finite A› ‹finite B› by (auto simp add: quotient_eq number_partition_of surj_on_implies_size_eq_card)
  show "functions_of A B ` {N. number_partition (card A) N ∧ size N = card B}
    ⊆ {f ∈ A →⇩E B. f ` A = B} // domain_and_range_permutation A B"
    using ‹finite A› ‹finite B› by (auto simp add: quotient_eq intro: functions_of functions_of_is_surj_on)
qed

lemma bij_betw_functions_of:
   assumes "finite A" "finite B"
  shows "bij_betw (functions_of A B) {N. number_partition (card A) N ∧ size N = card B} ({f ∈ A →⇩E B. f ` A = B} // domain_and_range_permutation A B)"
proof (rule bij_betw_byWitness[where f'="number_partition_of A B"])
  have quotient_eq: "{f ∈ A →⇩E B. f ` A = B} // domain_and_range_permutation A B = {F ∈ ((A →⇩E B) // domain_and_range_permutation A B). univ (λf. f ` A = B) F}"
    using equiv_domain_and_range_permutation[of A B] surjective_respects_domain_and_range_permutation[of A B] by (simp only: univ_preserves_predicate)
  show "∀F∈{f ∈ A →⇩E B. f ` A = B} // domain_and_range_permutation A B.
       functions_of A B (number_partition_of A B F) = F"
    using ‹finite A› ‹finite B› by (auto simp only: quotient_eq functions_of_number_partition_of)
  show "∀N∈{N. number_partition (card A) N  ∧ size N = card B}. number_partition_of A B (functions_of A B N) = N"
    using ‹finite A› ‹finite B› by (simp add: number_partition_of_functions_of)
  show "number_partition_of A B ` ({f ∈ A →⇩E B. f ` A = B} // domain_and_range_permutation A B)
    ⊆ {N. number_partition (card A) N  ∧ size N = card B}"
    using ‹finite A› ‹finite B› by (auto simp add: quotient_eq number_partition_of surj_on_implies_size_eq_card)
  show "functions_of A B ` {N. number_partition (card A) N ∧ size N = card B}
    ⊆ {f ∈ A →⇩E B. f ` A = B} // domain_and_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_domain_and_range_permutation:
  assumes "finite A" "finite B"
  shows "card ({f ∈ A →⇩E B. f ` A = B} // domain_and_range_permutation A B) = Partition (card A) (card B)"
proof -
  have "bij_betw (number_partition_of A B) ({f ∈ A →⇩E B. f ` A = B} // domain_and_range_permutation A B) {N. number_partition (card A) N ∧ size N = card B}"
     using ‹finite A› ‹finite B› by (rule bij_betw_number_partition_of)
  from this have "card ({f ∈ A →⇩E B. f ` A = B} // domain_and_range_permutation A B) = card {N. number_partition (card A) N ∧ size N = card B}"
    by (rule bij_betw_same_card)
  also have "card {N. number_partition (card A) N ∧ size N = card B} = Partition (card A) (card B)"
    by (rule card_partitions_with_k_parts)
  finally show ?thesis .
qed

end