fix errors; lint; shorten filename

leanprover-community · Feb 17, 2023 · 7f41cf3 · 7f41cf3
1 parent 5d6e14e
commit 7f41cf3
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 11 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -246,7 +246,7 @@ import Mathlib.CategoryTheory.Functor.FullyFaithful
 import Mathlib.CategoryTheory.Functor.Functorial
 import Mathlib.CategoryTheory.Functor.Hom
 import Mathlib.CategoryTheory.Functor.InvIsos
-import Mathlib.CategoryTheory.Functor.ReflectsIsomorphisms
+import Mathlib.CategoryTheory.Functor.ReflectsIso
 import Mathlib.CategoryTheory.Groupoid
 import Mathlib.CategoryTheory.Iso
 import Mathlib.CategoryTheory.LiftingProperties.Adjunction

diff --git a/...yTheory/Functor/ReflectsIsomorphisms.lean → ...b/CategoryTheory/Functor/ReflectsIso.lean b/...yTheory/Functor/ReflectsIsomorphisms.lean → ...b/CategoryTheory/Functor/ReflectsIso.lean
@@ -17,7 +17,7 @@ import Mathlib.CategoryTheory.Functor.FullyFaithful
 
 A functor `F` reflects isomorphisms if whenever `F.map f` is an isomorphism, `f` was too.
 
-It is formalized as a `Prop` valued typeclass `reflects_isomorphisms F`.
+It is formalized as a `Prop` valued typeclass `ReflectsIsomorphisms F`.
 
 Any fully faithful functor reflects isomorphisms.
 -/
@@ -42,6 +42,7 @@ morphism `f : A ⟶ B`, if `F.map f` is an isomorphism then `f` is as well.
 Note that we do not assume or require that `F` is faithful.
 -/
 class ReflectsIsomorphisms (F : C ⥤ D) : Prop where
+  /-- For any `f`, if `F.map f` is an iso, then so was `f`-/
   reflects : ∀ {A B : C} (f : A ⟶ B) [IsIso (F.map f)], IsIso f
 #align category_theory.reflects_isomorphisms CategoryTheory.ReflectsIsomorphisms
 
@@ -53,25 +54,25 @@ theorem isIso_of_reflects_iso {A B : C} (f : A ⟶ B) (F : C ⥤ D) [IsIso (F.ma
 
 instance (priority := 100) of_full_and_faithful (F : C ⥤ D) [Full F] [Faithful F] :
     ReflectsIsomorphisms F
-    where reflects X Y f i :=
+    where reflects f i :=
     ⟨⟨F.preimage (inv (F.map f)), ⟨F.map_injective (by simp), F.map_injective (by simp)⟩⟩⟩
 #align category_theory.of_full_and_faithful CategoryTheory.of_full_and_faithful
 
 instance (F : C ⥤ D) (G : D ⥤ E) [ReflectsIsomorphisms F] [ReflectsIsomorphisms G] :
     ReflectsIsomorphisms (F ⋙ G) :=
-  ⟨fun _ _ f (hf : IsIso (G.map _)) => by
+  ⟨fun f (hf : IsIso (G.map _)) => by
     skip
-    haveI := is_iso_of_reflects_iso (F.map f) G
-    exact is_iso_of_reflects_iso f F⟩
+    haveI := isIso_of_reflects_iso (F.map f) G
+    exact isIso_of_reflects_iso f F⟩
 
 instance (priority := 100) reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms
     [Balanced C] (F : C ⥤ D) [ReflectsMonomorphisms F] [ReflectsEpimorphisms F] :
-    ReflectsIsomorphisms F
-    where reflects A B f hf := by
+    ReflectsIsomorphisms F where 
+  reflects f hf := by
     skip
-    haveI : epi f := epi_of_epi_map F inferInstance
-    haveI : mono f := mono_of_mono_map F inferInstance
-    exact is_iso_of_mono_of_epi f
+    haveI : Epi f := epi_of_epi_map F inferInstance
+    haveI : Mono f := mono_of_mono_map F inferInstance
+    exact isIso_of_mono_of_epi f
 #align category_theory.reflects_isomorphisms_of_reflects_monomorphisms_of_reflects_epimorphisms CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms
 
 end ReflectsIso