Theory Twelvefold_Way.Twelvefold_Way_Entry11
section ‹Injections from A to B up to a permutation on A and B›
theory Twelvefold_Way_Entry11
imports Twelvefold_Way_Entry10
begin
subsection ‹Properties for Bijections›
lemma all_one_implies_inj_on:
assumes "finite A" "finite B"
assumes "∀n. n∈# N ⟶ n = 1" "number_partition (card A) N" "size N ≤ card B"
assumes "f ∈ functions_of A B N"
shows "inj_on f A"
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 ‹∀n. n∈# N ⟶ n = 1› have parts: "∀b ∈ B. card {x ∈ A. f x = b} = 1 ∨ {x ∈ A. f x = b} = {}"
using ‹finite B› by auto
show "inj_on f A"
proof
fix x y
assume a: "x ∈ A" "y ∈ A" "f x = f y"
from ‹f ∈ A →⇩E B› ‹x ∈ A› have "f x ∈ B" by auto
from a have 1: "x ∈ {x' ∈ A. f x' = f x}" "y ∈ {x' ∈ A. f x' = f x}" by auto
from this have 2: "card {x' ∈ A. f x' = f x} = 1"
using parts ‹f x ∈ B› by blast
from this have "is_singleton {x' ∈ A. f x' = f x}"
by (simp add: is_singleton_altdef)
from 1 this show "x = y"
by (metis is_singletonE singletonD)
qed
qed
lemma inj_on_implies_all_one:
assumes "finite A" "finite B"
assumes "F ∈ (A →⇩E B) // domain_and_range_permutation A B"
assumes "univ (λf. inj_on f A) F"
shows "∀n. n∈# number_partition_of A B F ⟶ n = 1"
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 inj_on_respects_domain_and_range_permutation, OF ‹f ∈ A →⇩E B›]
assms(4) have "inj_on f A" by (simp add: F_eq)
have "∀n. n ∈# image_mset card (mset_set ((λb. {x ∈ A. f x = b}) ` B - {{}})) ⟶ n = 1"
proof -
have "∀b ∈ B. card {x ∈ A. f x = b} = 1 ∨ {x ∈ A. f x = b} = {}"
proof
fix b
assume "b ∈ B"
show "card {x ∈ A. f x = b} = 1 ∨ {x ∈ A. f x = b} = {}"
proof (cases "b ∈ f ` A")
assume "b ∈ f ` A"
from ‹inj_on f A› this have "is_singleton {x ∈ A. f x = b}"
by (auto simp add: inj_on_eq_iff intro: is_singletonI')
from this have "card {x ∈ A. f x = b} = 1"
by (subst is_singleton_altdef[symmetric])
from this show ?thesis ..
next
assume "b ∉ f ` A"
from this have "{x ∈ A. f x = b} = {}" by auto
from this show ?thesis ..
qed
qed
from this show ?thesis
using ‹finite B› by auto
qed
from this show "∀n. n∈# number_partition_of A B F ⟶ n = 1"
unfolding eq by auto
qed
lemma functions_of_is_inj_on:
assumes "finite A" "finite B"
assumes "∀n. n∈# N ⟶ n = 1" "number_partition (card A) N" "size N ≤ card B"
shows "univ (λf. inj_on f A) (functions_of A B N)"
proof -
have "functions_of A B N ∈ (A →⇩E B) // domain_and_range_permutation A B"
using assms functions_of by auto
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 "inj_on f A"
using ‹f ∈ functions_of A B N› assms all_one_implies_inj_on by blast
from this show ?thesis
unfolding eq_f using equiv_domain_and_range_permutation inj_on_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. inj_on f A} // domain_and_range_permutation A B) {N. (∀n. n∈# N ⟶ n = 1) ∧ 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. inj_on f A} // domain_and_range_permutation A B = {F ∈ ((A →⇩E B) // domain_and_range_permutation A B). univ (λf. inj_on f A) F}"
using equiv_domain_and_range_permutation[of A B] inj_on_respects_domain_and_range_permutation[of A B] by (simp only: univ_preserves_predicate)
show "∀F∈{f ∈ A →⇩E B. inj_on f A} // 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. (∀n. n∈# N ⟶ n = 1) ∧ 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› number_partition_of_functions_of by auto
show "number_partition_of A B ` ({f ∈ A →⇩E B. inj_on f A} // domain_and_range_permutation A B)
⊆ {N. (∀n. n∈# N ⟶ n = 1) ∧ number_partition (card A) N ∧ size N ≤ card B}"
using ‹finite A› ‹finite B›
by (auto simp add: quotient_eq number_partition_of inj_on_implies_all_one simp del: One_nat_def)
show "functions_of A B ` {N. (∀n. n∈# N ⟶ n = 1) ∧ number_partition (card A) N ∧ size N ≤ card B}
⊆ {f ∈ A →⇩E B. inj_on f A} // domain_and_range_permutation A B"
using ‹finite A› ‹finite B› by (auto simp add: quotient_eq intro: functions_of functions_of_is_inj_on)
qed
lemma bij_betw_functions_of:
assumes "finite A" "finite B"
shows "bij_betw (functions_of A B) {N. (∀n. n∈# N ⟶ n = 1) ∧ number_partition (card A) N ∧ size N ≤ card B} ({f ∈ A →⇩E B. inj_on f A} // 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. inj_on f A} // domain_and_range_permutation A B = {F ∈ ((A →⇩E B) // domain_and_range_permutation A B). univ (λf. inj_on f A) F}"
using equiv_domain_and_range_permutation[of A B] inj_on_respects_domain_and_range_permutation[of A B] by (simp only: univ_preserves_predicate)
show "∀F∈{f ∈ A →⇩E B. inj_on f A} // 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. (∀n. n∈# N ⟶ n = 1) ∧ 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› number_partition_of_functions_of by auto
show "number_partition_of A B ` ({f ∈ A →⇩E B. inj_on f A} // domain_and_range_permutation A B)
⊆ {N. (∀n. n∈# N ⟶ n = 1) ∧ number_partition (card A) N ∧ size N ≤ card B}"
using ‹finite A› ‹finite B›
by (auto simp add: quotient_eq number_partition_of inj_on_implies_all_one simp del: One_nat_def)
show "functions_of A B ` {N. (∀n. n∈# N ⟶ n = 1) ∧ number_partition (card A) N ∧ size N ≤ card B}
⊆ {f ∈ A →⇩E B. inj_on f A} // domain_and_range_permutation A B"
using ‹finite A› ‹finite B› by (auto simp add: quotient_eq intro: functions_of functions_of_is_inj_on)
qed
subsection ‹Cardinality›
lemma card_injective_functions_domain_and_range_permutation:
assumes "finite A" "finite B"
shows "card ({f ∈ A →⇩E B. inj_on f A} // domain_and_range_permutation A B) = iverson (card A ≤ card B)"
proof -
have "bij_betw (number_partition_of A B) ({f ∈ A →⇩E B. inj_on f A} // domain_and_range_permutation A B) {N. (∀n. n∈# N ⟶ n = 1) ∧ 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. inj_on f A} // domain_and_range_permutation A B) = card {N. (∀n. n∈# N ⟶ n = 1) ∧ number_partition (card A) N ∧ size N ≤ card B}"
by (rule bij_betw_same_card)
also have "card {N. (∀n. n∈# N ⟶ n = 1) ∧ number_partition (card A) N ∧ size N ≤ card B} = iverson (card A ≤ card B)"
by (rule card_number_partitions_with_only_parts_1)
finally show ?thesis .
qed
end