feat(category/is_iso): make is_iso a Prop (#6662)

Perhaps long overdue, this makes `is_iso` into a Prop.

It hasn't been a big deal, as it was always a subsingleton. Nevertheless this is probably safer than carrying data around in the typeclass inference system. 

As a side effect `simple` is now a Prop as well.



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

src/algebra/category/Algebra/basic.lean

@@ -145,5 +145,5 @@ instance Algebra.forget_reflects_isos : reflects_isomorphisms (forget (Algebra.{
     resetI,
     let i := as_iso ((forget (Algebra.{u} R)).map f),
     let e : X ≃ₐ[R] Y := { ..f, ..i.to_equiv },
-    exact { ..e.to_Algebra_iso },
+    exact is_iso.of_iso e.to_Algebra_iso,
   end }

src/algebra/category/CommRing/basic.lean

@@ -202,7 +202,7 @@ instance Ring.forget_reflects_isos : reflects_isomorphisms (forget Ring.{u}) :=
     resetI,
     let i := as_iso ((forget Ring).map f),
     let e : X ≃+* Y := { ..f, ..i.to_equiv },
-    exact { ..e.to_Ring_iso },
+    exact is_iso.of_iso e.to_Ring_iso,
   end }
 
 instance CommRing.forget_reflects_isos : reflects_isomorphisms (forget CommRing.{u}) :=
@@ -211,7 +211,7 @@ instance CommRing.forget_reflects_isos : reflects_isomorphisms (forget CommRing.
     resetI,
     let i := as_iso ((forget CommRing).map f),
     let e : X ≃+* Y := { ..f, ..i.to_equiv },
-    exact { ..e.to_CommRing_iso },
+    exact is_iso.of_iso e.to_CommRing_iso,
   end }
 
 example : reflects_isomorphisms (forget₂ Ring AddCommGroup) := by apply_instance

src/algebra/category/Group/basic.lean

@@ -250,7 +250,7 @@ instance Group.forget_reflects_isos : reflects_isomorphisms (forget Group.{u}) :
     resetI,
     let i := as_iso ((forget Group).map f),
     let e : X ≃* Y := { ..f, ..i.to_equiv },
-    exact { ..e.to_Group_iso },
+    exact is_iso.of_iso e.to_Group_iso,
   end }
 
 @[to_additive]
@@ -260,5 +260,5 @@ instance CommGroup.forget_reflects_isos : reflects_isomorphisms (forget CommGrou
     resetI,
     let i := as_iso ((forget CommGroup).map f),
     let e : X ≃* Y := { ..f, ..i.to_equiv },
-    exact { ..e.to_CommGroup_iso },
+    exact is_iso.of_iso e.to_CommGroup_iso,
   end }

src/algebra/category/Mon/basic.lean

@@ -179,7 +179,7 @@ instance Mon.forget_reflects_isos : reflects_isomorphisms (forget Mon.{u}) :=
     resetI,
     let i := as_iso ((forget Mon).map f),
     let e : X ≃* Y := { ..f, ..i.to_equiv },
-    exact { ..e.to_Mon_iso },
+    exact is_iso.of_iso e.to_Mon_iso,
   end }
 
 @[to_additive]
@@ -189,7 +189,7 @@ instance CommMon.forget_reflects_isos : reflects_isomorphisms (forget CommMon.{u
     resetI,
     let i := as_iso ((forget CommMon).map f),
     let e : X ≃* Y := { ..f, ..i.to_equiv },
-    exact { ..e.to_CommMon_iso },
+    exact is_iso.of_iso e.to_CommMon_iso,
   end }
 
 /-!

src/algebra/category/Semigroup/basic.lean

@@ -168,7 +168,7 @@ instance Magma.forget_reflects_isos : reflects_isomorphisms (forget Magma.{u}) :
     resetI,
     let i := as_iso ((forget Magma).map f),
     let e : X ≃* Y := { ..f, ..i.to_equiv },
-    exact { ..e.to_Magma_iso },
+    exact is_iso.of_iso e.to_Magma_iso,
   end }
 
 @[to_additive]
@@ -178,7 +178,7 @@ instance Semigroup.forget_reflects_isos : reflects_isomorphisms (forget Semigrou
     resetI,
     let i := as_iso ((forget Semigroup).map f),
     let e : X ≃* Y := { ..f, ..i.to_equiv },
-    exact { ..e.to_Semigroup_iso },
+    exact is_iso.of_iso e.to_Semigroup_iso,
   end }
 
 /-!

src/algebra/homology/exact.lean

@@ -86,7 +86,7 @@ lemma exact_comp_mono [exact f g] [mono h] : exact f (g ≫ h) :=
 begin
   refine ⟨by simp, _⟩,
   letI : is_iso (kernel.lift (g ≫ h) (kernel.ι g) (by simp)) :=
-  { inv := kernel.lift g (kernel.ι (g ≫ h)) (by simp [←cancel_mono h]) },
+    ⟨kernel.lift g (kernel.ι (g ≫ h)) (by simp [←cancel_mono h]), by tidy⟩,
   rw image_to_kernel_map_comp_right f g h exact.w,
   exact epi_comp _ _
 end
@@ -95,8 +95,8 @@ lemma exact_kernel : exact (kernel.ι f) f :=
 begin
   refine ⟨kernel.condition _, _⟩,
   letI : is_iso (image_to_kernel_map (kernel.ι f) f (kernel.condition f)) :=
-  { inv := factor_thru_image (kernel.ι f),
-    hom_inv_id' := by simp [←cancel_mono (image.ι (kernel.ι f))] },
+    ⟨factor_thru_image (kernel.ι f),
+      ⟨by simp [←cancel_mono (image.ι (kernel.ι f))], by tidy⟩⟩,
   apply_instance
 end
 

src/algebraic_geometry/presheafed_space.lean

@@ -107,29 +107,29 @@ instance category_of_PresheafedSpaces : category (PresheafedSpace C) :=
     { dsimp, simp only [id_comp] },  -- See note [dsimp, simp].
     { ext U, op_induction, cases U,
       dsimp,
-      simp only [comp_id, id_comp, map_id, presheaf.pushforward.comp_inv_app],
+      simp only [presheaf.pushforward.comp_inv_app, opens.map_iso_inv_app],
       dsimp,
-      simp only [comp_id], },
+      simp only [comp_id, comp_id, map_id], },
   end,
   comp_id' := λ X Y f,
   begin
     ext1, swap,
     { dsimp, simp only [comp_id] },
     { ext U, op_induction, cases U,
       dsimp,
-      simp only [comp_id, id_comp, map_id, presheaf.pushforward.comp_inv_app],
+      simp only [presheaf.pushforward.comp_inv_app, opens.map_iso_inv_app],
       dsimp,
-      simp only [comp_id], }
+      simp only [id_comp, comp_id, map_id], }
   end,
   assoc' := λ W X Y Z f g h,
   begin
      ext1, swap,
      refl,
      { ext U, op_induction, cases U,
        dsimp,
-       simp only [assoc, map_id, comp_id, presheaf.pushforward.comp_inv_app],
+       simp only [assoc, presheaf.pushforward.comp_inv_app, opens.map_iso_inv_app],
        dsimp,
-       simp only [comp_id, id_comp], }
+       simp only [comp_id, id_comp, map_id], }
   end }
 
 end

src/algebraic_geometry/presheafed_space/has_colimits.lean

@@ -75,7 +75,7 @@ begin
   cases U,
   dsimp,
   simp only [PresheafedSpace.congr_app (F.map_comp f g)],
-  dsimp, simp,
+  dsimp, simp, dsimp, simp, -- See note [dsimp, simp]
 end
 
 /--

src/category_theory/abelian/basic.lean

@@ -144,7 +144,7 @@ variables {X Y : C} (f : X ⟶ Y)
 local attribute [instance] strong_epi_of_epi
 
 /-- In an abelian category, a monomorphism which is also an epimorphism is an isomorphism. -/
-def is_iso_of_mono_of_epi [mono f] [epi f] : is_iso f :=
+lemma is_iso_of_mono_of_epi [mono f] [epi f] : is_iso f :=
 is_iso_of_mono_of_strong_epi _
 
 end mono_epi_iso

src/category_theory/abelian/non_preadditive.lean

@@ -109,7 +109,7 @@ local attribute [instance] strong_epi_of_epi
 
 /-- In a `non_preadditive_abelian` category, a monomorphism which is also an epimorphism is an
     isomorphism. -/
-def is_iso_of_mono_of_epi [mono f] [epi f] : is_iso f :=
+lemma is_iso_of_mono_of_epi [mono f] [epi f] : is_iso f :=
 is_iso_of_mono_of_strong_epi _
 
 end mono_epi_iso
@@ -556,7 +556,7 @@ is_iso_of_mono_of_epi _
     followed by the inverse of `r`. In the category of modules, using the normal kernels and
     cokernels, this map is equal to the map `(a, b) ↦ a - b`, hence the name `σ` for
     "subtraction". -/
-abbreviation σ {A : C} : A ⨯ A ⟶ A := cokernel.π (diag A) ≫ is_iso.inv (r A)
+abbreviation σ {A : C} : A ⨯ A ⟶ A := cokernel.π (diag A) ≫ inv (r A)
 
 end
 

src/category_theory/action.lean

@@ -42,6 +42,7 @@ def action_category := (action_as_functor M X).elements
 
 namespace action_category
 
+noncomputable
 instance (G : Type*) [group G] [mul_action G X] : groupoid (action_category G X) :=
 category_theory.groupoid_of_elements _
 

src/category_theory/adjunction/basic.lean

@@ -412,6 +412,7 @@ If the unit and counit of a given adjunction are (pointwise) isomorphisms, then
 adjunction to an equivalence.
 -/
 @[simps]
+noncomputable
 def to_equivalence (adj : F ⊣ G) [∀ X, is_iso (adj.unit.app X)] [∀ Y, is_iso (adj.counit.app Y)] :
   C ≌ D :=
 { functor := F,
@@ -424,6 +425,7 @@ If the unit and counit for the adjunction corresponding to a right adjoint funct
 isomorphisms, then the functor is an equivalence of categories.
 -/
 @[simps]
+noncomputable
 def is_right_adjoint_to_is_equivalence [is_right_adjoint G]
   [∀ X, is_iso ((adjunction.of_right_adjoint G).unit.app X)]
   [∀ Y, is_iso ((adjunction.of_right_adjoint G).counit.app Y)] :

src/category_theory/adjunction/fully_faithful.lean

@@ -30,20 +30,17 @@ See
 instance unit_is_iso_of_L_fully_faithful [full L] [faithful L] : is_iso (adjunction.unit h) :=
 @nat_iso.is_iso_of_is_iso_app _ _ _ _ _ _ (adjunction.unit h) $ λ X,
 @yoneda.is_iso _ _ _ _ ((adjunction.unit h).app X)
-{ inv := { app := λ Y f, L.preimage ((h.hom_equiv (unop Y) (L.obj X)).symm f) },
-  inv_hom_id' :=
-  begin
-    ext, dsimp,
+⟨{ app := λ Y f, L.preimage ((h.hom_equiv (unop Y) (L.obj X)).symm f) },
+  ⟨begin
+    ext x f, dsimp,
+    apply L.map_injective,
+    simp,
+  end, begin
+    ext x f, dsimp,
     simp only [adjunction.hom_equiv_counit, preimage_comp, preimage_map, category.assoc],
     rw ←h.unit_naturality,
     simp,
-  end,
-  hom_inv_id' :=
-  begin
-    ext, dsimp,
-    apply L.map_injective,
-    simp,
-  end }.
+  end⟩⟩
 
 /--
 If the right adjoint is fully faithful, then the counit is an isomorphism.
@@ -54,20 +51,17 @@ instance counit_is_iso_of_R_fully_faithful [full R] [faithful R] : is_iso (adjun
 @nat_iso.is_iso_of_is_iso_app _ _ _ _ _ _ (adjunction.counit h) $ λ X,
 @is_iso_of_op _ _ _ _ _ $
 @coyoneda.is_iso _ _ _ _ ((adjunction.counit h).app X).op
-{ inv := { app := λ Y f, R.preimage ((h.hom_equiv (R.obj X) Y) f) },
-  inv_hom_id' :=
-  begin
-    ext, dsimp,
+⟨{ app := λ Y f, R.preimage ((h.hom_equiv (R.obj X) Y) f) },
+  ⟨begin
+    ext x f, dsimp,
+    apply R.map_injective,
+    simp,
+  end, begin
+    ext x f, dsimp,
     simp only [adjunction.hom_equiv_unit, preimage_comp, preimage_map],
     rw ←h.counit_naturality,
     simp,
-  end,
-  hom_inv_id' :=
-  begin
-    ext, dsimp,
-    apply R.map_injective,
-    simp,
-  end }
+  end⟩⟩
 
 -- TODO also prove the converses?
 -- def L_full_of_unit_is_iso [is_iso (adjunction.unit h)] : full L := sorry

src/category_theory/adjunction/mates.lean

@@ -213,26 +213,25 @@ The converse is given in `transfer_nat_trans_self_of_iso`.
 -/
 instance transfer_nat_trans_self_iso (f : L₂ ⟶ L₁) [is_iso f] :
   is_iso (transfer_nat_trans_self adj₁ adj₂ f) :=
-{ inv := transfer_nat_trans_self adj₂ adj₁ (inv f),
-  hom_inv_id' := transfer_nat_trans_self_comm _ _ (by simp),
-  inv_hom_id' := transfer_nat_trans_self_comm _ _ (by simp) }
+⟨transfer_nat_trans_self adj₂ adj₁ (inv f),
+  ⟨transfer_nat_trans_self_comm _ _ (by simp), transfer_nat_trans_self_comm _ _ (by simp)⟩⟩
 
 /--
 If `f` is an isomorphism, then the un-transferred natural transformation is an isomorphism.
 The converse is given in `transfer_nat_trans_self_symm_of_iso`.
 -/
 instance transfer_nat_trans_self_symm_iso (f : R₁ ⟶ R₂) [is_iso f] :
   is_iso ((transfer_nat_trans_self adj₁ adj₂).symm f) :=
-{ inv := (transfer_nat_trans_self adj₂ adj₁).symm (inv f),
-  hom_inv_id' := transfer_nat_trans_self_symm_comm _ _ (by simp),
-  inv_hom_id' := transfer_nat_trans_self_symm_comm _ _ (by simp) }
+⟨(transfer_nat_trans_self adj₂ adj₁).symm (inv f),
+  ⟨transfer_nat_trans_self_symm_comm _ _ (by simp),
+   transfer_nat_trans_self_symm_comm _ _ (by simp)⟩⟩
 
 /--
 If `f` is a natural transformation whose transferred natural transformation is an isomorphism,
 then `f` is an isomorphism.
 The converse is given in `transfer_nat_trans_self_iso`.
 -/
-def transfer_nat_trans_self_of_iso (f : L₂ ⟶ L₁) [is_iso (transfer_nat_trans_self adj₁ adj₂ f)] :
+lemma transfer_nat_trans_self_of_iso (f : L₂ ⟶ L₁) [is_iso (transfer_nat_trans_self adj₁ adj₂ f)] :
   is_iso f :=
 begin
   suffices :
@@ -246,7 +245,7 @@ If `f` is a natural transformation whose un-transferred natural transformation i
 then `f` is an isomorphism.
 The converse is given in `transfer_nat_trans_self_symm_iso`.
 -/
-def transfer_nat_trans_self_symm_of_iso (f : R₁ ⟶ R₂)
+lemma transfer_nat_trans_self_symm_of_iso (f : R₁ ⟶ R₂)
   [is_iso ((transfer_nat_trans_self adj₁ adj₂).symm f)] :
   is_iso f :=
 begin

src/category_theory/adjunction/opposites.lean

@@ -19,6 +19,7 @@ These constructions are used to show uniqueness of adjoints (up to natural isomo
 adjunction, opposite, uniqueness
 -/
 
+
 open category_theory
 
 universes v₁ v₂ u₁ u₂ -- declare the `v`'s first; see `category_theory.category` for an explanation

src/category_theory/adjunction/reflective.lean

@@ -70,7 +70,7 @@ reflection of `A`, with the isomorphism as `η_A`.
 
 (For any `B` in the reflective subcategory, we automatically have that `ε_B` is an iso.)
 -/
-def functor.ess_image.unit_is_iso [reflective i] {A : C} (h : A ∈ i.ess_image) :
+lemma functor.ess_image.unit_is_iso [reflective i] {A : C} (h : A ∈ i.ess_image) :
   is_iso ((adjunction.of_right_adjoint i).unit.app A) :=
 begin
   suffices : (adjunction.of_right_adjoint i).unit.app A =

src/category_theory/closed/cartesian.lean

@@ -316,7 +316,7 @@ i.e. any morphism to `I` is an iso.
 This actually shows a slightly stronger version: any morphism to an initial object from an
 exponentiable object is an isomorphism.
 -/
-def strict_initial {I : C} (t : is_initial I) (f : A ⟶ I) : is_iso f :=
+lemma strict_initial {I : C} (t : is_initial I) (f : A ⟶ I) : is_iso f :=
 begin
   haveI : mono (limits.prod.lift (𝟙 A) f ≫ (zero_mul t).hom) := mono_comp _ _,
   rw [zero_mul_hom, prod.lift_snd] at _inst,

src/category_theory/closed/functor.lean

@@ -87,12 +87,21 @@ transfer_nat_trans (exp.adjunction A) (exp.adjunction (F.obj A)) (prod_compariso
 lemma exp_comparison_ev (A B : C) :
   limits.prod.map (𝟙 (F.obj A)) ((exp_comparison F A).app B) ≫ (ev (F.obj A)).app (F.obj B) =
     inv (prod_comparison F _ _) ≫ F.map ((ev _).app _) :=
-by convert transfer_nat_trans_counit _ _ (prod_comparison_nat_iso F A).inv B
+begin
+  convert transfer_nat_trans_counit _ _ (prod_comparison_nat_iso F A).inv B,
+  ext,
+  simp,
+end
 
 lemma coev_exp_comparison (A B : C) :
   F.map ((coev A).app B) ≫ (exp_comparison F A).app (A ⨯ B) =
       (coev _).app (F.obj B) ≫ (exp (F.obj A)).map (inv (prod_comparison F A B)) :=
-by convert unit_transfer_nat_trans _ _ (prod_comparison_nat_iso F A).inv B
+begin
+  convert unit_transfer_nat_trans _ _ (prod_comparison_nat_iso F A).inv B,
+  ext,
+  dsimp,
+  simp,
+end
 
 lemma uncurry_exp_comparison (A B : C) :
   uncurry ((exp_comparison F A).app B) = inv (prod_comparison F _ _) ≫ F.map ((ev _).app _) :=
@@ -147,7 +156,7 @@ lemma frobenius_morphism_mate (h : L ⊣ F) (A : C) :
 If the exponential comparison transformation (at `A`) is an isomorphism, then the Frobenius morphism
 at `A` is an isomorphism.
 -/
-def frobenius_morphism_iso_of_exp_comparison_iso (h : L ⊣ F) (A : C)
+lemma frobenius_morphism_iso_of_exp_comparison_iso (h : L ⊣ F) (A : C)
   [i : is_iso (exp_comparison F A)] :
   is_iso (frobenius_morphism F h A) :=
 begin
@@ -159,7 +168,7 @@ end
 If the Frobenius morphism at `A` is an isomorphism, then the exponential comparison transformation
 (at `A`) is an isomorphism.
 -/
-def exp_comparison_iso_of_frobenius_morphism_iso (h : L ⊣ F) (A : C)
+lemma exp_comparison_iso_of_frobenius_morphism_iso (h : L ⊣ F) (A : C)
   [i : is_iso (frobenius_morphism F h A)] :
   is_iso (exp_comparison F A) :=
 by { rw ← frobenius_morphism_mate F h, apply_instance }

src/category_theory/comma.lean

@@ -141,7 +141,10 @@ def iso_mk {X Y : comma L₁ R₁} (l : X.left ≅ Y.left) (r : X.right ≅ Y.ri
   inv :=
   { left := l.inv,
     right := r.inv,
-    w' := by { erw [L₁.map_inv l.hom, iso.inv_comp_eq, reassoc_of h, ← R₁.map_comp], simp } } }
+    w' := begin
+      rw [←L₁.map_iso_inv l, iso.inv_comp_eq, L₁.map_iso_hom, reassoc_of h, ← R₁.map_comp],
+      simp
+    end, } }
 
 /-- A natural transformation `L₁ ⟶ L₂` induces a functor `comma L₂ R ⥤ comma L₁ R`. -/
 @[simps]

src/category_theory/core.lean

@@ -39,6 +39,7 @@ variables {G : Type u₂} [groupoid.{v₂} G]
 /-- A functor from a groupoid to a category C factors through the core of C. -/
 -- Note that this function is not functorial
 -- (consider the two functors from [0] to [1], and the natural transformation between them).
+noncomputable
 def functor_to_core (F : G ⥤ C) : G ⥤ core C :=
 { obj := λ X, F.obj X,
   map := λ X Y f, ⟨F.map f, F.map (inv f)⟩ }

src/category_theory/currying.lean

@@ -93,7 +93,7 @@ The equivalence of functor categories given by currying/uncurrying.
 def currying : (C ⥤ (D ⥤ E)) ≌ ((C × D) ⥤ E) :=
 equivalence.mk uncurry curry
   (nat_iso.of_components (λ F, nat_iso.of_components
-    (λ X, nat_iso.of_components (λ Y, as_iso (𝟙 _)) (by tidy)) (by tidy)) (by tidy))
+    (λ X, nat_iso.of_components (λ Y, iso.refl _) (by tidy)) (by tidy)) (by tidy))
   (nat_iso.of_components (λ F, nat_iso.of_components
     (λ X, eq_to_iso (by simp)) (by tidy)) (by tidy))
 

src/category_theory/discrete_category.lean

@@ -46,7 +46,7 @@ lemma eq_of_hom {X Y : discrete α} (i : X ⟶ Y) : X = Y := i.down.down
 variables {C : Type u₂} [category.{v₂} C]
 
 instance {I : Type u₁} {i j : discrete I} (f : i ⟶ j) : is_iso f :=
-{ inv := eq_to_hom (eq_of_hom f).symm, }
+⟨eq_to_hom (eq_of_hom f).symm, by tidy⟩
 
 /--
 Any function `I → C` gives a functor `discrete I ⥤ C`.