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" "∀x∈A. 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 ‹∀x∈A. 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" "∀x∈A. 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" "∀x∈A. 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 ‹∀x∈A. 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" "∀x∈A. 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 p⇩A p⇩B where "p⇩A permutes A" "p⇩B permutes B"
        and "∀x∈A. f' x = p⇩B (f (p⇩A x))"
        unfolding domain_and_range_permutation_def by auto
      from this have "bij_betw (p⇩B ∘ f ∘ p⇩A) 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 ‹∀x∈A. f' x = p⇩B (f (p⇩A 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" "∀x∈A. 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