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