Theory Card_Bijections_Direct

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

section ‹Direct Proofs for Cardinality of Bijections›

theory Card_Bijections_Direct
imports
  Equiv_Relations_on_Functions
  Twelvefold_Way_Core
begin

subsection ‹Bijections from A to B up to a Permutation on A›

subsubsection ‹Equivalence Class›

lemma bijections_in_domain_permutation:
  assumes "finite A" "finite B"
  assumes "card A = card B"
  shows "{f  A E B. bij_betw f A B}  {f  A E B. bij_betw f A B} // domain_permutation A B"
proof -
  from assms obtain f where f: "f  {f  A E B. bij_betw f A B}"
    by (metis finite_same_card_bij_on_ext_funcset mem_Collect_eq)
  moreover have proj_f: "{f  A E B. bij_betw f A B} = domain_permutation A B `` {f}"
  proof
    from f show "{f  A E B. bij_betw f A B}  domain_permutation A B `` {f}"
      unfolding domain_permutation_def
      by (auto elim: obtain_domain_permutation_for_two_bijections)
  next
    show "domain_permutation A B `` {f}  {f  A E B. bij_betw f A B}"
    proof
      fix f'
      assume "f'  domain_permutation A B `` {f}"
      have "(f', f)  domain_permutation A B"
        using f'  domain_permutation A B `` {f} equiv_domain_permutation[of A B]
        by (simp add: equiv_class_eq_iff)
      from this obtain p where "p permutes A" "xA. f' x = f (p x)"
        unfolding domain_permutation_def by auto
      from this have "bij_betw (f  p) A B"
        using bij_betw_comp_iff f permutes_imp_bij by fastforce
      from this have "bij_betw f' A B"
        using xA. f' x = f (p x)
        by (metis (mono_tags, lifting) bij_betw_cong comp_apply)
      moreover have "f'  A E B"
        using f'  domain_permutation A B `` {f}
        unfolding domain_permutation_def by auto
      ultimately show "f'  {f  A E B. bij_betw f A B}" by simp
    qed
  qed
  ultimately show ?thesis by (simp add: quotientI)
qed

lemma bij_betw_quotient_domain_permutation_eq:
  assumes "finite A" "finite B"
  assumes "card A = card B"
  shows "{f  A E B. bij_betw f A B} // domain_permutation A B = {{f  A E B. bij_betw f A B}}"
proof
  show "{{f  A E B. bij_betw f A B}}  {f  A E B. bij_betw f A B} // domain_permutation A B"
    by (simp add: bijections_in_domain_permutation[OF assms])
next
  show "{f  A E B. bij_betw f A B} // domain_permutation A B  {{f  A E B. bij_betw f A B}}"
  proof
    fix F
    assume F_in: "F  {f  A E B. bij_betw f A B} // domain_permutation A B"
    have "{f  A E B. bij_betw f A B} // domain_permutation A B = {F  ((A E B) // domain_permutation A B). univ (λf. bij_betw f A B) F}"
      using equiv_domain_permutation[of A B] bij_betw_respects_domain_permutation[of A B] by (simp only: univ_preserves_predicate)
    from F_in this have "F  (A E B) // domain_permutation A B"
      and "univ (λf. bij_betw f A B) F"
      by blast+
    have "F = {f  A E B. bij_betw f A B}"
    proof
      have "f  F. f  A E B"
        using F  (A E B) // domain_permutation A B
        by (metis ImageE equiv_class_eq_iff equiv_domain_permutation quotientE)
      moreover have "f  F. bij_betw f A B"
        using univ_predicate_impl_forall[OF equiv_domain_permutation bij_betw_respects_domain_permutation]
        using F  (A E B) // domain_permutation A B univ (λf. bij_betw f A B) F
        by auto
      ultimately show "F  {f  A E B. bij_betw f A B}" by auto
    next
      show "{f  A E B. bij_betw f A B}  F"
      proof
        fix f'
        assume "f'  {f  A E B. bij_betw f A B}"
        from this have "f'  A E B" "bij_betw f' A B" by auto
          obtain f where "f  A E B" and "F = domain_permutation A B `` {f}"
          using F  (A E B) // domain_permutation A B by (auto elim: quotientE)
        have "bij_betw f A B"
          using univ_commute'[OF equiv_domain_permutation bij_betw_respects_domain_permutation]
          using f  A E B F = domain_permutation A B `` {f} univ (λf. bij_betw f A B) F
          by auto
        obtain p where "p permutes A" "xA. f x = f' (p x)"
          using obtain_domain_permutation_for_two_bijections
          using bij_betw f A B bij_betw f' A B by blast
        from this f  A E B f'  A E B
        have "(f, f')  domain_permutation A B"
          unfolding domain_permutation_def by auto
        from this show "f'  F"
          using F = domain_permutation A B `` {f} by simp
      qed
    qed
    from this show "F  {{f  A E B. bij_betw f A B}}" by simp
  qed
qed

subsubsection ‹Cardinality›

lemma
  assumes "finite A" "finite B"
  assumes "card A = card B"
  shows "card ({f  A E B. bij_betw f A B} // domain_permutation A B) = 1"
using bij_betw_quotient_domain_permutation_eq[OF assms] by auto

subsection ‹Bijections from A to B up to a Permutation on B›

subsubsection ‹Equivalence Class›

lemma bijections_in_range_permutation:
  assumes "finite A" "finite B"
  assumes "card A = card B"
  shows "{f  A E B. bij_betw f A B}  {f  A E B. bij_betw f A B} // range_permutation A B"
proof -
  from assms obtain f where f: "f  {f  A E B. bij_betw f A B}"
    by (metis finite_same_card_bij_on_ext_funcset mem_Collect_eq)
  moreover have proj_f: "{f  A E B. bij_betw f A B} = range_permutation A B `` {f}"
  proof
    from f show "{f  A E B. bij_betw f A B}  range_permutation A B `` {f}"
      unfolding range_permutation_def
      by (auto elim: obtain_range_permutation_for_two_bijections)
  next
    show "range_permutation A B `` {f}  {f  A E B. bij_betw f A B}"
    proof
      fix f'
      assume "f'  range_permutation A B `` {f}"
      have "(f', f)  range_permutation A B"
        using f'  range_permutation A B `` {f} equiv_range_permutation[of A B]
        by (simp add: equiv_class_eq_iff)
      from this obtain p where "p permutes B" "xA. f' x = p (f x)"
        unfolding range_permutation_def by auto
      from this have "bij_betw (p  f) A B"
        using bij_betw_comp_iff f permutes_imp_bij by fastforce
      from this have "bij_betw f' A B"
        using xA. f' x = p (f x)
        by (metis (mono_tags, lifting) bij_betw_cong comp_apply)
      moreover have "f'  A E B"
        using f'  range_permutation A B `` {f}
        unfolding range_permutation_def by auto
      ultimately show "f'  {f  A E B. bij_betw f A B}" by simp
    qed
  qed
  ultimately show ?thesis by (simp add: quotientI)
qed

lemma bij_betw_quotient_range_permutation_eq:
  assumes "finite A" "finite B"
  assumes "card A = card B"
  shows "{f  A E B. bij_betw f A B} // range_permutation A B = {{f  A E B. bij_betw f A B}}"
proof
  show "{{f  A E B. bij_betw f A B}}  {f  A E B. bij_betw f A B} // range_permutation A B"
    by (simp add: bijections_in_range_permutation[OF assms])
next
  show "{f  A E B. bij_betw f A B} // range_permutation A B  {{f  A E B. bij_betw f A B}}"
  proof
    fix F
    assume F_in: "F  {f  A E B. bij_betw f A B} // range_permutation A B"
    have "{f  A E B. bij_betw f A B} // range_permutation A B = {F  ((A E B) // range_permutation A B). univ (λf. bij_betw f A B) F}"
      using equiv_range_permutation[of A B] bij_betw_respects_range_permutation[of A B] by (simp only: univ_preserves_predicate)
    from this F_in have "F  (A E B) // range_permutation A B"
      and "univ (λf. bij_betw f A B) F" by blast+
    have "F = {f  A E B. bij_betw f A B}"
    proof
      have "f  F. f  A E B"
        using F  (A E B) // range_permutation A B
        by (metis ImageE equiv_class_eq_iff equiv_range_permutation quotientE)
      moreover have "f  F. bij_betw f A B"
        using univ_predicate_impl_forall[OF equiv_range_permutation bij_betw_respects_range_permutation]
        using F  (A E B) // range_permutation A B univ (λf. bij_betw f A B) F
        by auto
      ultimately show "F  {f  A E B. bij_betw f A B}" by auto
    next
      show "{f  A E B. bij_betw f A B}  F"
      proof
        fix f'
        assume "f'  {f  A E B. bij_betw f A B}"
        from this have "f'  A E B" "bij_betw f' A B" by auto
          obtain f where "f  A E B" and "F = range_permutation A B `` {f}"
          using F  (A E B) // range_permutation A B by (auto elim: quotientE)
        have "bij_betw f A B"
          using univ_commute'[OF equiv_range_permutation bij_betw_respects_range_permutation]
          using f  A E B F = range_permutation A B `` {f} univ (λf. bij_betw f A B) F
          by auto
        obtain p where "p permutes B" "xA. f x = p (f' x)"
          using obtain_range_permutation_for_two_bijections
          using bij_betw f A B bij_betw f' A B by blast
        from this f  A E B f'  A E B
        have "(f, f')  range_permutation A B"
          unfolding range_permutation_def by auto
        from this show "f'  F"
          using F = range_permutation A B `` {f} by simp
      qed
    qed
    from this show "F  {{f  A E B. bij_betw f A B}}" by simp
  qed
qed

subsubsection ‹Cardinality›

lemma card_bijections_range_permutation_eq_1:
  assumes "finite A" "finite B"
  assumes "card A = card B"
  shows "card ({f  A E B. bij_betw f A B} // range_permutation A B) = 1"
using bij_betw_quotient_range_permutation_eq[OF assms] by auto

subsection ‹Bijections from A to B up to a Permutation on A and B›

subsubsection ‹Equivalence Class›

lemma bijections_in_domain_and_range_permutation:
  assumes "finite A" "finite B"
  assumes "card A = card B"
  shows "{f  A E B. bij_betw f A B}  {f  A E B. bij_betw f A B} // domain_and_range_permutation A B"
proof -
  from assms obtain f where f: "f  {f  A E B. bij_betw f A B}"
    by (metis finite_same_card_bij_on_ext_funcset mem_Collect_eq)
  moreover have proj_f: "{f  A E B. bij_betw f A B} = domain_and_range_permutation A B `` {f}"
  proof
    have "id permutes A" by (simp add: permutes_id)
    from f this show "{f  A E B. bij_betw f A B}  domain_and_range_permutation A B `` {f}"
      unfolding domain_and_range_permutation_def
      by (fastforce elim: obtain_range_permutation_for_two_bijections)
  next
    show "domain_and_range_permutation A B `` {f}  {f  A E B. bij_betw f A B}"
    proof
      fix f'
      assume "f'  domain_and_range_permutation A B `` {f}"
      have "(f', f)  domain_and_range_permutation A B"
        using f'  domain_and_range_permutation A B `` {f} equiv_domain_and_range_permutation[of A B]
        by (simp add: equiv_class_eq_iff)
      from this obtain pA pB where "pA permutes A" "pB permutes B"
        and "xA. f' x = pB (f (pA x))"
        unfolding domain_and_range_permutation_def by auto
      from this have "bij_betw (pB  f  pA) A B"
        using bij_betw_comp_iff f permutes_imp_bij
        by (metis (no_types, lifting) mem_Collect_eq)
      from this have "bij_betw f' A B"
        using xA. f' x = pB (f (pA x))
        by (auto intro: bij_betw_congI)
      moreover have "f'  A E B"
        using f'  domain_and_range_permutation A B `` {f}
        unfolding domain_and_range_permutation_def by auto
      ultimately show "f'  {f  A E B. bij_betw f A B}" by simp
    qed
  qed
  ultimately show ?thesis by (simp add: quotientI)
qed

lemma bij_betw_quotient_domain_and_range_permutation_eq:
  assumes "finite A" "finite B"
  assumes "card A = card B"
  shows "{f  A E B. bij_betw f A B} // domain_and_range_permutation A B = {{f  A E B. bij_betw f A B}}"
proof
  show "{{f  A E B. bij_betw f A B}}
     {f  A E B. bij_betw f A B} // domain_and_range_permutation A B"
    using bijections_in_domain_and_range_permutation[OF assms] by auto
next
  show "{f  A E B. bij_betw f A B} // domain_and_range_permutation A B  {{f  A E B. bij_betw f A B}}"
  proof
    fix F
    assume F_in: "F  {f  A E B. bij_betw f A B} // domain_and_range_permutation A B"
    have "{f  A E B. bij_betw f A B} // domain_and_range_permutation A B = {F  ((A E B) // domain_and_range_permutation A B). univ (λf. bij_betw f A B) F}"
      using equiv_domain_and_range_permutation[of A B] bij_betw_respects_domain_and_range_permutation[of A B] by (simp only: univ_preserves_predicate)
    from F_in this have "F  (A E B) // domain_and_range_permutation A B"
      and "univ (λf. bij_betw f A B) F" by blast+
    have "F = {f  A E B. bij_betw f A B}"
    proof
      have "f  F. f  A E B"
        using F  (A E B) // domain_and_range_permutation A B
        by (metis ImageE equiv_class_eq_iff equiv_domain_and_range_permutation quotientE)
      moreover have "f  F. bij_betw f A B"
        using univ_predicate_impl_forall[OF equiv_domain_and_range_permutation bij_betw_respects_domain_and_range_permutation]
        using F  (A E B) // domain_and_range_permutation A B univ (λf. bij_betw f A B) F
        by auto
      ultimately show "F  {f  A E B. bij_betw f A B}" by auto
    next
      show "{f  A E B. bij_betw f A B}  F"
      proof
        fix f'
        assume "f'  {f  A E B. bij_betw f A B}"
        from this have "f'  A E B" "bij_betw f' A B" by auto
          obtain f where "f  A E B" and "F = domain_and_range_permutation A B `` {f}"
          using F  (A E B) // domain_and_range_permutation A B by (auto elim: quotientE)
        have "bij_betw f A B"
          using univ_commute'[OF equiv_domain_and_range_permutation bij_betw_respects_domain_and_range_permutation]
          using f  A E B F = domain_and_range_permutation A B `` {f} univ (λf. bij_betw f A B) F
          by auto
        obtain p where "p permutes A" "xA. f x = f' (p x)"
          using obtain_domain_permutation_for_two_bijections
          using bij_betw f A B bij_betw f' A B by blast
        moreover have "id permutes B" by (simp add: permutes_id)
        moreover note f  A E B f'  A E B
        ultimately have "(f, f')  domain_and_range_permutation A B"
          unfolding domain_and_range_permutation_def id_def by auto
        from this show "f'  F"
          using F = domain_and_range_permutation A B `` {f} by simp
      qed
    qed
    from this show "F  {{f  A E B. bij_betw f A B}}" by simp
  qed
qed

subsubsection ‹Cardinality›

lemma card_bijections_domain_and_range_permutation_eq_1:
  assumes "finite A" "finite B"
  assumes "card A = card B"
  shows "card ({f  A E B. bij_betw f A B} // domain_and_range_permutation A B) = 1"
using bij_betw_quotient_domain_and_range_permutation_eq[OF assms] by auto

end