feat(category_theory/Fintype): Adds the category of finite types and …

…its "standard" skeleton. (#4809)

This PR adds the category `Fintype` of finite types, as well as its "standard" skeleton whose objects are `fin n`.



Co-authored-by: Bhavik Mehta <bhavikmehta8@gmail.com>

src/category_theory/Fintype.lean

@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2020 Adam Topaz. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bhavik Mehta, Adam Topaz
+-/
+
+import data.fintype.basic
+import data.fin
+import category_theory.concrete_category.bundled
+import category_theory.concrete_category
+import category_theory.full_subcategory
+import category_theory.skeletal
+
+/-!
+# The category of finite types.
+
+We define the category of finite types, denoted `Fintype` as
+(bundled) types with a `fintype` instance.
+
+We also define `Fintype.skeleton`, the standard skeleton of `Fintype` whose objects are `fin n`
+for `n : ℕ`. We prove that the obvious inclusion functor `Fintype.skeleton ⥤ Fintype` is an
+equivalence of categories in `Fintype.skeleton.equivalence`.
+We prove that `Fintype.skeleton` is a skeleton of `Fintype` in `Fintype.is_skeleton`.
+-/
+
+open_locale classical
+open category_theory
+
+/-- The category of finite types. -/
+@[derive has_coe_to_sort]
+def Fintype := bundled fintype
+
+namespace Fintype
+
+/-- Construct a bundled `Fintype` from the underlying type and typeclass. -/
+def of (X : Type*) [fintype X] : Fintype := bundled.of X
+instance : inhabited Fintype := ⟨⟨pempty⟩⟩
+instance {X : Fintype} : fintype X := X.2
+
+instance : category Fintype := induced_category.category bundled.α
+
+/-- The fully faithful embedding of `Fintype` into the category of types. -/
+@[derive [full, faithful], simps {rhs_md:=semireducible}]
+def incl : Fintype ⥤ Type* := induced_functor _
+
+instance : concrete_category Fintype := ⟨incl⟩
+
+/--
+The "standard" skeleton for `Fintype`. This is the full subcategory of `Fintype` spanned by objects
+of the form `fin n` for `n : ℕ`. We parameterize the objects of `Fintype.skeleton` directly as `ℕ`,
+as the type `fin m ≃ fin n` is nonempty if and only if `n = m`.
+-/
+def skeleton := ℕ
+
+namespace skeleton
+
+/-- Given any natural number `n`, this creates the associated object of `Fintype.skeleton`. -/
+def mk : ℕ → skeleton := id
+
+instance : inhabited skeleton := ⟨mk 0⟩
+
+/-- Given any object of `Fintype.skeleton`, this returns the associated natural number. -/
+def to_nat : skeleton → ℕ := id
+
+instance : category skeleton :=
+{ hom := λ X Y, fin X → fin Y,
+  id := λ _, id,
+  comp := λ _ _ _ f g, g ∘ f }
+
+lemma is_skeletal : skeletal skeleton := λ X Y ⟨h⟩, fin.equiv_iff_eq.mp $ nonempty.intro $
+{ to_fun := h.1,
+  inv_fun := h.2,
+  left_inv := λ _, by {change (h.hom ≫ h.inv) _ = _, simpa},
+  right_inv := λ _, by {change (h.inv ≫ h.hom) _ = _, simpa} }
+
+/-- The canonical fully faithful embedding of `Fintype.skeleton` into `Fintype`. -/
+def incl : skeleton ⥤ Fintype :=
+{ obj := λ X, Fintype.of (fin X),
+  map := λ _ _ f, f }
+
+instance : full incl := { preimage := λ _ _ f, f }
+instance : faithful incl := {}
+noncomputable instance : ess_surj incl :=
+{ obj_preimage := λ X, fintype.card X,
+  iso' := λ X,
+  let F := trunc.out (fintype.equiv_fin X) in
+  { hom := F.symm,
+    inv := F,
+    hom_inv_id' := by { change F.to_fun ∘ F.inv_fun = _, simpa },
+    inv_hom_id' := by { change F.inv_fun ∘ F.to_fun = _, simpa } } }
+
+noncomputable instance : is_equivalence incl :=
+equivalence.equivalence_of_fully_faithfully_ess_surj _
+
+/-- The equivalence between `Fintype.skeleton` and `Fintype`. -/
+noncomputable def equivalence : skeleton ≌ Fintype := incl.as_equivalence
+
+@[simp] lemma incl_mk_nat_card (n : ℕ) : fintype.card (incl.obj (mk n)) = n := finset.card_fin n
+
+end skeleton
+
+/-- `Fintype.skeleton` is a skeleton of `Fintype`. -/
+noncomputable def is_skeleton : is_skeleton_of Fintype skeleton skeleton.incl :=
+{ skel := skeleton.is_skeletal,
+  eqv := by apply_instance }
+
+end Fintype

src/data/fintype/basic.lean

@@ -318,6 +318,9 @@ list.length_fin_range n
 @[simp] lemma finset.card_fin (n : ℕ) : finset.card (finset.univ : finset (fin n)) = n :=
 by rw [finset.card_univ, fintype.card_fin]
 
+lemma fin.equiv_iff_eq {m n : ℕ} : nonempty (fin m ≃ fin n) ↔ m = n :=
+  ⟨λ ⟨h⟩, by simpa using fintype.card_congr h, λ h, ⟨equiv.cast $ h ▸ rfl ⟩ ⟩
+
 /-- Embed `fin n` into `fin (n + 1)` by prepending zero to the `univ` -/
 lemma fin.univ_succ (n : ℕ) :
   (univ : finset (fin (n + 1))) = insert 0 (univ.image fin.succ) :=