Theory Twelvefold_Way.Twelvefold_Way_Entry3

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

section ‹Surjections from A to B›

theory Twelvefold_Way_Entry3
imports
  Twelvefold_Way_Entry9
begin

lemma card_of_equiv_class:
  assumes "finite B"
  assumes "F ∈ {f ∈ A →⇩E B. f ` A = B} // range_permutation A B"
  shows "card F = fact (card B)"
proof -
  from ‹F ∈ {f ∈ A →⇩E B. f ` A = B} // range_permutation A B› obtain f where
    "f ∈ A →⇩E B" and "f ` A = B"
    and F_eq: "F = range_permutation A B `` {f}" using quotientE by blast
  have set_eq: "range_permutation A B `` {f} = (λp x. if x ∈ A then p (f x) else undefined) ` {p. p permutes B}"
  proof
    show "range_permutation A B `` {f} ⊆ (λp x. if x ∈ A then p (f x) else undefined) ` {p. p permutes B}"
    proof
      fix f'
      assume "f' ∈ range_permutation A B `` {f}"
      from this obtain p where "p permutes B" "∀x∈A. f x = p (f' x)"
        unfolding range_permutation_def by auto
      from ‹f' ∈ range_permutation A B `` {f}› have "f' ∈ A →⇩E B"
        unfolding range_permutation_def by auto
      have "f' = (λx. if x ∈ A then inv p (f x) else undefined)"
      proof
        fix x
        show "f' x = (if x ∈ A then inv p (f x) else undefined)"
          using ‹f ∈ A →⇩E B› ‹f' ∈ A →⇩E B› ‹∀x∈A. f x = p (f' x)›
            ‹p permutes B› permutes_inverses(2) by fastforce
      qed
      moreover have "inv p permutes B" using ‹p permutes B› by (simp add: permutes_inv)
      ultimately show "f' ∈ (λp. (λx. if x ∈ A then p (f x) else undefined)) ` {p. p permutes B}"
        by auto
    qed
  next
    show "(λp x. if x ∈ A then p (f x) else undefined) ` {p. p permutes B} ⊆ range_permutation A B `` {f}"
    proof
      fix f'
      assume "f' ∈ (λp x. if x ∈ A then p (f x) else undefined) ` {p. p permutes B}"
      from this obtain p where "p permutes B" and f'_eq: "f' = (λx. if x ∈ A then p (f x) else undefined)" by auto
      from this have "f' ∈ A →⇩E B"
        using ‹f ∈ A →⇩E B› permutes_in_image by fastforce
      moreover have "inv p permutes B" using ‹p permutes B› by (simp add: permutes_inv)
      moreover have "∀x∈A. f x = inv p (f' x)"
        using ‹f ∈ A →⇩E B› ‹f' ∈ A →⇩E B› f'_eq
          ‹p permutes B› permutes_inverses(2) by fastforce
      ultimately show "f' ∈ range_permutation A B `` {f}"
        using ‹f ∈ A →⇩E B› unfolding range_permutation_def by auto
    qed
  qed
  have "inj_on (λp x. if x ∈ A then p (f x) else undefined) {p. p permutes B}"
  proof (rule inj_onI)
    fix p p'
    assume "p ∈ {p. p permutes B}" "p' ∈ {p. p permutes B}"
      and eq: "(λx. if x ∈ A then p (f x) else undefined) = (λx. if x ∈ A then p' (f x) else undefined)"
    {
      fix x
      have "p x = p' x"
      proof cases
        assume "x ∈ B"
        from this obtain y where "y ∈ A" and "x = f y"
          using ‹f ` A = B› by blast
        from eq this have "p (f y) = p' (f y)" by meson
        from this ‹x = f y› show "p x = p' x" by simp
      next
        assume "x ∉ B"
        from this show "p x = p' x"
          using ‹p ∈ {p. p permutes B}› ‹p' ∈ {p. p permutes B}›
          by (simp add: permutes_def)
      qed
    }
    from this show "p = p'" by auto
  qed
  have "card F = card ((λp x. if x ∈ A then p (f x) else undefined) ` {p. p permutes B})"
    unfolding F_eq set_eq ..
  also have "… = card {p. p permutes B}"
    using ‹inj_on (λp x. if x ∈ A then p (f x) else undefined) {p. p permutes B}›
    by (simp add: card_image)
  also have "… = fact (card B)"
    using ‹finite B› by (simp add: card_permutations)
  finally show ?thesis .
qed

lemma card_extensional_funcset_surj_on:
  assumes "finite A" "finite B"
  shows "card {f ∈ A →⇩E B. f ` A = B} = fact (card B) * Stirling (card A) (card B)" (is "card ?F = _")
proof -
  have "card ?F = fact (card B) * card (?F // range_permutation A B)"
    using ‹finite B›
    by (simp only: card_equiv_class_restricted_same_size[OF equiv_range_permutation surj_on_respects_range_permutation card_of_equiv_class])
  also have "… = fact (card B) * Stirling (card A) (card B)"
    using ‹finite A› ‹finite B›
    by (simp only: card_surjective_functions_range_permutation)
  finally show ?thesis .
qed

end