chore(category_theory/Fintype): Fix universe restriction in skeleton (#…

…8855)

This removes a universe restriction in the existence of a skeleton for the category `Fintype`.
Once merged, `Fintype.skeleton.{u}` will be a (small) skeleton for `Fintype.{u}`, with `u` any universe parameter.

src/category_theory/Fintype.lean

@@ -45,53 +45,80 @@ def incl : Fintype ⥤ Type* := induced_functor _
 
 instance : concrete_category Fintype := ⟨incl⟩
 
+@[simp] lemma id_apply (X : Fintype) (x : X) : (𝟙 X : X → X) x = x := rfl
+@[simp] lemma comp_apply {X Y Z : Fintype} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X) :
+  (f ≫ g) x = g (f x) := rfl
+
+universe u
 /--
 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`.
+of the form `ulift (fin n)` for `n : ℕ`. We parameterize the objects of `Fintype.skeleton`
+directly as `ulift ℕ`, as the type `ulift (fin m) ≃ ulift (fin n)` is
+nonempty if and only if `n = m`. Specifying universes, `skeleton : Type u` is a small
+skeletal category equivalent to `Fintype.{u}`.
 -/
-def skeleton := ℕ
+def skeleton : Type u := ulift ℕ
 
 namespace skeleton
 
 /-- Given any natural number `n`, this creates the associated object of `Fintype.skeleton`. -/
-def mk : ℕ → skeleton := id
+def mk : ℕ → skeleton := ulift.up
 
 instance : inhabited skeleton := ⟨mk 0⟩
 
 /-- Given any object of `Fintype.skeleton`, this returns the associated natural number. -/
-def to_nat : skeleton → ℕ := id
+def len : skeleton → ℕ := ulift.down
+
+@[ext]
+lemma ext (X Y : skeleton) : X.len = Y.len → X = Y := ulift.ext _ _
 
-instance : category skeleton :=
-{ hom := λ X Y, fin X → fin Y,
+instance : small_category skeleton.{u} :=
+{ hom := λ X Y, ulift.{u} (fin X.len) → ulift.{u} (fin Y.len),
   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} }
+lemma is_skeletal : skeletal skeleton.{u} := λ X Y ⟨h⟩, ext _ _ $ fin.equiv_iff_eq.mp $
+  nonempty.intro $
+{ to_fun := λ x, (h.hom ⟨x⟩).down,
+  inv_fun := λ x, (h.inv ⟨x⟩).down,
+  left_inv := begin
+    intro a,
+    change ulift.down _ = _,
+    rw ulift.up_down,
+    change ((h.hom ≫ h.inv) _).down = _,
+    simpa,
+  end,
+  right_inv := begin
+    intro a,
+    change ulift.down _ = _,
+    rw ulift.up_down,
+    change ((h.inv ≫ h.hom) _).down = _,
+    simpa,
+  end }
 
 /-- The canonical fully faithful embedding of `Fintype.skeleton` into `Fintype`. -/
-def incl : skeleton ⥤ Fintype :=
-{ obj := λ X, Fintype.of (fin X),
+def incl : skeleton.{u} ⥤ Fintype.{u} :=
+{ obj := λ X, Fintype.of (ulift (fin X.len)),
   map := λ _ _ f, f }
 
 instance : full incl := { preimage := λ _ _ f, f }
 instance : faithful incl := {}
 instance : ess_surj incl :=
-{ mem_ess_image := λ X,
-  let F := fintype.equiv_fin X in
-  ⟨fintype.card X, ⟨⟨F.symm, F, F.self_comp_symm, F.symm_comp_self⟩⟩⟩ }
+ess_surj.mk $ λ X, let F := fintype.equiv_fin X in ⟨mk (fintype.card X), nonempty.intro
+  { hom := F.symm ∘ ulift.down,
+    inv := ulift.up ∘ F }⟩
 
 noncomputable instance : is_equivalence incl :=
 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
+@[simp] lemma incl_mk_nat_card (n : ℕ) : fintype.card (incl.obj (mk n)) = n :=
+begin
+  convert finset.card_fin n,
+  apply fintype.of_equiv_card,
+end
 
 end skeleton