Theory Twelvefold_Way_Entry8

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

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

theory Twelvefold_Way_Entry8
imports Twelvefold_Way_Entry7
begin

subsection ‹Properties for Bijections›

lemma inj_on_implies_partitions_of:
  assumes "F  (A E B) // range_permutation A B"
  assumes "univ (λf. inj_on f A) F"
  shows "X  partitions_of A B F. card X = 1"
proof -
  from F  (A E B) // range_permutation A B obtain f where "f  A E B"
    and F_eq: "F = range_permutation A B `` {f}" using quotientE by blast
  from this univ (λf. inj_on f A) F have "inj_on f A"
    using univ_commute'[OF equiv_range_permutation inj_on_respects_range_permutation f  A E B] by simp
  have "X(λb. {x  A. f x = b}) ` B - {{}}. card X = 1"
  proof
    fix X
    assume "X  (λb. {x  A. f x = b}) ` B - {{}}"
    from this obtain x where "X = {xa  A. f xa = f x}" "x  A" by auto
    from this have "X = {x}"
      using inj_on f A by (auto dest!: inj_onD)
    from this show "card X = 1" by simp
  qed
  from this show ?thesis
    unfolding partitions_of_def F_eq
    using equiv_range_permutation domain_partitions_respects_range_permutation f  A E B
    by (subst univ_commute') assumption+
qed

lemma unique_part_eq_singleton:
  assumes "partition_on A P"
  assumes "XP. card X = 1"
  assumes "x  A"
  shows "(THE X. x  X  X  P) = {x}"
proof -
  have "(THE X. x  X  X  P)  P"
    using partition_on A P x  A by (simp add: partition_on_the_part_mem)
  from this have "card (THE X. x  X  X  P) = 1"
    using XP. card X = 1 by auto
  moreover have "x  (THE X. x  X  X  P)"
    using partition_on A P x  A by (simp add: partition_on_in_the_unique_part)
  ultimately show ?thesis
    by (metis card_1_singletonE singleton_iff)
qed

lemma functions_of_is_inj_on:
  assumes "finite A" "finite B" "partition_on A P" "card P  card B"
  assumes "XP. card X = 1"
  shows "univ (λf. inj_on f A) (functions_of P A B)"
proof -
  have "functions_of P A B  (A E B) // range_permutation A B"
    using functions_of finite A finite B partition_on A P card P  card B by blast
  from this obtain f where eq_f: "functions_of P A B = range_permutation A B `` {f}" and "f  A E B"
    using quotientE by blast
  from eq_f have "f  functions_of P A B"
    using f  A E B equiv_range_permutation equiv_class_self by fastforce
  from this have eq: "(λb. {x  A. f x = b}) ` B - {{}} = P"
    unfolding functions_of_def by auto
  have "inj_on f A"
  proof (rule inj_onI)
    fix x y
    assume "x  A" "y  A" "f x = f y"
    from x  A have "x  {x'  A. f x' = f x}" by auto
    moreover from y  A f x = f y have "y  {x'  A. f x' = f x}" by auto
    moreover have "card {x'  A. f x' = f x} = 1"
    proof -
      from x  A f  A E B have "f x  B" by auto
      from this x  A have "{x'  A. f x' = f x}  (λb. {x  A. f x = b}) ` B - {{}}" by auto
      from this XP. card X = 1 eq show ?thesis by auto
    qed
    ultimately show "x = y" by (metis card_1_singletonE singletonD)
  qed
  from this show ?thesis
    unfolding eq_f using equiv_range_permutation inj_on_respects_range_permutation f  A E B
    by (subst univ_commute') assumption+
qed

subsection ‹Bijections›

lemma bij_betw_partitions_of:
  assumes "finite A" "finite B"
  shows "bij_betw (partitions_of A B) ({f  A E B. inj_on f A} // range_permutation A B) {P. partition_on A P  card P  card B  (XP. card X = 1)}"
proof (rule bij_betw_byWitness[where f'="λP. functions_of P A B"])
  have quotient_eq: "{f  A E B. inj_on f A} // range_permutation A B = {F  ((A E B) // range_permutation A B). univ (λf. inj_on f A) F}"
    by (simp add: equiv_range_permutation inj_on_respects_range_permutation univ_preserves_predicate)
  show "F{f  A E B. inj_on f A} // range_permutation A B. functions_of (partitions_of A B F) A B = F"
    using finite B by (simp add: quotient_eq functions_of_partitions_of)
  show "P{P. partition_on A P  card P  card B  (XP. card X = 1)}. partitions_of A B (functions_of P A B) = P"
    using finite A finite B by (simp add: partitions_of_functions_of)
  show "partitions_of A B ` ({f  A E B. inj_on f A} // range_permutation A B)  {P. partition_on A P  card P  card B  (XP. card X = 1)}"
    using finite B quotient_eq partitions_of inj_on_implies_partitions_of by fastforce
  show "(λP. functions_of P A B) ` {P. partition_on A P  card P  card B  (XP. card X = 1)}  {f  A E B. inj_on f A} // 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_range_permutation:
  assumes "finite A" "finite B"
  shows "card ({f  A E B. inj_on f A} // range_permutation A B) = iverson (card A  card B)"
proof -
  obtain enum where "bij_betw enum {0..<card A} A"
    using finite A ex_bij_betw_nat_finite by blast
  have "bij_betw (partitions_of A B) ({f  A E B. inj_on f A} // range_permutation A B) {P. partition_on A P  card P  card B  (XP. card X = 1)}"
    using finite A finite B by (rule bij_betw_partitions_of)
  from this have "card ({f  A E B. inj_on f A} // range_permutation A B) = card {P. partition_on A P  card P  card B  (XP. card X = 1)}"
    by (rule bij_betw_same_card)
  also have "card {P. partition_on A P  card P  card B  (XP. card X = 1)} = iverson (card A  card B)"
    using finite A by (rule card_partition_on_size1_eq_iverson)
  finally show ?thesis .
qed

end