chore(category_theory/equivalence): weaken essential surjectivity (#3821

)

Weaken essential surjectivity to be a Prop, rather than the data of the inverse.

src/algebra/category/Group/Z_Module_equivalence.lean

@@ -29,8 +29,7 @@ instance : full (forget₂ (Module ℤ) AddCommGroup.{u}) :=
 
 /-- The forgetful functor from `ℤ` modules to `AddCommGroup` is essentially surjective. -/
 instance : ess_surj (forget₂ (Module ℤ) AddCommGroup.{u}) :=
-{ obj_preimage := λ A, Module.of ℤ A,
-  iso' := λ A, { hom := 𝟙 A, inv := 𝟙 A, } }
+{ obj_preimage := λ A, ⟨Module.of ℤ A, ⟨{ hom := 𝟙 A, inv := 𝟙 A }⟩⟩}
 
-instance : is_equivalence (forget₂ (Module ℤ) AddCommGroup.{u}) :=
+noncomputable instance : is_equivalence (forget₂ (Module ℤ) AddCommGroup.{u}) :=
 equivalence_of_fully_faithfully_ess_surj (forget₂ (Module ℤ) AddCommGroup)

src/category_theory/Fintype.lean

@@ -80,14 +80,10 @@ def incl : skeleton ⥤ Fintype :=
 
 instance : full incl := { preimage := λ _ _ f, f }
 instance : faithful incl := {}
-noncomputable instance : ess_surj incl :=
-{ obj_preimage := λ X, fintype.card X,
-  iso' := λ X,
+instance : ess_surj incl :=
+{ obj_preimage := λ 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 } } }
+  ⟨fintype.card X, ⟨⟨F.symm, F, F.self_comp_symm, F.symm_comp_self⟩⟩⟩ }
 
 noncomputable instance : is_equivalence incl :=
 equivalence.equivalence_of_fully_faithfully_ess_surj _

src/category_theory/equivalence.lean

@@ -495,27 +495,21 @@ so `F.obj c ≅ D`.
 
 See https://stacks.math.columbia.edu/tag/001C.
 -/
--- TODO should we make this a `Prop` that merely asserts the existence of a preimage,
--- rather than choosing one?
-class ess_surj (F : C ⥤ D) :=
-(obj_preimage (d : D) : C)
-(iso' (d : D) : F.obj (obj_preimage d) ≅ d . obviously)
-
-restate_axiom ess_surj.iso'
-
-/-- Applying an essentially surjective functor to a preimage of `d` yields an object that is
-    isomorphic to `d`. -/
-add_decl_doc ess_surj.iso
+class ess_surj (F : C ⥤ D) : Prop :=
+(obj_preimage [] (d : D) : ∃ c, nonempty (F.obj c ≅ d))
 
 namespace functor
 /-- Given an essentially surjective functor, we can find a preimage for every object `d` in the
     codomain. Applying the functor to this preimage will yield an object isomorphic to `d`, see
     `fun_obj_preimage_iso`. -/
-def obj_preimage (F : C ⥤ D) [ess_surj F] (d : D) : C := ess_surj.obj_preimage.{v₁ v₂} F d
+noncomputable def obj_preimage (F : C ⥤ D) [sF : ess_surj F] (d : D) : C :=
+classical.some (ess_surj.obj_preimage F d)
 /-- Applying an essentially surjective functor to a preimage of `d` yields an object that is
     isomorphic to `d`. -/
-def fun_obj_preimage_iso (F : C ⥤ D) [ess_surj F] (d : D) : F.obj (F.obj_preimage d) ≅ d :=
-ess_surj.iso d
+noncomputable def fun_obj_preimage_iso (F : C ⥤ D) [sF : ess_surj F] (d : D) :
+  F.obj (F.obj_preimage d) ≅ d :=
+classical.choice (classical.some_spec (ess_surj.obj_preimage F d))
+
 end functor
 
 namespace equivalence
@@ -525,8 +519,8 @@ An equivalence is essentially surjective.
 
 See https://stacks.math.columbia.edu/tag/02C3.
 -/
-def ess_surj_of_equivalence (F : C ⥤ D) [is_equivalence F] : ess_surj F :=
-⟨ λ Y : D, F.inv.obj Y, λ Y : D, (F.inv_fun_id.app Y) ⟩
+lemma ess_surj_of_equivalence (F : C ⥤ D) [is_equivalence F] : ess_surj F :=
+⟨λ Y, ⟨F.inv.obj Y, ⟨F.inv_fun_id.app Y⟩⟩⟩
 
 /--
 An equivalence is faithful.
@@ -552,7 +546,7 @@ instance full_of_equivalence (F : C ⥤ D) [is_equivalence F] : full F :=
   witness' := λ X Y f, F.inv.map_injective
   (by simpa only [is_equivalence.inv_fun_map, assoc, iso.hom_inv_id_app_assoc, iso.hom_inv_id_app] using comp_id _) }
 
-@[simp] private def equivalence_inverse (F : C ⥤ D) [full F] [faithful F] [ess_surj F] : D ⥤ C :=
+@[simps] private noncomputable def equivalence_inverse (F : C ⥤ D) [full F] [faithful F] [ess_surj F] : D ⥤ C :=
 { obj  := λ X, F.obj_preimage X,
   map := λ X Y f, F.preimage ((F.fun_obj_preimage_iso X).hom ≫ f ≫ (F.fun_obj_preimage_iso Y).inv),
   map_id' := λ X, begin apply F.map_injective, tidy end,
@@ -563,29 +557,19 @@ A functor which is full, faithful, and essentially surjective is an equivalence.
 
 See https://stacks.math.columbia.edu/tag/02C3.
 -/
-def equivalence_of_fully_faithfully_ess_surj
+noncomputable def equivalence_of_fully_faithfully_ess_surj
   (F : C ⥤ D) [full F] [faithful F] [ess_surj F] : is_equivalence F :=
 is_equivalence.mk (equivalence_inverse F)
   (nat_iso.of_components
     (λ X, (preimage_iso $ F.fun_obj_preimage_iso $ F.obj X).symm)
     (λ X Y f, by { apply F.map_injective, obviously }))
-  (nat_iso.of_components
-    (λ Y, F.fun_obj_preimage_iso Y)
-    (by obviously))
+  (nat_iso.of_components F.fun_obj_preimage_iso (by tidy))
 
 @[simp] lemma functor_map_inj_iff (e : C ≌ D) {X Y : C} (f g : X ⟶ Y) : e.functor.map f = e.functor.map g ↔ f = g :=
-begin
-  split,
-  { intro w, apply e.functor.map_injective, exact w, },
-  { rintro ⟨rfl⟩, refl, }
-end
+⟨λ h, e.functor.map_injective h, λ h, h ▸ rfl⟩
 
 @[simp] lemma inverse_map_inj_iff (e : C ≌ D) {X Y : D} (f g : X ⟶ Y) : e.inverse.map f = e.inverse.map g ↔ f = g :=
-begin
-  split,
-  { intro w, apply e.inverse.map_injective, exact w, },
-  { rintro ⟨rfl⟩, refl, }
-end
+functor_map_inj_iff e.symm f g
 
 end equivalence
 

src/category_theory/monad/adjunction.lean

@@ -110,8 +110,7 @@ let h : L ⊣ R := (is_right_adjoint.adj) in
 instance comparison_ess_surj [reflective R] : ess_surj (monad.comparison R) :=
 let L := left_adjoint R in
 let h : L ⊣ R := is_right_adjoint.adj in
-{ obj_preimage := λ X, L.obj X.A,
-  iso' := λ X,
+⟨λ X, ⟨L.obj X.A, ⟨
   { hom :=
     { f := (as_iso (h.unit.app X.A)).inv,
       h' :=
@@ -135,7 +134,8 @@ let h : L ⊣ R := is_right_adjoint.adj in
         erw [comp_id, id_comp],
       end },
     hom_inv_id' := by { ext, exact (as_iso (h.unit.app X.A)).inv_hom_id, },
-    inv_hom_id' := by { ext, exact (as_iso (h.unit.app X.A)).hom_inv_id, }, } }
+    inv_hom_id' := by { ext, exact (as_iso (h.unit.app X.A)).hom_inv_id, }, }
+⟩⟩⟩
 
 instance comparison_full [full R] [is_right_adjoint R] : full (monad.comparison R) :=
 { preimage := λ X Y f, R.preimage f.f }
@@ -144,10 +144,12 @@ instance comparison_faithful [faithful R] [is_right_adjoint R] : faithful (monad
 
 end reflective
 
+-- It is possible to do this computably since the construction gives the data of the inverse, not
+-- just the existence of an inverse on each object.
 /-- Any reflective inclusion has a monadic right adjoint.
     cf Prop 5.3.3 of [Riehl][riehl2017] -/
 @[priority 100] -- see Note [lower instance priority]
-instance monadic_of_reflective [reflective R] : monadic_right_adjoint R :=
+noncomputable instance monadic_of_reflective [reflective R] : monadic_right_adjoint R :=
 { eqv := equivalence.equivalence_of_fully_faithfully_ess_surj _ }
 
 end category_theory

src/topology/category/Compactum.lean

@@ -432,9 +432,8 @@ noncomputable def iso_of_topological_space {D : CompHaus} :
       λ _ h1, by {rw is_open_iff_ultrafilter', intros _ h2, exact h1 _ h2} } }
 
 /-- The functor Compactum_to_CompHaus is essentially surjective. -/
-noncomputable def ess_surj : ess_surj Compactum_to_CompHaus :=
-{ obj_preimage := λ X, Compactum.of_topological_space X,
-  iso' := λ _, iso_of_topological_space }
+lemma ess_surj : ess_surj Compactum_to_CompHaus :=
+{ obj_preimage := λ X, ⟨Compactum.of_topological_space X, ⟨iso_of_topological_space⟩⟩ }
 
 /-- The functor Compactum_to_CompHaus is an equivalence of categories. -/
 noncomputable def is_equivalence : is_equivalence Compactum_to_CompHaus :=