feat(data/countable): add countable typeclass (#15280)

Also add a few new operations on `equiv`s.

src/data/countable/basic.lean

@@ -0,0 +1,106 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import logic.equiv.nat
+import logic.equiv.fin
+import data.countable.defs
+
+/-!
+# Countable types
+
+In this file we provide basis instances of the `countable` typeclass defined elsewhere.
+-/
+
+universes u v w
+
+open function
+
+instance : countable ℤ := countable.of_equiv ℕ equiv.int_equiv_nat.symm
+
+/-!
+### Definition in terms of `function.embedding`
+-/
+
+section embedding
+
+variables {α : Sort u} {β : Sort v}
+
+lemma countable_iff_nonempty_embedding : countable α ↔ nonempty (α ↪ ℕ) :=
+⟨λ ⟨⟨f, hf⟩⟩, ⟨⟨f, hf⟩⟩, λ ⟨f⟩, ⟨⟨f, f.2⟩⟩⟩
+
+lemma nonempty_embedding_nat (α) [countable α] : nonempty (α ↪ ℕ) :=
+countable_iff_nonempty_embedding.1 ‹_›
+
+protected lemma function.embedding.countable [countable β] (f : α ↪ β) : countable α :=
+f.injective.countable
+
+end embedding
+
+/-!
+### Operations on `Type*`s
+-/
+
+section type
+
+variables {α : Type u} {β : Type v} {π : α → Type w}
+
+instance [countable α] [countable β] : countable (α ⊕ β) :=
+begin
+  rcases exists_injective_nat α with ⟨f, hf⟩,
+  rcases exists_injective_nat β with ⟨g, hg⟩,
+  exact (equiv.nat_sum_nat_equiv_nat.injective.comp $ hf.sum_map hg).countable
+end
+
+instance [countable α] : countable (option α) :=
+countable.of_equiv _ (equiv.option_equiv_sum_punit α).symm
+
+instance [countable α] [countable β] : countable (α × β) :=
+begin
+  rcases exists_injective_nat α with ⟨f, hf⟩,
+  rcases exists_injective_nat β with ⟨g, hg⟩,
+  exact (equiv.nat_prod_nat_equiv_nat.injective.comp $ hf.prod_map hg).countable
+end
+
+instance [countable α] [Π a, countable (π a)] : countable (sigma π) :=
+begin
+  rcases exists_injective_nat α with ⟨f, hf⟩,
+  choose g hg using λ a, exists_injective_nat (π a),
+  exact ((equiv.sigma_equiv_prod ℕ ℕ).injective.comp $ hf.sigma_map hg).countable
+end
+
+end type
+
+section sort
+
+variables {α : Sort u} {β : Sort v} {π : α → Sort w}
+
+/-!
+### Operations on and `Sort*`s
+-/
+
+@[priority 500]
+instance set_coe.countable {α} [countable α] (s : set α) : countable s := subtype.countable
+
+instance [countable α] [countable β] : countable (psum α β) :=
+countable.of_equiv (plift α ⊕ plift β) (equiv.plift.sum_psum equiv.plift)
+
+instance [countable α] [countable β] : countable (pprod α β) :=
+countable.of_equiv (plift α × plift β) (equiv.plift.prod_pprod equiv.plift)
+
+instance [countable α] [Π a, countable (π a)] : countable (psigma π) :=
+countable.of_equiv (Σ a : plift α, plift (π a.down)) (equiv.psigma_equiv_sigma_plift π).symm
+
+instance [finite α] [Π a, countable (π a)] : countable (Π a, π a) :=
+begin
+  haveI : ∀ n, countable (fin n → ℕ),
+  { intro n, induction n with n ihn,
+    { apply_instance },
+    { exactI countable.of_equiv _ (equiv.pi_fin_succ _ _).symm } },
+  rcases finite.exists_equiv_fin α with ⟨n, ⟨e⟩⟩,
+  have f := λ a, (nonempty_embedding_nat (π a)).some,
+  exact ((embedding.Pi_congr_right f).trans (equiv.Pi_congr_left' _ e).to_embedding).countable
+end
+
+end sort

src/data/countable/defs.lean

@@ -0,0 +1,89 @@
+/-
+Copyright (c) 2022 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import data.finite.defs
+
+/-!
+# Countable types
+
+In this file we define a typeclass saying that a given `Sort*` is countable. See also `encodable`
+for a version that singles out a specific encoding of elements of `α` by natural numbers.
+
+This file also provides a few instances of this typeclass. More instances can be found in other
+files.
+-/
+
+open function
+universes u v
+variables {α : Sort u} {β : Sort v}
+
+/-!
+### Definition and basic properties
+-/
+
+/-- A type `α` is countable if there exists an injective map `α → ℕ`. -/
+@[mk_iff countable_iff_exists_injective] class countable (α : Sort u) : Prop :=
+(exists_injective_nat [] : ∃ f : α → ℕ, injective f)
+
+instance : countable ℕ := ⟨⟨id, injective_id⟩⟩
+
+export countable (exists_injective_nat)
+
+protected lemma function.injective.countable [countable β] {f : α → β} (hf : injective f) :
+  countable α :=
+let ⟨g, hg⟩ := exists_injective_nat β in ⟨⟨g ∘ f, hg.comp hf⟩⟩
+
+protected lemma function.surjective.countable [countable α] {f : α → β} (hf : surjective f) :
+  countable β :=
+(injective_surj_inv hf).countable
+
+lemma exists_surjective_nat (α : Sort u) [nonempty α] [countable α] : ∃ f : ℕ → α, surjective f :=
+let ⟨f, hf⟩ := exists_injective_nat α in ⟨inv_fun f, inv_fun_surjective hf⟩
+
+lemma countable_iff_exists_surjective [nonempty α] : countable α ↔ ∃ f : ℕ → α, surjective f :=
+⟨@exists_surjective_nat _ _, λ ⟨f, hf⟩, hf.countable⟩
+
+lemma countable.of_equiv (α : Sort*) [countable α] (e : α ≃ β) : countable β :=
+e.symm.injective.countable
+
+lemma equiv.countable_iff (e : α ≃ β) : countable α ↔ countable β :=
+⟨λ h, @countable.of_equiv _ _ h e, λ h, @countable.of_equiv _ _ h e.symm⟩
+
+instance {β : Type v} [countable β] : countable (ulift.{u} β) :=
+countable.of_equiv _ equiv.ulift.symm
+
+/-!
+### Operations on `Sort*`s
+-/
+
+instance [countable α] : countable (plift α) := equiv.plift.injective.countable
+
+@[priority 100]
+instance subsingleton.to_countable [subsingleton α] : countable α :=
+⟨⟨λ _, 0, λ x y h, subsingleton.elim x y⟩⟩
+
+@[priority 500]
+instance [countable α] {p : α → Prop} : countable {x // p x} := subtype.val_injective.countable
+
+instance {n : ℕ} : countable (fin n) := subtype.countable
+
+@[priority 100]
+instance finite.to_countable [finite α] : countable α :=
+let ⟨n, ⟨e⟩⟩ := finite.exists_equiv_fin α in countable.of_equiv _ e.symm
+
+instance : countable punit.{u} := subsingleton.to_countable
+
+@[nolint instance_priority]
+instance Prop.countable (p : Prop) : countable p := subsingleton.to_countable
+
+instance bool.countable : countable bool :=
+⟨⟨λ b, cond b 0 1, bool.injective_iff.2 nat.one_ne_zero⟩⟩
+
+instance Prop.countable' : countable Prop := countable.of_equiv bool equiv.Prop_equiv_bool.symm
+
+@[priority 500] instance [countable α] {r : α → α → Prop} : countable (quot r) :=
+(surjective_quot_mk r).countable
+
+@[priority 500] instance [countable α] {s : setoid α} : countable (quotient s) := quot.countable

src/logic/equiv/basic.lean

@@ -395,13 +395,31 @@ def pprod_equiv_prod {α β : Type*} : pprod α β ≃ α × β :=
   left_inv := λ ⟨x, y⟩, rfl,
   right_inv := λ ⟨x, y⟩, rfl }
 
+/-- Product of two equivalences, in terms of `pprod`. If `α ≃ β` and `γ ≃ δ`, then
+`pprod α γ ≃ pprod β δ`. -/
+@[congr, simps apply]
+def pprod_congr {δ : Sort z} (e₁ : α ≃ β) (e₂ : γ ≃ δ) : pprod α γ ≃ pprod β δ :=
+{ to_fun := λ x, ⟨e₁ x.1, e₂ x.2⟩,
+  inv_fun := λ x, ⟨e₁.symm x.1, e₂.symm x.2⟩,
+  left_inv := λ ⟨x, y⟩, by simp,
+  right_inv := λ ⟨x, y⟩, by simp }
+
+/-- Combine two equivalences using `pprod` in the domain and `prod` in the codomain. -/
+@[simps apply symm_apply]
+def pprod_prod {α₁ β₁ : Sort*} {α₂ β₂ : Type*} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) :
+  pprod α₁ β₁ ≃ α₂ × β₂ :=
+(ea.pprod_congr eb).trans pprod_equiv_prod
+
+/-- Combine two equivalences using `pprod` in the codomain and `prod` in the domain. -/
+@[simps apply symm_apply]
+def prod_pprod {α₁ β₁ : Type*} {α₂ β₂ : Sort*} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) :
+  α₁ × β₁ ≃ pprod α₂ β₂ :=
+(ea.symm.pprod_prod eb.symm).symm
+
 /-- `pprod α β` is equivalent to `plift α × plift β` -/
 @[simps apply symm_apply]
 def pprod_equiv_prod_plift {α β : Sort*} : pprod α β ≃ plift α × plift β :=
-{ to_fun := λ x, (plift.up x.1, plift.up x.2),
-  inv_fun := λ x, ⟨x.1.down, x.2.down⟩,
-  left_inv := λ ⟨x, y⟩, rfl,
-  right_inv := λ ⟨⟨x⟩, ⟨y⟩⟩, rfl }
+equiv.plift.symm.pprod_prod equiv.plift.symm
 
 /-- equivalence of propositions is the same as iff -/
 def of_iff {P Q : Prop} (h : P ↔ Q) : P ≃ Q :=
@@ -634,18 +652,34 @@ end
 
 section
 open sum
+
 /-- `psum` is equivalent to `sum`. -/
 def psum_equiv_sum (α β : Type*) : psum α β ≃ α ⊕ β :=
-⟨λ s, psum.cases_on s inl inr,
- λ s, sum.cases_on s psum.inl psum.inr,
- λ s, by cases s; refl,
- λ s, by cases s; refl⟩
+{ to_fun := λ s, psum.cases_on s inl inr,
+  inv_fun := sum.elim psum.inl psum.inr,
+  left_inv := λ s, by cases s; refl,
+  right_inv := λ s, by cases s; refl }
 
 /-- If `α ≃ α'` and `β ≃ β'`, then `α ⊕ β ≃ α' ⊕ β'`. This is `sum.map` as an equivalence. -/
 @[simps apply]
 def sum_congr {α₁ β₁ α₂ β₂ : Type*} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : α₁ ⊕ β₁ ≃ α₂ ⊕ β₂ :=
 ⟨sum.map ea eb, sum.map ea.symm eb.symm, λ x, by simp, λ x, by simp⟩
 
+/-- If `α ≃ α'` and `β ≃ β'`, then `psum α β ≃ psum α' β'`. -/
+def psum_congr {δ : Sort z} (e₁ : α ≃ β) (e₂ : γ ≃ δ) : psum α γ ≃ psum β δ :=
+{ to_fun := λ x, psum.cases_on x (psum.inl ∘ e₁) (psum.inr ∘ e₂),
+  inv_fun := λ x, psum.cases_on x (psum.inl ∘ e₁.symm) (psum.inr ∘ e₂.symm),
+  left_inv := by rintro (x|x); simp,
+  right_inv := by rintro (x|x); simp }
+
+/-- Combine two `equiv`s using `psum` in the domain and `sum` in the codomain. -/
+def psum_sum {α₁ β₁ : Sort*} {α₂ β₂ : Type*} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : psum α₁ β₁ ≃ α₂ ⊕ β₂ :=
+(ea.psum_congr eb).trans (psum_equiv_sum _ _)
+
+/-- Combine two `equiv`s using `sum` in the domain and `psum` in the codomain. -/
+def sum_psum {α₁ β₁ : Type*} {α₂ β₂ : Sort*} (ea : α₁ ≃ α₂) (eb : β₁ ≃ β₂) : α₁ ⊕ β₁ ≃ psum α₂ β₂ :=
+(ea.symm.psum_sum eb.symm).symm
+
 @[simp] lemma sum_congr_trans {α₁ α₂ β₁ β₂ γ₁ γ₂ : Sort*}
   (e : α₁ ≃ β₁) (f : α₂ ≃ β₂) (g : β₁ ≃ γ₁) (h : β₂ ≃ γ₂) :
   (equiv.sum_congr e f).trans (equiv.sum_congr g h) = (equiv.sum_congr (e.trans g) (f.trans h)) :=