Theory Twelvefold_Way_Entry6

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

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

theory Twelvefold_Way_Entry6
imports Twelvefold_Way_Entry4
begin

subsection ‹Properties for Bijections›

lemma set_mset_eq_implies_surj_on:
  assumes "finite A"
  assumes "size M = card A" "set_mset M = B"
  assumes "f  functions_of A M"
  shows   "f ` A = B"
proof -
  from f  functions_of A M have "image_mset f (mset_set A) = M"
    unfolding functions_of_def by auto
  from image_mset f (mset_set A) = M show "f ` A = B"
    using set_mset M = B finite A finite_set_mset_mset_set set_image_mset by force
qed

lemma surj_on_implies_set_mset_eq:
  assumes "finite A"
  assumes "F  (A E B) // domain_permutation A B"
  assumes "univ (λf. f ` A = B) F"
  shows "set_mset (msubset_of A F) = B"
proof -
  from F  (A E B) // domain_permutation A B obtain f where "f  A E B"
    and F_eq: "F = domain_permutation A B `` {f}" using quotientE by blast
  have "msubset_of A F = univ (λf. image_mset f (mset_set A)) F"
    unfolding msubset_of_def ..
  also have " = univ (λf. image_mset f (mset_set A)) (domain_permutation A B `` {f})"
    unfolding F_eq ..
  also have " = image_mset f (mset_set A)"
    using equiv_domain_permutation image_mset_respects_domain_permutation f  A E B
    by (subst univ_commute') auto
  finally have eq: "msubset_of A F = image_mset f (mset_set A)" .
  from iffD1[OF univ_commute', OF equiv_domain_permutation, OF surjective_respects_domain_permutation, OF f  A E B]
    univ (λf. f ` A = B) F have "f ` A = B" by (simp add: F_eq)
  have "set_mset (image_mset f (mset_set A)) = B"
  proof
    show "set_mset (image_mset f (mset_set A))  B"
      using finite A f ` A = B by auto
  next
    show "B  set_mset (image_mset f (mset_set A))"
      using finite A by (simp add: f ` A = B[symmetric] in_image_mset)
  qed
  from this show "set_mset (msubset_of A F) = B"
    unfolding eq .
qed

lemma functions_of_is_surj_on:
  assumes "finite A"
  assumes "size M = card A" "set_mset M = B"
  shows "univ (λf. f ` A = B) (functions_of A M)"
proof -
  have "functions_of A M  (A E B) // domain_permutation A B"
    using functions_of finite A size M = card A set_mset M = B  by fastforce
  from this obtain f where eq_f: "functions_of A M = domain_permutation A B `` {f}" and "f  A E B"
    using quotientE by blast
  from eq_f have "f  functions_of A M"
    using f  A E B equiv_domain_permutation equiv_class_self by fastforce
  have "f ` A = B"
    using f  functions_of A M assms set_mset_eq_implies_surj_on by fastforce
  from this show ?thesis
    unfolding eq_f using equiv_domain_permutation surjective_respects_domain_permutation f  A E B
    by (subst univ_commute') assumption+
qed

subsection ‹Bijections›

lemma bij_betw_msubset_of:
  assumes "finite A"
  shows "bij_betw (msubset_of A) ({f  A E B. f ` A = B} // domain_permutation A B)
    {M. set_mset M = B  size M = card A}"
    (is "bij_betw _ ?FSet ?MSet")
proof (rule bij_betw_byWitness[where f'="λM. functions_of A M"])
  have quotient_eq: "?FSet = {F  ((A E B) // domain_permutation A B). univ (λf. f ` A = B) F}"
    using equiv_domain_permutation[of A B] surjective_respects_domain_permutation[of A B]
    by (simp only: univ_preserves_predicate)
  show "f?FSet. functions_of A (msubset_of A f) = f"
    using finite A by (auto simp only: quotient_eq functions_of_msubset_of)
  show "M?MSet. msubset_of A (functions_of A M) = M"
    using finite A msubset_of_functions_of by blast
  show "msubset_of A ` ?FSet  ?MSet"
    using finite A by (auto simp add: quotient_eq surj_on_implies_set_mset_eq msubset_of)
  show "functions_of A ` ?MSet  ?FSet"
    using finite A by (auto simp add: quotient_eq intro: functions_of functions_of_is_surj_on)
qed

subsection ‹Cardinality›

lemma card_surjective_functions_domain_permutation:
  assumes "finite A" "finite B"
  assumes "card B  card A"
  shows "card ({f  A E B. f ` A = B} // domain_permutation A B) = (card A - 1) choose (card A - card B)"
proof -
  let ?FSet = "{f  A E B. f ` A = B} // domain_permutation A B"
  and ?MSet = "{M. set_mset M = B  size M = card A}"
  have "bij_betw (msubset_of A) ?FSet ?MSet"
    using finite A by (rule bij_betw_msubset_of)
  from this have "card ?FSet = card ?MSet"
    by (rule bij_betw_same_card)
  also have "card ?MSet = (card A - 1) choose (card A - card B)"
    using finite B card B  card A by (rule card_multisets_covering_set)
  finally show ?thesis .
qed

end