feat(category_theory): Type u is well-powered (#6812)

A minor test of the `well_powered` API: we can verify that `Type u` is well-powered, and show `subobject α ≃o set α`.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/category_theory/concrete_category/basic.lean

@@ -86,7 +86,7 @@ def concrete_category.has_coe_to_fun {X Y : C} : has_coe_to_fun (X ⟶ Y) :=
 local attribute [instance] concrete_category.has_coe_to_fun
 
 /-- In any concrete category, we can test equality of morphisms by pointwise evaluations.-/
-lemma concrete_category.hom_ext {X Y : C} (f g : X ⟶ Y) (w : ∀ x : X, f x  = g x) : f = g :=
+lemma concrete_category.hom_ext {X Y : C} (f g : X ⟶ Y) (w : ∀ x : X, f x = g x) : f = g :=
 begin
   apply faithful.map_injective (forget C),
   ext,
@@ -95,6 +95,13 @@ end
 
 @[simp] lemma forget_map_eq_coe {X Y : C} (f : X ⟶ Y) : (forget C).map f = f := rfl
 
+/--
+Analogue of `congr_fun h x`,
+when `h : f = g` is an equality between morphisms in a concrete category.
+-/
+lemma congr_hom {X Y : C} {f g : X ⟶ Y} (h : f = g) (x : X) : f x = g x :=
+congr_fun (congr_arg (λ k : X ⟶ Y, (k : X → Y)) h) x
+
 @[simp] lemma coe_id {X : C} (x : X) : ((𝟙 X) : X → X) x = x :=
 congr_fun ((forget _).map_id X) x
 

src/category_theory/equivalence.lean

@@ -548,4 +548,32 @@ equivalence_of_fully_faithfully_ess_surj _
 
 end equivalence
 
+section partial_order
+variables {α β : Type*} [partial_order α] [partial_order β]
+
+/--
+A categorical equivalence between partial orders is just an order isomorphism.
+-/
+def equivalence.to_order_iso (e : α ≌ β) : α ≃o β :=
+{ to_fun := e.functor.obj,
+  inv_fun := e.inverse.obj,
+  left_inv := λ a, (e.unit_iso.app a).to_eq.symm,
+  right_inv := λ b, (e.counit_iso.app b).to_eq,
+  map_rel_iff' := λ a a',
+    ⟨λ h, le_of_hom
+      ((equivalence.unit e).app a ≫ e.inverse.map (hom_of_le h) ≫ (equivalence.unit_inv e).app a'),
+     λ (h : a ≤ a'), le_of_hom (e.functor.map (hom_of_le h))⟩, }
+
+-- `@[simps]` on `equivalence.to_order_iso` produces lemmas that fail the `simp_nf` linter,
+-- so we provide them by hand:
+@[simp]
+lemma equivalence.to_order_iso_apply (e : α ≌ β) (a : α) :
+  e.to_order_iso a = e.functor.obj a := rfl
+
+@[simp]
+lemma equivalence.to_order_iso_symm_apply (e : α ≌ β) (b : β) :
+  e.to_order_iso.symm b = e.inverse.obj b := rfl
+
+end partial_order
+
 end category_theory

src/category_theory/isomorphism.lean

@@ -387,4 +387,12 @@ by simp
 
 end functor
 
+section partial_order
+variables {α β : Type*} [partial_order α] [partial_order β]
+
+lemma iso.to_eq {X Y : α} (f : X ≅ Y) : X = Y :=
+le_antisymm (le_of_hom f.hom) (le_of_hom f.inv)
+
+end partial_order
+
 end category_theory

src/category_theory/skeletal.lean

@@ -266,4 +266,20 @@ adjunction.mk_of_unit_counit
 
 end thin_skeleton
 
+open thin_skeleton
+
+section
+variables {C} {α : Type*} [partial_order α]
+
+/--
+When `e : C ≌ α` is a categorical equivalence from a thin category `C` to some partial order `α`,
+the `thin_skeleton C` is order isomorphic to `α`.
+-/
+noncomputable
+def equivalence.thin_skeleton_order_iso
+  [∀ X Y : C, subsingleton (X ⟶ Y)] (e : C ≌ α) : thin_skeleton C ≃o α :=
+((from_thin_skeleton C).as_equivalence.trans e).to_order_iso
+
+end
+
 end category_theory

src/category_theory/subobject/types.lean

@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2021 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import category_theory.subobject.well_powered
+import category_theory.types
+
+/-!
+# `Type u` is well-powered
+
+By building a categorical equivalence `mono_over α ≌ set α` for any `α : Type u`,
+we deduce that `subobject α ≃o set α` and that `Type u` is well-powered.
+
+One would hope that for a particular concrete category `C` (`AddCommGroup`, etc)
+it's viable to prove `[well_powered C]` without explicitly aligning `subobject X`
+with the "hand-rolled" definition of subobjects.
+
+This may be possible using Lawvere theories,
+but it remains to be seen whether this just pushes lumps around in the carpet.
+-/
+
+universes u
+
+open category_theory
+open category_theory.subobject
+
+open_locale category_theory.Type
+
+lemma subtype_val_mono {α : Type u} (s : set α) : mono ↾(subtype.val : s → α) :=
+(mono_iff_injective _).mpr subtype.val_injective
+
+local attribute [instance] subtype_val_mono
+
+/--
+The category of `mono_over α`, for `α : Type u`, is equivalent to the partial order `set α`.
+-/
+@[simps]
+noncomputable
+def types.mono_over_equivalence_set (α : Type u) : mono_over α ≌ set α :=
+{ functor :=
+  { obj := λ f, set.range f.1.hom,
+    map := λ f g t, hom_of_le begin
+      rintro a ⟨x, rfl⟩,
+      exact ⟨t.1 x, congr_fun t.w x⟩,
+    end, },
+  inverse :=
+  { obj := λ s, mono_over.mk' (subtype.val : s → α),
+    map := λ s t b, mono_over.hom_mk (λ w, ⟨w.1, set.mem_of_mem_of_subset w.2 (le_of_hom b)⟩)
+      (by { ext, simp, }), },
+  unit_iso := nat_iso.of_components
+    (λ f, mono_over.iso_mk
+      (equiv.of_injective f.1.hom ((mono_iff_injective _).mp f.2)).to_iso (by tidy))
+    (by tidy),
+  counit_iso := nat_iso.of_components
+    (λ s, eq_to_iso subtype.range_val)
+    (by tidy), }
+
+instance : well_powered (Type u) :=
+well_powered_of_essentially_small_mono_over
+  (λ α, essentially_small.mk' (types.mono_over_equivalence_set α))
+
+/--
+For `α : Type u`, `subobject α` is order isomorphic to `set α`.
+-/
+noncomputable def types.subobject_equiv_set (α : Type u) : subobject α ≃o set α :=
+(types.mono_over_equivalence_set α).thin_skeleton_order_iso