Theory Twelvefold_Way.Card_Bijections

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

section ‹Cardinality of Bijections›

theory Card_Bijections
imports
  Twelvefold_Way_Entry2
  Twelvefold_Way_Entry3
  Twelvefold_Way_Entry5
  Twelvefold_Way_Entry6
  Twelvefold_Way_Entry8
  Twelvefold_Way_Entry9
  Twelvefold_Way_Entry11
  Twelvefold_Way_Entry12
begin

subsection ‹Bijections from A to B›

lemma bij_betw_set_is_empty:
  assumes "finite A" "finite B"
  assumes "card A ≠ card B"
  shows "{f ∈ A →⇩E B. bij_betw f A B} = {}"
using assms bij_betw_same_card by blast

lemma card_bijections_eq_zero:
  assumes "finite A" "finite B"
  assumes "card A ≠ card B"
  shows "card {f ∈ A →⇩E B. bij_betw f A B} = 0"
using bij_betw_set_is_empty[OF assms] by (simp only: card.empty)

text ‹Two alternative proofs for the cardinality of bijections up to a permutation on A.›

lemma
  assumes "finite A" "finite B"
  assumes "card A = card B"
  shows "card {f ∈ A →⇩E B. bij_betw f A B} = fact (card B)"
proof -
  have "card {f ∈ A →⇩E B. bij_betw f A B} = card {f ∈ A →⇩E B. inj_on f A}"
    using ‹finite B› ‹card A = card B› by (metis bij_betw_implies_inj_on_and_card_eq)
  also have "… = fact (card B)"
    using ‹finite A› ‹finite B› ‹card A = card B› by (simp add: card_extensional_funcset_inj_on)
  finally show ?thesis .
qed

lemma card_bijections:
  assumes "finite A" "finite B"
  assumes "card A = card B"
  shows "card {f ∈ A →⇩E B. bij_betw f A B} = fact (card B)"
proof -
  have "card {f ∈ A →⇩E B. bij_betw f A B} = card {f ∈ A →⇩E B. f ` A = B}"
    using ‹finite A› ‹card A = card B›
    by (metis bij_betw_implies_surj_on_and_card_eq)
  also have "… = fact (card B)"
    using ‹finite A› ‹finite B› ‹card A = card B›
    by (simp add: card_extensional_funcset_surj_on)
  finally show ?thesis .
qed

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

lemma bij_betw_quotient_domain_permutation_eq_empty:
  assumes "card A ≠ card B"
  shows "{f ∈ A →⇩E B. bij_betw f A B} // domain_permutation A B = {}"
using ‹card A ≠ card B› bij_betw_same_card by auto

lemma card_bijections_domain_permutation_eq_0:
  assumes "card A ≠ card B"
  shows "card ({f ∈ A →⇩E B. bij_betw f A B} // domain_permutation A B) = 0"
using bij_betw_quotient_domain_permutation_eq_empty[OF assms] by (simp only: card.empty)

text ‹Two alternative proofs for the cardinality of bijections up to a permutation on A.›

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"
proof -
  from assms have "{f ∈ A →⇩E B. bij_betw f A B} // domain_permutation A B
    = {f ∈ A →⇩E B. inj_on f A} // domain_permutation A B"
    by (metis (no_types, lifting) PiE_cong bij_betw_implies_inj_on_and_card_eq)
  from this show ?thesis
    using assms by (simp add: card_injective_functions_domain_permutation)
qed

lemma card_bijections_domain_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_permutation A B) = 1"
proof -
  from assms have "{f ∈ A →⇩E B. bij_betw f A B} // domain_permutation A B
    = {f ∈ A →⇩E B. f ` A = B} // domain_permutation A B"
    by (metis (no_types, lifting) PiE_cong bij_betw_implies_surj_on_and_card_eq)
  from this show ?thesis
    using assms by (simp add: card_surjective_functions_domain_permutation)
qed

lemma card_bijections_domain_permutation:
  assumes "finite A" "finite B"
  shows "card ({f ∈ A →⇩E B. bij_betw f A B} // domain_permutation A B) = iverson (card A = card B)"
using assms card_bijections_domain_permutation_eq_0 card_bijections_domain_permutation_eq_1
unfolding iverson_def by auto

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

lemma bij_betw_quotient_range_permutation_eq_empty:
  assumes "card A ≠ card B"
  shows "{f ∈ A →⇩E B. bij_betw f A B} // range_permutation A B = {}"
using ‹card A ≠ card B› bij_betw_same_card by auto

lemma card_bijections_range_permutation_eq_0:
  assumes "card A ≠ card B"
  shows "card ({f ∈ A →⇩E B. bij_betw f A B} // range_permutation A B) = 0"
using bij_betw_quotient_range_permutation_eq_empty[OF assms] by (simp only: card.empty)

text ‹Two alternative proofs for the cardinality of bijections up to a permutation on B.›

lemma
  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"
proof -
  from assms have "{f ∈ A →⇩E B. bij_betw f A B} // range_permutation A B =
    {f ∈ A →⇩E B. inj_on f A} // range_permutation A B"
    by (metis (no_types, lifting) PiE_cong bij_betw_implies_inj_on_and_card_eq)
  from this show ?thesis
    using assms by (simp add: iverson_def card_injective_functions_range_permutation)
qed

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"
proof -
  from assms have "{f ∈ A →⇩E B. bij_betw f A B} // range_permutation A B =
    {f ∈ A →⇩E B. f ` A = B} // range_permutation A B"
    by (metis (no_types, lifting) PiE_cong bij_betw_implies_surj_on_and_card_eq)
  from this show ?thesis
    using assms by (simp add: card_surjective_functions_range_permutation)
qed

lemma card_bijections_range_permutation:
  assumes "finite A" "finite B"
  shows "card ({f ∈ A →⇩E B. bij_betw f A B} // range_permutation A B) = iverson (card A = card B)"
using assms card_bijections_range_permutation_eq_0 card_bijections_range_permutation_eq_1
unfolding iverson_def by auto

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

lemma bij_betw_quotient_domain_and_range_permutation_eq_empty:
  assumes "card A ≠ card B"
  shows "{f ∈ A →⇩E B. bij_betw f A B} // domain_and_range_permutation A B = {}"
using ‹card A ≠ card B› bij_betw_same_card by auto

lemma card_bijections_domain_and_range_permutation_eq_0:
  assumes "card A ≠ card B"
  shows "card ({f ∈ A →⇩E B. bij_betw f A B} // domain_and_range_permutation A B) = 0"
using bij_betw_quotient_domain_and_range_permutation_eq_empty[OF assms] by (simp only: card.empty)

text ‹Two alternative proofs for the cardinality of bijections up to a permutation on A and B.›

lemma
  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"
proof -
  from assms have "{f ∈ A →⇩E B. bij_betw f A B} // domain_and_range_permutation A B =
    {f ∈ A →⇩E B. inj_on f A} // domain_and_range_permutation A B"
    by (metis (no_types, lifting) PiE_cong bij_betw_implies_inj_on_and_card_eq)
  from this show ?thesis
    using assms by (simp add: iverson_def card_injective_functions_domain_and_range_permutation)
qed

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"
proof -
  from assms have "{f ∈ A →⇩E B. bij_betw f A B} // domain_and_range_permutation A B =
    {f ∈ A →⇩E B. f ` A = B} // domain_and_range_permutation A B"
    by (metis (no_types, lifting) PiE_cong bij_betw_implies_surj_on_and_card_eq)
  from this show ?thesis
    using assms by (simp add: card_surjective_functions_domain_and_range_permutation Partition_diag)
qed

lemma card_bijections_domain_and_range_permutation:
  assumes "finite A" "finite B"
  shows "card ({f ∈ A →⇩E B. bij_betw f A B} // domain_and_range_permutation A B) = iverson (card A = card B)"
using assms card_bijections_domain_and_range_permutation_eq_0 card_bijections_domain_and_range_permutation_eq_1
unfolding iverson_def by auto

end